Theorems · Definition · probability
PMF.toMeasure
{α : Type u_1} → [inst : MeasurableSpace α] → PMF α → MeasureTheory.Measure αSince every set is Carathéodory-measurable under PMF.toOuterMeasure,
we can further extend this OuterMeasure to a Measure on α.
- Cited by
- 34 results in Mathlib
- Foundations
- Depth 170 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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 · cited by 10,939
- PMFstatement and proof · cited by 127
- PMF.toOuterMeasureproof · cited by 26
- MeasureTheory.OuterMeasure.toMeasureproof · cited by 11
Cited by34
Results whose statement or proof uses this declaration.
- PMF.toMeasure_apply_eq_toOuterMeasure_applystatement · cited by 15
- PMF.toMeasure_apply_singletonstatement · cited by 4
- PMF.toMeasure_apply_eq_toOuterMeasurestatement · cited by 3
- MeasureTheory.Measure.toPMF_toMeasurestatement · cited by 2
- PMF.restrict_toMeasure_supportstatement and proof · cited by 2
- PMF.toMeasure_injstatement · cited by 2
- PMF.integral_eq_sumstatement and proof · cited by 1
- PMF.toMeasure_applystatement · cited by 1
- PMF.toMeasure_apply_inter_supportstatement · cited by 1
- PMF.toMeasure_injectivestatement and proof · cited by 1
- PMF.toMeasure_map_applystatement and proof · cited by 1
- PMF.toMeasure_monostatement and proof · cited by 1