Public statement.

theorem AVenhance.mTheta0_isLeast {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) {Λ : ℕ} (hΛ : 2 ^ 7 ≤ Λ) {R : ℝ} (hR : 0 < R) : IsLeast {m : ℕ | 2 ≤ m ∧ epsilon β Λ (m - 1) ^ (1 + gamma β / 2) ≤ R} (mTheta0 β Λ R)

The set defining m_{θ₀} is nonempty (ε_m → 0), so mTheta0 is its least element, not the junk value 0 of sInf ∅.