Suitable Weak Solution Integrable #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
def
CKN.IsSuitableWeakSolutionIntegrable
(Ω : 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)
:
The suitable weak-solution class from def:sws, with explicit measurability,
finite energies, support integrability, and interval time domains. The a.e.
uniqueness of the weak gradient is CKN.HasWeakPartialDerivOn.ae_eq from
CKN/Foundation/Sobolev/WeakDerivative.lean.
Equations
- One or more equations did not get rendered due to their size.