Continuous L² representatives from kernel limits

If mollifications of a field with a square-integrable time derivative converge in the slab, and the slice pairings of the mollified fields and their time derivatives are represented by convergent dual fields, then the field has a continuous L²-valued representative with an energy identity in time (prop:lps-local-strong).

theorem ESS.LPS.lps_kernel_limit_curve {a b : ℝ} {w r : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hab : a < b) (hwm : MeasureTheory.StronglyMeasurable w) (hrm : MeasureTheory.StronglyMeasurable r) (hw : MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hr : MeasureTheory.MemLp r 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hweak : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b), ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, w p * CKN.timePartial φ p = -∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, r p * φ p) {k : ℕ → CKN.Foundation.Parabolic.Vec3 → ℝ} (hk : ∀ (n : ℕ), CKN.IsVlKernel (k n)) {P Q : ℕ → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hPm : ∀ (n : ℕ), MeasureTheory.StronglyMeasurable (P n)) (hQm : ∀ (n : ℕ), MeasureTheory.StronglyMeasurable (Q n)) (hP : ∀ (n : ℕ), MeasureTheory.MemLp (P n) 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hQ : ∀ (n : ℕ), MeasureTheory.MemLp (Q n) 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (c : ℝ) (hpairDiff : ∀ (n m : ℕ), ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConvT (k n - k m) w x s * CKN.vlConvT (k n - k m) r x s = c * ∫ (x : CKN.Foundation.Parabolic.Vec3), (P n (x, s) - P m (x, s)) * (Q n (x, s) - Q m (x, s))) (hpairDiag : ∀ (n : ℕ), ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConvT (k n) w x s * CKN.vlConvT (k n) r x s = c * ∫ (x : CKN.Foundation.Parabolic.Vec3), P n (x, s) * Q n (x, s)) {q p q' : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hqm : MeasureTheory.StronglyMeasurable q) (hq : MeasureTheory.MemLp q 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hp : MeasureTheory.MemLp p 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hq' : MeasureTheory.MemLp q' 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hSslab : Filter.Tendsto (fun (n : ℕ) => ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, (CKN.vlConvT (k n) w z.1 z.2 - q z) ^ 2) Filter.atTop (nhds 0)) (hSslice : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), Filter.Tendsto (fun (n : ℕ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), (CKN.vlConvT (k n) w x s - q (x, s)) ^ 2) Filter.atTop (nhds 0)) (hPlim : Filter.Tendsto (fun (n : ℕ) => ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, (P n z - p z) ^ 2) Filter.atTop (nhds 0)) (hQlim : Filter.Tendsto (fun (n : ℕ) => ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, (Q n z - q' z) ^ 2) Filter.atTop (nhds 0)) : ∃ (L : ↑(Set.Icc a b) → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)), Continuous L ∧ (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ (hs : s ∈ Set.Icc a b), ↑↑(L ⟨s, hs⟩) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => q (x, s)) ∧ ∀ (s t : ℝ) (hs : s ∈ Set.Icc a b) (ht : t ∈ Set.Icc a b), s ≤ t → ‖L ⟨t, ht⟩‖ ^ 2 - ‖L ⟨s, hs⟩‖ ^ 2 = 2 * c * ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab s t, p z * q' z

The kernel-limit theorem: a continuous L² curve representing the limit of the mollified fields, with the energy identity in time.