OAI/NumberTheory/Ostmann/Arithmetic/SmoothPrimeAllRoots.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.PublishedProgressionInput.smooth_prime_all_roots line 13

   Source documentation

   The root partition is internal to the proof. Both sides retain the entire original interval, including its endpoint primes.

   theorem PublishedProgressionInput.smooth_prime_all_roots (P : PublishedProgressionInput)
       {Q q a : ℕ} (hQ : 2 ≤ Q) (hq : 1 ≤ q) (hqQ : q ≤ Q) (ha : a.Coprime q)
       (u v : ℝ) (hu : 1 ≤ u) (huv : u ≤ v) (hshort : v ≤ u + 1)
       {k : ℕ} (F : Fin k → ClippedPolynomialFactor) (S : Finset ℝ)
       (hroots : ∀ i r, r ∈ (F i).polynomial.derivative.roots → r ∈ S) :
       ‖complexPrimeInterval q a u v (fun y => smoothPolynomialWeight F (Real.exp y)) -
         ∫ y in Set.Ioc u v, smoothPolynomialWeight F (Real.exp y) *
           (selectedPrimeLogDensity P Q q a y : ℂ)‖ ≤
         (S.card + 1 : ℕ) * smoothPolynomialBudget F *
           (18 * P.errorConstant * Real.exp (-P.decay * Real.sqrt u) +
             Real.exp (-P.kappa * u / Real.log (4 * (Q : ℝ))) + 2 * Real.exp (-u)) := by
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.ClippedPolynomialFactor, OAI.Ostmann.complexPrimeInterval, OAI.Ostmann.smoothPolynomialWeight, OAI.Ostmann.selectedPrimeLogDensity, OAI.Ostmann.smoothPolynomialBudget