Uniform limits of smooth functions and their ordered derivatives

If smooth functions on ℝ³ converge uniformly together with all ordered derivatives up to order k, the limit is C^k and its ordered derivatives are the limits (lem:lps-Bochner-joint-smooth).

theorem ESS.lps_spatialDeriv_eq_of_hasFDerivAt {f : CKN.Foundation.Parabolic.Vec3 → ℝ} {f' : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3 →L[ℝ] ℝ} (h : ∀ (x : CKN.Foundation.Parabolic.Vec3), HasFDerivAt f (f' x) x) (j : Fin 3) : CKN.spatialDeriv f j = fun (x : CKN.Foundation.Parabolic.Vec3) => (f' x) (CKN.basisVec j)

The first-order derivative along j of a C¹ function is the value of its Fréchet derivative on the jth basis vector.

theorem ESS.lps_uniform_limit_contDiff (k : ℕ) (g : ℕ → CKN.Foundation.Parabolic.Vec3 → ℝ) : (∀ (n : ℕ), ContDiff ℝ (↑⊤) (g n)) → (∀ (α : List (Fin 3)), α.length ≤ k → ∃ (h : CKN.Foundation.Parabolic.Vec3 → ℝ), TendstoUniformly (fun (n : ℕ) => CKN.wordDeriv α (g n)) h Filter.atTop) → ∃ (f : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑k) f ∧ ∀ (α : List (Fin 3)), α.length ≤ k → TendstoUniformly (fun (n : ℕ) => CKN.wordDeriv α (g n)) (CKN.wordDeriv α f) Filter.atTop

Uniform limits of smooth functions whose ordered derivatives up to order k converge uniformly are C^k, with the limit of the derivatives as derivatives (lem:lps-Bochner-joint-smooth).