CharacterEnergyPrimeRange.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Dyadic data for the actual prime-cell energy theorem

theorem OAI.Ostmann.naturalTransferCutoff_pos line 10
theorem OAI.Ostmann.eventual_twice_natural_cutoff_power_le line 17

theorem OAI.Ostmann.eventual_character_energy_prime_range line 40

Source documentation

Both dyadic endpoints are explicit ceilings/floors of the physical prime range. The finite denominator power is below the first dyadic point.

theorem eventual_character_energy_prime_range (k r : ℕ) (d z α β : ℝ)
    (hd : 0 ≤ d) (hz : 0 ≤ z) (hα : 0 < α) (hβ : 0 ≤ β) :
    ∀ᶠ L : ℝ in atTop, ∀ m : ℝ, 1 ≤ m → m ≤ z * L →
      ∀ S : Finset ℕ,
      (∀ p ∈ S, Real.exp (Real.exp (α * L)) ≤ p ∧
        (p : ℝ) ≤ Real.exp (Real.exp (β * L))) →
      ∃ h J : ℕ,
        (∀ j ≤ k, naturalTransferCutoff (d * m) m j ^ r ≤ 2 ^ h) ∧
        (∀ p ∈ S, 2 ^ h ≤ p ∧ p < 2 ^ (h + J)) ∧
        (J : ℝ) ≤ Real.exp ((β + Real.log ((Real.log 2)⁻¹ + 1)) * L) := by
…

Mentions: OAI.Ostmann.naturalTransferCutoff