Corrected parameter bookkeeping for the four §5.2 nondivergence terms. The physical unit-cell frequency is ε_m⁻¹, not ε_(m-1)/ε_m. Composed analyticity, its order-zero estimate, and both means remain explicit inputs.

noncomputable def AVenhance.Infra.Section5.ergodicFrequency (β : ℝ) (Λ m : ℕ) : ℕ

The actual integer fast frequency on the unit cell.

Equations

• AVenhance.Infra.Section5.ergodicFrequency β Λ m = if m = 0 then 1 else ⌈↑Λ ^ (AVenhance.q β ^ m / (AVenhance.q β - 1))⌉₊

theorem AVenhance.Infra.Section5.ergodicFrequency_cast (β : ℝ) (Λ m : ℕ) : ↑(ergodicFrequency β Λ m) = (epsilon β Λ m)⁻¹

theorem AVenhance.Infra.Section5.ergodicFrequency_pos {β : ℝ} {Λ m : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) : 0 < ergodicFrequency β Λ m