Sup-in-time bound of the tail θ − θ_M in terms of ‖θ₀‖_{L²} #
tail_sup: for a weak solution θ of the limit drift streamVel φ and the classical solution
θ_M of streamVel (Φ M), both with diffusivity κ ≥ ½ ε_M^{β-γ} and the same datum,
‖θ(t) − θ_M(t)‖ ≤ 2 C_t (1+A)^β ε_M^{a} ‖θ₀‖.
theorem
AVenhance.Infra.FullTheorem.NoSel.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 : ℝ)
: