C^k representatives of whole-space weak families

lem:lps-Bochner-joint-smooth: a function with a Sobolev family through order k + 2 on ℝ³ has a C^k representative whose ordered derivatives represent the family, with sup norms controlled by the Sobolev norm.

theorem ESS.lps_toReal_eLpNorm_le_add {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) : (MeasureTheory.eLpNorm f 2 MeasureTheory.volume).toReal ≤ (MeasureTheory.eLpNorm g 2 MeasureTheory.volume).toReal + (MeasureTheory.eLpNorm (f - g) 2 MeasureTheory.volume).toReal

Triangle inequality for real L² norms (lem:lps-Bochner-joint-smooth).

theorem ESS.lps_tendstoUniformly_of_uniformCauchy {a : ℕ → CKN.Foundation.Parabolic.Vec3 → ℝ} (h : ∀ (ε : ℝ), 0 < ε → ∃ (N : ℕ), ∀ n ≥ N, ∀ m ≥ N, ∀ (x : CKN.Foundation.Parabolic.Vec3), |a n x - a m x| < ε) : ∃ (l : CKN.Foundation.Parabolic.Vec3 → ℝ), TendstoUniformly a l Filter.atTop

Uniformly Cauchy sequences of real functions converge uniformly (lem:lps-Bochner-joint-smooth).

theorem ESS.lps_sobolevFamily_contDiff_rep (k : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (f : CKN.Foundation.Parabolic.Vec3 → ℝ) (D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ), CKN.IsSobolevFamilyOn (k + 2) Set.univ f D → ∃ (g : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑k) g ∧ g =ᵐ[MeasureTheory.volume] f ∧ (∀ (α : List (Fin 3)), α.length ≤ k → CKN.wordDeriv α g =ᵐ[MeasureTheory.volume] D α) ∧ ∀ (α : List (Fin 3)), α.length ≤ k → ∀ (x : CKN.Foundation.Parabolic.Vec3), |CKN.wordDeriv α g x| ≤ C * √(CKN.sobolevNormSqOn (k + 2) Set.univ D)

lem:lps-Bochner-joint-smooth: a whole-space weak family through order k + 2 has a C^k representative, its ordered derivatives represent the family, and their sup norms are bounded by the Sobolev norm.