RelativeError item 12: the stream-difference estimate #
A weak solution θ for the limit drift b = σ∇φ and the classical solution θ_M for a smooth
stream Ψ, with the same datum and diffusivity, have η/κ-close dissipation whenever
|φ - Ψ| ≤ η.
theorem
AVenhance.Infra.Section5.RelativeError.sigma_gradient_memLp
{θM : ℝ → Homogenization.Vec 2 → ℝ}
(hDM :
∀ (i : Fin 2),
MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (θM p.1) p.2 i) 2
(MeasureTheory.volume.restrict timeCube))
(i : Fin 2)
:
MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => sigmaMat.mulVec (spaceGrad (θM p.1) p.2) i) 2
(MeasureTheory.volume.restrict timeCube)
The skew rotation of a classical gradient field is coordinatewise L².
theorem
AVenhance.Infra.Section5.RelativeError.stream_difference_energy
{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| ≤ η)
:
√κ * √(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => Dθ t x - spaceGrad (θM t) x) ≤ η / κ * (√κ * √(spaceTimeGradNormSq fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θM t) x))
RelativeError item 12 (stream form, 9294–9330): a weak solution for the limit drift b = σ∇φ
and the
classical solution for a smooth stream Ψ with the same datum and diffusivity are η/κ-close in
dissipation whenever |φ − Ψ| ≤ η on the spacetime cell.