Quadratic heat energy from weak L² data

The weak heat vector is square-integrable whenever its specified second spatial and time derivative fields are square-integrable.

theorem ESS.bu_memLp_heat_sq_integrable (S : Set CKN.Foundation.Parabolic.ParabolicPoint) (D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hD2w : MeasureTheory.MemLp D2w 2 (MeasureTheory.volume.restrict S)) (hDtw : MeasureTheory.MemLp Dtw 2 (MeasureTheory.volume.restrict S)) : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2w Dtw z) ^ 2) S MeasureTheory.volume

The squared Euclidean norm of the weak heat vector is integrable from L² second spatial and time derivative data.