Genuine strong operator approximation on Bochner L² time spaces.

theorem EulerTimeLp.strong_operator_timeLp_tendsto {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (T : ℝ) (A : ℕ → E →L[ℝ] E) (M : ℝ) (hA : ∀ (n : ℕ) (x : E), ‖(A n) x‖ ≤ M * ‖x‖) (hlim : ∀ (x : E), Filter.Tendsto (fun (n : ℕ) => (A n) x) Filter.atTop (nhds x)) (u : ↥(TimeLp T E)) : Filter.Tendsto (fun (n : ℕ) => (ContinuousLinearMap.compLpL 2 (timeMeasure T) (A n)) u) Filter.atTop (nhds u)

Uniformly bounded strong operator approximation converges on every actual Bochner L² time field.