Energy equality in the Serrin class #
A finite-energy weak solution with pressure that lies in space-time L⁵
satisfies the energy equality at almost every time: this is the cross-testing
identity of the solution with itself, whose convection term vanishes. It gives
the strong solution's side of the comparison in lem:pv-serrin-uniqueness.
theorem
ESS.serrin_slab_integral_eq_zero
{t T : ℝ}
(ht0 : 0 ≤ t)
(htT : t ≤ T)
{F : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 t))))
(hzero : ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∫ (y : CKN.Foundation.Parabolic.Vec3), F (y, τ) = 0)
:
An integrable space-time density whose spatial integrals vanish at almost every time has vanishing integral on every shorter slab.
theorem
ESS.serrinWeak_slice_ae
{T : ℝ}
{a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hU : IsSerrinWeakSolution T a u Du p)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), SerrinSlice (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, s)) fun (x : CKN.Foundation.Parabolic.Vec3) => Du (x, s)
The slice facts of a finite-energy weak solution at almost every time.
theorem
ESS.serrin_energy_equality
{T : ℝ}
{a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hU : IsSerrinWeakSolution T a u Du p)
(hu5 :
MeasureTheory.MemLp u (ENNReal.ofReal 5) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, u (x, t) k * u (x, t) k) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, a x k * a x k = -2 * ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Du q k j * Du q k j
Energy equality at almost every time for a finite-energy weak solution with
pressure in space-time L⁵.