The integrand of the divergence-free identity

The divergence-free clause of def:sws pairs the identity ∫ ∑ᵢ uᵢ ∂ᵢψ = 0 with an integrability side condition on the integrand, stated on the closed support of the test function ψ.

This file proves that side condition from the data clauses alone. The closed support is compact, so Lebesgue measure restricted to it is finite and the square integrable velocity of the data clauses is integrable there; each spatial derivative of a test function is a bounded factor, and the integrand is a finite sum of such products.

Nothing about the identities of def:sws is used, so the conclusion is available while those identities are still being established.

theorem CKN.velocity_component_integrableOn_compact_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) {K : Set Foundation.Parabolic.ParabolicPoint} (hK : IsCompact K) (hKsub : K ⊆ spaceTimeSet Ω I) (i : Fin 3) : MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) K MeasureTheory.volume

Each component of the velocity is integrable on a compact subset of the carrier: it is square integrable there, and the restricted measure is finite.

theorem CKN.divergenceFree_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) => ∑ i : Fin 3, u z i * spatialPartial ψ i z) (tsupport ψ) MeasureTheory.volume

The integrand of the divergence-free clause of def:sws is integrable on the closed support of the test function. Only the data clauses are used.