Sup-in-time L² stream-difference estimate #
Same setup as Section5.RelativeError.stream_difference_energy, but the energy identity is used
at every
time t ∈ [0,1] (region (0,t) × cube), giving
‖θ(t) − θ_M(t)‖ ≤ (η/κ) √κ ‖∇θ_M‖_{L²((0,1)×𝕋²)}.
theorem
AVenhance.Infra.FullTheorem.Uniform.stream_difference_sup
{b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hb_meas :
MeasureTheory.AEStronglyMeasurable (fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2)
(MeasureTheory.volume.restrict (Set.Icc 0 1 ×ˢ Set.univ)))
(hb_bdd : ∃ (C : ℝ), ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖b t x‖ ≤ C)
(hb_per : ∀ t ∈ Set.Icc 0 1, IsZ2Periodic (b t))
(hdiv : IsDivFree b)
{φ : ℝ → Homogenization.Vec 2 → ℝ}
(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φ : ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), b t x = streamVel φ t x)
{Ψ : ℝ → Homogenization.Vec 2 → ℝ}
(hΨ : IsAdmissibleStream Ψ)
{κ : ℝ}
(hκ : 0 < κ)
{g : Homogenization.Vec 2 → ℝ}
(hg : ContDiff ℝ (↑⊤) g)
(_hgp : IsZ2Periodic g)
{θM : ℝ → Homogenization.Vec 2 → ℝ}
(hθM : IsClassicalSol (streamVel Ψ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θM)
{θ : ℝ → Homogenization.Vec 2 → ℝ}
{Dθ : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hθ : IsWeakSolutionGrad b κ g θ Dθ)
{η : ℝ}
(hη : ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), |φ t x - Ψ t x| ≤ η)
(t : ℝ)
:
Sup-in-time L² form of the stream-difference estimate (same hypotheses as
stream_difference_energy): ‖θ(t) − θ_M(t)‖ ≤ (η/κ) √κ ‖∇θ_M‖_{L²} for every t ∈ [0,1].