MovingPatternPrimeRate.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Ostmann.PublishedProgressionInput.movingPattern_original_prime_rate line 20
Source documentation
The three arithmetic costs are combined for the literal original prime mean. The only analytic input is the published progression theorem; local cancellation is proved from the balanced spectator sets and their mixed Fourier bounds. All prime normalizers are those before idealization.
```
theorem PublishedProgressionInput.movingPattern_original_prime_rate
    (P : PublishedProgressionInput) (ψ : 𝓢(ℝ, ℂ)) (n r₀ k : ℕ)
    (A lo hi Bφ Dφ F Cmass gain : ℝ)
    (hA : 0 ≤ A) (hlo : 1 ≤ lo) (hhi : lo ≤ hi) (hF : 0 ≤ F) (hCmass : 1 ≤ Cmass)
    (hBφ : 0 ≤ Bφ) (hDφ : 0 ≤ Dφ) :
    ∃ ε : ℝ, 0 < ε ∧ ε ≤ 1 ∧ ∃ cutoff : ℕ, 3 ≤ cutoff ∧
    ∀ᶠ L : ℝ in atTop, let m := spectatorBulkCount k L
…
```
Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.spectatorBulkCount