Integrability

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.u_sq_mul_test_integrable {Ω : 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} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ψ ∈ spaceTimeTestFunction Ω I) : MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u z) ^ 2 * ψ z) MeasureTheory.volume

The squared velocity times a compactly supported test function is integrable.

Compact rectangular time-slice bounds

theorem CKN.sws_timeSliceBallEnergy_essSup_lt_top {Ω : 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} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {x₀ : Foundation.Parabolic.Vec3} {R a b : ℝ} (hR : 0 < R) (hab : a < b) (hrect : euclideanClosedBall x₀ R ×ˢ Set.Icc a b ⊆ spaceTimeSet Ω I) : essSup (fun (x : ℝ) => Foundation.Parabolic.Integration.timeSliceBallEnergy x₀ R x fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u w)) (MeasureTheory.volume.restrict (Set.Ioc a b)) < ⊤

The velocity time-slice energy is essentially bounded on a compact rectangular portion of the open space-time carrier.