def AnalyticNumberTheory.LargeSieve.nonquadraticPointwiseSWHeightExponent (D : ℕ) : ℕ

The polylogarithmic height used in the pointwise nonquadratic contour.

Equations

• AnalyticNumberTheory.LargeSieve.nonquadraticPointwiseSWHeightExponent D = 2 * D + 30

noncomputable def AnalyticNumberTheory.LargeSieve.nonquadraticPointwiseSWHeight (D N : ℕ) : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.nonquadraticPointwiseSWHeight D N = Real.log ↑N ^ AnalyticNumberTheory.LargeSieve.nonquadraticPointwiseSWHeightExponent D

noncomputable def AnalyticNumberTheory.LargeSieve.nonquadraticPointwiseSWEpsilon (D N : ℕ) : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.nonquadraticPointwiseSWEpsilon D N = (Real.log ↑N ^ (D + 3))⁻¹

noncomputable def AnalyticNumberTheory.LargeSieve.nonquadraticPointwiseSWDelta (N : ℕ) : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.nonquadraticPointwiseSWDelta N = (Real.log ↑N)⁻¹

theorem AnalyticNumberTheory.LargeSieve.dirichletLTwistedSmoothedConductorLogLM_le_loglog_pointwise (C D N q : ℕ) [NeZero q] (hlog : Real.exp 1 ≤ Real.log ↑N) (hq : q ≤ logConductorThreshold N C) : dirichletLTwistedSmoothedConductorLogLM q (nonquadraticPointwiseSWHeight D N) ≤ ↑(C + nonquadraticPointwiseSWHeightExponent D + 3) * Real.log (Real.log ↑N)

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.

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.

theorem AnalyticNumberTheory.LargeSieve.rpow_one_add_inv_log_nat (N : ℕ) (hN : 1 < N) : ↑N ^ (1 + (Real.log ↑N)⁻¹) = Real.exp 1 * ↑N

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.

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.

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.

theorem AnalyticNumberTheory.LargeSieve.pointwiseSW_tail_smoothing_payments {X L : ℝ} {D P : ℕ} (hX : 0 ≤ X) (hL : 2 ≤ L) (hDP : D + 20 ≤ P) : Real.exp 1 * X * (1 + L ^ 2) / ((L ^ (P + 3))⁻¹ * L ^ (2 * P + 30)) ≤ X / L ^ D ∧ (L ^ (P + 3))⁻¹ * X * L ≤ X / L ^ D

Common scalar payments for the right tails and smoothing removal. Only the shared height and smoothing exponents enter; the left-edge decay and any additional quadratic base payment remain in their respective branches.

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.

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.