OAI/NumberTheory/Ostmann/Construction/OriginalHarmonicRate.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.deleted_prime_mass_relative_rate line 12
2. theorem OAI.Ostmann.PublishedProgressionInput.short_prime_cell_mass_two line 35
3. theorem OAI.Ostmann.PublishedProgressionInput.original_harmonic_box_rate line 51

   Source documentation

   The three original-prior mass premises used by the signed bulk bound hold simultaneously. No renormalization after idealization is introduced.

   theorem PublishedProgressionInput.original_harmonic_box_rate (P : PublishedProgressionInput)
       (C : ℝ) (hC : 1 ≤ C) :
       ∀ᶠ L : ℝ in atTop, ∀ (Cell : Type) [Fintype Cell] (Q : ℕ), 2 ≤ Q →
         Real.log (4 * (Q : ℝ)) ≤ 2 * Real.exp ((12 / 10000 : ℝ) * L) →
         (Fintype.card Cell : ℝ) ≤ Real.exp (Real.exp ((14 / 10000 : ℝ) * L)) →
         ∀ (u v : Cell → ℝ) (D : Finset ℕ),
         (∀ c, 1 ≤ u c) → (∀ c, Real.exp ((39 / 10000 : ℝ) * L) ≤ u c) →
         (∀ c, u c ≤ v c) → (∀ c, v c ≤ u c + 1) →
         (∀ c d, c ≠ d → v c ≤ u d ∨ v d ≤ u c) →
         (D.card : ℝ) ≤ Real.exp (C * L) →
         let S := primeCellSupport 1 (fun _ : Cell => 0) u v
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.primeCellSupport