The stream-difference estimate #
For a weak solution θ of the limit drift b = σ∇φ and the classical solution θ_M for a smooth
stream Ψ with the same datum and diffusivity, the difference satisfies the energy balance with the
skew flux (φ - Ψ) σ∇θ_M; Cauchy–Schwarz then gives the η/κ bound on the dissipation.
theorem
AVenhance.Infra.Section5.RelativeError.stream_grad_bound
{φ : ℝ → Homogenization.Vec 2 → ℝ}
{C s : ℝ}
(hC : ∀ (x : Homogenization.Vec 2), ‖streamVel φ s x‖ ≤ C)
(i : Fin 2)
:
The gradient coordinates of a stream with bounded velocity are bounded.
theorem
AVenhance.Infra.Section5.RelativeError.streamVel_sub_eq
{φ Ψ : ℝ → Homogenization.Vec 2 → ℝ}
{s : ℝ}
(hφ : Differentiable ℝ (φ s))
(hΨ : Differentiable ℝ (Ψ s))
(x : Homogenization.Vec 2)
:
The difference of the stream velocities is the skew gradient of the stream difference.
theorem
AVenhance.Infra.Section5.RelativeError.stream_flux_slice
{φ Ψ : ℝ → Homogenization.Vec 2 → ℝ}
{s C : ℝ}
(hφd : Differentiable ℝ (φ s))
(hφp : IsZ2Periodic (φ s))
(hC : ∀ (x : Homogenization.Vec 2), ‖streamVel φ s x‖ ≤ C)
(hΨ : IsAdmissibleStream Ψ)
{θ ψ : Homogenization.Vec 2 → ℝ}
(hθ : ContDiff ℝ (↑⊤) θ)
(hθp : IsZ2Periodic θ)
(hψ : ContDiff ℝ (↑⊤) ψ)
(hψp : IsZ2Periodic ψ)
:
MeasureTheory.IntegrableOn
(fun (x : Homogenization.Vec 2) => Homogenization.vecDot (streamVel φ s x - streamVel Ψ s x) (spaceGrad θ x) * ψ x)
unitCube MeasureTheory.volume ∧ ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (streamVel φ s x - streamVel Ψ s x) (spaceGrad θ x) * ψ x = ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (fun (i : Fin 2) => (φ s x - Ψ s x) * sigmaMat.mulVec (spaceGrad θ x) i) (spaceGrad ψ x)
A fixed-time slice of the stream difference satisfies the flux representation of the cross transport against smooth periodic tests.