LongPrimeSW.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Prime cancellation on the long-prime range used to prove the stopped sequence condition. The scale T can be log X while the prime scale is only exp(sqrt(log X)); no positive power of X is required.

theorem OAI.CubicFirstMoment.long_prime_interval_bound line 16

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 long_prime_interval_bound (hSW : KummerPrimeSiegelWalfisz)
    {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)*cubicSymbol p v‖ ≤
        (C*(R*P)/T^D)*(‖f a‖+‖f b‖+∫ t in Set.Ioc a b, ‖deriv f t‖) := by
…

Mentions: OAI.CubicFirstMoment.KummerPrimeSiegelWalfisz, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primeCutoff, OAI.CubicFirstMoment.cubicSymbol