Amplitude-generic leading-energy estimates on the actual datum and T iterates. The quadratic error has amplitude S squared; the base consumes only integrated gradients.

Abstract real arithmetic

theorem AVenhance.Infra.Section5.RelativeError.RelativeSpaceKill.rpow_half_neg_le {e q γ ε : ℝ} (he : 0 < e) (hγ : 0 ≤ γ) (hε : e ^ q / 2 ≤ ε) : ε ^ (-γ) ≤ 2 ^ γ * e ^ (-(q * γ))

e^{-qγ} dominates 1 for e ≤ 1, and (e^q/2)^{-γ} = 2^γ e^{-qγ}.

theorem AVenhance.Infra.Section5.RelativeError.RelativeSpaceKill.two_mul_add_le {B b : ℝ} (hB : 0 ≤ B) (hBb : B ≤ b) (hb : 1 ≤ b) : 2 * B + 2 * B ^ 2 ≤ 4 * b ^ 2

2 B + 2 B² ≤ 4 b² for 0 ≤ B ≤ b, 1 ≤ b.

theorem AVenhance.Infra.Section5.RelativeError.RelativeSpaceKill.rpow_exponents_combine {e : ℝ} (he : 0 < e) (P qγ : ℝ) : e ^ (-P) * (e ^ (-qγ)) ^ 2 * e ^ (500 + P + 2 * qγ) = e ^ 500

Exponents combine: e^{-P} · (e^{-qγ})² · e^{500+P+2qγ} = e^{500}.

theorem AVenhance.Infra.Section5.RelativeError.space_kill_scalar (A K q γ g P W : ℝ) (hA : 0 < A) (hK : 1 ≤ K) (hq : 0 ≤ q) (hγ : 0 ≤ γ) (hg : 0 < g) (hP : 0 ≤ P) (hW : 0 ≤ W) : ∃ (C' : ℝ), 0 ≤ C' ∧ ∀ (e ε κ B rN θ2 : ℝ), 0 < e → e ≤ 1 → e ^ q / 2 ≤ ε → 0 < κ → κ ≤ K → 0 ≤ B → B ≤ K * ε ^ (-γ) → e ^ (-g) / (A * K) ≤ rN → 0 ≤ θ2 → κ * (4 * 512 * (A * e ^ (-P) * θ2) * (2 * B + 2 * B ^ 2) * W * Real.exp (-rN / 1024)) ≤ C' * e ^ 500 * θ2

The pure-real core of the scaled estimate.

theorem AVenhance.Infra.Section5.RelativeError.RelativeSpaceKill.rN_lower {e ε A K q γ : ℝ} (he : 0 < e) (hε : 0 < ε) (hA : 0 < A) (hεK : ε ≤ K * e ^ q) : e ^ (-(q - 1 - γ / 2)) / (A * K) ≤ e ^ (1 + γ / 2) / A * ε⁻¹

r N ≥ ε_{m-1}^{-(q-1-γ/2)}/(AK) from ε_m ≤ K ε_{m-1}^q.

theorem AVenhance.Infra.Section5.RelativeError.RelativeSpaceKill.one_le_of_small {e Λ A K g : ℝ} (he : 0 < e) (hΛ : 0 < Λ) (hA : 0 < A) (hK : 0 < K) (hg : 0 < g) (heΛ : e ≤ Λ⁻¹) (hΛ' : (A * K) ^ (1 / g) ≤ Λ) : 1 ≤ e ^ (-g) / (A * K)

1 ≤ ε^{-g}/(AK) once ε ≤ Λ⁻¹ and (AK)^{1/g} ≤ Λ.

theorem AVenhance.Infra.Section5.RelativeError.RelativeSpaceKill.l2NormSq_nonneg_sk (f : Homogenization.Vec 2 → ℝ) : 0 ≤ l2NormSq f

theorem AVenhance.Infra.Section5.RelativeError.RelativeSpaceKill.a_nonneg_sk {β : ℝ} (I : Ingredients β) (m : ℕ) : 0 ≤ a β I.Λ m

theorem AVenhance.Infra.Section5.RelativeError.RelativeSpaceKill.norm_intervalIntegral_le_of_Ioo {f : ℝ → ℝ} {c : ℝ} (h : ∀ t ∈ Set.Ioo 0 1, |f t| ≤ c) : |∫ (t : ℝ) in 0..1, f t| ≤ c

Integrating a pointwise bound on (0,1) over [0,1] (the endpoint is null).

theorem AVenhance.Infra.Section5.RelativeError.relative_ergodic_space_kill (β C₀ A P : ℝ) (hA : 0 < A) (hP : 0 ≤ P) : ∃ (C : ℝ), ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → C ≤ ↑I.Λ → ∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ) (hΦ : IsStreamSeq I Φ), ∀ κ ∈ permissibleSet β I.Λ, ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → ∀ (m : ℕ), 2 ≤ m → m ≤ M → ∀ (S : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (θprev : ℝ → Homogenization.Vec 2 → ℝ) (T : ℕ → ℝ → Homogenization.Vec 2 → ℝ), I.IsTIterates hΦ m (I.kappaSeq κ M m) (I.kappaSeq κ M (m - 1)) θ₀ θprev T → (∀ t ∈ Set.Ioo 0 1, ∀ (k : ℤ), Odd k → I.xiMK m k t ≠ 0 → ∀ (i j : Fin 2), Ergodic.HasCoordinateAnalyticL1Bounds (fun (y : Homogenization.Vec 2) => ↑(spaceGrad (T (Nstar β) t) (I.xFlow hΦ m (lIdx β I.Λ m k) t y) i * spaceGrad (T (Nstar β) t) (I.xFlow hΦ m (lIdx β I.Λ m k) t y) j)) (A * epsilon β I.Λ (m - 1) ^ (-P) * S ^ 2) (epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) / A)) → I.kappaSeq κ M m * |∫ (t : ℝ) in 0..1, (∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (LeftToShow.leadingGrad I hΦ m (I.kappaSeq κ M m) (T (Nstar β)) t x)) - LeftToShow.gradQuad (T (Nstar β)) (LeftToShow.leadingGramAvg I hΦ m (I.kappaSeq κ M m) t) t| ≤ C * epsilon β I.Λ (m - 1) ^ 500 * S ^ 2

e.ergodic.space.kill (8510–8633).