RoundedEnergyCutoffs.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Ostmann.card_transferFrequencyRange line 12
Source documentation
The signed root-frequency set includes zero and both endpoints.
```
theorem card_transferFrequencyRange (V : ℕ) : (transferFrequencyRange V).card = 2 * V + 1 := by
…
```
Mentions: OAI.Ostmann.transferFrequencyRange
theorem OAI.Ostmann.eventual_rounded_frequency_card line 18
Source documentation
At fixed depth the whole rounded frequency family has an exponential bound linear in the word length, with its square-root reserve absorbed.
```
theorem eventual_rounded_frequency_card (n : ℕ) (d : ℝ) (hd : 0 ≤ d) :
    ∀ᶠ m : ℝ in atTop, ∀ j ≤ n,
      ((transferFrequencyRange (naturalTransferCutoff (d * m) m j)).card : ℝ) ≤
        Real.exp (((2 : ℝ) ^ n * d + 1) * m) := by
…
```
Mentions: OAI.Ostmann.transferFrequencyRange, OAI.Ostmann.naturalTransferCutoff
theorem OAI.Ostmann.rounded_bottom_frequency_bound line 47
Source documentation
The rate theorem's square-root parameter is four times the actual word length, so it covers the literal 2 sqrt(m) bottom-frequency reserve.
```
theorem rounded_bottom_frequency_bound (Δ m : ℝ) :
    (naturalTransferCutoff Δ m 0 : ℝ) ≤ Real.exp (Δ + Real.sqrt (4 * m)) := by
…
```
Mentions: OAI.Ostmann.naturalTransferCutoff