Abstract-real scale arithmetic for the twistie1 source contract

Pure real lemmas (no objects) for e.monster.est.5 (enhance.tex 7371–7460):

• se_main_scale: the main term ε_m^{2-γ} √κ_{m-1} ε_{m-1}^{-(2+γ)} is ≲ ε_{m-1}^δ √κ_m, from the diffusivity upper bound κ_{m-1} ≲ ε_{m-1}^{β+γ}, the lower bound ε_m^{β+γ} ≲ κ_m and the supergeometric comparison ε_m ≃ ε_{m-1}^q; the exponent is 8δ (se_exponent_ge).

theorem AVenhance.Infra.Section5.Contracts.se_exponent_ge {β : ℝ} (hβ : 1 < β) (hβ' : β < 4 / 3) : delta β ≤ (1 - q β) * (β + gamma β) / 2 + q β * (2 - gamma β) - (2 + gamma β)

The exponent of the main term is 8 δ ≥ δ.

theorem AVenhance.Infra.Section5.Contracts.se_main_scale {x εm κm κp K Ca β γ q δ : ℝ} (hx0 : 0 < x) (hx1 : x ≤ 1) (hεm : 0 < εm) (hκm : 0 < κm) (hK : 1 ≤ K) (hCa : 0 ≤ Ca) (hγ2 : γ ≤ 2) (hβγ : 0 ≤ β + γ) (hlow : x ^ q ≤ 2 * εm) (hup : εm ≤ K * x ^ q) (hκpA : κp ≤ Ca * x ^ (β + γ)) (hκmL : εm ^ (β + γ) ≤ K * κm) (hexp : δ ≤ (1 - q) * (β + γ) / 2 + q * (2 - γ) - (2 + γ)) : εm ^ (2 - γ) * √κp * x ^ (-(2 + γ)) ≤ K ^ (2 - γ) * (√Ca * √K * 2 ^ ((β + γ) / 2)) * x ^ δ * √κm

√κ_{m-1} ≤ C x^s ε_m^{-s} √κ_m, then the main scale estimate.

theorem AVenhance.Infra.Section5.Contracts.se_partA {x εm κm κp K Ca A' CB1 Aj Bm CE u c7 U β γ q δ : ℝ} (hx0 : 0 < x) (hx1 : x ≤ 1) (hεm : 0 < εm) (hκm : 0 < κm) (hK : 1 ≤ K) (hCa : 0 ≤ Ca) (hγ2 : γ ≤ 2) (hβγ : 0 ≤ β + γ) (hlow : x ^ q ≤ 2 * εm) (hup : εm ≤ K * x ^ q) (hκpA : κp ≤ Ca * x ^ (β + γ)) (hκmL : εm ^ (β + γ) ≤ K * κm) (hexp : δ ≤ (1 - q) * (β + γ) / 2 + q * (2 - γ) - (2 + γ)) (hCB1 : 0 ≤ CB1) (hAj : 0 ≤ Aj) (hBm : 0 ≤ Bm) (hCE : 0 ≤ CE) (hc7 : 0 ≤ c7) (hu : u ≤ K * εm ^ (-γ)) (hU : √U ≤ c7 * (CB1 * Aj * Bm * (A' ^ 2 * x ^ (-(2 + γ)))) * √κp) : 4 * CE * εm * (εm * u) * √U ≤ 4 * CE * K * c7 * CB1 * Aj * A' ^ 2 * (K ^ (2 - γ) * (√Ca * √K * 2 ^ ((β + γ) / 2))) * x ^ δ * √κm * Bm

Part A of the final chain: the main (ergodic 1/N) term.

theorem AVenhance.Infra.Section5.Contracts.se_partB {x εm κm κp K A' CB1 Aj Bm CE u M₁ c8 Ev β γ q δ : ℝ} (hx0 : 0 < x) (hεm : 0 < εm) (hεm1 : εm ≤ 1) (hK : 1 ≤ K) (hγ1 : γ ≤ 1) (hκpK : κp ≤ K) (hCB1 : 0 ≤ CB1) (hAj : 0 ≤ Aj) (hBm : 0 ≤ Bm) (hCE : 0 ≤ CE) (hA' : 0 ≤ A') (hu0 : 0 ≤ u) (hu : u ≤ K * εm ^ (-γ)) (hM₁ : 0 ≤ M₁) (hEv : 0 ≤ Ev) (hdec : Ev * (x ^ (3 + 3 * γ / 2 + q * β))⁻¹ ≤ M₁ * x ^ δ) (hc8 : x ^ (q * β) ≤ c8 * √κm) : CE * (2048 * 40 * (κp * CB1) * (Aj * Bm) * (A' / x ^ (1 + γ / 2)) ^ 3) * (εm * u) * Ev ≤ CE * 2048 * 40 * K * CB1 * Aj * A' ^ 3 * K * M₁ * c8 * x ^ δ * √κm * Bm

Part B of the final chain: the exponentially small term.

theorem AVenhance.Infra.Section5.Contracts.se_kappa_lower {x εm κm κp K q β : ℝ} (hx0 : 0 < x) (hεm : 0 < εm) (hκm : 0 < κm) (hK : 1 ≤ K) (hβ : 0 < β) (hlow : x ^ q ≤ 2 * εm) (hκpK : κp ≤ K) (h2 : εm ^ (2 * β) ≤ K * κp * κm) : x ^ (q * β) ≤ 2 ^ β * K * √κm

x^{qβ} ≲ √κ_m, from ε_m^{2β} ≤ K κ_{m-1} κ_m, κ_{m-1} ≤ K and x^q ≤ 2 ε_m.

theorem AVenhance.Infra.Section5.Contracts.se_radius_freq {x εm K A' q γ : ℝ} (hx0 : 0 < x) (hεm : 0 < εm) (hK : 1 ≤ K) (hA' : 1 ≤ A') (hup : εm ≤ K * x ^ q) : 1 / (2 ^ 15 * A' * K) * x ^ (-(q - 1 - γ / 2)) ≤ (16 * (A' / x ^ (1 + γ / 2)))⁻¹ / 2 ^ 11 * εm⁻¹

r N ≥ x^{-p} / (2^{15} A' K) for the composed radius r = (16 L)⁻¹ / 2^{11}, L = A'/x^{1+γ/2}, N = ε_m⁻¹, ε_m ≤ K x^q, p = q - 1 - γ/2.

theorem AVenhance.Infra.Section5.Contracts.se_rpow_neg_ge {x Λ p c : ℝ} (hx0 : 0 < x) (hxΛ : x ≤ Λ⁻¹) (hΛ : 0 < Λ) (hp : 0 < p) (hc : 0 ≤ c) (hΛc : c ^ (1 / p) ≤ Λ) : c ≤ x ^ (-p)

c ≤ x^{-p} for x ≤ Λ⁻¹ and c^{1/p} ≤ Λ.

theorem AVenhance.Infra.Section5.Contracts.se_rate_le {x γ δ A' : ℝ} (hx0 : 0 < x) (hx1 : x ≤ 1) (hA' : 2 ^ 10 ≤ A') (hδγ : 2 * δ ≤ γ / 2) (hδ : 0 ≤ δ) : 2 ^ 10 / x ≤ A' / x ^ (1 + γ / 2) ∧ 2 ^ 10 / x / x ^ (2 * δ) ≤ A' / x ^ (1 + γ / 2)

The coefficient radius and the flow radius are dominated by the common rate L = A'/x^{1+γ/2}.

theorem AVenhance.Infra.Section5.Contracts.se_L_sq {x γ A' : ℝ} (hx0 : 0 < x) : (A' / x ^ (1 + γ / 2)) ^ 2 = A' ^ 2 * x ^ (-(2 + γ))