OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternHalfLogTwoPrimeSelectedNormRate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   Uniform prime-cell comparison for the actual arithmetic absolute mean. The sharp Fourier window factor is retained in the main term. The published progression input controls the cell, collision and deletion errors.

   theorem PublishedProgressionInput.movingPattern_half_log_selected_two_prime_norm_rate
       (P : PublishedProgressionInput) (ψ : 𝓢(ℝ, ℂ)) (n r₀ k : ℕ)
       (A Wwin Bφ Dφ F Cmass : ℝ)
       (hA : 0 ≤ A) (hWwin : 0 ≤ Wwin) (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 ≤ 4 * 2 ^ n) :
       ∀ᶠ L : ℝ in atTop, let m := spectatorBulkCount k L
   …

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