e.ergodic.space.kill, integrated in time and scaled

Source: enhance.tex 8510-8633. The fixed-time estimate ergodic_space_kill_slice is integrated over t ∈ (0,1); with the scales ε_m ≈ ε_{m-1}^q, a_m ε_m²/κ_m ≲ ε_m^{-γ} and r N = ε_{m-1}^{1+γ/2} ε_m⁻¹ / A ≳ ε_{m-1}^{-(q-1-γ/2)}, the exponential factor exp(-rN/1024) beats every power of ε_{m-1}.

Abstract real arithmetic

theorem AVenhance.Infra.Section5.LeftToShow.SpaceKill.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.LeftToShow.SpaceKill.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.LeftToShow.SpaceKill.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.LeftToShow.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.LeftToShow.SpaceKill.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.LeftToShow.SpaceKill.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.LeftToShow.SpaceKill.l2NormSq_nonneg_sk (f : Homogenization.Vec 2 → ℝ) : 0 ≤ l2NormSq f

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

theorem AVenhance.Infra.Section5.LeftToShow.SpaceKill.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.LeftToShow.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 → ∀ (θ₀ : 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) * l2NormSq θ₀) (epsilon β I.Λ (m - 1) ^ (1 + gamma β / 2) / A)) → I.kappaSeq κ M m * |∫ (t : ℝ) in 0..1, (∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (leadingGrad I hΦ m (I.kappaSeq κ M m) (T (Nstar β)) t x)) - gradQuad (T (Nstar β)) (leadingGramAvg I hΦ m (I.kappaSeq κ M m) t) t| ≤ C * epsilon β I.Λ (m - 1) ^ 500 * l2NormSq θ₀

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