Theorems · Theorem · general topology

AEMeasurable.tsum

∀ {X : Type u_6} {E : Type u_7} {ι : Type u_8} [inst : MeasurableSpace X] [inst_1 : AddCommMonoid E]
  [inst_2 : TopologicalSpace E] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace E] [SecondCountableTopology E]
  [inst_5 : MeasurableSpace E] [BorelSpace E] [MeasurableAdd₂ E] [Countable ι] {L : SummationFilter ι} [L.NeBot]
  [L.filter.IsCountablyGenerated] {μ : MeasureTheory.Measure X} {f : ι → X → E},
  (∀ (i : ι), AEMeasurable (f i) μ) → AEMeasurable (fun x => ∑'[L] (i : ι), f i x) μ

The sum of almost everywhere measurable functions is measurable.

Defined in: Mathlib.MeasureTheory.Constructions.Polish.Basic
Cited by: 2 results in Mathlib
Foundations: Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace AddCommMonoid TopologicalSpace TopologicalSpace.IsCompletelyPseudoMetrizableSpace SecondCountableTopology MeasurableSpace BorelSpace MeasurableAdd₂ Countable SummationFilter.NeBot Filter.IsCountablyGenerated

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites24

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

TopologicalSpacestatement and proof · cited by 24,529
Finsetstatement · cited by 13,712
MeasurableSpacestatement and proof · cited by 13,106
AddCommMonoidstatement and proof · cited by 12,281
MeasureTheory.Measurestatement and proof · cited by 10,939
MeasureTheory.aeproof · cited by 2,352
Filter.EventuallyEqproof · cited by 1,912
Filter.univ_mem'proof · cited by 1,672
BorelSpacestatement and proof · cited by 1,602
Filter.mp_memproof · cited by 1,537
Measurableproof · cited by 1,499
tsumstatement and proof · cited by 1,148

Cited by2

Results whose statement or proof uses this declaration.

MeasureTheory.setToFun_tsumproof · cited by 3
MeasureTheory.summable_norm_of_tsum_eLpNorm_ne_topproof · cited by 0