Scale facts for the analytic case of r.LeBron.2

• the lower bound ε_{m₀-1} ≥ c · min(1,R)^{q/(1+γ/2)} for m₀ = mTheta0 R (minimality);
• the elementary exponent identities 2β/(q+1) = β - γ, γ < β;
• two-sided bound of an element of a permitted interval;
• E^{-e} ≤ c^{-e} (1 + R^{-re}) from c min(1,R)^r ≤ E.

theorem AVenhance.Infra.FullTheorem.gamma_lt_beta {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : gamma β < β

theorem AVenhance.Infra.FullTheorem.two_beta_div_eq {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : 2 * β / (q β + 1) = β - gamma β

theorem AVenhance.Infra.FullTheorem.epsilon_mTheta0_lower {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) {R : ℝ} (hR : 0 < R) : min (epsilon β Λ 1) (1 / 2) * min 1 R ^ (q β / (1 + gamma β / 2)) ≤ epsilon β Λ (mTheta0 β Λ R - 1)

Lower bound for the scale ε_{m₀ - 1}.

theorem AVenhance.Infra.FullTheorem.inv_rpow_le {c R r e E : ℝ} (hc : 0 < c) (hR : 0 < R) (he : 0 ≤ e) (hE : c * min 1 R ^ r ≤ E) : E ^ (-e) ≤ c ^ (-e) * (1 + R ^ (-(r * e)))

E^{-e} ≤ c^{-e} (1 + R^{-(r e)}) from c min(1,R)^r ≤ E.

theorem AVenhance.Infra.FullTheorem.permitted_bounds {β : ℝ} {Λ : ℕ} (hβ : 1 < β) (hβ' : β < 4 / 3) (hΛ : 2 ^ 7 ≤ Λ) (hΛs : 2 ^ (1 / (β - gamma β)) ≤ ↑Λ) {κ : ℝ} {M : ℕ} (hM : 1 ≤ M) (hκM : κ ∈ permittedInterval β Λ M) : 1 / 2 * epsilon β Λ M ^ (β - gamma β) ≤ κ ∧ κ ≤ 1

Every element of a permitted interval (M ≥ 1, Λ large) lies in [½ ε_M^{β-γ}, 1].