OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternLogWindowPrimeRate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.PublishedProgressionInput.movingPattern_log_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_log_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φ)
       (Dlog : ℝ) (hDlog : 0 ≤ Dlog)
       (hloglip : ∀ x y, |logCellProfile x - logCellProfile y| ≤ Dlog * |x - y|)
       (tlog : ℕ) (htlog : tlog ≤ 2 * 2 ^ (n + 2)) :
       ∃ ε : ℝ, 0 < ε ∧ ε ≤ 1 ∧ ∃ cutoff : ℕ, 3 ≤ cutoff ∧
       ∀ᶠ L : ℝ in atTop, let m := spectatorBulkCount k L
   …

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