Public statement.

noncomputable def AVenhance.mTheta0 (β : ℝ) (Λ : ℕ) (R : ℝ) : ℕ

m_{θ₀} := min { m ∈ ℕ : m ≥ 2, ε_{m-1}^{1+γ/2} ≤ R_{θ₀} } (e.mtheta0.def 8037-8041; e.m.restriction 7010). The set is nonempty for R > 0 (mTheta0_isLeast).

Equations

• AVenhance.mTheta0 β Λ R = sInf {m : ℕ | 2 ≤ m ∧ AVenhance.epsilon β Λ (m - 1) ^ (1 + AVenhance.gamma β / 2) ≤ R}