Theorems · Theorem · measure theory
AEMeasurable.add
∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Add M] {m : MeasurableSpace α} {f g : α → M}
{μ : MeasureTheory.Measure α} [MeasurableAdd₂ M], AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (f + g) μ- Defined in
- Mathlib.MeasureTheory.Group.Arithmetic
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 175 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- AEMeasurablestatement and proof · cited by 840
- MeasurableAdd₂statement and proof · cited by 155
- Measurable.comp_aemeasurableproof · cited by 99
- AEMeasurable.prodMkproof · cited by 54
- MeasurableAdd₂.measurable_addproof · cited by 8
Cited by8
Results whose statement or proof uses this declaration.
- ProbabilityTheory.variance_addproof · cited by 5
- AEMeasurable.fun_addproof · cited by 5
- ProbabilityTheory.IndepFun.hasLaw_addproof · cited by 3
- List.aemeasurable_sumproof · cited by 2
- AEMeasurable.add_iff_rightproof · cited by 1
- ProbabilityTheory.IndepFun.add_hasPDF'proof · cited by 1
- ENNReal.lintegral_rpow_add_le_add_eLpNorm_mul_lintegral_rpow_addproof · cited by 0
- AEMeasurable.add'proof · cited by 0