MovingPatternWindowPrimeRate.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Ostmann.PublishedProgressionInput.movingPattern_original_prime_rate_window 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_window
    (P : PublishedProgressionInput) (ψ : 𝓢(ℝ, ℂ)) (n r₀ k : ℕ)
    (A H Bφ Dφ F Cmass gain : ℝ)
    (hA : 0 ≤ A) (hH : 0 ≤ H) (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