MovingCutoffReserve.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual Section 7 gaps supply both integer-transfer reserves

theorem OAI.Ostmann.moving_sqrt_reserve line 9
theorem OAI.Ostmann.movingStepGap_succ line 15

theorem OAI.Ostmann.movingCutoff_diagonal_reserve line 27

Source documentation

The next pivot gap exceeds the current Fourier exponent by a positive linear amount, uniformly over all tree levels.

theorem movingCutoff_diagonal_reserve (Bs BD Bz z m : ℝ)
    (hBD : Bs + 1 ≤ BD) (hBz : 8 ≤ Bz)
    (hz : 1 ≤ z) (hm : 64 ≤ m) (n : ℕ) :
    (3 / 20 : ℝ) * (2 : ℝ) ^ n * m ≤
      spectatorStepGap BD Bz z ((2 : ℝ) ^ n) m - movingCutoffExponent Bs BD Bz z m n := by
…

Mentions: OAI.Ostmann.spectatorStepGap, OAI.Ostmann.movingCutoffExponent

theorem OAI.Ostmann.movingCutoff_frequency_reserve line 57
Source documentation
The frequency range at the next level has a square-root reserve after paying both the previous frequency and the current pivot gap.
```
theorem movingCutoff_frequency_reserve (Bs BD Bz z m : ℝ) (n : ℕ) :
    movingCutoffExponent Bs BD Bz z m (n + 1) -
      (movingCutoffExponent Bs BD Bz z m n +
        spectatorStepGap BD Bz z ((2 : ℝ) ^ n) m) =
      (2 : ℝ) ^ n * Real.sqrt (4 * m) := by
…
```
Mentions: OAI.Ostmann.movingCutoffExponent, OAI.Ostmann.spectatorStepGap