One level of the chain, telescoping, and the L² triangle for norms

• abs_sqrt_l2_sub_le: |‖f‖ − ‖g‖| ≤ ‖f − g‖ for L²(unitCube) functions;
• step_sup: the sup part (i) of the step-down estimate for one classical level, with the iterate witness from RelativeError.exists_TIterates;
• telescope_l2: the sum of the level increments bounds ‖θ_k − θ_{n₀}‖.

theorem AVenhance.Infra.FullTheorem.NoSel.l2NormSq_sub_comm (f g : Homogenization.Vec 2 → ℝ) : (l2NormSq fun (x : Homogenization.Vec 2) => g x - f x) = l2NormSq fun (x : Homogenization.Vec 2) => f x - g x

theorem AVenhance.Infra.FullTheorem.NoSel.abs_sqrt_l2_sub_le {f g : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) (hg : Homogenization.MemL2On unitCube g) : |√(l2NormSq f) - √(l2NormSq g)| ≤ √(l2NormSq fun (x : Homogenization.Vec 2) => f x - g x)

theorem AVenhance.Infra.FullTheorem.NoSel.telescope_l2 {θs : ℕ → ℝ → Homogenization.Vec 2 → ℝ} {n₀ M : ℕ} {t : ℝ} {a : ℕ → ℝ} (hc : ∀ (j : ℕ), n₀ ≤ j → j ≤ M → Continuous (θs j t)) (hstep : ∀ (l : ℕ), n₀ < l → l ≤ M → √(l2NormSq fun (x : Homogenization.Vec 2) => θs l t x - θs (l - 1) t x) ≤ a l) (k : ℕ) : n₀ ≤ k → k ≤ M → √(l2NormSq fun (x : Homogenization.Vec 2) => θs k t x - θs n₀ t x) ≤ ∑ l ∈ Finset.Ioc n₀ k, a l

The L² norm of a difference along a telescoping chain of continuous slices.

theorem AVenhance.Infra.FullTheorem.NoSel.step_sup (β C₀ : ℝ) : ∃ (C₈ : ℝ), 0 ≤ C₈ ∧ ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ C₀ → C₈ ≤ ↑I.Λ → ∀ (Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ), IsStreamSeq I Φ → ∀ κ ∈ permissibleSet β I.Λ, ∀ (M : ℕ), 1 ≤ M → κ ∈ permittedInterval β I.Λ M → ∀ (R : ℝ), 0 < R → ∀ (θ₀ : Homogenization.Vec 2 → ℝ), ContDiff ℝ (↑⊤) θ₀ → IsZ2Periodic θ₀ → Homogenization.MeanZeroOn unitCube θ₀ → IsThetaAnalytic R θ₀ → ∀ (m : ℕ), mTheta0 β I.Λ R ≤ m → m ≤ M → 0 < I.kappaSeq κ M m → 0 < I.kappaSeq κ M (m - 1) → ∀ (θm θprev : ℝ → Homogenization.Vec 2 → ℝ), IsClassicalSol (streamVel (Φ m)) (I.kappaSeq κ M m) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θm → IsClassicalSol (streamVel (Φ (m - 1))) (I.kappaSeq κ M (m - 1)) (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev → ∀ t ∈ Set.Icc 0 1, √(l2NormSq fun (x : Homogenization.Vec 2) => θm t x - θprev t x) ≤ C₈ * epsilon β I.Λ (m - 1) ^ delta β * √(l2NormSq θ₀)

Sup part (i) of the step-down estimate for one classical level, uniform in the permitted data.