Lᵖ convergence implies L¹ convergence on a finite measure space #
On a finite measure space the Lᵖ seminorm dominates the L¹ seminorm up to the factor
μ(univ)^(1 - 1/p), so a sequence converging in Lᵖ converges in L¹. Stated with the L¹
distance written as a lower Lebesgue integral, which is the form consumed by arguments that pass
an integral identity to a limit.
Main declarations #
TauCeti.tendsto_lintegral_enorm_sub_of_tendsto_Lp:Lᵖconvergence gives∫⁻ ‖f i - g‖ₑ → 0.
theorem
TauCeti.tendsto_lintegral_enorm_sub_of_tendsto_Lp
{α : Type u_1}
{G : Type u_2}
{ι : Type u_3}
[MeasurableSpace α]
{ν : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure ν]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{q : ENNReal}
[Fact (1 ≤ q)]
{l : Filter ι}
{f : ι → ↥(MeasureTheory.Lp G q ν)}
{g : ↥(MeasureTheory.Lp G q ν)}
(h : Filter.Tendsto f l (nhds g))
:
On a finite measure space, Lᵖ convergence implies L¹ convergence.