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

The accepted 2^42 width; the final left edge uses one quarter of it.

Equations

• AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedConductorLogEdgeWidth q T = 1 / (4398046511104 * AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedConductorLogLM q T ^ 9)

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

The final left edge 1 - w/4.

Equations

• AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedConductorLogFinalLeft q T = 1 - AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedConductorLogEdgeWidth q T / 4

def AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedConductorLogRight (d : ℝ) : ℝ

The variable right edge 1 + d.

Equations

• AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedConductorLogRight d = 1 + d

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

The final variable-right rectangle.

Equations

• AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedConductorLogEdgeRectangle q T d = (↑(AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedConductorLogFinalLeft q T) - Complex.I * ↑T).Rectangle (↑(AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedConductorLogRight d) + Complex.I * ↑T)

theorem AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedConductorLogEdgeRectangle_subset (q : ℕ) [NeZero q] (T d : ℝ) (hT : 3 ≤ T) (hd0 : 0 < d) (hd1 : d ≤ 1) : dirichletLTwistedSmoothedConductorLogEdgeRectangle q T d ⊆ dirichletLTwistedSmoothedConductorLogRectangle q T

The final rectangle is contained in the already accepted quantitative rectangle.

theorem AnalyticNumberTheory.LargeSieve.twistedSmoothedPerronIntegrand_holomorphicOn_conductorLogEdgeRectangle {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {T d : ℝ} (hχsq : χ ^ 2 ≠ 1) (hT : 3 ≤ T) (hd0 : 0 < d) (hd1 : d ≤ 1) {ν : ℝ → ℝ} (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 : ℝ} (X_pos : 0 < X) {ε : ℝ} (εpos : 0 < ε) (ε_lt_one : ε < 1) : HolomorphicOn (χ.twistedSmoothedPerronIntegrand ν ε X) (dirichletLTwistedSmoothedConductorLogEdgeRectangle q T d)

The complete Perron integrand is holomorphic on every final variable-right rectangle.

theorem AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedPerron_conductorLogEdgeRectangleIntegral_eq_zero {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {T d : ℝ} (hχsq : χ ^ 2 ≠ 1) (hT : 3 ≤ T) (hd0 : 0 < d) (hd1 : d ≤ 1) {ν : ℝ → ℝ} (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 : ℝ} (X_pos : 0 < X) {ε : ℝ} (εpos : 0 < ε) (ε_lt_one : ε < 1) : RectangleIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) (↑(dirichletLTwistedSmoothedConductorLogFinalLeft q T) - Complex.I * ↑T) (↑(dirichletLTwistedSmoothedConductorLogRight d) + Complex.I * ↑T) = 0

The final variable-right rectangle integral vanishes.

theorem AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedPerron_conductorLogEdgeFiniteContourIdentity {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {T d : ℝ} (hχsq : χ ^ 2 ≠ 1) (hT : 3 ≤ T) (hd0 : 0 < d) (hd1 : d ≤ 1) {ν : ℝ → ℝ} (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 : ℝ} (X_pos : 0 < X) {ε : ℝ} (εpos : 0 < ε) (ε_lt_one : ε < 1) : VIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) (dirichletLTwistedSmoothedConductorLogRight d) (-T) T - VIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) (dirichletLTwistedSmoothedConductorLogFinalLeft q T) (-T) T = HIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) (dirichletLTwistedSmoothedConductorLogFinalLeft q T) (dirichletLTwistedSmoothedConductorLogRight d) T - HIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) (dirichletLTwistedSmoothedConductorLogFinalLeft q T) (dirichletLTwistedSmoothedConductorLogRight d) (-T)

Finite contour identity with a genuinely variable right edge.

theorem AnalyticNumberTheory.LargeSieve.norm_dirichletLFunction_ge_sub_one_div {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {σ t : ℝ} (hσ : 1 < σ) : (σ - 1) / σ ≤ ‖DirichletCharacter.LFunction χ (↑σ + Complex.I * ↑t)‖

In the absolute-convergence half-plane, the L-value has the elementary lower bound (σ - 1) / σ.

theorem AnalyticNumberTheory.LargeSieve.norm_logDeriv_LFunction_le_on_conductorLogEdgeRectangle {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {T d η σ : ℝ} (hχsq : χ ^ 2 ≠ 1) (hT : 3 ≤ T) (hd0 : 0 < d) (hd1 : d ≤ 1) (hη : |η| ≤ T) (hσleft : dirichletLTwistedSmoothedConductorLogFinalLeft q T ≤ σ) (hσright : σ ≤ dirichletLTwistedSmoothedConductorLogRight d) : ‖deriv (DirichletCharacter.LFunction χ) (↑σ + Complex.I * ↑η) / DirichletCharacter.LFunction χ (↑σ + Complex.I * ↑η)‖ ≤ 2251799813685248 * dirichletLTwistedSmoothedConductorLogLM q T ^ 11

Uniform 2^51 LM^11 logarithmic-derivative bound on the entire final rectangle. The left branch is anchored at 1-w/4 and uses the sharp derivative estimate over a segment of length at most w/2; the right branch uses the quantitative absolute-convergence lower bound.