Slices

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

theorem CKN.divfree_slice_weak_countable {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hS2 : ∀ ψ ∈ spaceTimeTestFunction Ω I, MeasureTheory.IntegrableOn (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, u z i * spatialPartial ψ i z) (tsupport ψ) MeasureTheory.volume ∧ ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, ∑ i : Fin 3, u z i * spatialPartial ψ i z = 0) (hI : IsOpen I) {C : Set (Foundation.Parabolic.Vec3 → ℝ)} (hC : C.Countable) (hCtest : ∀ ψ ∈ C, ContDiff ℝ (↑⊤) ψ ∧ HasCompactSupport ψ ∧ tsupport ψ ⊆ Ω) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ ψ ∈ C, ∫ (x : Foundation.Parabolic.Vec3) in Ω, ∑ i : Fin 3, u (x, s) i * (fderiv ℝ ψ x) (basisVec i) = 0

The slice divergence identity holds simultaneously for every member of any countable family of admissible spatial test functions.

theorem CKN.weakGradient_slice_ae_of_sws {Ω : 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} (h : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψΩ : tsupport ψ ⊆ Ω) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i j : Fin 3), ∫ (x : Foundation.Parabolic.Vec3) in Ω, u (x, s) i * (fderiv ℝ ψ x) (basisVec j) = -∫ (x : Foundation.Parabolic.Vec3) in Ω, Du (x, s) i j * ψ x

For a fixed compactly supported smooth test function, the local weak-gradient clause of a suitable weak solution holds for almost every time in the full interval, after integrating by parts on the fixed spatial support.