Dominated convergence in genuine L², also for Banach-valued representatives.

theorem EulerLpConvergence.norm_sq_eq_integral {X : Type u_1} {V : Type u_2} [MeasurableSpace X] [NormedAddCommGroup V] (μ : MeasureTheory.Measure X) (u : ↥(MeasureTheory.Lp V 2 μ)) : ‖u‖ ^ 2 = ∫ (x : X), ‖↑↑u x‖ ^ 2 ∂μ

theorem EulerLpConvergence.tendsto_of_dominated {X : Type u_1} {V : Type u_2} [MeasurableSpace X] [NormedAddCommGroup V] (μ : MeasureTheory.Measure X) {ι : Type u_3} {l : Filter ι} [l.IsCountablyGenerated] (U : ι → ↥(MeasureTheory.Lp V 2 μ)) (v : ↥(MeasureTheory.Lp V 2 μ)) (F : ι → X → V) (g : X → V) (hU : ∀ (i : ι), ↑↑(U i) =ᵐ[μ] F i) (hv : ↑↑v =ᵐ[μ] g) (M : X → ℝ) (hM : MeasureTheory.MemLp M 2 μ) (hbound : ∀ᶠ (i : ι) in l, ∀ᵐ (x : X) ∂μ, ‖F i x - g x‖ ≤ M x) (hlim : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (i : ι) => F i x) l (nhds (g x))) : Filter.Tendsto U l (nhds v)

Domination of literal representatives controls convergence of their actual L² classes.