Pointwise convergence of infinite sums in Lᵖ #
If a series in Lᵖ is converging in norm, then the series also converges pointwise
almost everywhere.
theorem
MeasureTheory.summable_norm_of_tsum_eLpNorm_ne_top
{X : Type u_1}
{E : Type u_2}
{x✝ : MeasurableSpace X}
{μ : Measure X}
[NormedAddCommGroup E]
{ι : Type u_3}
[Countable ι]
{p : ENNReal}
(hp : 1 ≤ p)
{f : ι → X → E}
(hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ)
(h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ⊤)
:
If a series of functions has summable L^p norms for some 1 ≤ p, then the norms are ae
pointwise summable.
theorem
MeasureTheory.Lp.hasSum_coeFn_tsum
{X : Type u_1}
{E : Type u_2}
{x✝ : MeasurableSpace X}
{μ : Measure X}
[NormedAddCommGroup E]
{p : ENNReal}
[hp : Fact (1 ≤ p)]
{ι : Type u_3}
[Countable ι]
[CompleteSpace E]
{f : ι → ↥(Lp E p μ)}
(hf : ∑' (n : ι), ‖f n‖ₑ ≠ ⊤)
:
If a series is converging in L^p, then it also converges pointwise almost everywhere.
theorem
MeasureTheory.Lp.coeFn_tsum
{X : Type u_1}
{E : Type u_2}
{x✝ : MeasurableSpace X}
{μ : Measure X}
[NormedAddCommGroup E]
{ι : Type u_3}
[Countable ι]
{p : ENNReal}
[hp : Fact (1 ≤ p)]
[CompleteSpace E]
{f : ι → ↥(Lp E p μ)}
(hf : ∑' (n : ι), ‖f n‖ₑ ≠ ⊤)
: