Statement file: epsilon (Ingredients). This file contains exactly one declaration of the formalization's public statement surface.

noncomputable def AVenhance.epsilon (β : ℝ) (Λ m : ℕ) : ℝ

e.epm.choice (1041-1052): ε_0 := 1, ε_m⁻¹ := ⌈Λ^{q^m/(q-1)}⌉ for m ≥ 1.

Equations

• AVenhance.epsilon β Λ m = if m = 0 then 1 else (↑⌈↑Λ ^ (AVenhance.q β ^ m / (AVenhance.q β - 1))⌉₊)⁻¹