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

The fixed cutoff used by the quantitative conductor-logarithmic contour.

Equations

• AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedConductorLogCutoff q T = AnalyticNumberTheory.LargeSieve.dirichletLNonquadraticConductorLogCutoff q T

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

1 + log M(q,T), kept as a named contour parameter.

Equations

• AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedConductorLogLM q T = 1 + Real.log ↑(AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedConductorLogCutoff q T)

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

The quantitative 2^42 left edge.

Equations

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

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

The closed quantitative contour rectangle from the 2^42 edge to 2.

Equations

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

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

At height at least three, the quantitative edge lies strictly right of 1/2.

theorem AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedConductorLogLeftEdge_lt_one {q : ℕ} [NeZero q] {T : ℝ} (hT : 3 ≤ T) : dirichletLTwistedSmoothedConductorLogLeftEdge q T < 1

The quantitative edge lies strictly left of one.

theorem AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedConductorLogRectangle_subset (q : ℕ) [NeZero q] (T : ℝ) (hT : 3 ≤ T) : dirichletLTwistedSmoothedConductorLogRectangle q T ⊆ dirichletLNonquadraticConductorLogRectangle q T

The 2^42 contour is contained in the accepted 2^38 zero-free rectangle.

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

The logarithmic derivative is holomorphic on the quantitative contour.

theorem AnalyticNumberTheory.LargeSieve.twistedSmoothedPerronIntegrand_holomorphicOn_conductorLogRectangle {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {T : ℝ} (hχsq : χ ^ 2 ≠ 1) (hT : 3 ≤ T) {ν : ℝ → ℝ} (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) (dirichletLTwistedSmoothedConductorLogRectangle q T)

The complete smoothed Perron integrand is holomorphic on the quantitative contour.

theorem AnalyticNumberTheory.LargeSieve.norm_logDeriv_LFunction_le_on_conductorLogLeftEdge {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {T t : ℝ} (hχsq : χ ^ 2 ≠ 1) (_hT : 3 ≤ T) (ht : |t| ≤ T) : ‖deriv (DirichletCharacter.LFunction χ) (↑(dirichletLTwistedSmoothedConductorLogLeftEdge q T) + Complex.I * ↑t) / DirichletCharacter.LFunction χ (↑(dirichletLTwistedSmoothedConductorLogLeftEdge q T) + Complex.I * ↑t)‖ ≤ 2199023255552 * dirichletLTwistedSmoothedConductorLogLM q T ^ 9

Along the left edge, the local 2^42 strip estimate is uniform in |t| ≤ T.

theorem AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedPerron_conductorLogRectangleIntegral_eq_zero {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {T : ℝ} (hχsq : χ ^ 2 ≠ 1) (hT : 3 ≤ T) {ν : ℝ → ℝ} (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) (↑(dirichletLTwistedSmoothedConductorLogLeftEdge q T) - Complex.I * ↑T) (2 + Complex.I * ↑T) = 0

The complete integral around the quantitative rectangle vanishes.

theorem AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedPerron_conductorLogFiniteContourIdentity {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {T : ℝ} (hχsq : χ ^ 2 ≠ 1) (hT : 3 ≤ T) {ν : ℝ → ℝ} (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) 2 (-T) T - VIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) (dirichletLTwistedSmoothedConductorLogLeftEdge q T) (-T) T = HIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) (dirichletLTwistedSmoothedConductorLogLeftEdge q T) 2 T - HIntegral (χ.twistedSmoothedPerronIntegrand ν ε X) (dirichletLTwistedSmoothedConductorLogLeftEdge q T) 2 (-T)

Finite contour identity: V₂ - V_left = H_top - H_bottom.