Exact bounded-map compatibility for the actual continuous-path to Bochner L² inclusion.

theorem EulerTimeLp.pathLp_map {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) (A : E →L[ℝ] F) (f : C(↑(Set.Icc 0 T), E)) : (ContinuousLinearMap.compLpL 2 (timeMeasure T) A) (pathLp T hT f) = pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) A) f)

Applying a bounded spatial map commutes exactly with the genuine L² time embedding.

theorem EulerTimeLp.limit_restriction_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) (A : E →L[ℝ] F) (f : ℕ → C(↑(Set.Icc 0 T), E)) (g : C(↑(Set.Icc 0 T), F)) (U : ↥(TimeLp T E)) (hf : Filter.Tendsto (fun (n : ℕ) => pathLp T hT (f n)) Filter.atTop (nhds U)) (hg : Filter.Tendsto (fun (n : ℕ) => (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) A) (f n)) Filter.atTop (nhds g)) : (ContinuousLinearMap.compLpL 2 (timeMeasure T) A) U = pathLp T hT g

A strong Bochner limit is identified by the limit of any actual bounded spatial restriction.

theorem EulerTimeLp.limit_restriction_ae {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) (A : E →L[ℝ] F) (f : ℕ → C(↑(Set.Icc 0 T), E)) (g : C(↑(Set.Icc 0 T), F)) (U : ↥(TimeLp T E)) (hf : Filter.Tendsto (fun (n : ℕ) => pathLp T hT (f n)) Filter.atTop (nhds U)) (hg : Filter.Tendsto (fun (n : ℕ) => (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) A) (f n)) Filter.atTop (nhds g)) : (fun (t : ℝ) => A (↑↑U t)) =ᵐ[timeMeasure T] EulerVolterraConvolution.extendPath T hT g

The limiting restriction equality identifies genuine pointwise fields almost everywhere in time.