noncomputable def AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedQuadraticConditionalLeft (A c η : ℝ) (q : ℕ) (T : ℝ) : ℝ

The quadratic contour uses the full conditional cross-zero width and a quarter-width extension into the absolutely convergent half-plane.

Equations

• AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedQuadraticConditionalLeft A c η q T = 1 - AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalCrossZeroWidth A c η q T

noncomputable def AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedQuadraticConditionalDelta (A c η : ℝ) (q : ℕ) (T : ℝ) : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedQuadraticConditionalDelta A c η q T = AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalCrossZeroWidth A c η q T / 4

noncomputable def AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedQuadraticConditionalRight (A c η : ℝ) (q : ℕ) (T : ℝ) : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedQuadraticConditionalRight A c η q T = 1 + AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedQuadraticConditionalDelta A c η q T

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

The finite quadratic Perron rectangle.

Equations

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

theorem AnalyticNumberTheory.LargeSieve.norm_logDerivative_le_on_quadraticConditionalPerronLeft (Z : ℝ) (hZ : 0 < Z) (hzeta : ∀ (x u : ℝ), 0 < x → x ≤ 1 → u ≠ 0 → ‖riemannZeta (1 + ↑x + Complex.I * ↑u)‖ ≤ Z * (1 + Real.log (|u| + 2) + 1 / |u|)) {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) (hχ : χ ≠ 1) {A c η T t : ℝ} (hA : 0 < A) (hAc : A ≤ c / 256) (hAhalf : A ≤ 1 / 2) (hAsmall : A ≤ 1 / (16 * Z * 192 ^ 4)) (hc : 0 < c) (hη : 0 < η) (hT : 0 < T) (hSiegel : c * ↑q ^ (-η) ≤ (DirichletCharacter.LFunction χ 1).re) (hw : 0 < dirichletLQuadraticConditionalCrossZeroWidth A c η q T) (ht : |t| ≤ T) : ‖deriv (DirichletCharacter.LFunction χ) (↑(dirichletLTwistedSmoothedQuadraticConditionalLeft A c η q T) + Complex.I * ↑t) / DirichletCharacter.LFunction χ (↑(dirichletLTwistedSmoothedQuadraticConditionalLeft A c η q T) + Complex.I * ↑t)‖ ≤ 128 * dirichletLQuadraticConditionalCentralH q T ^ 2 / (c * ↑q ^ (-η)) + dirichletLQuadraticConditionalFixedH q (dirichletLQuadraticConditionalCentralHeight c η q T) T ^ 12 / (A * ↑q ^ (-2 * η))

The whole-band estimate pays the complete left edge of the quadratic Perron rectangle. This is the quantitative edge needed by the later Bochner integral estimate; no nonquadratic hypothesis occurs.

theorem AnalyticNumberTheory.LargeSieve.twistedSmoothedPerronIntegrand_holomorphicOn_quadraticConditionalRectangle {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) {ν : ℝ → ℝ} (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) (dirichletLTwistedSmoothedQuadraticConditionalRectangle A c η q T)

A zero-free quadratic cross-zero rectangle gives a holomorphic Perron integrand on the narrower variable-right rectangle.

theorem AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedPerron_quadraticConditionalFiniteContourIdentity {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) {ν : ℝ → ℝ} (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) (dirichletLTwistedSmoothedQuadraticConditionalRight A c η q T) (-T) T - VIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) (dirichletLTwistedSmoothedQuadraticConditionalLeft A c η q T) (-T) T = HIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) (dirichletLTwistedSmoothedQuadraticConditionalLeft A c η q T) (dirichletLTwistedSmoothedQuadraticConditionalRight A c η q T) T - HIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) (dirichletLTwistedSmoothedQuadraticConditionalLeft A c η q T) (dirichletLTwistedSmoothedQuadraticConditionalRight A c η q T) (-T)

Exact finite contour shift for the quadratic conditional rectangle.

theorem AnalyticNumberTheory.LargeSieve.exists_dirichletLTwistedSmoothedPerron_quadraticConditionalFiniteContourIdentity (c η : ℝ) (hc : 0 < c) (hη : 0 < η) : ∃ (A : ℝ), 0 < A ∧ ∀ (q : ℕ) [inst : NeZero q] (χ : DirichletCharacter ℂ q) (T : ℝ), χ ^ 2 = 1 → χ ≠ 1 → 3 ≤ T → c * ↑q ^ (-η) ≤ (DirichletCharacter.LFunction χ 1).re → ∀ {ν : ℝ → ℝ}, ContDiff ℝ 1 ν → (∀ x > 0, 0 ≤ ν x) → Function.support ν ⊆ Set.Icc (1 / 2) 2 → ∫ (x : ℝ) in Set.Ioi 0, ν x / x = 1 → ∀ {X ε : ℝ}, 0 < X → 0 < ε → ε < 1 → VIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) (dirichletLTwistedSmoothedQuadraticConditionalRight A c η q T) (-T) T - VIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) (dirichletLTwistedSmoothedQuadraticConditionalLeft A c η q T) (-T) T = HIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) (dirichletLTwistedSmoothedQuadraticConditionalLeft A c η q T) (dirichletLTwistedSmoothedQuadraticConditionalRight A c η q T) T - HIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) (dirichletLTwistedSmoothedQuadraticConditionalLeft A c η q T) (dirichletLTwistedSmoothedQuadraticConditionalRight A c η q T) (-T)

Raw Landau--Siegel data select one positive quadratic contour width, after which every primitive/nonprincipal quadratic character admits the exact finite Perron shift. Unlike the old contour theorem this has no χ² ≠ 1 premise.