noncomputable def AnalyticNumberTheory.LargeSieve.dirichletLNonquadraticConductorLogHeightBlock (T : ℝ) : ℕ

The fixed integral height block attached to a height bound T.

Equations

• AnalyticNumberTheory.LargeSieve.dirichletLNonquadraticConductorLogHeightBlock T = ⌊T⌋₊ + 1

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

The fixed-height conductor cutoff M(q,T) = q * (⌊T⌋₊ + 1).

Equations

• AnalyticNumberTheory.LargeSieve.dirichletLNonquadraticConductorLogCutoff q T = q * AnalyticNumberTheory.LargeSieve.dirichletLNonquadraticConductorLogHeightBlock T

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

The left edge associated with the fixed conductor-height cutoff.

Equations

• AnalyticNumberTheory.LargeSieve.dirichletLNonquadraticConductorLogLeftEdge q T = 1 - 1 / (274877906944 * (1 + Real.log ↑(AnalyticNumberTheory.LargeSieve.dirichletLNonquadraticConductorLogCutoff q T)) ^ 9)

def AnalyticNumberTheory.LargeSieve.dirichletLNonquadraticConductorLogRectangle (q : ℕ) (T : ℝ) : Set ℂ

The closed fixed-height rectangle, extending to real part 2 and heights ±T.

Equations

• AnalyticNumberTheory.LargeSieve.dirichletLNonquadraticConductorLogRectangle q T = (↑(AnalyticNumberTheory.LargeSieve.dirichletLNonquadraticConductorLogLeftEdge q T) - Complex.I * ↑T).Rectangle (2 + Complex.I * ↑T)

theorem AnalyticNumberTheory.LargeSieve.dirichletLHeightBlock_le_fixedHeightBlock {t T : ℝ} (ht : |t| ≤ T) : DirichletLGlobalConductorLogValueBound.dirichletLHeightBlock t ≤ dirichletLNonquadraticConductorLogHeightBlock T

theorem AnalyticNumberTheory.LargeSieve.dirichletLConductorHeightCutoff_le_fixedHeightCutoff {q : ℕ} {t T : ℝ} (ht : |t| ≤ T) : DirichletLGlobalConductorLogValueBound.dirichletLConductorHeightCutoff q t ≤ dirichletLNonquadraticConductorLogCutoff q T

theorem AnalyticNumberTheory.LargeSieve.four_le_dirichletLNonquadraticConductorLogCutoff {q : ℕ} [NeZero q] {T : ℝ} (hT : 3 ≤ T) : 4 ≤ dirichletLNonquadraticConductorLogCutoff q T

theorem AnalyticNumberTheory.LargeSieve.one_half_lt_dirichletLNonquadraticConductorLogLeftEdge {q : ℕ} [NeZero q] {T : ℝ} (hT : 3 ≤ T) : 1 / 2 < dirichletLNonquadraticConductorLogLeftEdge q T

The fixed left edge is explicitly to the right of 1/2.

theorem AnalyticNumberTheory.LargeSieve.LFunction_ne_zero_on_nonquadratic_conductorLogRectangle {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {T : ℝ} (hχsq : χ ^ 2 ≠ 1) (hT : 3 ≤ T) (s : ℂ) : s ∈ dirichletLNonquadraticConductorLogRectangle q T → DirichletCharacter.LFunction χ s ≠ 0

Every nonquadratic Dirichlet L-function is zero-free on the fixed-height conductor-logarithmic rectangle.

theorem AnalyticNumberTheory.LargeSieve.logDerivative_holomorphicOn_nonquadratic_conductorLogRectangle {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {T : ℝ} (hχsq : χ ^ 2 ≠ 1) (hT : 3 ≤ T) : HolomorphicOn (fun (s : ℂ) => deriv (DirichletCharacter.LFunction χ) s / DirichletCharacter.LFunction χ s) (dirichletLNonquadraticConductorLogRectangle q T)

The logarithmic derivative is holomorphic throughout the fixed rectangle.