Time calculus for the slices of a strong solution

For a strong solution, the fixed-time kinetic energy and the fixed-time squared gradient obey the time-integrated chain rule with the specified weak derivatives (prop:lps-local-strong).

theorem ESS.LPS.lps_component2_eLpNorm_le {v : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hv : MeasureTheory.AEStronglyMeasurable v MeasureTheory.volume) (i j : Fin 3) : MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => v x i j) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm v 2 MeasureTheory.volume

A component of a matrix-valued function is bounded in L² by the function.

theorem ESS.LPS.lps_strong_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} (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)))) (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

The energy of the specified gradient of a strong solution changes in time by the pairing of the time derivative with the Laplacian (prop:lps-local-strong).