Theorems · Theorem · measure theory

MeasureTheory.Lp.hasSum_coeFn_tsum

∀ {X : Type u_1} {E : Type u_2} {x : MeasurableSpace X} {μ : MeasureTheory.Measure X} [inst : NormedAddCommGroup E]
  {p : ENNReal} [hp : Fact (1 ≤ p)] {ι : Type u_3} [Countable ι] [CompleteSpace E] {f : ι → ↥(MeasureTheory.Lp E p μ)},
  ∑' (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.

Defined in

Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum

Cited by

1 results in Mathlib

Foundations

Depth 237 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupFactCountableCompleteSpace