A fixed quadratic rectangle crossing height zero

The high-height quadratic argument contains 1 / |2t|, so its fixed-height majorant degenerates as t → 0. Here the low two-segment argument is kept separate. A fixed conductor cutoff at height T, paid for directly by the raw lower bound for L(1, χ), supplies a positive central band. The existing annular rectangles cover the two remaining bands. Their common left edge then gives one rectangle across the whole interval [-T,T].

noncomputable def AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalCentralH (q : ℕ) (T : ℝ) : ℝ

The nonsingular conductor scale used in the central low-height band.

Equations

• AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalCentralH q T = 1 + Real.log ↑(AnalyticNumberTheory.LargeSieve.dirichletLNonquadraticConductorLogCutoff q T)

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

A positive central half-height whose vertical derivative budget is paid by c q⁻η. The minimum also makes it automatically no larger than T.

Equations

• AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalCentralHeight c η q T = min T (c * ↑q ^ (-η) / (256 * AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalCentralH q T ^ 2))

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

The final width uses the annular majorant at the positive central cutoff.

Equations

• AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalCrossZeroWidth A c η q T = A * ↑q ^ (-2 * η) / AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalFixedH q (AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalCentralHeight c η q T) T ^ 12

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

One fixed rectangle crossing t = 0.

Equations

• AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalCrossZeroRectangle A c η q T = (↑(1 - AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalCrossZeroWidth A c η q T) - Complex.I * ↑T).Rectangle (2 + Complex.I * ↑T)

theorem AnalyticNumberTheory.LargeSieve.exists_LFunction_ne_zero_on_quadraticConditionalCrossZeroRectangle (c η : ℝ) (hc : 0 < c) (hη : 0 < η) : ∃ (A : ℝ), 0 < A ∧ ∀ (q : ℕ) [inst : NeZero q] (χ : DirichletCharacter ℂ q) (T : ℝ), χ ^ 2 = 1 → χ ≠ 1 → 0 < T → c * ↑q ^ (-η) ≤ (DirichletCharacter.LFunction χ 1).re → ∀ s ∈ dirichletLQuadraticConditionalCrossZeroRectangle A c η q T, DirichletCharacter.LFunction χ s ≠ 0

A raw quadratic L(1) lower bound produces a single positive-width fixed rectangle over every bounded height interval, including height zero.