ConditionalProbability

📁 Source: Mathlib/Probability/ConditionalProbability.lean

Statistics

Metric	Count
Definitions cond, condUnexpander, delabCondApplied, «term__[_|_In_]», «term__[_|_]», «term__[_|_←_]», «term__[|_In_]», «term__[|_]», «term__[|_←_]»	9
Theorems absolutelyContinuous_cond_univ, ae_cond_mem, ae_cond_mem₀, ae_cond_of_forall_mem, comap_cond, cond_absolutelyContinuous, cond_add_cond_compl_eq, cond_apply, cond_apply', cond_apply_self, cond_cond_eq_cond_inter, cond_cond_eq_cond_inter', cond_empty, cond_eq_inv_mul_cond_mul, cond_eq_zero, cond_eq_zero_of_meas_eq_zero, cond_inter_self, cond_isProbabilityMeasure, cond_isProbabilityMeasure_of_finite, cond_mul_eq_inter, cond_mul_eq_inter', cond_pos_of_inter_ne_zero, cond_toMeasurable_eq, cond_univ, instIsZeroOrProbabilityMeasureCond, inter_pos_of_cond_ne_zero, sum_meas_smul_cond_fiber	27
Total	36

ProbabilityTheory

Definitions

Name	Category	Theorems
cond 📖	CompOp	33 math math: cond_apply, sum_meas_smul_cond_fiber, cond_apply_self, cond_pos_of_inter_ne_zero, cond_isProbabilityMeasure_of_finite, cond_eq_zero_of_meas_eq_zero, comap_cond, ae_cond_mem, cond_inter_self, ae_cond_mem₀, condExp_set_generateFrom_singleton, cond_eq_inv_mul_cond_mul, condExp_generateFrom_singleton, iIndepFun.cond, condExpKernel_singleton_ae_eq_cond, cond_iInter, cond_isProbabilityMeasure, cond_add_cond_compl_eq, cond_toMeasurable_eq, cond_mul_eq_inter', cond_absolutelyContinuous, instIsZeroOrProbabilityMeasureCond, cond_cond_eq_cond_inter, absolutelyContinuous_cond_univ, cond_cond_eq_cond_inter', cond_eq_zero, cond_apply', ae_cond_of_forall_mem, cond_empty, cond_univ, cond_mul_eq_inter, MeasureTheory.pdf.IsUniform.cond, Kernel.iIndepFun.cond_iInter
condUnexpander 📖	CompOp	—
delabCondApplied 📖	CompOp	—
«term__[_|_In_]» 📖	CompOp	—
«term__[_|_]» 📖	CompOp	—
«term__[_|_←_]» 📖	CompOp	—
«term__[|_In_]» 📖	CompOp	—
«term__[|_]» 📖	CompOp	—
«term__[|_←_]» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absolutelyContinuous_cond_univ 📖	mathematical	—	MeasureTheory.Measure.AbsolutelyContinuous cond Set.univ	—	cond.eq_1 MeasureTheory.Measure.restrict_univ MeasureTheory.Measure.absolutelyContinuous_smul
ae_cond_mem 📖	mathematical	MeasurableSet	Filter.Eventually Set Set.instMembership MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass cond	—	MeasureTheory.Measure.ae_smul_measure MeasureTheory.ae_restrict_mem
ae_cond_mem₀ 📖	mathematical	MeasureTheory.NullMeasurableSet	Filter.Eventually Set Set.instMembership MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass cond	—	MeasureTheory.Measure.ae_smul_measure MeasureTheory.ae_restrict_mem₀
ae_cond_of_forall_mem 📖	mathematical	MeasurableSet	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass cond	—	MeasureTheory.Measure.ae_smul_measure MeasureTheory.ae_restrict_of_forall_mem
comap_cond 📖	mathematical	MeasurableEmbedding Filter.Eventually Set Set.instMembership Set.range MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasurableSet	MeasureTheory.Measure.comap cond Set.preimage	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.ext cond_apply MeasurableEmbedding.measurable MeasureTheory.Measure.comap_apply MeasurableEmbedding.injective MeasurableEmbedding.measurableSet_image' MeasurableSet.inter Set.image_inter Set.image_preimage_eq_inter_range Set.inter_right_comm MeasureTheory.measure_inter_conull
cond_absolutelyContinuous 📖	mathematical	—	MeasureTheory.Measure.AbsolutelyContinuous cond	—	MeasureTheory.Measure.AbsolutelyContinuous.trans IsScalarTower.right MeasureTheory.Measure.smul_absolutelyContinuous LE.le.absolutelyContinuous MeasureTheory.Measure.restrict_le_self
cond_add_cond_compl_eq 📖	mathematical	MeasurableSet	ENNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Distrib.toMul DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike cond Compl.compl Set.instCompl	—	cond_mul_eq_inter MeasurableSet.compl Set.inter_comm MeasureTheory.measure_inter_add_diff
cond_apply 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike cond Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instInv Set.instInter	—	cond.eq_1 MeasureTheory.Measure.smul_apply MeasureTheory.Measure.restrict_apply' Set.inter_comm smul_eq_mul
cond_apply' 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike cond Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instInv Set.instInter	—	cond.eq_1 MeasureTheory.Measure.smul_apply MeasureTheory.Measure.restrict_apply Set.inter_comm smul_eq_mul
cond_apply_self 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike cond AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	MeasureTheory.Measure.restrict_apply_self ENNReal.inv_mul_cancel
cond_cond_eq_cond_inter 📖	mathematical	MeasurableSet	cond Set Set.instInter	—	cond_cond_eq_cond_inter' MeasureTheory.measure_ne_top
cond_cond_eq_cond_inter' 📖	mathematical	MeasurableSet	cond Set Set.instInter	—	MeasureTheory.Measure.ext eq_or_ne MeasureTheory.measure_mono_null MeasureTheory.Measure.instOuterMeasureClass Set.inter_subset_left cond_apply MulZeroClass.mul_zero ENNReal.inv_zero LT.lt.ne' MeasureTheory.measure_pos_of_superset ENNReal.mul_inv inv_inv mul_comm ENNReal.inv_mul_cancel one_mul MeasurableSet.inter
cond_empty 📖	mathematical	—	cond Set Set.instEmptyCollection MeasureTheory.Measure MeasureTheory.Measure.instZero	—	MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass ENNReal.inv_zero MeasureTheory.Measure.restrict_empty smul_zero IsScalarTower.right
cond_eq_inv_mul_cond_mul 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike cond Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instInv	—	mul_assoc cond_mul_eq_inter Set.inter_comm cond_apply
cond_eq_zero 📖	mathematical	—	cond MeasureTheory.Measure MeasureTheory.Measure.instZero DFunLike.coe Set ENNReal MeasureTheory.Measure.instFunLike Top.top instTopENNReal instZeroENNReal	—	IsScalarTower.right
cond_eq_zero_of_meas_eq_zero 📖	mathematical	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike instZeroENNReal	cond MeasureTheory.Measure.instZero	—	—
cond_inter_self 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike cond Set.instInter	—	cond_apply Set.inter_assoc Set.inter_self
cond_isProbabilityMeasure 📖	mathematical	—	MeasureTheory.IsProbabilityMeasure cond	—	cond_isProbabilityMeasure_of_finite MeasureTheory.measure_ne_top
cond_isProbabilityMeasure_of_finite 📖	mathematical	—	MeasureTheory.IsProbabilityMeasure cond	—	MeasureTheory.Measure.restrict_apply Set.univ_inter ENNReal.inv_mul_cancel
cond_mul_eq_inter 📖	mathematical	MeasurableSet	ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike cond Set.instInter	—	cond_mul_eq_inter' MeasureTheory.measure_ne_top
cond_mul_eq_inter' 📖	mathematical	MeasurableSet	ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike cond Set.instInter	—	eq_or_ne MulZeroClass.mul_zero MeasureTheory.measure_inter_null_of_null_left cond_apply mul_comm mul_assoc ENNReal.mul_inv_cancel one_mul
cond_pos_of_inter_ne_zero 📖	mathematical	MeasurableSet	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike cond	—	cond_apply ENNReal.mul_pos ENNReal.inv_ne_zero MeasureTheory.measure_ne_top
cond_toMeasurable_eq 📖	mathematical	—	cond MeasureTheory.toMeasurable	—	MeasureTheory.measure_toMeasurable ENNReal.inv_top zero_smul IsScalarTower.right MeasureTheory.Measure.restrict_toMeasurable
cond_univ 📖	mathematical	—	cond Set.univ	—	MeasureTheory.IsProbabilityMeasure.measure_univ inv_one MeasureTheory.Measure.restrict_univ one_smul IsScalarTower.right
instIsZeroOrProbabilityMeasureCond 📖	mathematical	—	MeasureTheory.IsZeroOrProbabilityMeasure cond	—	MeasureTheory.Measure.restrict_apply Set.univ_inter eq_or_ne ENNReal.zero_div NeZero.charZero_one ENNReal.instCharZero ENNReal.div_top ENNReal.div_self
inter_pos_of_cond_ne_zero 📖	mathematical	MeasurableSet	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Set.instInter	—	pos_iff_ne_zero ENNReal.instCanonicallyOrderedAdd right_ne_zero_of_mul MeasureTheory.Measure.restrict_apply' Set.inter_comm
sum_meas_smul_cond_fiber 📖	mathematical	Measurable	Finset.sum MeasureTheory.Measure MeasureTheory.Measure.instAddCommMonoid Finset.univ ENNReal MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right DFunLike.coe Set MeasureTheory.Measure.instFunLike Set.preimage Set.instSingletonSet cond	—	MeasureTheory.Measure.ext IsScalarTower.right MeasureTheory.Measure.coe_finset_sum Finset.sum_congr Finset.sum_apply mul_comm cond_mul_eq_inter MeasurableSet.singleton DiscreteMeasurableSpace.toMeasurableSingletonClass Set.ext Set.iUnion_congr_Prop Set.iUnion_true MeasureTheory.measure_biUnion_finset Finset.coe_univ MeasurableSet.inter

---

← Back to Index