Theorem C #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
Theorem CProvider #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
This module assembles Theorem C from the gradient criterion of Theorem B
for IsSuitableWeakSolutionIntegrable. It is imported by CKN.Main.TheoremC
and participates in the public theorem assembly.
theorem
CKN.caffarelliKohnNirenberg_provider_of_epsilonRegularityGradient
(hB :
∀ (q : ℝ),
5 / 2 < q →
∃ (ε₁ : ℝ),
0 < ε₁ ∧ ∀ (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ)
(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),
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
∀ z₀ ∈ spaceTimeSet Ω I,
Filter.limsup
(fun (r : ℝ) =>
(ENNReal.ofReal r)⁻¹ * ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 r, ENNReal.ofReal (spatialGradientSq u Du w))
(nhdsWithin 0 (Set.Ioi 0)) < ENNReal.ofReal (ε₁ ^ 2) →
IsRegularPoint Ω I u z₀)
(q : ℝ)
:
5 / 2 < q →
∀ (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ)
(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),
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
(Foundation.Parabolic.parabolicHausdorffMeasure 1) (SingularSet Ω I u) = 0
Conditional assembly of Theorem C from the reduction in
TheoremCOfB.lean.
theorem
CKN.Main.caffarelliKohnNirenberg
(q : ℝ)
(hq : 5 / 2 < q)
(Ω : Set Foundation.Parabolic.Vec3)
(I : Set ℝ)
(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)
:
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
(Foundation.Parabolic.parabolicHausdorffMeasure 1) (SingularSet Ω I u) = 0
The parabolic singular set of a suitable weak solution has zero one dimensional Hausdorff measure.