The dissipation integrand of the local energy inequality

The local energy inequality of def:sws carries an integrability side condition on its left-hand side: the Dirichlet density spatialGradientSq u Du multiplied by the test function must be integrable on the closed support of that test function.

This file proves that side condition from the data clauses alone. The closed support is compact, so the Dirichlet density is already integrable there (CKN.spatialGradientSq_integrableOn_compact_of_data), and the test function is a bounded factor. Nothing about the identities of def:sws is used, so the conclusion is available while those identities are still being established.

theorem CKN.dissipation_integrand_integrableOn_of_data {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hdata : IsSuitableWeakSolutionData Ω I q u Du p f) {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ψ ∈ spaceTimeTestFunction Ω I) : MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialGradientSq u Du z * ψ z) (tsupport ψ) MeasureTheory.volume

The dissipation integrand of the local energy inequality of def:sws is integrable on the closed support of the test function. Only the data clauses are used; the nonnegativity of the test function that the clause also assumes is not needed for integrability and is therefore omitted here.