Theorems · Definition · probability
ProbabilityTheory.cond
{Ω : Type u_1} → {m : MeasurableSpace Ω} → MeasureTheory.Measure Ω → Set Ω → MeasureTheory.Measure ΩThe conditional probability measure of measure μ on set s is μ restricted to s
and scaled by the inverse of μ s (to make it a probability measure):
(μ s)⁻¹ • μ.restrict s.
- Cited by
- 43 results in Mathlib
- Foundations
- Depth 193 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- DFunLike.coeproof · cited by 62,936
- Setstatement and proof · cited by 53,352
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- MeasureTheory.Measure.restrictproof · cited by 1,646
Cited by46
Results whose statement or proof uses this declaration.
- ProbabilityTheory.uniformOnproof · cited by 27
- ProbabilityTheory.cond_applystatement · cited by 20
- MeasureTheory.pdf.IsUniformproof · cited by 14
- MeasureTheory.Measure.toFiniteproof · cited by 10
- ProbabilityTheory.cond_isProbabilityMeasure_of_finitestatement · cited by 3
- ProbabilityTheory.cond_mul_eq_interstatement · cited by 3
- MeasureTheory.pdf.IsUniform.pdf_eqproof · cited by 3
- Ergodic.of_mem_extremePoints_measure_univ_eqproof · cited by 2
- ProbabilityTheory.uniformOn_disjoint_unionproof · cited by 1
- ProbabilityTheory.cond_absolutelyContinuousstatement · cited by 1
- ProbabilityTheory.cond_apply'statement · cited by 1
- ProbabilityTheory.cond_cond_eq_cond_inter'statement and proof · cited by 1