L² convergence gives L¹ convergence on a finite measure space

Mathlib supplies the exponent comparison eLpNorm_le_eLpNorm_mul_rpow_measure_univ, which costs a fixed finite factor μ univ ^ (1/p - 1/q). Packaging it as a statement about convergence — and in the ∫ ‖·‖ form rather than the eLpNorm form — is what consumers usually want, and is not in Mathlib.

Both de Finetti proof routes need it: the mean-ergodic theorem and the L² block estimates each produce L² convergence, while the block factorizations consume L¹ convergence written as an integral of an absolute difference.

theorem TauCeti.MeasureTheory.tendsto_integral_norm_of_tendsto_eLpNorm_two {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {l : Filter ι} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : ι → Ω → E} (hf_meas : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) (h : Filter.Tendsto (fun (i : ι) => MeasureTheory.eLpNorm (f i) 2 μ) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => ∫ (ω : Ω), ‖f i ω‖ ∂μ) l (nhds 0)

L² convergence implies L¹ convergence on a finite measure space. If a family f tends to 0 in L² along a filter l, then ∫ ‖f i‖ tends to 0 along l.

The exponent comparison costs the fixed finite factor μ univ ^ (1/1 - 1/2), which the limit absorbs. Nothing in the argument constrains the index, the filter, or the codomain beyond having a norm, so all three are arbitrary; the usual difference form is the instance f i = W i - a.