Abstract-real scale arithmetic for the leading-error estimate

Pure real lemmas (no project definitions) used to combine the corrector bounds with the scale package left_to_show_scales: the size of Χ_{m,k}, the products (a ε_m²/κ_m) √κ_m ≤ √K √κ_{m-1} and the ratios ε_m / ε_{m-1}^s ≤ K ε_{m-1}^d.

theorem AVenhance.Infra.Section5.RelativeError.corrector_size_le {a ε κ : ℝ} (ha : 0 ≤ a) (hε : 0 < ε) (hκ : 0 < κ) : (4 * Real.pi ^ 2 * κ / ε ^ 2)⁻¹ * |2 * Real.pi * a * ε| ≤ ε * (a * ε ^ 2 / κ)

The corrector bound (4π²κ/ε²)⁻¹ |2π a ε| = a ε³/(2πκ) is at most ε · (a ε²/κ).

theorem AVenhance.Infra.Section5.RelativeError.corr_mul_sqrt_le {a ε κ K κp : ℝ} (ha : 0 ≤ a) (hκ : 0 < κ) (hK : 0 ≤ K) (hκp : 0 ≤ κp) (h : a ^ 2 * ε ^ 4 / κ ≤ K * κp) : a * ε ^ 2 / κ * √κ ≤ √K * √κp

c √κ ≤ √K √κ' from a² ε⁴/κ ≤ K κ', where c = a ε²/κ.

theorem AVenhance.Infra.Section5.RelativeError.eps_ratio_le {εm e K q s d : ℝ} (he : 0 < e) (he1 : e ≤ 1) (hK : 0 ≤ K) (hm : εm ≤ K * e ^ q) (hd : d + s ≤ q) : εm / e ^ s ≤ K * e ^ d

ε_m / e^s ≤ K e^d from ε_m ≤ K e^q and d + s ≤ q, 0 < e ≤ 1.

theorem AVenhance.Infra.Section5.RelativeError.gradient_term_le {c sm sp nT εm e₁ e K A S : ℝ} (hsp : 0 ≤ sp) (hnT : 0 ≤ nT) (hεm : 0 ≤ εm) (he₁ : 0 < e₁) (hK : 1 ≤ K) (he : 0 ≤ e) (hcs : c * sm ≤ √K * sp) (hT : sp * nT ≤ A * S) (hr : εm / e₁ ≤ K * e) : sm * ((20 * e * c + εm * c * (16 * (2 ^ 16 * e₁⁻¹))) * nT) ≤ √K * (20 + 2 ^ 20 * K) * A * e * S

First-order terms: √κ_m ((20 e c + ε_m c D) ‖∇T‖) ≤ √K (20 + 2^20 K) A e S.

theorem AVenhance.Infra.Section5.RelativeError.hessian_term_le {c sm sp s εm ρ e K A S : ℝ} (hs : 0 ≤ s) (hεm : 0 ≤ εm) (hρ : 0 < ρ) (hK : 1 ≤ K) (hS : 0 ≤ S) (hcs : c * sm ≤ √K * sp) (hT : sp * s ≤ A * (A / ρ) * S) (hr : εm / ρ ≤ K * e) : sm * (4 * εm * c * s) ≤ 4 * √K * K * A ^ 2 * e * S

Second-order terms: √κ_m (4 ε_m c ‖∇∂_pT‖) ≤ 4 √K K A² e S.

theorem AVenhance.Infra.Section5.RelativeError.rpow_four_le_two {e δ : ℝ} (he : 0 < e) (he1 : e ≤ 1) (hδ : 0 ≤ δ) : e ^ (4 * δ) ≤ e ^ (2 * δ)

e^{4δ} ≤ e^{2δ} for 0 < e ≤ 1, 0 ≤ δ.