UniformOn

📁 Source: Mathlib/Probability/UniformOn.lean

Statistics

Metric	Count
Definitions uniformOn	1
Theorems finite_of_uniformOn_ne_zero, instIsProbabilityMeasure_uniformOn_univ, instIsZeroOrProbabilityMeasureUniformOn, isProbabilityMeasure_uniformOn, isProbabilityMeasure_uniformOn', pred_true_of_uniformOn_eq_one, uniformOn_add_compl_eq, uniformOn_compl, uniformOn_disjoint_union, uniformOn_empty, uniformOn_empty_meas, uniformOn_eq_one_of, uniformOn_eq_zero, uniformOn_eq_zero', uniformOn_eq_zero_iff, uniformOn_inter, uniformOn_inter', uniformOn_inter_self, uniformOn_isProbabilityMeasure, uniformOn_of_univ, uniformOn_self, uniformOn_singleton, uniformOn_union, uniformOn_univ	24
Total	25

ProbabilityTheory

Definitions

Name	Category	Theorems
uniformOn 📖	CompOp	24 math math: uniformOn_inter, uniformOn_of_univ, uniformOn_empty, uniformOn_eq_zero, isProbabilityMeasure_uniformOn, uniformOn_empty_meas, uniformOn_eq_zero_iff, isProbabilityMeasure_uniformOn', uniformOn_eq_one_of, uniformOn_self, instIsZeroOrProbabilityMeasureUniformOn, essSup_uniformOn_eq_ciSup, uniformOn_add_compl_eq, uniformOn_inter_self, uniformOn_univ, uniformOn_inter', uniformOn_union, instIsProbabilityMeasure_uniformOn_univ, uniformOn_compl, essInf_cond_count_eq_ciInf, uniformOn_singleton, uniformOn_disjoint_union, uniformOn_isProbabilityMeasure, uniformOn_eq_zero'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_of_uniformOn_ne_zero 📖	mathematical	—	Set.Finite	—	MeasureTheory.Measure.count_apply_infinite ENNReal.inv_top zero_smul IsScalarTower.right
instIsProbabilityMeasure_uniformOn_univ 📖	mathematical	—	MeasureTheory.IsProbabilityMeasure uniformOn Set.univ	—	isProbabilityMeasure_uniformOn' Set.finite_univ Set.univ_nonempty MeasurableSet.univ
instIsZeroOrProbabilityMeasureUniformOn 📖	mathematical	—	MeasureTheory.IsZeroOrProbabilityMeasure uniformOn	—	instIsZeroOrProbabilityMeasureCond
isProbabilityMeasure_uniformOn 📖	mathematical	Set.Nonempty	MeasureTheory.IsProbabilityMeasure uniformOn	—	cond_isProbabilityMeasure_of_finite MeasureTheory.Measure.count_ne_zero_iff LT.lt.ne MeasureTheory.Measure.count_apply_lt_top
isProbabilityMeasure_uniformOn' 📖	mathematical	Set.Nonempty MeasurableSet	MeasureTheory.IsProbabilityMeasure uniformOn	—	cond_isProbabilityMeasure_of_finite MeasureTheory.Measure.count_ne_zero_iff LT.lt.ne MeasureTheory.Measure.count_apply_lt_top'
pred_true_of_uniformOn_eq_one 📖	mathematical	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike uniformOn AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	Set.instHasSubset	—	finite_of_uniformOn_ne_zero one_ne_zero NeZero.charZero_one ENNReal.instCharZero ENNReal.eq_inv_of_mul_eq_one_left mul_comm cond_apply Set.Finite.measurableSet uniformOn.eq_1 Set.Finite.inter_of_left Finset.eq_of_subset_of_card_le Set.Finite.toFinset_mono Set.inter_subset_left Eq.ge MeasureTheory.Measure.count_apply_finite inv_inv
uniformOn_add_compl_eq 📖	mathematical	—	ENNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Distrib.toMul DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike uniformOn Set.instInter Compl.compl Set.instCompl	—	Set.inter_union_compl uniformOn_disjoint_union Set.Finite.inter_of_left Disjoint.mono inf_le_right disjoint_compl_right uniformOn_inter_self
uniformOn_compl 📖	mathematical	Set.Nonempty	ENNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike uniformOn Compl.compl Set.instCompl AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	uniformOn_union disjoint_compl_right Set.union_compl_self MeasureTheory.IsProbabilityMeasure.measure_univ isProbabilityMeasure_uniformOn
uniformOn_disjoint_union 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	ENNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Distrib.toMul DFunLike.coe MeasureTheory.Measure MeasureTheory.Measure.instFunLike uniformOn Set.instUnion	—	Set.eq_empty_or_nonempty uniformOn_empty_meas Set.union_self MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass MulZeroClass.mul_zero add_zero Set.empty_union uniformOn_self mul_one zero_add Set.union_empty uniformOn.eq_1 cond_apply Set.Finite.measurableSet Set.Finite.union Set.union_inter_cancel_left Set.union_inter_cancel_right mul_comm mul_assoc ENNReal.mul_inv_cancel MeasureTheory.Measure.count_ne_zero LT.lt.ne MeasureTheory.Measure.count_apply_lt_top one_mul add_mul Distrib.rightDistribClass MeasureTheory.measure_union Disjoint.mono inf_le_left Set.Finite.inter_of_left Set.union_inter_distrib_right
uniformOn_empty 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike uniformOn Set.instEmptyCollection instZeroENNReal	—	MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass
uniformOn_empty_meas 📖	mathematical	—	uniformOn Set Set.instEmptyCollection MeasureTheory.Measure MeasureTheory.Measure.instZero	—	cond_empty
uniformOn_eq_one_of 📖	mathematical	Set.Nonempty Set Set.instHasSubset	DFunLike.coe MeasureTheory.Measure ENNReal MeasureTheory.Measure.instFunLike uniformOn AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	eq_of_le_of_not_lt MeasureTheory.prob_le_one instIsZeroOrProbabilityMeasureUniformOn not_lt uniformOn_self MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass
uniformOn_eq_zero 📖	mathematical	—	uniformOn MeasureTheory.Measure MeasureTheory.Measure.instZero Set.Infinite Set Set.instEmptyCollection	—	—
uniformOn_eq_zero' 📖	mathematical	MeasurableSet	uniformOn MeasureTheory.Measure MeasureTheory.Measure.instZero Set.Infinite Set Set.instEmptyCollection	—	—
uniformOn_eq_zero_iff 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike uniformOn instZeroENNReal Set.instInter Set.instEmptyCollection	—	Set.Finite.inter_of_left cond_apply Set.Finite.measurableSet MeasureTheory.Measure.count_apply_finite ENNReal.instNoZeroDivisors Set.not_infinite ENNReal.instCharZero
uniformOn_inter 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike uniformOn Set.instInter Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	uniformOn_empty_meas MeasureTheory.Measure.coe_zero Pi.zero_apply MulZeroClass.zero_mul uniformOn_eq_zero_iff Set.inter_assoc Set.empty_inter uniformOn.eq_1 cond_apply Set.Finite.measurableSet Set.Finite.inter_of_left mul_comm mul_assoc ENNReal.mul_inv_cancel MeasureTheory.Measure.count_eq_zero_iff LT.lt.ne MeasureTheory.Measure.count_apply_lt_top one_mul
uniformOn_inter' 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike uniformOn Set.instInter Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	Set.inter_comm uniformOn_inter
uniformOn_inter_self 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike uniformOn Set.instInter	—	uniformOn.eq_1 cond_inter_self Set.Finite.measurableSet
uniformOn_isProbabilityMeasure 📖	mathematical	Set.Nonempty	MeasureTheory.IsProbabilityMeasure uniformOn	—	isProbabilityMeasure_uniformOn
uniformOn_of_univ 📖	mathematical	Set.Nonempty	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike uniformOn Set.univ AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	uniformOn_eq_one_of Set.subset_univ
uniformOn_self 📖	mathematical	Set.Nonempty	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike uniformOn AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	uniformOn.eq_1 cond_apply Set.Finite.measurableSet Set.inter_self ENNReal.inv_mul_cancel MeasureTheory.Measure.count_ne_zero_iff LT.lt.ne MeasureTheory.Measure.count_apply_lt_top
uniformOn_singleton 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike uniformOn Set.instSingletonSet Set.instMembership AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal instZeroENNReal	—	uniformOn.eq_1 cond_apply MeasurableSingletonClass.measurableSet_singleton MeasureTheory.Measure.count_singleton inv_one one_mul
uniformOn_union 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	DFunLike.coe MeasureTheory.Measure ENNReal MeasureTheory.Measure.instFunLike uniformOn Set.instUnion Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	uniformOn.eq_1 cond_apply Set.Finite.measurableSet Set.inter_union_distrib_left MeasureTheory.measure_union Disjoint.mono inf_le_right Set.Finite.inter_of_left mul_add Distrib.leftDistribClass
uniformOn_univ 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike uniformOn Set.univ DivInvMonoid.toDiv ENNReal.instDivInvMonoid MeasureTheory.Measure.count AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Fintype.card	—	cond_apply MeasureTheory.Measure.count_univ ENat.card_eq_coe_fintype_card Set.univ_inter

---

← Back to Index