Real quadratic energy from weak L² data

The Euclidean vector and spatial-gradient energies used in the short-time Carleman argument are integrable wherever the corresponding weak fields belong to L².

theorem ESS.bu_memLp_quadratic_energy_integrable (S : Set CKN.Foundation.Parabolic.ParabolicPoint) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (hw : MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict S)) (hDw : MeasureTheory.MemLp Dw 2 (MeasureTheory.volume.restrict S)) : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2) S MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialGradientSq w Dw z) S MeasureTheory.volume

Square-integrable field and weak gradient data yield integrable real quadratic energy on the same set.