OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternHalfLogCellError.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.PublishedProgressionInput.movingPattern_half_log_cell_error_rate_window line 14

   Source documentation

   The cell threshold is uniform over the moving Fourier window.

   theorem PublishedProgressionInput.movingPattern_half_log_cell_error_rate_window
       (P : PublishedProgressionInput) (ψ : 𝓢(ℝ, ℂ)) (n r₀ k : ℕ)
       (A H B D F Cnorm Dlog : ℝ) (hA : 0 ≤ A) (hH : 0 ≤ H) (hF : 0 ≤ F)
       (hDlog : 0 ≤ Dlog) (tlog : ℕ) (htlog : tlog ≤ 4 * 2 ^ n) :
       ∃ C : ℝ, 1 ≤ C ∧ Cnorm ≤ C ∧ ∀ᶠ L : ℝ in atTop,
         let m := spectatorBulkCount k L
   …

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