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 μ))
:
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.