OAI/NumberTheory/Ostmann/ZeroDensity/BulkProgressionRate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   The Section 8 bulk row absorbs variable polynomial-cut counts, residue counts, and the complete smooth budget. No fixed bound on the number of roots is needed: those costs are all included in V.

   theorem PublishedProgressionInput.bulk_full_progression_budget_rate (P : PublishedProgressionInput)
       (C : ℝ) (d : ℕ) :
       ∀ᶠ L : ℝ in atTop, ∀ Q : ℕ, 2 ≤ Q →
         Real.log (4 * (Q : ℝ)) ≤ 2 * Real.exp ((12 / 10000 : ℝ) * L) →
         ∀ u V : ℝ, Real.exp ((39 / 10000 : ℝ) * L) ≤ u →
         V ≤ Real.exp (C * L ^ d + C * L * Real.exp ((14 / 10000 : ℝ) * L)) →
         V * (18 * P.errorConstant * Real.exp (-P.decay * Real.sqrt u) +
           Real.exp (-P.kappa * u / Real.log (4 * (Q : ℝ))) + 2 * Real.exp (-u)) ≤
             Real.exp (-Real.exp ((125 / 100000 : ℝ) * L)) := by
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput