Theorems · Inductive type · measure theory
MeasureTheory.IsZeroOrProbabilityMeasure
{α : Type u_1} → {m0 : MeasurableSpace α} → MeasureTheory.Measure α → PropA measure μ is zero or a probability measure if μ univ = 0 or μ univ = 1. This class
of measures appears naturally when conditioning on events, and many results which are true for
probability measures hold more generally over this class.
- Cited by
- 46 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement · cited by 13,106
- MeasureTheory.Measurestatement · cited by 10,939
Cited by48
Results whose statement or proof uses this declaration.
- MeasureTheory.prob_le_onestatement and proof · cited by 11
- MeasureTheory.eq_zero_or_isProbabilityMeasurestatement and proof · cited by 6
- ProbabilityTheory.IndepFun.indepFun_process₀statement and proof · cited by 4
- MeasureTheory.IsZeroOrProbabilityMeasure.measure_univstatement and proof · cited by 4
- ProbabilityTheory.IndepFun.process_indepFun_process₀statement and proof · cited by 3
- ProbabilityTheory.IndepFun.process_indepFun₀statement and proof · cited by 2
- ProbabilityTheory.HasSubgaussianMGF.sum_of_hasCondSubgaussianMGFstatement and proof · cited by 2
- ProbabilityTheory.cgf_zerostatement and proof · cited by 1
- ProbabilityTheory.exists_cgf_eq_iteratedDeriv_two_cgf_mulstatement and proof · cited by 1
- MeasureTheory.measureReal_le_onestatement and proof · cited by 1
- ProbabilityTheory.HasSubgaussianMGF.fun_zerostatement and proof · cited by 1
- ProbabilityTheory.indepSet_iff_indepSets_singletonstatement and proof · cited by 1