CharacterPrimeFrequency.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Natural character-frequency cutoffs lie below the actual prime ranges

theorem OAI.Ostmann.transferErrorScale_linear_bound line 12
Source documentation
A fixed depth has a linear exponent, including the rounded bottom cutoff with its original factor two in front of sqrt(m).
```
theorem transferErrorScale_linear_bound (k j : ℕ) (d m : ℝ)
    (hj : j ≤ k) (hd : 0 ≤ d) (hm : 1 ≤ m) :
    transferErrorScale (d * m) m j ≤ ((2 : ℝ) ^ k * d + 2 * (4 : ℝ) ^ k) * m := by
…
```
Mentions: OAI.Ostmann.transferErrorScale

theorem OAI.Ostmann.eventual_natural_cutoff_power_lt line 25

Source documentation

This supplies both the prime-frequency separation and the finite powers of the cutoff used for denominator removal in the selected energy estimate.

theorem eventual_natural_cutoff_power_lt (k r : ℕ) (d z α c : ℝ)
    (hd : 0 ≤ d) (_hz : 0 ≤ z) (hα : 0 < α) (hc : 0 < c) :
    ∀ᶠ L : ℝ in atTop, ∀ m : ℝ, 1 ≤ m → m ≤ z * L → ∀ j ≤ k,
      (((naturalTransferCutoff (d * m) m j) ^ r : ℕ) : ℝ) <
        Real.exp (c * Real.exp (α * L)) := by
…

Mentions: OAI.Ostmann.naturalTransferCutoff

theorem OAI.Ostmann.eventual_natural_cutoff_below_primes line 54