Basic

📁 Source: Mathlib/Probability/ProbabilityMassFunction/Basic.lean

Statistics

Metric	Count
Definitions `toPMF`, `PMF`, `instFunLike`, `support`, `toMeasure`, `toOuterMeasure`	6
Theorems `toPMF_apply`, `toPMF_toMeasure`, `apply_eq_one_iff`, `apply_eq_zero_iff`, `apply_lt_top`, `apply_ne_top`, `apply_pos_iff`, `coe_le_one`, `coe_ne_zero`, `ext`, `ext_iff`, `hasSum_coe_one`, `mem_support_iff`, `restrict_toMeasure_support`, `support_countable`, `support_nonempty`, `isProbabilityMeasure`, `toMeasure_apply`, `toMeasure_apply_eq_of_inter_support_eq`, `toMeasure_apply_eq_one_iff`, `toMeasure_apply_eq_toOuterMeasure`, `toMeasure_apply_eq_toOuterMeasure_apply`, `toMeasure_apply_eq_tsum`, `toMeasure_apply_eq_zero_iff`, `toMeasure_apply_finset`, `toMeasure_apply_fintype`, `toMeasure_apply_inter_support`, `toMeasure_apply_singleton`, `toMeasure_eq_iff_eq_toPMF`, `toMeasure_inj`, `toMeasure_injective`, `toMeasure_mono`, `toMeasure_toPMF`, `toOuterMeasure_apply`, `toOuterMeasure_apply_eq_of_inter_support_eq`, `toOuterMeasure_apply_eq_one_iff`, `toOuterMeasure_apply_eq_zero_iff`, `toOuterMeasure_apply_finset`, `toOuterMeasure_apply_fintype`, `toOuterMeasure_apply_inter_support`, `toOuterMeasure_apply_le_toMeasure_apply`, `toOuterMeasure_apply_singleton`, `toOuterMeasure_caratheodory`, `toOuterMeasure_inj`, `toOuterMeasure_injective`, `toOuterMeasure_mono`, `toPMF_eq_iff_toMeasure_eq`, `tsum_coe`, `tsum_coe_indicator_ne_top`, `tsum_coe_ne_top`	50
Total	56

MeasureTheory.Measure

Definitions

Name	Category	Theorems
`toPMF` 📖	CompOp	6 math math: `PMF.toMeasure_toPMF`, `PMF.toPMF_dirac`, `PMF.toPMF_eq_iff_toMeasure_eq`, `toPMF_toMeasure`, `PMF.toMeasure_eq_iff_eq_toPMF`, `toPMF_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toPMF_apply` 📖	mathematical	—	`DFunLike.coe` `PMF` `ENNReal` `PMF.instFunLike` `toPMF` `MeasureTheory.Measure` `Set` `instFunLike` `Set.instSingletonSet`	—	—
`toPMF_toMeasure` 📖	mathematical	—	`PMF.toMeasure` `toPMF`	—	`ext` `PMF.toMeasure_apply` `tsum_indicator_apply_singleton`

PMF

Definitions

Name	Category	Theorems
`instFunLike` 📖	CompOp	50 math math: `tsum_coe`, `toMeasure_bind_apply`, `binomial_apply_zero`, `toMeasure_apply_singleton`, `toMeasure_apply`, `uniformOfFinset_apply_of_mem`, `ext_iff`, `toOuterMeasure_apply_singleton`, `ofFinset_apply`, `uniformOfFintype_apply`, `filter_apply_eq_zero_iff`, `integral_eq_tsum`, `seq_apply`, `pure_apply_of_ne`, `apply_lt_top`, `coe_le_one`, `toOuterMeasure_bindOnSupport_apply`, `apply_eq_zero_iff`, `binomial_apply`, `uniformOfFinset_apply_of_notMem`, `binomial_apply_self`, `apply_eq_one_iff`, `integral_eq_sum`, `apply_pos_iff`, `bernoulli_apply`, `bindOnSupport_eq_zero_iff`, `hasSum_coe_one`, `toMeasure_bindOnSupport_apply`, `uniformOfFinset_apply`, `toOuterMeasure_apply`, `filter_apply`, `toOuterMeasure_apply_finset`, `pure_apply_self`, `bind_apply`, `ofFintype_apply`, `map_apply`, `toOuterMeasure_bind_apply`, `bindOnSupport_apply`, `pure_apply`, `filter_apply_eq_zero_of_notMem`, `binomial_apply_last`, `ofMultiset_apply_of_notMem`, `toMeasure_apply_fintype`, `ofMultiset_apply`, `ofFinset_apply_of_notMem`, `toOuterMeasure_apply_fintype`, `toMeasure_apply_eq_tsum`, `toMeasure_apply_finset`, `MeasureTheory.Measure.toPMF_apply`, `normalize_apply`
`support` 📖	CompOp	39 math math: `mem_support_bindOnSupport_iff`, `mem_support_map_iff`, `support_bernoulli`, `mem_support_seq_iff`, `support_nonempty`, `mem_support_ofFinset_iff`, `support_pure`, `mem_support_ofMultiset_iff`, `pure_bindOnSupport`, `mem_support_normalize_iff`, `support_map`, `support_ofFintype`, `support_bind`, `support_ofMultiset`, `mem_support_bind_iff`, `support_normalize`, `support_countable`, `apply_eq_zero_iff`, `support_ofFinset`, `support_bindOnSupport`, `support_uniformOfFinset`, `mem_support_iff`, `toOuterMeasure_apply_inter_support`, `apply_eq_one_iff`, `toMeasure_apply_eq_one_iff`, `mem_support_ofFintype_iff`, `apply_pos_iff`, `bindOnSupport_bindOnSupport`, `mem_support_pure_iff`, `mem_support_bernoulli_iff`, `toOuterMeasure_apply_eq_zero_iff`, `toMeasure_apply_inter_support`, `support_seq`, `mem_support_uniformOfFintype`, `toOuterMeasure_apply_eq_one_iff`, `restrict_toMeasure_support`, `support_uniformOfFintype`, `mem_support_uniformOfFinset_iff`, `toMeasure_apply_eq_zero_iff`
`toMeasure` 📖	CompOp	34 math math: `toMeasure_pure_apply`, `toMeasure_bind_apply`, `toMeasure_toPMF`, `toMeasure_ofFinset_apply`, `bernoulli_expectation`, `toMeasure_apply_singleton`, `toMeasure_ofFintype_apply`, `toMeasure_apply`, `toMeasure_ofMultiset_apply`, `toMeasure_apply_eq_toOuterMeasure_apply`, `toOuterMeasure_apply_le_toMeasure_apply`, `toPMF_eq_iff_toMeasure_eq`, `toMeasure_map`, `toMeasure_uniformOfFintype_apply`, `toMeasure_pure`, `integral_eq_sum`, `toMeasure_apply_eq_one_iff`, `MeasureTheory.Measure.toPMF_toMeasure`, `toMeasure_apply_eq_of_inter_support_eq`, `toMeasure_injective`, `toMeasure.isProbabilityMeasure`, `toMeasure_bindOnSupport_apply`, `toMeasure_apply_inter_support`, `restrict_toMeasure_support`, `toMeasure_apply_eq_toOuterMeasure`, `toMeasure_mono`, `toMeasure_eq_iff_eq_toPMF`, `toMeasure_uniformOfFinset_apply`, `toMeasure_apply_eq_zero_iff`, `toMeasure_apply_fintype`, `toMeasure_inj`, `toMeasure_map_apply`, `toMeasure_apply_eq_tsum`, `toMeasure_apply_finset`
`toOuterMeasure` 📖	CompOp	24 math math: `toOuterMeasure_mono`, `toOuterMeasure_pure_apply`, `toOuterMeasure_injective`, `toOuterMeasure_ofFinset_apply`, `toOuterMeasure_apply_eq_of_inter_support_eq`, `toOuterMeasure_caratheodory`, `toOuterMeasure_inj`, `toMeasure_apply_eq_toOuterMeasure_apply`, `toOuterMeasure_apply_le_toMeasure_apply`, `toOuterMeasure_apply_singleton`, `toOuterMeasure_ofMultiset_apply`, `toOuterMeasure_ofFintype_apply`, `toOuterMeasure_uniformOfFinset_apply`, `toOuterMeasure_bindOnSupport_apply`, `toOuterMeasure_apply_inter_support`, `toOuterMeasure_map_apply`, `toOuterMeasure_apply`, `toOuterMeasure_apply_eq_zero_iff`, `toOuterMeasure_apply_finset`, `toOuterMeasure_apply_eq_one_iff`, `toOuterMeasure_uniformOfFintype_apply`, `toOuterMeasure_bind_apply`, `toMeasure_apply_eq_toOuterMeasure`, `toOuterMeasure_apply_fintype`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_eq_one_iff` 📖	mathematical	—	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `support` `Set` `Set.instSingletonSet`	—	`Set.Subset.antisymm` `by_contra` `pos_iff_ne_zero` `ENNReal.instCanonicallyOrderedAdd` `Summable.tsum_ne_zero_iff` `ENNReal.instIsOrderedAddMonoid` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `ENNReal.summable` `ite_ne_left_iff` `mem_support_iff` `add_zero` `ENNReal.add_lt_add_of_le_of_lt` `ENNReal.one_ne_top` `le_of_eq` `symm` `IsEquiv.toSymm` `eq_isEquiv` `tsum_eq_single` `SummationFilter.instLeAtTopUnconditional` `ENNReal.tsum_add` `tsum_congr` `zero_add` `ne_of_lt` `tsum_coe` `zero_ne_one` `NeZero.one` `trans` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `apply_eq_zero_iff`
`apply_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `instZeroENNReal` `Set` `Set.instMembership` `support`	—	`mem_support_iff`
`apply_lt_top` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `PMF` `instFunLike` `Top.top` `instTopENNReal`	—	`lt_of_le_of_ne` `le_top` `apply_ne_top`
`apply_ne_top` 📖	—	—	—	—	`ne_of_lt` `lt_of_le_of_lt` `coe_le_one` `ENNReal.one_lt_top`
`apply_pos_iff` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `PMF` `instFunLike` `Set` `Set.instMembership` `support`	—	`pos_iff_ne_zero` `ENNReal.instCanonicallyOrderedAdd` `mem_support_iff`
`coe_le_one` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `PMF` `instFunLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`hasSum_le` `ENNReal.instIsOrderedAddMonoid` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `ENNReal.instCanonicallyOrderedAdd` `hasSum_ite_eq` `SummationFilter.instLeAtTopUnconditional` `hasSum_coe_one` `SummationFilter.instNeBotUnconditional`
`coe_ne_zero` 📖	—	—	—	—	`zero_ne_one` `NeZero.one` `tsum_zero` `tsum_congr` `symm` `IsEquiv.toSymm` `eq_isEquiv` `tsum_coe`
`ext` 📖	—	`DFunLike.coe` `PMF` `ENNReal` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `PMF` `ENNReal` `instFunLike`	—	`ext`
`hasSum_coe_one` 📖	mathematical	—	`HasSum` `ENNReal` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `DFunLike.coe` `PMF` `instFunLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `SummationFilter.unconditional`	—	—
`mem_support_iff` 📖	mathematical	—	`Set` `Set.instMembership` `support`	—	—
`restrict_toMeasure_support` 📖	mathematical	—	`MeasureTheory.Measure.restrict` `toMeasure` `support`	—	`MeasureTheory.Measure.ext` `MeasureTheory.Measure.restrict_apply` `toMeasure_apply_inter_support`
`support_countable` 📖	mathematical	—	`Set.Countable` `support`	—	`Summable.countable_support_ennreal` `tsum_coe_ne_top`
`support_nonempty` 📖	mathematical	—	`Set.Nonempty` `support`	—	`Function.support_nonempty_iff` `coe_ne_zero`
`toMeasure_apply` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Set.indicator` `instZeroENNReal` `PMF` `instFunLike` `SummationFilter.unconditional`	—	`toMeasure_apply_eq_toOuterMeasure_apply` `toOuterMeasure_apply`
`toMeasure_apply_eq_of_inter_support_eq` 📖	mathematical	`MeasurableSet` `Set` `Set.instInter` `support`	`DFunLike.coe` `MeasureTheory.Measure` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure`	—	`toMeasure_apply_eq_toOuterMeasure_apply` `toOuterMeasure_apply_eq_of_inter_support_eq`
`toMeasure_apply_eq_one_iff` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Set.instHasSubset` `support`	—	`toOuterMeasure_apply_eq_one_iff` `toMeasure_apply_eq_toOuterMeasure_apply`
`toMeasure_apply_eq_toOuterMeasure` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure` `MeasureTheory.OuterMeasure` `MeasureTheory.OuterMeasure.instFunLikeSetENNReal` `toOuterMeasure`	—	`Set.Countable.measurableSet` `Set.Countable.mono` `Set.inter_subset_right` `support_countable` `restrict_toMeasure_support` `MeasureTheory.Measure.restrict_apply'` `toMeasure_apply_eq_toOuterMeasure_apply` `toOuterMeasure_apply_inter_support`
`toMeasure_apply_eq_toOuterMeasure_apply` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure` `MeasureTheory.OuterMeasure` `MeasureTheory.OuterMeasure.instFunLikeSetENNReal` `toOuterMeasure`	—	`MeasureTheory.toMeasure_apply`
`toMeasure_apply_eq_tsum` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Set.indicator` `instZeroENNReal` `PMF` `instFunLike` `SummationFilter.unconditional`	—	`toMeasure_apply_eq_toOuterMeasure` `toOuterMeasure_apply`
`toMeasure_apply_eq_zero_iff` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure` `instZeroENNReal` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `support`	—	`toMeasure_apply_eq_toOuterMeasure_apply` `toOuterMeasure_apply_eq_zero_iff`
`toMeasure_apply_finset` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.sum` `ENNReal.instAddCommMonoid` `PMF` `instFunLike`	—	`toMeasure_apply_eq_toOuterMeasure` `toOuterMeasure_apply_finset`
`toMeasure_apply_fintype` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure` `Finset.sum` `ENNReal.instAddCommMonoid` `Finset.univ` `Set.indicator` `instZeroENNReal` `PMF` `instFunLike`	—	`toMeasure_apply_eq_toOuterMeasure` `toOuterMeasure_apply_fintype`
`toMeasure_apply_inter_support` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure` `Set.instInter` `support`	—	`LE.le.antisymm` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Set.inter_subset_left` `toMeasure_mono` `refl` `Set.instReflSubset`
`toMeasure_apply_singleton` 📖	mathematical	`MeasurableSet` `Set` `Set.instSingletonSet`	`DFunLike.coe` `MeasureTheory.Measure` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure` `PMF` `instFunLike`	—	`toMeasure_apply_eq_toOuterMeasure_apply` `toOuterMeasure_apply_singleton`
`toMeasure_eq_iff_eq_toPMF` 📖	mathematical	—	`toMeasure` `MeasureTheory.Measure.toPMF`	—	`MeasureTheory.Measure.toPMF_toMeasure`
`toMeasure_inj` 📖	mathematical	—	`toMeasure`	—	`toMeasure_injective`
`toMeasure_injective` 📖	mathematical	—	`PMF` `MeasureTheory.Measure` `toMeasure`	—	`ext` `toMeasure_apply_singleton` `MeasurableSingletonClass.measurableSet_singleton`
`toMeasure_mono` 📖	mathematical	`MeasurableSet` `Set` `Set.instHasSubset` `Set.instInter` `support`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `toMeasure`	—	`toMeasure_apply_eq_toOuterMeasure_apply` `LE.le.trans` `toOuterMeasure_mono` `toOuterMeasure_apply_le_toMeasure_apply`
`toMeasure_toPMF` 📖	mathematical	—	`MeasureTheory.Measure.toPMF` `toMeasure` `toMeasure.isProbabilityMeasure`	—	`ext` `toMeasure.isProbabilityMeasure` `toMeasure_apply_singleton` `MeasurableSingletonClass.measurableSet_singleton` `MeasureTheory.Measure.toPMF_apply`
`toOuterMeasure_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `MeasureTheory.OuterMeasure.instFunLikeSetENNReal` `toOuterMeasure` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Set.indicator` `instZeroENNReal` `PMF` `instFunLike` `SummationFilter.unconditional`	—	`tsum_congr` `MeasureTheory.OuterMeasure.smul_dirac_apply`
`toOuterMeasure_apply_eq_of_inter_support_eq` 📖	mathematical	`Set` `Set.instInter` `support`	`DFunLike.coe` `MeasureTheory.OuterMeasure` `ENNReal` `MeasureTheory.OuterMeasure.instFunLikeSetENNReal` `toOuterMeasure`	—	`le_antisymm` `toOuterMeasure_mono` `Set.inter_subset_left`
`toOuterMeasure_apply_eq_one_iff` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `MeasureTheory.OuterMeasure.instFunLikeSetENNReal` `toOuterMeasure` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Set.instHasSubset` `support`	—	`by_contra` `ne_of_lt` `Set.indicator_apply_eq_zero` `apply_pos_iff` `ENNReal.tsum_lt_tsum` `tsum_coe_indicator_ne_top` `Set.indicator_apply_le` `ENNReal.instCanonicallyOrderedAdd` `le_rfl` `tsum_coe` `apply_eq_zero_iff` `Set.notMem_subset` `trans` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `eq_isEquiv` `tsum_congr` `Set.indicator_apply` `symm` `IsEquiv.toSymm` `toOuterMeasure_apply`
`toOuterMeasure_apply_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `MeasureTheory.OuterMeasure.instFunLikeSetENNReal` `toOuterMeasure` `instZeroENNReal` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `support`	—	`toOuterMeasure_apply` `ENNReal.tsum_eq_zero` `Set.indicator_eq_zero'`
`toOuterMeasure_apply_finset` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `MeasureTheory.OuterMeasure.instFunLikeSetENNReal` `toOuterMeasure` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.sum` `ENNReal.instAddCommMonoid` `PMF` `instFunLike`	—	`toOuterMeasure_apply` `tsum_eq_sum` `SummationFilter.instLeAtTopUnconditional` `Set.indicator_of_notMem` `Iff.not` `Finset.mem_coe` `Finset.sum_congr` `Set.indicator_of_mem`
`toOuterMeasure_apply_fintype` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `MeasureTheory.OuterMeasure.instFunLikeSetENNReal` `toOuterMeasure` `Finset.sum` `ENNReal.instAddCommMonoid` `Finset.univ` `Set.indicator` `instZeroENNReal` `PMF` `instFunLike`	—	`toOuterMeasure_apply` `tsum_eq_sum` `SummationFilter.instLeAtTopUnconditional` `Finset.mem_univ`
`toOuterMeasure_apply_inter_support` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `MeasureTheory.OuterMeasure.instFunLikeSetENNReal` `toOuterMeasure` `Set.instInter` `support`	—	`toOuterMeasure_apply` `Set.indicator_inter_support`
`toOuterMeasure_apply_le_toMeasure_apply` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `MeasureTheory.OuterMeasure.instFunLikeSetENNReal` `toOuterMeasure` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `toMeasure`	—	`MeasureTheory.le_toMeasure_apply`
`toOuterMeasure_apply_singleton` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `MeasureTheory.OuterMeasure.instFunLikeSetENNReal` `toOuterMeasure` `Set.instSingletonSet` `PMF` `instFunLike`	—	`toOuterMeasure_apply` `tsum_eq_single` `SummationFilter.instLeAtTopUnconditional`
`toOuterMeasure_caratheodory` 📖	mathematical	—	`MeasureTheory.OuterMeasure.caratheodory` `toOuterMeasure` `Top.top` `MeasurableSpace` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `MeasurableSpace.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`eq_top_iff` `le_trans` `le_sInf` `LE.le.trans` `IsScalarTower.right` `le_of_eq` `MeasureTheory.OuterMeasure.dirac_caratheodory` `MeasureTheory.OuterMeasure.le_smul_caratheodory` `MeasureTheory.OuterMeasure.le_sum_caratheodory`
`toOuterMeasure_inj` 📖	mathematical	—	`toOuterMeasure`	—	`toOuterMeasure_injective`
`toOuterMeasure_injective` 📖	mathematical	—	`PMF` `MeasureTheory.OuterMeasure` `toOuterMeasure`	—	`ext` `toOuterMeasure_apply_singleton`
`toOuterMeasure_mono` 📖	mathematical	`Set` `Set.instHasSubset` `Set.instInter` `support`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.OuterMeasure` `MeasureTheory.OuterMeasure.instFunLikeSetENNReal` `toOuterMeasure`	—	`le_trans` `le_of_eq` `toOuterMeasure_apply_inter_support` `MeasureTheory.OuterMeasure.mono`
`toPMF_eq_iff_toMeasure_eq` 📖	mathematical	—	`MeasureTheory.Measure.toPMF` `toMeasure`	—	`MeasureTheory.Measure.toPMF_toMeasure`
`tsum_coe` 📖	mathematical	—	`tsum` `ENNReal` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `DFunLike.coe` `PMF` `instFunLike` `SummationFilter.unconditional` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`HasSum.tsum_eq` `ENNReal.instT2Space` `SummationFilter.instNeBotUnconditional` `hasSum_coe_one`
`tsum_coe_indicator_ne_top` 📖	—	—	—	—	`ne_of_lt` `lt_of_le_of_lt` `ENNReal.tsum_le_tsum` `Set.indicator_apply_le` `ENNReal.instCanonicallyOrderedAdd` `le_rfl` `lt_of_le_of_ne` `le_top` `tsum_coe_ne_top`
`tsum_coe_ne_top` 📖	—	—	—	—	`ENNReal.one_ne_top` `tsum_coe`

PMF.toMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isProbabilityMeasure` 📖	mathematical	—	`MeasureTheory.IsProbabilityMeasure` `PMF.toMeasure`	—	`PMF.toMeasure_apply_eq_toOuterMeasure_apply` `PMF.toOuterMeasure_apply` `Set.indicator_univ` `PMF.tsum_coe`

(root)

Definitions

Name	Category	Theorems
`PMF` 📖	CompOp	58 math math: `PMF.tsum_coe`, `PMF.toMeasure_bind_apply`, `PMF.binomial_apply_zero`, `PMF.toMeasure_apply_singleton`, `PMF.toOuterMeasure_injective`, `PMF.toMeasure_apply`, `PMF.uniformOfFinset_apply_of_mem`, `PMF.ext_iff`, `PMF.instLawfulFunctor`, `PMF.toOuterMeasure_apply_singleton`, `PMF.bind_map`, `PMF.ofFinset_apply`, `PMF.uniformOfFintype_apply`, `PMF.monad_seq_eq_seq`, `PMF.filter_apply_eq_zero_iff`, `PMF.monad_map_eq_map`, `PMF.integral_eq_tsum`, `PMF.seq_apply`, `PMF.pure_apply_of_ne`, `PMF.apply_lt_top`, `PMF.coe_le_one`, `PMF.toOuterMeasure_bindOnSupport_apply`, `PMF.apply_eq_zero_iff`, `PMF.binomial_apply`, `PMF.uniformOfFinset_apply_of_notMem`, `PMF.binomial_apply_self`, `PMF.apply_eq_one_iff`, `PMF.integral_eq_sum`, `PMF.instLawfulMonad`, `PMF.apply_pos_iff`, `PMF.bernoulli_apply`, `PMF.bindOnSupport_eq_zero_iff`, `PMF.toMeasure_injective`, `PMF.bind_pure_comp`, `PMF.hasSum_coe_one`, `PMF.toMeasure_bindOnSupport_apply`, `PMF.uniformOfFinset_apply`, `PMF.toOuterMeasure_apply`, `PMF.filter_apply`, `PMF.toOuterMeasure_apply_finset`, `PMF.pure_apply_self`, `PMF.bind_apply`, `PMF.ofFintype_apply`, `PMF.map_apply`, `PMF.toOuterMeasure_bind_apply`, `PMF.bindOnSupport_apply`, `PMF.pure_apply`, `PMF.filter_apply_eq_zero_of_notMem`, `PMF.binomial_apply_last`, `PMF.ofMultiset_apply_of_notMem`, `PMF.toMeasure_apply_fintype`, `PMF.ofMultiset_apply`, `PMF.ofFinset_apply_of_notMem`, `PMF.toOuterMeasure_apply_fintype`, `PMF.toMeasure_apply_eq_tsum`, `PMF.toMeasure_apply_finset`, `MeasureTheory.Measure.toPMF_apply`, `PMF.normalize_apply`

---

← Back to Index