AngularLongPrimeCutoff.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A concrete free selected-bin prime satisfies the needed prime cancellation, uniformly in its cutoff scale and interval endpoints.

theorem OAI.CubicFirstMoment.angular_long_prime_cutoff_bound line 16

theorem OAI.CubicFirstMoment.angular_long_prime_cutoff_excluded_bound line 44

Source documentation

The exact logarithmic deletion error is retained, so this theorem also applies to the polynomial-norm exclusions in the stopped sequence.

theorem angular_long_prime_cutoff_excluded_bound (hEF : AngularKummerPrimeExplicitEstimate)
    (ℓ : ℤ) (hℓ : ℓ ≠ 0)
    {A D : ℝ} (hA : 0 < A) (hD : 0 < D) :
    ∃ C P₀ : ℝ, 0 < C ∧ 1 < P₀ ∧ ∀ (T P a b c u : ℝ),
      1 ≤ T → P₀ ≤ P → T ≤ (Real.log P)^2 →
      P ≤ a → a ≤ b → b ≤ 2*P → 0 < c →
      ∀ v e : Eisenstein, v ≠ 0 → (¬∃ j : Eisenstein, j^3 = v) → norm v ≤ T^A → e ≠ 0 →
      ‖∑ p ∈ ((primeCutoff b).filter (fun p => a < norm p)).filter (fun p => IsCoprime p e),
        (primeDetectorCutoff (norm p/c):ℂ)*mellinPhase u (norm p)*angularCubicSymbol ℓ p v‖ ≤
        C*P/T^D*(1+|u|)+Real.log (norm e)/Real.log 2 := by
…

Mentions: OAI.CubicFirstMoment.AngularKummerPrimeExplicitEstimate, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primeCutoff, OAI.CubicFirstMoment.primeDetectorCutoff, OAI.CubicFirstMoment.mellinPhase, OAI.CubicFirstMoment.angularCubicSymbol