Documentation

MathlibNt.AnalyticNumberTheory.Chen1973.Chen1973Lemma6Equation19DyadicAlphaMoment

source
theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation14_dyadic_log_power (H D Q : ℕ) (s : ℂ) (hH : 2 ≤ H) (hD : 0 < D) (hDQ : D < Q) (hs : 1 ≤ s.re) :
∑ d ∈ Finset.Ioc D Q, 1 / ↑d.totient * ∑ χ : PrimitiveCharacter d, ‖chen1973Lemma6OneSubLS H s χ‖ ^ 2 ≤ 2 * chen1973Lemma6Eq14DyadicConstant * (↑Q / ↑H + 1 / ↑D) * (1 + Real.log ↑(H + 1)) ^ 5 + 2 * ↑Q * (40 * ‖s‖ * √↑Q * Real.log ↑Q * ↑(H + 1) ^ (-s.re) * (1 + Real.log ↑H)) ^ 2

Full actual equation-(14) moment: dyadic finite polynomial plus actual PV remainder.

Inspect dependencies

AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation14_dyadic_log_power · compiled type and proof/definition references.

source
theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_oneSub_second_moment_dyadic (x L level H D Q : ℕ) (s : ℂ) (hH : 2 ≤ H) (hD : 0 < D) (hDQ : D < Q) (hs : 1 ≤ s.re) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) :
chen1973Lemma6Eq19OneSubSecondMoment x L level H s ≤ chen1973Lemma6Eq19I x L level * (2 * chen1973Lemma6Eq14DyadicConstant * (↑Q / ↑H + 1 / ↑D) * (1 + Real.log ↑(H + 1)) ^ 5 + 2 * ↑Q * (40 * ‖s‖ * √↑Q * Real.log ↑Q * ↑(H + 1) ^ (-s.re) * (1 + Real.log ↑H)) ^ 2)

Transport the complete dyadic alpha moment to the actual conductor weights.

Inspect dependencies

AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_oneSub_second_moment_dyadic · compiled type and proof/definition references.

source
noncomputable def AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq14DyadicBudget (H D Q : ℕ) (s : ℂ) :
ℝ

Explicit complete alpha-moment budget; both summands are proved above.

Equations
Instances For
    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq14DyadicBudget · compiled type and proof/definition references.

    source
    theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_A_le_dyadic_moments (x L level B k m H D Q : ℕ) (hx : 3 ≤ x) (hB : 0 < B) (σ v : ℝ) (hσ : 1 ≤ σ) (hH : 2 ≤ H) (hD : 0 < D) (hDQ : D < Q) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) :
    chen1973Lemma6A x L level B k m H (↑σ + ↑v * Complex.I) ≤ √(9 * chen1973Lemma6Eq19SharpConstant * chen1973Lemma6Eq19I x L level / Real.log ↑x ^ 2 * (↑Q + ↑(B * 2 ^ k) / ↑D) * ↑(B * 2 ^ k) ^ (1 - 2 * σ)) * √(chen1973Lemma6Eq19I x L level * chen1973Lemma6Eq14DyadicBudget H D Q (↑σ + ↑v * Complex.I))

    The actual alpha numerator now consumes both genuinely dyadic producers. No x² pair interval and no H²/D finite-polynomial loss remains.

    Inspect dependencies

    AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_A_le_dyadic_moments · compiled type and proof/definition references.