Sobolev embedding for whole-space weak families

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

theorem ESS.lps_integral_sq_sub_small {a : ℕ → CKN.Foundation.Parabolic.Vec3 → ℝ} {D : CKN.Foundation.Parabolic.Vec3 → ℝ} (ha : ∀ (n : ℕ), MeasureTheory.MemLp (a n) 2 MeasureTheory.volume) (hD : MeasureTheory.MemLp D 2 MeasureTheory.volume) (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (a n - D) 2 MeasureTheory.volume) Filter.atTop (nhds 0)) (ε : ℝ) : 0 < ε → ∃ (N : ℕ), ∀ n ≥ N, ∀ m ≥ N, ∫ (x : CKN.Foundation.Parabolic.Vec3), (a n x - a m x) ^ 2 < ε

A square-integrable function that is the L² limit of smooth compactly supported functions with square-integrable difference a n - a m has Cauchy square integrals (lem:lps-Bochner-joint-smooth).

theorem ESS.lps_sobolevNormSq_two_sub_small {g : ℕ → CKN.Foundation.Parabolic.Vec3 → ℝ} {D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ} {k : ℕ} (hg : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (g n)) (hgc : ∀ (n : ℕ), HasCompactSupport (g n)) (hD : ∀ (α : List (Fin 3)), α.length ≤ k + 2 → MeasureTheory.MemLp (D α) 2 MeasureTheory.volume) (hconv : ∀ (α : List (Fin 3)), α.length ≤ k + 2 → Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (CKN.wordDeriv α (g n) - D α) 2 MeasureTheory.volume) Filter.atTop (nhds 0)) (α : List (Fin 3)) (hα : α.length ≤ k) (ε : ℝ) : 0 < ε → ∃ (N : ℕ), ∀ n ≥ N, ∀ m ≥ N, (CKN.sobolevNormSqOn 2 Set.univ fun (β : List (Fin 3)) => CKN.wordDeriv β (CKN.wordDeriv α fun (x : CKN.Foundation.Parabolic.Vec3) => g n x - g m x)) < ε

The H² norm squared of an ordered derivative of a difference of two members of an L²-convergent smooth family is eventually small (lem:lps-Bochner-joint-smooth).