PublishedAngularKummerPrime.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Fixed-angular prime estimates for the literal ramified numerator

This is the nonexceptional degree-two specialization of Kaneko--Thorner, Highly uniform prime number theorems, Ann. Inst. Fourier 75 (2025), Theorem 1.2, pp.1904--1905 (Iwaniec--Kowalski, Theorem 5.13), with the fixed-type zero-free region of Rajan (1998), Proposition 1 and Section 1. The finite character is cubicNumeratorChar of modulus 9*v; its identification on primary elements is proved from CubicSupplementaryPeriodicity in CubicNumeratorCharacter.

The analytic conductor majorant is 3 * N(9*v) * (|ell|/2+3) * (|ell|/2+4): N(9*v)=81*N(v), so its constant is 243. The nonzero angular type excludes a principal/exceptional-real character. The raw input below retains the exponential conductor error and the prime-power deletion term. Logarithmic and weighted estimates are deductions, not inputs.

def OAI.CubicFirstMoment.angularKummerCharacter line 29
def OAI.CubicFirstMoment.angularKummerConductorFactor line 32
def OAI.CubicFirstMoment.angularKummerAnalyticConductor line 35
lemma OAI.CubicFirstMoment.angularKummerConductorFactor_ge_one line 38
lemma OAI.CubicFirstMoment.angularKummerAnalyticConductor_ge_one line 44
def OAI.CubicFirstMoment.AngularKummerPrimeExplicitEstimate line 55
Source documentation
Precisely the raw fixed-angular prime Chebyshev estimate for the finite numerator character, including ramification and unit factors. No stopped-sequence, smooth-weight, or dispersion conclusion is assumed.
```
def AngularKummerPrimeExplicitEstimate : Prop :=
…
```
lemma OAI.CubicFirstMoment.angularKummerCharacter_eq_residue line 63
theorem OAI.CubicFirstMoment.angular_kummer_chebyshev_logSaving line 70

theorem OAI.CubicFirstMoment.weighted_angular_kummer_prime_log_bound line 96

Source documentation

Partial summation removes the logarithmic prime weight, permitting smooth weights and norm phases. The derivative cost is retained exactly.

theorem weighted_angular_kummer_prime_log_bound (hEF : AngularKummerPrimeExplicitEstimate)
    (ℓ : ℤ) (hℓ : ℓ ≠ 0) (A D : ℝ) (hA : 0 < A) (hD : 0 < D) :
    ∃ C X₀ : ℝ, 0 < C ∧ 1 < X₀ ∧
      ∀ a b : ℝ, X₀ ≤ a → a ≤ b → ∀ v : Eisenstein, v ≠ 0 → (¬∃ n : Eisenstein, n^3 = v) →
        norm v ≤ (Real.log a) ^ A → ∀ f : ℝ → ℂ,
          (∀ t ∈ Set.Icc a b, DifferentiableAt ℝ (fun t => f t / (Real.log t : ℂ)) t) →
          IntegrableOn (deriv (fun t => f t / (Real.log t : ℂ))) (Set.Icc a b) →
          ‖∑ p ∈ (primeCutoff b).filter (fun p => a < norm p),
            f (norm p) * angularKummerCharacter ℓ v p‖ ≤
          (C * b / (Real.log a) ^ D) *
            (‖f a / (Real.log a : ℂ)‖ + ‖f b / (Real.log b : ℂ)‖ +
              ∫ t in Set.Ioc a b, ‖deriv (fun t => f t / (Real.log t : ℂ)) t‖) := by
…

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