Energy identities of a strong solution #
A strong solution satisfies the H¹ energy identity, with the specified
time derivative and Laplacian, and the kinetic energy equality on every
subinterval of its lifespan (prop:lps-local-strong).
theorem
ESS.LPS.lps_unregularised_h1_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),
CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo t₀ T) u Du D2u Dtu ∧ MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ T))) ∧ MeasureTheory.MemLp Dtu 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, ∑ j : Fin 3, Du (x, t) i j ^ 2 = (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, Du (x, s) i j ^ 2) - 2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo s t), ∑ i : Fin 3, Dtu z i * ∑ j : Fin 3, D2u z i j j) ∧ ∀ (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 unregularized energy identities of a strong solution: the weak
derivative witnesses are square integrable, the squared gradient changes by
minus twice the pairing of the time derivative with the Laplacian, and the
kinetic energy satisfies the equality on every closed subinterval
(prop:lps-local-strong).