AngularKummerPrimeSum.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The raw angular Chebyshev estimate implies the ordinary prime Siegel--Walfisz bound. A square-root initial segment is bounded directly; partial summation on the remaining interval has bounded reciprocal-log variation.

lemma OAI.CubicFirstMoment.reciprocal_log_variation line 16
lemma OAI.CubicFirstMoment.angularKummerCharacter_norm_le_one line 81

theorem OAI.CubicFirstMoment.angular_kummer_prime_logSaving line 88

Source documentation

The unweighted prime estimate is derived from the raw published Chebyshev error; it is not an additional analytic input.

theorem angular_kummer_prime_logSaving (hEF : AngularKummerPrimeExplicitEstimate)
    (ℓ : ℤ) (hℓ : ℓ ≠ 0) (A D : ℝ) (hA : 0 < A) (hD : 0 < D) :
    ∃ C X₀ : ℝ, 0 < C ∧ 1 < X₀ ∧ ∀ X : ℝ, X₀ ≤ X →
      ∀ v : Eisenstein, v ≠ 0 → (¬∃ n : Eisenstein, n^3 = v) →
      norm v ≤ (Real.log X)^A →
      ‖primeCutoffSum (angularKummerCharacter ℓ v) X‖ ≤ C*X/(Real.log X)^D := by
…

Mentions: OAI.CubicFirstMoment.AngularKummerPrimeExplicitEstimate, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primeCutoffSum, OAI.CubicFirstMoment.angularKummerCharacter