OAI/NumberTheory/Ostmann/Arithmetic/SmoothPrimeComparison.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.ClippedPolynomialFactor.continuous_value line 12
2. theorem OAI.Ostmann.continuous_smoothPolynomialWeight line 25
3. theorem OAI.Ostmann.PublishedProgressionInput.smooth_prime_comparison line 31

   Source documentation

   On one genuine polynomial root cell, the full smooth weight admits prime-to-Page comparison with its explicit product variation budget.

   theorem PublishedProgressionInput.smooth_prime_comparison (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)
       {n : ℕ} (F : Fin n → ClippedPolynomialFactor)
       (S : Finset ℝ) (hroots : ∀ i r, r ∈ (F i).polynomial.derivative.roots → r ∈ S)
       (hcode : rootCellCode S (Real.exp u) = rootCellCode S (Real.exp v)) :
       ‖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 : ℂ)‖ ≤
         smoothPolynomialBudget F *
           (18 * P.errorConstant * Real.exp (-P.decay * Real.sqrt u) +
             Real.exp (-P.kappa * u / Real.log (4 * (Q : ℝ)))) := by
   …

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