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} (h'f : ∑' (n : ι), eLpNorm (f n) p μ ≠ ⊤) : ∀ᵐ (a : X) ∂μ, Summable fun (n : ι) => ‖f n a‖

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‖ₑ ≠ ⊤) : ∀ᵐ (a : X) ∂μ, HasSum (fun (n : ι) => ↑↑(f n) a) (↑↑(∑' (n : ι), f n) a)

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‖ₑ ≠ ⊤) : ↑↑(∑' (n : ι), f n) =ᵐ[μ] fun (x : X) => ∑' (n : ι), ↑↑(f n) x