MovingPatternGiantVariation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform giant variation cost at the selected-prime scales

theorem OAI.Ostmann.movingFourierVariationBudget_mono_frequency line 11

theorem OAI.Ostmann.movingWindow_width_le_exp line 21

Source documentation

The manuscript's bottom window has logarithmic height Δ + O(1).

theorem movingWindow_width_le_exp (Δ C A m hi : ℝ) (hm : 1 ≤ m)
    (hΔ : Δ ≤ A * m) (hhi : hi ≤ Real.exp (Δ + C)) :
    hi - Real.exp Δ ≤ Real.exp ((A + |C|) * m) := by
…

theorem OAI.Ostmann.movingPattern_pointwise_cost_budget line 32
Source documentation
The complete pointwise cost needed for both giant integrations is bounded before choosing the Fourier window, its frequencies, or the spectator primes.
```
theorem movingPattern_pointwise_cost_budget (ψ : 𝓢(ℝ, ℂ)) (n r₀ k : ℕ)
    (A Wwin B D : ℝ) (hA : 0 ≤ A) (hWwin : 0 ≤ Wwin) :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ L : ℝ, 1 ≤ L →
      let m := spectatorBulkCount k L
…
```
Mentions: OAI.Ostmann.spectatorBulkCount

theorem OAI.Ostmann.movingPattern_giant_variation_budget line 105

Source documentation

The giant comparison uses a weaker upper scale than the spectator cost.

theorem movingPattern_giant_variation_budget (ψ : 𝓢(ℝ, ℂ)) (n r₀ k : ℕ)
    (A Wwin B D : ℝ) (hA : 0 ≤ A) (hWwin : 0 ≤ Wwin) :
    ∃ C : ℝ, 1 ≤ C ∧ ∀ L : ℝ, 1 ≤ L →
      let m := spectatorBulkCount k L
…

Mentions: OAI.Ostmann.spectatorBulkCount