Fixed-height quadratic rectangles away from height zero

The power-width quadratic headline contains the term 1 / |2t|. Consequently it does not by itself contain a positive-width rectangle crossing t = 0. This file extracts the strongest literal rectangular consequence: two closed rectangles at heights τ ≤ |t| ≤ T. It also records the quantitative derivative and logarithmic-derivative estimates available there. The latter keeps the actual L-value in the denominator; no lower bound for that value is silently postulated.

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

A uniform majorant for the height-dependent scale on τ ≤ |t| ≤ T.

Equations

• AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalFixedH q τ T = 1 + Real.log ↑(AnalyticNumberTheory.LargeSieve.dirichletLNonquadraticConductorLogCutoff q T) + (1 + Real.log (2 * T + 2) + 1 / (2 * τ))

noncomputable def AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalFixedLeft (A η : ℝ) (q : ℕ) (τ T : ℝ) : ℝ

The fixed left edge obtained from a power-width headline on an annulus of heights.

Equations

• AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalFixedLeft A η q τ T = 1 - A * ↑q ^ (-2 * η) / AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalFixedH q τ T ^ 12

def AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalUpperRectangle (A η : ℝ) (q : ℕ) (τ T : ℝ) : Set ℂ

The upper fixed rectangle, with heights from τ to T.

Equations

• AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalUpperRectangle A η q τ T = (↑(AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalFixedLeft A η q τ T) + Complex.I * ↑τ).Rectangle (2 + Complex.I * ↑T)

def AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalLowerRectangle (A η : ℝ) (q : ℕ) (τ T : ℝ) : Set ℂ

The lower fixed rectangle, with heights from -T to -τ.

Equations

• AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalLowerRectangle A η q τ T = (↑(AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalFixedLeft A η q τ T) - Complex.I * ↑T).Rectangle (2 - Complex.I * ↑τ)

theorem AnalyticNumberTheory.LargeSieve.dirichletLQuadraticConditionalPowerZeroFreeH_le_fixedH {q : ℕ} [NeZero q] {τ T t : ℝ} (hτ : 0 < τ) (_hT : τ ≤ T) (htlow : τ ≤ |t|) (hthigh : |t| ≤ T) : dirichletLQuadraticConditionalPowerZeroFreeH q t ≤ dirichletLQuadraticConditionalFixedH q τ T

On a closed height annulus, the singular height scale has a genuine fixed majorant.

theorem AnalyticNumberTheory.LargeSieve.LFunction_ne_zero_on_quadraticConditionalUpperRectangle {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) {A η τ T : ℝ} (hA : 0 < A) (hτ : 0 < τ) (hT : τ ≤ T) (hzero : ∀ (β t : ℝ), β ∈ Set.Ico (1 - A * ↑q ^ (-2 * η) / dirichletLQuadraticConditionalPowerZeroFreeH q t ^ 12) 1 → DirichletCharacter.LFunction χ (↑β + Complex.I * ↑t) ≠ 0) (s : ℂ) : s ∈ dirichletLQuadraticConditionalUpperRectangle A η q τ T → DirichletCharacter.LFunction χ s ≠ 0

The all-height power-width hypothesis gives zero-freeness on the upper fixed rectangle.

theorem AnalyticNumberTheory.LargeSieve.LFunction_ne_zero_on_quadraticConditionalLowerRectangle {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) {A η τ T : ℝ} (hA : 0 < A) (hτ : 0 < τ) (hT : τ ≤ T) (hzero : ∀ (β t : ℝ), β ∈ Set.Ico (1 - A * ↑q ^ (-2 * η) / dirichletLQuadraticConditionalPowerZeroFreeH q t ^ 12) 1 → DirichletCharacter.LFunction χ (↑β + Complex.I * ↑t) ≠ 0) (s : ℂ) : s ∈ dirichletLQuadraticConditionalLowerRectangle A η q τ T → DirichletCharacter.LFunction χ s ≠ 0

The analogous lower fixed rectangle is zero-free.

theorem AnalyticNumberTheory.LargeSieve.logDerivative_holomorphicOn_quadraticConditionalUpperRectangle {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) {A η τ T : ℝ} (hA : 0 < A) (hτ : 0 < τ) (hT : τ ≤ T) (hzero : ∀ (β t : ℝ), β ∈ Set.Ico (1 - A * ↑q ^ (-2 * η) / dirichletLQuadraticConditionalPowerZeroFreeH q t ^ 12) 1 → DirichletCharacter.LFunction χ (↑β + Complex.I * ↑t) ≠ 0) : HolomorphicOn (fun (s : ℂ) => deriv (DirichletCharacter.LFunction χ) s / DirichletCharacter.LFunction χ s) (dirichletLQuadraticConditionalUpperRectangle A η q τ T)

The logarithmic derivative is holomorphic on the upper fixed rectangle.

theorem AnalyticNumberTheory.LargeSieve.norm_logDerivative_le_derivativeBudget_div_LValue {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) {σ t : ℝ} (hσhalf : 1 / 2 ≤ σ) (hσtwo : σ ≤ 2) (hnear : 1 - 1 / Real.log ↑(DirichletLGlobalConductorLogValueBound.dirichletLConductorHeightCutoff q t) ≤ σ) : ‖deriv (DirichletCharacter.LFunction χ) (↑σ + Complex.I * ↑t) / DirichletCharacter.LFunction χ (↑σ + Complex.I * ↑t)‖ ≤ 64 * (1 + Real.log ↑(DirichletLGlobalConductorLogValueBound.dirichletLConductorHeightCutoff q t)) ^ 2 / ‖DirichletCharacter.LFunction χ (↑σ + Complex.I * ↑t)‖

Explicit quantitative bound supplied by the production derivative theorem. Unlike a fictitious uniform lower bound, this statement displays the exact remaining denominator.