OAI/NumberTheory/Ostmann/Arithmetic/SmoothGatedPrimeRoots.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   A sharp gate can change at every included polynomial root. Its exact values at the roots are retained in the prime sum; endpoint atoms are part of the error.

   theorem PublishedProgressionInput.gated_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)
       (w : ℝ → ℂ) (C : ℝ) (hC : 0 ≤ C) (hw : ∀ x, ‖w x‖ ≤ C)
       (hconst : ∀ x y, rootCellCode S x = rootCellCode S y → w x = w y) :
       ‖complexPrimeInterval q a u v (fun y => w (Real.exp y) * smoothPolynomialWeight F (Real.exp y)) -
         ∫ y in Set.Ioc u v, w (Real.exp y) * smoothPolynomialWeight F (Real.exp y) *
           (selectedPrimeLogDensity P Q q a y : ℂ)‖ ≤
         (S.card + 1 : ℕ) * (C * smoothPolynomialBudget F) *
           (18 * P.errorConstant * Real.exp (-P.decay * Real.sqrt u) +
   …

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