The kinetic energy identity of a strong solution #
For a strong solution, the fixed-time kinetic energy changes by minus twice
the space-time integral of the squared specified gradient
(prop:lps-local-strong).
theorem
ESS.LPS.lps_slab_sum_slice_integral
{ι : Type u_1}
(S : Finset ι)
{s t : ℝ}
{F : ι → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hF : ∀ k ∈ S, MeasureTheory.Integrable (F k) (MeasureTheory.volume.restrict (CKN.vlSlab s t)))
:
A finite sum of slab integrals is the time integral of the sum of the slice integrals.
theorem
ESS.LPS.lps_component1_eLpNorm_le
{v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
(hv : MeasureTheory.AEStronglyMeasurable v MeasureTheory.volume)
(i : Fin 3)
:
MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => v x i) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm v 2 MeasureTheory.volume
A component of a vector-valued function is bounded in L² by the
function.
theorem
ESS.LPS.lps_strong_kinetic_energy_identity
{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)
(hMemU : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))))
(hMemDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))))
(hMemD2u : MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))))
(hMemDtu : MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))))
(hMemP : MeasureTheory.MemLp p 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))))
(s t : ℝ)
:
s ∈ Set.Icc t₀ T →
t ∈ Set.Icc t₀ T →
s ≤ t →
(∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i ^ 2) + 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo s t), ∑ i : Fin 3, ∑ j : Fin 3, Du z i j ^ 2 = ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, s) i ^ 2
The kinetic energy of a strong solution changes by minus twice the
space-time integral of the squared specified gradient (prop:lps-local-strong).