Consistency of the slice families of different orders

prop:lps-smoothing: two families of slices, each L²-continuous in time and each representing the same field for almost every time, coincide at every time, and hence have the same weak derivatives.

theorem ESS.lps_curves_eq_of_ae_eq {a b : ℝ} (hab : a < b) {f g : ℝ → CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : ∀ t ∈ Set.Icc a b, MeasureTheory.MemLp (f t) 2 MeasureTheory.volume) (hg : ∀ t ∈ Set.Icc a b, MeasureTheory.MemLp (g t) 2 MeasureTheory.volume) (hcf : ∀ t ∈ Set.Icc a b, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (f s - f t) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc a b)) (nhds 0)) (hcg : ∀ t ∈ Set.Icc a b, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (g s - g t) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc a b)) (nhds 0)) (hae : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), f t =ᵐ[MeasureTheory.volume] g t) (t : ℝ) : t ∈ Set.Icc a b → f t =ᵐ[MeasureTheory.volume] g t

Two L²-continuous curves of functions that agree for almost every time agree at every time of the closed interval (prop:lps-smoothing).