MovingProductInitialCutoff.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Ostmann.movingProductNaturalCutoff_zero_translate line 11
Source documentation
The initial cutoff depends on the quotient of the two product scales.
```
theorem movingProductNaturalCutoff_zero_translate (T : ℕ → ℝ) (W Y m D : ℝ) :
    movingProductNaturalCutoff T (W - D) (Y - D) m 0 =
      movingProductNaturalCutoff T W Y m 0 := by
…
```
Mentions: OAI.Ostmann.movingProductNaturalCutoff
theorem OAI.Ostmann.movingProductFrequency_mono_mass line 19
theorem OAI.Ostmann.movingProductNaturalCutoff_zero_window line 30
Source documentation
Using one quarter of the bulk mass in the frequency reserve leaves room for the fixed width of the actual initial product window. The diagonal energy estimate retains its original sqrt (4m) cutoff.
```
theorem movingProductNaturalCutoff_zero_window (T : ℕ → ℝ)
    (W Y Δ m H : ℝ) (hW : W - Y ≤ Δ + H)
    (hwidth : H ≤ Real.sqrt m) :
    (movingProductNaturalCutoff T W Y (m / 4) 0 : ℝ) ≤
      Real.exp (Δ + Real.sqrt (4 * m)) := by
…
```
Mentions: OAI.Ostmann.movingProductNaturalCutoff
theorem OAI.Ostmann.eventually_initial_product_reserve line 46
theorem OAI.Ostmann.movingProductNaturalCutoff_card_bound line 52