Decomposition SWSBasic

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

theorem CKN.decomposition_laplacian_hasCompactSupport_sws {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψc : HasCompactSupport ψ) : HasCompactSupport (spatialLaplacian ψ)

theorem CKN.decomposition_full_of_on_sws {Ω : Set Foundation.Parabolic.Vec3} {g : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.IntegrableOn g Ω MeasureTheory.volume) (hΩ : tsupport g ⊆ Ω) : MeasureTheory.Integrable g MeasureTheory.volume

theorem CKN.decomposition_ts_support_sum₂_sws {Ω : Set Foundation.Parabolic.Vec3} {F : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ} (hF : ∀ (i j : Fin 3), tsupport (F i j) ⊆ Ω) : (tsupport fun (x : Foundation.Parabolic.Vec3) => ∑ i : Fin 3, ∑ j : Fin 3, F i j x) ⊆ Ω

theorem CKN.decomposition_ts_support_sum₃_sws {Ω : Set Foundation.Parabolic.Vec3} {F : Fin 3 → Foundation.Parabolic.Vec3 → ℝ} (hF : ∀ (i : Fin 3), tsupport (F i) ⊆ Ω) : (tsupport fun (x : Foundation.Parabolic.Vec3) => ∑ i : Fin 3, F i x) ⊆ Ω