Scale arithmetic for e.tildethetam.to.Tm.A

Abstract-real lemmas: the corrector sup-norm a ε_m³ / (2π κ_m) times ε_{m-1}^{-(1+γ/2)} is at most K² ε_{m-1}^δ once a ε_m²/κ_m ≤ K ε_m^{-γ} and ε_m ≤ K ε_{m-1}^q (the exponent identity q(1-γ) - 1 - γ/2 = 4δ, e.tildethetam.to.Tm.A).

theorem AVenhance.Infra.Section5.Integration.gamma_lt_one_of_range {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : gamma β < 1

γ < 1 on the range.

theorem AVenhance.Infra.Section5.Integration.chi_const_eq {a e κ : ℝ} (ha : 0 < a) (he : 0 < e) (hκ : 0 < κ) : (4 * Real.pi ^ 2 * κ / e ^ 2)⁻¹ * |2 * Real.pi * a * e| = a * e ^ 2 / κ * e / (2 * Real.pi)

The explicit corrector sup-norm constant, rewritten in terms of a ε² / κ.

theorem AVenhance.Infra.Section5.Integration.ansatz_scale_bound {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) {K e em A : ℝ} (hK : 1 ≤ K) (he : 0 < e) (he1 : e ≤ 1) (hem : 0 < em) (hA0 : 0 ≤ A) (hA : A ≤ K * em ^ (-gamma β)) (hemK : em ≤ K * e ^ q β) : A * em / (2 * Real.pi) * e ^ (-(1 + gamma β / 2)) ≤ K ^ 2 * e ^ delta β

The scale bound: c ≤ (a e_m²/κ) e_m / 2π, a e_m²/κ ≤ K e_m^{-γ}, e_m ≤ K e^q give c e^{-(1+γ/2)} ≤ K² e^δ.