Slice Identity #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
Per-test and parametrized forms #
theorem
CKN.pressure_slice_identity_ae
{Ω : 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, ∫ (x : Foundation.Parabolic.Vec3) in Ω, p (x, s) * spatialLaplacian ψ x = (-∫ (x : Foundation.Parabolic.Vec3) in Ω, ∑ i : Fin 3, ∑ j : Fin 3, u (x, s) i * u (x, s) j * mixedSecond ψ i j x) - ∫ (x : Foundation.Parabolic.Vec3) in Ω, ∑ i : Fin 3, f (x, s) i * spatialDeriv ψ i x
The pressure slice identity, including the force term, holds for each fixed compactly supported smooth spatial test function for almost every time.
theorem
CKN.pressure_slice_identity_ae_countable
{Ω : 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)
{C : Set (Foundation.Parabolic.Vec3 → ℝ)}
(hC : C.Countable)
(hCtest : ∀ ψ ∈ C, ContDiff ℝ (↑⊤) ψ ∧ HasCompactSupport ψ ∧ tsupport ψ ⊆ Ω)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ ψ ∈ C,
∫ (x : Foundation.Parabolic.Vec3) in Ω, p (x, s) * spatialLaplacian ψ x = (-∫ (x : Foundation.Parabolic.Vec3) in Ω, ∑ i : Fin 3, ∑ j : Fin 3, u (x, s) i * u (x, s) j * mixedSecond ψ i j x) - ∫ (x : Foundation.Parabolic.Vec3) in Ω, ∑ i : Fin 3, f (x, s) i * spatialDeriv ψ i x
The per-test pressure identity holds simultaneously for a countable family of compactly supported smooth tests.