@[reducible, inline]

abbrev AnalyticNumberTheory.LargeSieve.RawLandauSiegelLowerBound : Prop

The raw Landau--Siegel input is kept with the exact outer quantifier order requested by the production adapter.

Equations

• AnalyticNumberTheory.LargeSieve.RawLandauSiegelLowerBound = ∀ (η : ℝ), 0 < η → ∃ (c : ℝ), 0 < c ∧ ∀ (q : ℕ) [inst : NeZero q] (χ : DirichletCharacter ℂ q), χ.IsPrimitive → χ ^ 2 = 1 → χ ≠ 1 → c * ↑q ^ (-η) ≤ (DirichletCharacter.LFunction χ 1).re

noncomputable def AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedQuadraticPointwiseRectangle (A c η : ℝ) (q : ℕ) (T δ : ℝ) : Set ℂ

The pointwise quadratic contour keeps the conditional left edge but lets the right edge move anywhere inside the quarter-width strip.

Equations

• AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedQuadraticPointwiseRectangle A c η q T δ = (↑(AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedQuadraticConditionalLeft A c η q T) - Complex.I * ↑T).Rectangle (↑(1 + δ) + Complex.I * ↑T)

theorem AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedQuadraticPointwiseRectangle_subset {A c η T δ : ℝ} {q : ℕ} (hT : 0 ≤ T) (hδ : 0 < δ) (hδwidth : δ ≤ dirichletLTwistedSmoothedQuadraticConditionalDelta A c η q T) : dirichletLTwistedSmoothedQuadraticPointwiseRectangle A c η q T δ ⊆ dirichletLTwistedSmoothedQuadraticConditionalRectangle A c η q T

theorem AnalyticNumberTheory.LargeSieve.twistedSmoothedPerronIntegrand_holomorphicOn_quadraticPointwiseRectangle {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {A A₀ c η T δ : ℝ} (hAA₀ : A ≤ A₀) (hA : 0 < A) (hc : 0 < c) (hη : 0 < η) (hT : 0 < T) (hχ : χ ≠ 1) (hw : 0 < dirichletLQuadraticConditionalCrossZeroWidth A c η q T) (hw2 : dirichletLQuadraticConditionalCrossZeroWidth A c η q T ≤ 1 / 2) (hwidthle : dirichletLQuadraticConditionalCrossZeroWidth A c η q T ≤ dirichletLQuadraticConditionalCrossZeroWidth A₀ c η q T) (hzero : ∀ s ∈ dirichletLQuadraticConditionalCrossZeroRectangle A₀ c η q T, DirichletCharacter.LFunction χ s ≠ 0) (hT0 : 0 < T) (hδ : 0 < δ) (hδwidth : δ ≤ dirichletLTwistedSmoothedQuadraticConditionalDelta A c η q T) {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (νpos : ∀ x > 0, 0 ≤ ν x) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, ν x / x = 1) {X ε : ℝ} (hX : 0 < X) (hε : 0 < ε) (hε1 : ε < 1) : HolomorphicOn (χ.twistedSmoothedPerronIntegrand ν ε X) (dirichletLTwistedSmoothedQuadraticPointwiseRectangle A c η q T δ)

theorem AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedPerron_quadraticPointwiseFiniteContourIdentity {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {A A₀ c η T δ : ℝ} (hAA₀ : A ≤ A₀) (hA : 0 < A) (hc : 0 < c) (hη : 0 < η) (hT : 0 < T) (hχ : χ ≠ 1) (hw : 0 < dirichletLQuadraticConditionalCrossZeroWidth A c η q T) (hw2 : dirichletLQuadraticConditionalCrossZeroWidth A c η q T ≤ 1 / 2) (hwidthle : dirichletLQuadraticConditionalCrossZeroWidth A c η q T ≤ dirichletLQuadraticConditionalCrossZeroWidth A₀ c η q T) (hzero : ∀ s ∈ dirichletLQuadraticConditionalCrossZeroRectangle A₀ c η q T, DirichletCharacter.LFunction χ s ≠ 0) (hT0 : 0 < T) (hδ : 0 < δ) (hδwidth : δ ≤ dirichletLTwistedSmoothedQuadraticConditionalDelta A c η q T) {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (νpos : ∀ x > 0, 0 ≤ ν x) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, ν x / x = 1) {X ε : ℝ} (hX : 0 < X) (hε : 0 < ε) (hε1 : ε < 1) : VIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) (1 + δ) (-T) T - VIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) (dirichletLTwistedSmoothedQuadraticConditionalLeft A c η q T) (-T) T = HIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) (dirichletLTwistedSmoothedQuadraticConditionalLeft A c η q T) (1 + δ) T - HIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) (dirichletLTwistedSmoothedQuadraticConditionalLeft A c η q T) (1 + δ) (-T)

Exact finite contour shift for the quadratic pointwise rectangle with variable right edge 1 + δ.

theorem AnalyticNumberTheory.LargeSieve.exists_dirichletLTwistedSmoothedQuadraticPointwiseContourNormBounds {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) : ∃ C > 0, ∀ (Z : ℝ), 0 < Z → (∀ (x u : ℝ), 0 < x → x ≤ 1 → u ≠ 0 → ‖riemannZeta (1 + ↑x + Complex.I * ↑u)‖ ≤ Z * (1 + Real.log (|u| + 2) + 1 / |u|)) → ∀ {q : ℕ} [inst : NeZero q] (χ : DirichletCharacter ℂ q) {A c η T δ ε X : ℝ}, χ ^ 2 = 1 → χ ≠ 1 → 0 < A → A ≤ c / 256 → A ≤ 1 / 2 → A ≤ 1 / (16 * Z * 192 ^ 4) → 0 < η → 3 ≤ T → c * ↑q ^ (-η) ≤ (DirichletCharacter.LFunction χ 1).re → 0 < δ → δ ≤ dirichletLTwistedSmoothedQuadraticConditionalDelta A c η q T → 0 < ε → ε < 1 → 1 ≤ X → have Q := 128 * dirichletLQuadraticConditionalCentralH q T ^ 2 / (c * ↑q ^ (-η)) + dirichletLQuadraticConditionalFixedH q (dirichletLQuadraticConditionalCentralHeight c η q T) T ^ 12 / (A * ↑q ^ (-2 * η)); have a := dirichletLTwistedSmoothedQuadraticConditionalLeft A c η q T; ‖VIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) a (-T) T‖ ≤ C * T * Q * X ^ a / ε ∧ ‖HIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) a (1 + δ) T‖ ≤ C * Q * X ^ (1 + δ) / (ε * (1 + T ^ 2)) ∧ ‖HIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) a (1 + δ) (-T)‖ ≤ C * Q * X ^ (1 + δ) / (ε * (1 + T ^ 2))

Contour norms for the variable-right quadratic pointwise rectangle.

theorem AnalyticNumberTheory.LargeSieve.exists_dirichletLTwistedSmoothedQuadraticPointwiseErrorAssembly (c η : ℝ) (hc : 0 < c) (hη : 0 < η) {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (νpos : ∀ x > 0, 0 ≤ ν x) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, ν x / x = 1) : ∃ A > 0, ∃ K > 0, ∀ {q : ℕ} [inst : NeZero q] (χ : DirichletCharacter ℂ q) {T δ ε X : ℝ}, χ ^ 2 = 1 → χ ≠ 1 → 3 ≤ T → c * ↑q ^ (-η) ≤ (DirichletCharacter.LFunction χ 1).re → 0 < δ → δ ≤ dirichletLTwistedSmoothedQuadraticConditionalDelta A c η q T → 0 < ε → ε < 1 → 1 ≤ X → have Q := 128 * dirichletLQuadraticConditionalCentralH q T ^ 2 / (c * ↑q ^ (-η)) + dirichletLQuadraticConditionalFixedH q (dirichletLQuadraticConditionalCentralHeight c η q T) T ^ 12 / (A * ↑q ^ (-2 * η)); have a := dirichletLTwistedSmoothedQuadraticConditionalLeft A c η q T; ‖χ.twistedSmoothedPsi ν ε X‖ ≤ K * (T * Q * X ^ a / ε + Q * X ^ (1 + δ) / (ε * (1 + T ^ 2)) + X ^ (1 + δ) * (1 + δ⁻¹ ^ 2) / (ε * T))

Smoothed quadratic pointwise error assembly at a variable right edge.

theorem AnalyticNumberTheory.LargeSieve.exists_quadraticPointwiseExactPrefix_of_four_payments (c η : ℝ) (hc : 0 < c) (hη : 0 < η) {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (νpos : ∀ x > 0, 0 ≤ ν x) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, ν x / x = 1) : ∃ A > 0, ∃ K > 0, ∀ {q : ℕ} [inst : NeZero q] (χ : DirichletCharacter ℂ q) {T δ ε X R : ℝ}, χ ^ 2 = 1 → χ ≠ 1 → 3 ≤ T → c * ↑q ^ (-η) ≤ (DirichletCharacter.LFunction χ 1).re → 0 < δ → δ ≤ dirichletLTwistedSmoothedQuadraticConditionalDelta A c η q T → 0 < ε → ε < 1 → 3 < X → 2 < X * ε → 0 ≤ R → have Q := 128 * dirichletLQuadraticConditionalCentralH q T ^ 2 / (c * ↑q ^ (-η)) + dirichletLQuadraticConditionalFixedH q (dirichletLQuadraticConditionalCentralHeight c η q T) T ^ 12 / (A * ↑q ^ (-2 * η)); have a := dirichletLTwistedSmoothedQuadraticConditionalLeft A c η q T; T * Q * X ^ a / ε ≤ R → Q * X ^ (1 + δ) / (ε * (1 + T ^ 2)) ≤ R → X ^ (1 + δ) * (1 + δ⁻¹ ^ 2) / (ε * T) ≤ R → ε * X * Real.log X ≤ R → ‖lambdaCharacterPrefix ⌊X⌋₊ q χ‖ ≤ K * R

Exact-prefix closure once the four variable-right quadratic payments are paid by a common ambient target R.

noncomputable def AnalyticNumberTheory.LargeSieve.quadraticPointwiseSWEta (C D : ℕ) : ℝ

The small exponent selected before q, χ; it depends only on the target loss parameters.

Equations

• AnalyticNumberTheory.LargeSieve.quadraticPointwiseSWEta C D = (4096 * (↑C + ↑D + 1))⁻¹

theorem AnalyticNumberTheory.LargeSieve.eventually_quadraticPointwiseSW_four_payments (c A : ℝ) (hc : 0 < c) (hA : 0 < A) (C D : ℕ) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (q : ℕ), NeZero q → q ≤ logConductorThreshold N C → have P := D + 40; have η := quadraticPointwiseSWEta C D; have T := nonquadraticPointwiseSWHeight P N; have δ := (Real.log ↑N)⁻¹; have ε := nonquadraticPointwiseSWEpsilon P N; have H := dirichletLQuadraticConditionalFixedH q (dirichletLQuadraticConditionalCentralHeight c η q T) T; have Q := 128 * dirichletLQuadraticConditionalCentralH q T ^ 2 / (c * ↑q ^ (-η)) + H ^ 12 / (A * ↑q ^ (-2 * η)); have a := dirichletLTwistedSmoothedQuadraticConditionalLeft A c η q T; have R := ↑N / Real.log ↑N ^ D; 3 ≤ T ∧ 0 < δ ∧ δ ≤ dirichletLTwistedSmoothedQuadraticConditionalDelta A c η q T ∧ 0 < ε ∧ ε < 1 ∧ 3 < ↑N ∧ 2 < ↑N * ε ∧ 0 ≤ R ∧ T * Q * ↑N ^ a / ε ≤ R ∧ T * Q / ε ≤ R ∧ Q * ↑N ^ (1 + δ) / (ε * (1 + T ^ 2)) ≤ R ∧ ↑N ^ (1 + δ) * (1 + δ⁻¹ ^ 2) / (ε * T) ≤ R ∧ ε * ↑N * Real.log ↑N ≤ R

At the strengthened loss P = D + 40, the quadratic scale bounds pay all four variable-right contour terms against N / log(N)^D, uniformly in the conductor.

theorem AnalyticNumberTheory.LargeSieve.exists_quadraticPointwiseSiegelWalfisz_uniform (c : ℝ) (hc : 0 < c) {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (νpos : ∀ x > 0, 0 ≤ ν x) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, ν x / x = 1) (C D : ℕ) (hSiegel : ∀ (q : ℕ) [inst : NeZero q] (χ : DirichletCharacter ℂ q), χ.IsPrimitive → χ ^ 2 = 1 → χ ≠ 1 → c * ↑q ^ (-quadraticPointwiseSWEta C D) ≤ (DirichletCharacter.LFunction χ 1).re) : ∃ K > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (q : ℕ), NeZero q → q ≤ logConductorThreshold N C → ∀ (χ : DirichletCharacter ℂ q), χ.IsPrimitive → χ ^ 2 = 1 → χ ≠ 1 → ∀ y ≤ N, ‖lambdaCharacterPrefix y q χ‖ ≤ K * ↑N / Real.log ↑N ^ D

Uniform-in-y quadratic pointwise Siegel--Walfisz bound from the selected Landau--Siegel lower bound.

theorem AnalyticNumberTheory.LargeSieve.exists_quadraticPointwiseSiegelWalfisz_uniform_of_rawLandauSiegelLowerBound (hLandauSiegel : RawLandauSiegelLowerBound) {ν : ℝ → ℝ} (diffν : ContDiff ℝ 1 ν) (νpos : ∀ x > 0, 0 ≤ ν x) (suppν : Function.support ν ⊆ Set.Icc (1 / 2) 2) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, ν x / x = 1) (C D : ℕ) : ∃ K > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (q : ℕ), NeZero q → q ≤ logConductorThreshold N C → ∀ (χ : DirichletCharacter ℂ q), χ.IsPrimitive → χ ^ 2 = 1 → χ ≠ 1 → ∀ y ≤ N, ‖lambdaCharacterPrefix y q χ‖ ≤ K * ↑N / Real.log ↑N ^ D

The raw Landau--Siegel hypothesis alone now supplies the quadratic uniform-in-prefix pointwise bound.