Weak dissipation versus classical dissipation

From the stream-difference estimate stream_difference_energy with η/κ ≤ 1/10 and the squared triangle inequality, a weak solution for the limit drift dissipates at least 49/100 of the classical dissipation for the smooth stream Ψ.

theorem AVenhance.Infra.Section5.RelativeError.spaceTimeGradNormSq_nonneg' (D : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : 0 ≤ spaceTimeGradNormSq D

theorem AVenhance.Infra.Section5.RelativeError.spaceTimeGrad_integrable {D : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hD : ∀ (i : Fin 2), MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => D p.1 p.2 i) 2 (MeasureTheory.volume.restrict timeCube)) : MeasureTheory.Integrable (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecNormSq (D p.1 p.2)) (MeasureTheory.volume.restrict timeCube)

theorem AVenhance.Infra.Section5.RelativeError.AssemblyGradient.square_triangle' (u v : ℝ) : v ^ 2 ≤ 2 * u ^ 2 + 2 * (u - v) ^ 2

theorem AVenhance.Infra.Section5.RelativeError.spaceTimeGrad_triangle {D E : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hD : ∀ (i : Fin 2), MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => D p.1 p.2 i) 2 (MeasureTheory.volume.restrict timeCube)) (hE : ∀ (i : Fin 2), MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => E p.1 p.2 i) 2 (MeasureTheory.volume.restrict timeCube)) : spaceTimeGradNormSq E ≤ 2 * spaceTimeGradNormSq D + 2 * spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => D t x - E t x

Squared triangle inequality for the spacetime gradient norm.

theorem AVenhance.Infra.Section5.RelativeError.weighted_triangle_real {κ S1 S2 SD : ℝ} (hκ : 0 < κ) (h1 : 0 ≤ S1) (h2 : 0 ≤ S2) (htri : S2 ≤ 2 * SD + 2 * S1) (hd : √κ * √S1 ≤ 1 / 10 * (√κ * √S2)) : 49 / 100 * (κ * S2) ≤ κ * SD

Abstract form: d ≤ a/10 in the √κ-weighted norms gives 49/100 · κ S₂ ≤ κ S_D.

theorem AVenhance.Infra.Section5.RelativeError.weak_dissipation_ge_classical {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| ≤ η) (hηκ : η / κ ≤ 1 / 10) : 49 / 100 * (κ * spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θM t) x) ≤ κ * spaceTimeGradNormSq Dθ

Weak dissipation for the limit drift dominates 49/100 of the classical dissipation for a smooth stream Ψ uniformly η-close to φ, provided η/κ ≤ 1/10.