Trivial Solution

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

The identically zero suitable weak solution

The class IsSuitableWeakSolutionIntegrable (from def:sws in paper/ckn.tex) is a conjunction of analytic hypotheses on the velocity u, its gradient Du, the pressure p, and the forcing f. This file certifies that the identically zero data satisfies every hypothesis, so the class is inhabited and quantified statements over it are not vacuous.

theorem CKN.isSuitableWeakSolutionIntegrable_zero {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) (hIc : I.OrdConnected) (hq : 5 / 2 < q) : IsSuitableWeakSolutionIntegrable Ω I q (fun (x : Foundation.Parabolic.ParabolicPoint) => 0) (fun (x : Foundation.Parabolic.ParabolicPoint) (x_1 : Fin 3) => 0) (fun (x : Foundation.Parabolic.ParabolicPoint) => 0) fun (x : Foundation.Parabolic.ParabolicPoint) => 0

The identically zero velocity, pressure, and forcing satisfy IsSuitableWeakSolutionIntegrable.