Singular Set

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

def CKN.SingularSet (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) : Set Foundation.Parabolic.ParabolicPoint

The singular set from paper label def:regular.

Equations

• CKN.SingularSet Ω I u = {z : CKN.Foundation.Parabolic.ParabolicPoint | z ∈ CKN.spaceTimeSet Ω I ∧ ¬CKN.IsRegularPoint Ω I u z}