Local integrability from the data clauses alone

The data clauses of def:sws bound the fields on every local box Ω' × J. A compact subset of the space-time carrier always sits inside such a box (CKN.caccioppoli_localBox_of_compact_subset), so each of those bounds transfers to an arbitrary compact set, and that is the form in which the integrability clauses of def:sws need them: they are all stated on the closed support of a test function, which is compact.

Every statement here takes CKN.IsSuitableWeakSolutionData and not the full class. The same facts already exist in the tree stated with the full class - CKN.spatialGradientSq_integrableOn_compact is the closest one - but a lemma of that shape cannot be used while establishing the class's own integrability clauses, since it would assume what is being proved. The proofs below use nothing beyond the data clauses.

theorem CKN.velocity_memLp_two_on_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) : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict K)

The velocity is square integrable on every compact subset of the carrier.

theorem CKN.gradient_memLp_two_on_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) : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict K)

The velocity gradient is square integrable on every compact subset of the carrier.

theorem CKN.pressure_memLp_threeHalves_on_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) : MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict K)

The pressure is L^{3/2} on every compact subset of the carrier.

theorem CKN.force_memLp_on_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) : MeasureTheory.MemLp f (ENNReal.ofReal q) (MeasureTheory.volume.restrict K)

The force is L^q on every compact subset of the carrier.

theorem CKN.spatialGradientSq_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) : MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialGradientSq u Du z) K MeasureTheory.volume

The Dirichlet density of the velocity is integrable on every compact subset of the carrier. This is the data-clause form of CKN.spatialGradientSq_integrableOn_compact.