MovingPatternCellError.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Weighted cell error at the original pattern and spectator scales

theorem OAI.Ostmann.PublishedProgressionInput.movingPattern_cell_error_rate line 15

Source documentation

The sharp kernel and every pointwise spectator factor fit one uniform weighted comparison bound at the manuscript's actual linear bulk size.

theorem PublishedProgressionInput.movingPattern_cell_error_rate
    (P : PublishedProgressionInput) (ψ : 𝓢(ℝ, ℂ)) (n r₀ k : ℕ)
    (A lo hi B D F Cnorm : ℝ) (hA : 0 ≤ A) (hhi : lo ≤ hi) (hF : 0 ≤ F) :
    ∃ C : ℝ, 1 ≤ C ∧ Cnorm ≤ C ∧ ∀ᶠ L : ℝ in atTop,
      let m := spectatorBulkCount k L
…

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

theorem OAI.Ostmann.PublishedProgressionInput.movingPattern_cell_error_rate_window line 93

Source documentation

The cell threshold is uniform over the moving Fourier window.

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

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