The kinetic energy identity of a strong solution #
The mollified equation, paired with the mollified velocity, passes to the
limit on almost every time slice, where the transport and pressure terms vanish
and the Laplacian pairs to minus the squared gradient
(prop:lps-local-strong).
theorem
ESS.LPS.lps_slab_slice_memLp_aem
{a b : ℝ}
{f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b)))
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, t)) 2 MeasureTheory.volume
Almost every time slice of a square-integrable slab field is square integrable, for fields that are only almost everywhere strongly measurable.
theorem
ESS.LPS.lps_strong_slice_serrin
{t₀ T t : ℝ}
{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 : IsLpsStrongSolution t₀ T u Du p)
(ht : t ∈ Set.Icc t₀ T)
:
(SerrinSlice (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) fun (x : CKN.Foundation.Parabolic.Vec3) =>
Du (x, t)) ∧ MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t)) (ENNReal.ofReal 4) MeasureTheory.volume
Every closed-interval slice of a strong solution is a Serrin slice, and
its velocity is in L⁴.
theorem
ESS.LPS.lps_strong_kinetic_slice
{t₀ T : ℝ}
{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 : IsLpsStrongSolution t₀ T u Du p)
{D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hDerivs : CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo t₀ T) u Du D2u Dtu)
(hu :
∀ (i : Fin 3),
MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z i) 2
(MeasureTheory.volume.restrict (CKN.vlSlab t₀ T)))
(hDu :
∀ (i j : Fin 3),
MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Du z i j) 2
(MeasureTheory.volume.restrict (CKN.vlSlab t₀ T)))
(hD2 :
∀ (i j : Fin 3),
MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => D2u z i j j) 2
(MeasureTheory.volume.restrict (CKN.vlSlab t₀ T)))
(hDt :
∀ (i : Fin 3),
MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Dtu z i) 2
(MeasureTheory.volume.restrict (CKN.vlSlab t₀ T)))
(hp : MeasureTheory.MemLp p 2 (MeasureTheory.volume.restrict (CKN.vlSlab t₀ T)))
:
On almost every time slice, the pairing of the time derivative with the
velocity is minus the squared gradient (prop:lps-local-strong).