Suitable Weak Solution

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

def CKN.IsSuitableWeakSolution (Ω : 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) : Prop

The suitable weak-solution class exactly as def:sws of the manuscript states it: explicit measurability, finite energies and interval time domains, together with the divergence-free identity, the weak momentum identity and the local energy inequality, each carrying no integrability side condition on the integrand it tests. The a.e. uniqueness of the weak gradient is CKN.HasWeakPartialDerivOn.ae_eq from CKN/Foundation/Sobolev/WeakDerivative.lean.

CKN.IsSuitableWeakSolutionIntegrable of CKN/Statements/SuitableWeakSolutionIntegrable.lean adds four integrability conjuncts to the identity clauses. Those follow from the regularity clauses above, so the two classes have the same inhabitants; the proof is CKN.isSuitableWeakSolution_iff_integrable.

Equations

• One or more equations did not get rendered due to their size.