Sup-in-time pieces for the no-selection limit

• tail_sup: sup_t ‖θ(t) − θ_M(t)‖ ≤ 2 C_t (1+A)^β ε_M^{a} ‖θ₀‖ for a weak solution θ (limit drift) and the classical solution θ_M (drift Φ_M) with the same diffusivity;
• step_sup: sup form of the step-down estimate (i): sup_t ‖θ_m − θ_{m-1}‖ ≤ C ε_{m-1}^δ ‖θ₀‖.

theorem AVenhance.Infra.FullTheorem.tail_sup {β Ct Bφ : ℝ} (hCt : 0 ≤ Ct) {I : Ingredients β} {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {φ : ℝ → Homogenization.Vec 2 → ℝ} (htail : ∀ (M : ℕ) (t : ℝ) (x : Homogenization.Vec 2), |φ t x - Φ M t x| ≤ Ct * epsilon β I.Λ (M + 1) ^ β) (hφ_meas : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ))) (hφ_per : ∀ t ∈ Set.Icc 0 1, IsZ2Periodic (φ t)) (hφ_diff : ∀ t ∈ Set.Icc 0 1, Differentiable ℝ (φ t)) (hb_meas : MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => streamVel φ p.1 p.2) (MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ))) (hb_per : ∀ t ∈ Set.Icc 0 1, IsZ2Periodic (streamVel φ t)) (hdiv : IsDivFree (streamVel φ)) (hb_bdd : ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖streamVel φ t x‖ ≤ Bφ) {κ : ℝ} {M : ℕ} (hM : 1 ≤ M) (hκlo : 1 / 2 * epsilon β I.Λ M ^ (β - gamma β) ≤ κ) {θ₀ : Homogenization.Vec 2 → ℝ} (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hper : IsZ2Periodic θ₀) {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : IsWeakSolution (streamVel φ) κ θ₀ θ) {θM : ℝ → Homogenization.Vec 2 → ℝ} (hθM : IsClassicalSol (streamVel (Φ M)) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θM) (t : ℝ) : t ∈ Set.Icc 0 1 → √(l2NormSq fun (x : Homogenization.Vec 2) => θ t x - θM t x) ≤ 2 * Ct * (1 + Ingredients.supergeoConstant β) ^ β * epsilon β I.Λ M ^ tailExp β * √(l2NormSq θ₀)

theorem AVenhance.Infra.FullTheorem.step_sup (β C₀ : ℝ) : ∃ (C : ℝ) (Λ₀ : ℝ), 0 ≤ C ∧ ∀ (I : Ingredients β), I.Czeta ≤ C₀ → I.Cxi ≤ C₀ → I.Chat ≤ 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 → ∀ (θ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 form of the step-down estimate (i) at one level of the chain.