Decomposition SWS

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

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