AngularLongPrimeSW.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed-angular weighted and long-interval prime bounds derived from AngularKummerPrimeExplicitEstimate. The surviving angular character is literal, and the interval may begin at exp(sqrt(log X)).

theorem OAI.CubicFirstMoment.weighted_angular_kummer_prime_bound line 13

theorem OAI.CubicFirstMoment.angular_long_prime_interval_bound line 43

Source documentation

The precise raw Kummer prime input, followed by partial summation, gives arbitrary T-power saving on every interval above a prime scale P as soon as T <= (log P)^2. Smooth weights retain their actual variation.

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

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