Constructions

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

Statistics

Metric	Count
Definitions `bernoulli`, `filter`, `instULiftable`, `map`, `normalize`, `ofFinset`, `ofFintype`, `seq`	8
Theorems `bernoulli_apply`, `bind_map`, `bind_pure_comp`, `filter_apply`, `filter_apply_eq_zero_iff`, `filter_apply_eq_zero_of_notMem`, `filter_apply_ne_zero_iff`, `instLawfulFunctor`, `instLawfulMonad`, `map_apply`, `map_bind`, `map_comp`, `map_const`, `map_id`, `map_ofFintype`, `mem_support_bernoulli_iff`, `mem_support_filter_iff`, `mem_support_map_iff`, `mem_support_normalize_iff`, `mem_support_ofFinset_iff`, `mem_support_ofFintype_iff`, `mem_support_seq_iff`, `monad_map_eq_map`, `monad_seq_eq_seq`, `normalize_apply`, `ofFinset_apply`, `ofFinset_apply_of_notMem`, `ofFintype_apply`, `pure_map`, `seq_apply`, `support_bernoulli`, `support_filter`, `support_map`, `support_normalize`, `support_ofFinset`, `support_ofFintype`, `support_seq`, `toMeasure_map`, `toMeasure_map_apply`, `toMeasure_ofFinset_apply`, `toMeasure_ofFintype_apply`, `toOuterMeasure_map_apply`, `toOuterMeasure_ofFinset_apply`, `toOuterMeasure_ofFintype_apply`	44
Total	52

PMF

Definitions

Name	Category	Theorems
`bernoulli` 📖	CompOp	5 math math: `bernoulli_expectation`, `support_bernoulli`, `binomial_one_eq_bernoulli`, `bernoulli_apply`, `mem_support_bernoulli_iff`
`filter` 📖	CompOp	5 math math: `mem_support_filter_iff`, `filter_apply_eq_zero_iff`, `support_filter`, `filter_apply`, `filter_apply_eq_zero_of_notMem`
`instULiftable` 📖	CompOp	—
`map` 📖	CompOp	16 math math: `map_bind`, `mem_support_map_iff`, `map_comp`, `bind_map`, `support_map`, `monad_map_eq_map`, `toMeasure_map`, `map_id`, `toOuterMeasure_map_apply`, `binomial_one_eq_bernoulli`, `bind_pure_comp`, `map_ofFintype`, `pure_map`, `map_const`, `map_apply`, `toMeasure_map_apply`
`normalize` 📖	CompOp	3 math math: `mem_support_normalize_iff`, `support_normalize`, `normalize_apply`
`ofFinset` 📖	CompOp	6 math math: `toMeasure_ofFinset_apply`, `toOuterMeasure_ofFinset_apply`, `mem_support_ofFinset_iff`, `ofFinset_apply`, `support_ofFinset`, `ofFinset_apply_of_notMem`
`ofFintype` 📖	CompOp	6 math math: `toMeasure_ofFintype_apply`, `support_ofFintype`, `toOuterMeasure_ofFintype_apply`, `mem_support_ofFintype_iff`, `map_ofFintype`, `ofFintype_apply`
`seq` 📖	CompOp	4 math math: `mem_support_seq_iff`, `monad_seq_eq_seq`, `seq_apply`, `support_seq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bernoulli_apply` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal`	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `bernoulli` `ENNReal.ofNNReal` `NNReal.instSub`	—	—
`bind_map` 📖	mathematical	—	`bind` `map` `PMF`	—	`bind_bind` `pure_bind`
`bind_pure_comp` 📖	mathematical	—	`bind` `PMF` `pure` `map`	—	—
`filter_apply` 📖	mathematical	`Set` `Set.instMembership` `support`	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `filter` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Set.indicator` `instZeroENNReal` `ENNReal.instInv` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional`	—	`tsum_coe_indicator_ne_top` `filter.eq_1` `normalize_apply`
`filter_apply_eq_zero_iff` 📖	mathematical	`Set` `Set.instMembership` `support`	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `filter` `instZeroENNReal`	—	`apply_eq_zero_iff` `support_filter` `Set.mem_inter_iff` `not_and_or`
`filter_apply_eq_zero_of_notMem` 📖	mathematical	`Set` `Set.instMembership` `support`	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `filter` `instZeroENNReal`	—	`filter_apply` `Set.indicator_apply_eq_zero` `MulZeroClass.zero_mul`
`filter_apply_ne_zero_iff` 📖	—	`Set` `Set.instMembership` `support`	—	—	`filter_apply_eq_zero_iff`
`instLawfulFunctor` 📖	mathematical	—	`PMF` `instMonad`	—	`bind_pure` `map_comp`
`instLawfulMonad` 📖	mathematical	—	`PMF` `instMonad`	—	`instLawfulFunctor` `pure_bind` `bind_bind`
`map_apply` 📖	mathematical	—	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `map` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `instZeroENNReal` `SummationFilter.unconditional`	—	`mul_ite` `mul_one` `MulZeroClass.mul_zero`
`map_bind` 📖	mathematical	—	`map` `bind`	—	`bind_bind`
`map_comp` 📖	mathematical	—	`map`	—	`bind_bind` `pure_bind`
`map_const` 📖	mathematical	—	`map` `pure`	—	`bind_const`
`map_id` 📖	mathematical	—	`map`	—	`bind_pure`
`map_ofFintype` 📖	mathematical	`Finset.sum` `ENNReal` `ENNReal.instAddCommMonoid` `Finset.univ` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`map` `ofFintype` `Finset.filter`	—	`ext` `map_apply` `Finset.sum_congr` `Finset.filter.congr_simp` `Finset.sum_filter` `ofFintype.congr_simp` `tsum_eq_sum` `SummationFilter.instLeAtTopUnconditional` `Finset.mem_univ`
`mem_support_bernoulli_iff` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal`	`Set` `Set.instMembership` `support` `bernoulli` `instZeroNNReal`	—	`support_bernoulli`
`mem_support_filter_iff` 📖	mathematical	`Set` `Set.instMembership` `support`	`filter`	—	`tsum_coe_indicator_ne_top` `mem_support_normalize_iff` `Set.indicator_apply_ne_zero`
`mem_support_map_iff` 📖	mathematical	—	`Set` `Set.instMembership` `support` `map`	—	`support_map`
`mem_support_normalize_iff` 📖	mathematical	—	`Set` `Set.instMembership` `support` `normalize`	—	`support_normalize`
`mem_support_ofFinset_iff` 📖	mathematical	`Finset.sum` `ENNReal` `ENNReal.instAddCommMonoid` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `instZeroENNReal`	`Set` `Set.instMembership` `support` `ofFinset` `Finset` `Finset.instMembership`	—	`support_ofFinset`
`mem_support_ofFintype_iff` 📖	mathematical	`Finset.sum` `ENNReal` `ENNReal.instAddCommMonoid` `Finset.univ` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`Set` `Set.instMembership` `support` `ofFintype`	—	—
`mem_support_seq_iff` 📖	mathematical	—	`Set` `Set.instMembership` `support` `seq` `Set.image`	—	`support_seq` `Set.iUnion_congr_Prop`
`monad_map_eq_map` 📖	mathematical	—	`PMF` `instMonad` `map`	—	—
`monad_seq_eq_seq` 📖	mathematical	—	`PMF` `instMonad` `seq`	—	—
`normalize_apply` 📖	mathematical	—	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `normalize` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instInv` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional`	—	—
`ofFinset_apply` 📖	mathematical	`Finset.sum` `ENNReal` `ENNReal.instAddCommMonoid` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `instZeroENNReal`	`DFunLike.coe` `PMF` `instFunLike` `ofFinset`	—	—
`ofFinset_apply_of_notMem` 📖	mathematical	`Finset.sum` `ENNReal` `ENNReal.instAddCommMonoid` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `instZeroENNReal` `Finset` `Finset.instMembership`	`DFunLike.coe` `PMF` `instFunLike` `ofFinset`	—	—
`ofFintype_apply` 📖	mathematical	`Finset.sum` `ENNReal` `ENNReal.instAddCommMonoid` `Finset.univ` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`DFunLike.coe` `PMF` `instFunLike` `ofFintype`	—	—
`pure_map` 📖	mathematical	—	`map` `pure`	—	`pure_bind`
`seq_apply` 📖	mathematical	—	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `seq` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `instZeroENNReal` `SummationFilter.unconditional`	—	`mul_boole` `tsum_congr` `ENNReal.tsum_mul_left` `MulZeroClass.mul_zero` `mul_ite`
`support_bernoulli` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal`	`support` `bernoulli` `setOf` `instZeroNNReal`	—	`Set.ext` `bernoulli_apply` `ENNReal.coe_sub` `eq_of_le_of_ge` `ENNReal.instCanonicallyOrderedAdd` `ENNReal.instOrderedSub` `tsub_self`
`support_filter` 📖	mathematical	`Set` `Set.instMembership` `support`	`filter` `Set.instInter`	—	`Set.ext` `mem_support_filter_iff`
`support_map` 📖	mathematical	—	`support` `map` `Set.image`	—	`Set.ext` `support_bind` `Set.iUnion_congr_Prop` `support_pure`
`support_normalize` 📖	mathematical	—	`support` `normalize` `Function.support` `ENNReal` `instZeroENNReal`	—	`Set.ext` `ENNReal.instNoZeroDivisors`
`support_ofFinset` 📖	mathematical	`Finset.sum` `ENNReal` `ENNReal.instAddCommMonoid` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `instZeroENNReal`	`support` `ofFinset` `Set` `Set.instInter` `SetLike.coe` `Finset` `Finset.instSetLike` `Function.support`	—	`Set.ext`
`support_ofFintype` 📖	mathematical	`Finset.sum` `ENNReal` `ENNReal.instAddCommMonoid` `Finset.univ` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`support` `ofFintype` `Function.support` `instZeroENNReal`	—	—
`support_seq` 📖	mathematical	—	`support` `seq` `Set.iUnion` `Set` `Set.instMembership` `Set.image`	—	`Set.ext` `support_bind` `Set.iUnion_congr_Prop` `support_pure`
`toMeasure_map` 📖	mathematical	`Measurable`	`MeasureTheory.Measure.map` `toMeasure` `map`	—	`MeasureTheory.Measure.ext` `toMeasure_map_apply` `MeasureTheory.Measure.map_apply`
`toMeasure_map_apply` 📖	mathematical	`Measurable` `MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure` `map` `Set.preimage`	—	`toMeasure_apply_eq_toOuterMeasure_apply` `measurableSet_preimage` `toOuterMeasure_map_apply`
`toMeasure_ofFinset_apply` 📖	mathematical	`Finset.sum` `ENNReal` `ENNReal.instAddCommMonoid` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `instZeroENNReal` `MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `toMeasure` `ofFinset` `tsum` `ENNReal.instTopologicalSpace` `Set.indicator` `SummationFilter.unconditional`	—	`toMeasure_apply_eq_toOuterMeasure_apply` `toOuterMeasure_ofFinset_apply`
`toMeasure_ofFintype_apply` 📖	mathematical	`Finset.sum` `ENNReal` `ENNReal.instAddCommMonoid` `Finset.univ` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `toMeasure` `ofFintype` `tsum` `ENNReal.instTopologicalSpace` `Set.indicator` `instZeroENNReal` `SummationFilter.unconditional`	—	`toMeasure_apply_eq_toOuterMeasure_apply` `toOuterMeasure_ofFintype_apply`
`toOuterMeasure_map_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `MeasureTheory.OuterMeasure.instFunLikeSetENNReal` `toOuterMeasure` `map` `Set.preimage`	—	`toOuterMeasure_bind_apply` `toOuterMeasure_pure_apply` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `toOuterMeasure_apply`
`toOuterMeasure_ofFinset_apply` 📖	mathematical	`Finset.sum` `ENNReal` `ENNReal.instAddCommMonoid` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `instZeroENNReal`	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `MeasureTheory.OuterMeasure.instFunLikeSetENNReal` `toOuterMeasure` `ofFinset` `tsum` `ENNReal.instTopologicalSpace` `Set.indicator` `SummationFilter.unconditional`	—	`toOuterMeasure_apply`
`toOuterMeasure_ofFintype_apply` 📖	mathematical	`Finset.sum` `ENNReal` `ENNReal.instAddCommMonoid` `Finset.univ` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `MeasureTheory.OuterMeasure.instFunLikeSetENNReal` `toOuterMeasure` `ofFintype` `tsum` `ENNReal.instTopologicalSpace` `Set.indicator` `instZeroENNReal` `SummationFilter.unconditional`	—	`toOuterMeasure_apply`

---

← Back to Index