MathlibNt.AnalyticNumberTheory.LargeSieve.DirichLTwistedNonquadraticPointwiseSiegelWalfisz

Uniform log log control of the conductor-height logarithm at the chosen polylogarithmic height. This is the arithmetic input needed to make the left edge exponential dominate every prescribed logarithmic loss.

source

theorem AnalyticNumberTheory.LargeSieve.eventually_nonquadraticPointwiseSW_leftEdge (C D E : ℕ) :

∀ᶠ (N : ℕ) in Filter.atTop , ∀ (q : ℕ), NeZero q → q ≤ logConductorThreshold N C → ↑N ^ dirichletLTwistedSmoothedConductorLogFinalLeft q (nonquadraticPointwiseSWHeight D N) ≤ ↑N / Real.log ↑N ^ E

The quantitative left edge supplies an arbitrary fixed logarithmic saving, uniformly for conductors below logConductorThreshold. This is the genuinely non-polynomial part of the parameter selection.

source

theorem AnalyticNumberTheory.LargeSieve.rpow_one_add_inv_log_nat (N : ℕ) (hN : 1 < N) :

↑N ^ (1 + (Real.log ↑N)⁻¹) = Real.exp 1 * ↑N

source

theorem AnalyticNumberTheory.LargeSieve.norm_lambdaCharacterPrefix_le_const_mul_self (N q : ℕ) [NeZero q] (χ : DirichletCharacter ℂ q) :

‖lambdaCharacterPrefix N q χ‖ ≤ (Real.log 4 + 4) * ↑N

The exact twisted prefix has the same elementary linear majorant as Chebyshev's psi, uniformly in the character. This is used to absorb all prefixes below the square-root split.

source

theorem AnalyticNumberTheory.LargeSieve.exists_uniform_twistedSmoothedPsiClose {SmoothingF : ℝ → ℝ} (_diffSmoothingF : ContDiff ℝ 1 SmoothingF) (suppSmoothingF : Function.support SmoothingF ⊆ Set.Icc (1 / 2) 2) (SmoothingFnonneg : ∀ x > 0, 0 ≤ SmoothingF x) (mass_one : ∫ (x : ℝ) in Set.Ioi 0, SmoothingF x / x = 1) :

∃ C > 0, ∀ {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (X : ℝ), 3 < X → ∀ (ε : ℝ), 0 < ε → ε < 1 → 2 < X * ε → ‖χ.twistedSmoothedPsi SmoothingF ε X - lambdaCharacterPrefix ⌊X⌋₊ q χ‖ ≤ C * ε * X * Real.log X

The smoothing-removal constant is uniform in both the modulus and the character. This is the quantifier order needed by pointwise applications.

source

theorem AnalyticNumberTheory.LargeSieve.exists_nonquadraticExactPrefix_of_four_payments {ν : ℝ → ℝ} (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) :

∃ K > 0, ∀ {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {T d ε X R : ℝ}, χ ^ 2 ≠ 1 → 3 ≤ T → 0 < d → d ≤ 1 → 0 < ε → ε < 1 → 3 < X → 2 < X * ε → 0 ≤ R → T * dirichletLTwistedSmoothedConductorLogLM q T ^ 11 * X ^ dirichletLTwistedSmoothedConductorLogFinalLeft q T / ε ≤ R → dirichletLTwistedSmoothedConductorLogLM q T ^ 11 * X ^ (1 + d) / (ε * (1 + T ^ 2)) ≤ R → X ^ (1 + d) * (1 + d⁻¹ ^ 2) / (ε * T) ≤ R → ε * X * Real.log X ≤ R → ‖lambdaCharacterPrefix ⌊X⌋₊ q χ‖ ≤ K * R

Exact-prefix closure of the nonquadratic contour once the four scalar payments (left edge, horizontal edges, right tails, and smoothing removal) have been made. The constants are chosen before the modulus and character.

source

theorem AnalyticNumberTheory.LargeSieve.eventually_nonquadraticPointwiseSW_four_payments (C D : ℕ) :

∀ᶠ (N : ℕ) in Filter.atTop , ∀ (q : ℕ), NeZero q → q ≤ logConductorThreshold N C → have P := D + 20; have T := nonquadraticPointwiseSWHeight P N; have d := nonquadraticPointwiseSWDelta N; have ε := nonquadraticPointwiseSWEpsilon P N; have R := ↑N / Real.log ↑N ^ D; 3 ≤ T ∧ 0 < d ∧ d ≤ 1 ∧ 0 < ε ∧ ε < 1 ∧ 3 < ↑N ∧ 2 < ↑N * ε ∧ 0 ≤ R ∧ T * dirichletLTwistedSmoothedConductorLogLM q T ^ 11 * ↑N ^ dirichletLTwistedSmoothedConductorLogFinalLeft q T / ε ≤ R ∧ dirichletLTwistedSmoothedConductorLogLM q T ^ 11 * ↑N ^ (1 + d) / (ε * (1 + T ^ 2)) ≤ R ∧ ↑N ^ (1 + d) * (1 + d⁻¹ ^ 2) / (ε * T) ≤ R ∧ ε * ↑N * Real.log ↑N ≤ R

At the strengthened loss P = D + 20, the prescribed polylogarithmic height, reciprocal-log displacement, and smoothing width pay all four contour terms against the common target N / log(N)^D, uniformly in the conductor.

source

theorem AnalyticNumberTheory.LargeSieve.exists_nonquadraticPointwiseSiegelWalfisz_uniform {ν : ℝ → ℝ} (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) (C D : ℕ) :

∃ K > 0, ∀ᶠ (N : ℕ) in Filter.atTop , ∀ (q : ℕ), NeZero q → q ≤ logConductorThreshold N C → ∀ (χ : DirichletCharacter ℂ q), χ ^ 2 ≠ 1 → ∀ y ≤ N, ‖lambdaCharacterPrefix y q χ‖ ≤ K * ↑N / Real.log ↑N ^ D

Uniform-in-y nonquadratic pointwise Siegel--Walfisz bound. The conductor cutoff is measured at the ambient endpoint N; for large prefixes the same N-based contour is used, while prefixes below 2√N are paid by the elementary Chebyshev bound.