OAI/NumberTheory/Ostmann/Arithmetic/MovingSelectedPrimeEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.PublishedProgressionInput.moving_selected_prime_energy line 15

   Source documentation

   The Section 7 energy estimate with its original prime-pattern premise fully supplied by the published progression estimate and the concrete cells.

   theorem PublishedProgressionInput.moving_selected_prime_energy
       (P : PublishedProgressionInput) (C : ℝ) (hM : MertensEstimate C)
       (ψ : 𝓢(ℝ, ℂ)) (n r₀ k : ℕ) (hk : 0 < k) (hn : n ≤ k)
       (A Wwin Bφ Dφ c K ε : ℝ)
       (hA : 0 ≤ A) (hWwin : 0 ≤ Wwin) (hBφ : 0 ≤ Bφ) (hDφ : 0 ≤ Dφ)
       (hc : 0 < c) (hK : 0 ≤ K) (hε : 0 < ε)
       (hdepth : 8 * (K + 1 + 1) ≤ (k : ℝ) ^ 3) :
       ∀ᶠ L : ℝ in atTop, let m := spectatorBulkCount k L
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.MertensEstimate, OAI.Ostmann.spectatorBulkCount