Jointly smooth representative from all-order slice curves

lem:lps-Bochner-joint-smooth: if the slices of a scalar space-time field are L²-continuous curves of all-order Sobolev families whose spatial pairings are differentiable in time with derivative the next slice, then the field has a representative that is C^∞ on ℝ³ × [a,b], with one-sided time derivatives at the endpoints.

theorem ESS.lps_hasFDerivAt_sum_spatialDeriv {h : CKN.Foundation.Parabolic.Vec3 → ℝ} (hd : Differentiable ℝ h) (x : CKN.Foundation.Parabolic.Vec3) : HasFDerivAt h (∑ i : Fin 3, CKN.spatialDeriv h i x • ContinuousLinearMap.proj i) x

The Fréchet derivative of a differentiable function on ℝ³ is the sum of its coordinate derivatives.

theorem ESS.lps_smooth_rep_of_curves {a b : ℝ} (hab : a < b) {Z : ℕ → ℝ → List (Fin 3) → CKN.Foundation.Parabolic.Vec3 → ℝ} (hfam : ∀ (j : ℕ), ∀ t ∈ Set.Icc a b, ∀ (m : ℕ), CKN.IsSobolevFamilyOn m Set.univ (Z j t []) (Z j t)) (hcont : ∀ (j : ℕ) (α : List (Fin 3)), ∀ t ∈ Set.Icc a b, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (Z j s α - Z j t α) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc a b)) (nhds 0)) (hderiv : ∀ (j : ℕ) (α : List (Fin 3)) (ψ : CKN.Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∀ t ∈ Set.Icc a b, HasDerivWithinAt (fun (s : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), Z j s α x * ψ x) (∫ (x : CKN.Foundation.Parabolic.Vec3), Z (j + 1) t α x * ψ x) (Set.Icc a b) t) : ∃ (R : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiffOn ℝ (↑⊤) R (Set.univ ×ˢ Set.Icc a b) ∧ ∀ t ∈ Set.Icc a b, (fun (x : CKN.Foundation.Parabolic.Vec3) => R (x, t)) =ᵐ[MeasureTheory.volume] Z 0 t []

lem:lps-Bochner-joint-smooth: a scalar space-time field whose slices form L²-continuous curves of all-order Sobolev families with pairing-differentiable time chain has a representative that is C^∞ on the closed slab.