Energy balance for the difference of two weak solutions #
For weak solutions with the same datum and diffusivity, a bounded divergence-free drift for
the first, and a flux F representing the cross transport against smooth periodic tests, the
difference satisfies ‖w(t)‖² + 2κ∫∫|Dw|² = -2∫∫F·Dw.
theorem
AVenhance.Infra.Section5.RelativeError.forced_vecDot_integrable_fields
{Y Z : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2}
(hY :
∀ (i : Fin 2),
MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => Y p i) 2 (MeasureTheory.volume.restrict timeCube))
(hZ :
∀ (i : Fin 2),
MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => Z p i) 2 (MeasureTheory.volume.restrict timeCube))
:
MeasureTheory.Integrable (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecDot (Y p) (Z p))
(MeasureTheory.volume.restrict timeCube)
Coordinatewise L² fields have integrable dot product on the time cell.
theorem
AVenhance.Infra.Section5.RelativeError.difference_energy_identity
{b bM : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{κ : ℝ}
{g : Homogenization.Vec 2 → ℝ}
{θ θM : ℝ → Homogenization.Vec 2 → ℝ}
{Dθ DM : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
(hθ : IsWeakSolutionGrad b κ g θ Dθ)
(hM : IsWeakSolutionGrad bM κ g θM DM)
(hg : Homogenization.MemL2On unitCube g)
(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)
{F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2}
(hF :
∀ (i : Fin 2),
MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => F p i) 2 (MeasureTheory.volume.restrict timeCube))
(hflux :
∀ s ∈ Set.Icc 0 1,
∀ (ψ : Homogenization.Vec 2 → ℝ),
ContDiff ℝ (↑⊤) ψ →
IsZ2Periodic ψ →
MeasureTheory.Integrable
(fun (x : Homogenization.Vec 2) => Homogenization.vecDot (b s x - bM s x) (DM s x) * ψ x)
(MeasureTheory.volume.restrict unitCube) ∧ ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (b s x - bM s x) (DM s x) * ψ x = ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (F (s, x)) (spaceGrad ψ x))
{t : ℝ}
(ht : t ∈ Set.Icc 0 1)
:
(l2NormSq fun (x : Homogenization.Vec 2) => θ t x - θM t x) + 2 * κ * ∫ (p : ℝ × Homogenization.Vec 2) in Parabolic.WeakUniqueness.weakEnergyRegion t, Homogenization.vecDot (Dθ p.1 p.2 - DM p.1 p.2) (Dθ p.1 p.2 - DM p.1 p.2) = -2 * ∫ (p : ℝ × Homogenization.Vec 2) in Parabolic.WeakUniqueness.weakEnergyRegion t, Homogenization.vecDot (F p) (Dθ p.1 p.2 - DM p.1 p.2)