Monad

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

Statistics

Metric	Count
Definitions `Monad`, `Monad`, `bind`, `bindOnSupport`, `instInhabited`, `instMonad`, `pure`	7
Theorems `bindOnSupport_apply`, `bindOnSupport_bindOnSupport`, `bindOnSupport_comm`, `bindOnSupport_eq_bind`, `bindOnSupport_eq_zero_iff`, `bindOnSupport_pure`, `bind_apply`, `bind_bind`, `bind_comm`, `bind_const`, `bind_pure`, `mem_support_bindOnSupport_iff`, `mem_support_bind_iff`, `mem_support_pure_iff`, `pure_apply`, `pure_apply_of_ne`, `pure_apply_self`, `pure_bind`, `pure_bindOnSupport`, `support_bind`, `support_bindOnSupport`, `support_pure`, `toMeasure_bindOnSupport_apply`, `toMeasure_bind_apply`, `toMeasure_pure`, `toMeasure_pure_apply`, `toOuterMeasure_bindOnSupport_apply`, `toOuterMeasure_bind_apply`, `toOuterMeasure_pure_apply`, `toPMF_dirac`	30
Total	37

CategoryTheory

Definitions

Name	Category	Theorems
`Monad` 📖	CompData	31 math math: `Monad.monadMonEquiv_unitIso_inv_app_toNatTrans_app`, `MonadIso.toNatIso_hom`, `instReflectsIsomorphismsMonadFunctorMonadToFunctor`, `Monad.algebraFunctorOfMonadHomId_inv_app_f`, `Monad.algebraEquivOfIsoMonads_inverse`, `Monad.monadMonEquiv_counitIso_hom_app_hom`, `MonadHom.comp_toNatTrans`, `Monad.algebraFunctorOfMonadHomId_hom_app_f`, `Monad.algebraEquivOfIsoMonads_unitIso`, `Monad.monadToMon_obj`, `monadToFunctor_obj`, `Monad.monToMonad_obj`, `MonadIso.mk_hom_toNatTrans`, `Monad.algebraFunctorOfMonadHomComp_hom_app_f`, `Monad.monadToMon_map_hom`, `MonadIso.toNatIso_inv`, `Monad.algebraEquivOfIsoMonads_functor`, `Adjunction.adjToMonadIso_inv_toNatTrans_app`, `Monad.monToMonad_map_toNatTrans`, `Monad.algebraEquivOfIsoMonads_counitIso`, `monadToFunctor_mapIso_monad_iso_mk`, `Monad.monadMonEquiv_inverse`, `monadToFunctor_map`, `instFaithfulMonadFunctorMonadToFunctor`, `Monad.algebraFunctorOfMonadHomComp_inv_app_f`, `Monad.monadMonEquiv_counitIso_inv_app_hom`, `MonadIso.mk_inv_toNatTrans`, `Monad.monadMonEquiv_functor`, `Adjunction.adjToMonadIso_hom_toNatTrans_app`, `Monad.monadMonEquiv_unitIso_hom_app_toNatTrans_app`, `MonadHom.id_toNatTrans`

Erased

Definitions

Name	Category	Theorems
`Monad` 📖	CompOp	4 math math: `bind_def`, `pure_def`, `instLawfulMonad`, `map_def`

PMF

Definitions

Name	Category	Theorems
`bind` 📖	CompOp	14 math math: `map_bind`, `bind_bind`, `toMeasure_bind_apply`, `bindOnSupport_eq_bind`, `pure_bind`, `bind_map`, `support_bind`, `mem_support_bind_iff`, `bind_comm`, `bind_const`, `bind_pure_comp`, `bind_pure`, `bind_apply`, `toOuterMeasure_bind_apply`
`bindOnSupport` 📖	CompOp	11 math math: `mem_support_bindOnSupport_iff`, `bindOnSupport_eq_bind`, `bindOnSupport_comm`, `pure_bindOnSupport`, `toOuterMeasure_bindOnSupport_apply`, `support_bindOnSupport`, `bindOnSupport_bindOnSupport`, `bindOnSupport_eq_zero_iff`, `toMeasure_bindOnSupport_apply`, `bindOnSupport_apply`, `bindOnSupport_pure`
`instInhabited` 📖	CompOp	—
`instMonad` 📖	CompOp	4 math math: `instLawfulFunctor`, `monad_seq_eq_seq`, `monad_map_eq_map`, `instLawfulMonad`
`pure` 📖	CompOp	16 math math: `toMeasure_pure_apply`, `toOuterMeasure_pure_apply`, `pure_bind`, `toPMF_dirac`, `support_pure`, `pure_bindOnSupport`, `pure_apply_of_ne`, `toMeasure_pure`, `mem_support_pure_iff`, `bind_pure_comp`, `pure_map`, `pure_apply_self`, `bind_pure`, `map_const`, `pure_apply`, `bindOnSupport_pure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bindOnSupport_apply` 📖	mathematical	—	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `bindOnSupport` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `instZeroENNReal` `LinearOrder.toDecidableEq` `ENNReal.instLinearOrder` `SummationFilter.unconditional`	—	—
`bindOnSupport_bindOnSupport` 📖	mathematical	—	`bindOnSupport` `Set` `Set.instMembership` `support` `mem_support_bindOnSupport_iff`	—	`ext` `mem_support_bindOnSupport_iff` `ENNReal.tsum_mul_right` `ENNReal.tsum_mul_left` `ENNReal.tsum_comm` `tsum_congr` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_pf_add_zero` `ENNReal.instNoZeroDivisors` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul`
`bindOnSupport_comm` 📖	mathematical	—	`bindOnSupport`	—	`ext` `ENNReal.tsum_mul_left` `trans` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `eq_isEquiv` `ENNReal.tsum_comm` `tsum_congr` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_pf_add_zero`
`bindOnSupport_eq_bind` 📖	mathematical	—	`bindOnSupport` `bind`	—	`ext` `symm` `IsEquiv.toSymm` `eq_isEquiv` `MulZeroClass.zero_mul` `bindOnSupport_apply` `mul_ite` `MulZeroClass.mul_zero`
`bindOnSupport_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `bindOnSupport` `instZeroENNReal`	—	`ENNReal.instNoZeroDivisors`
`bindOnSupport_pure` 📖	mathematical	—	`bindOnSupport` `pure`	—	`bindOnSupport_eq_bind` `bind_pure`
`bind_apply` 📖	mathematical	—	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `bind` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `SummationFilter.unconditional`	—	—
`bind_bind` 📖	mathematical	—	`bind`	—	`ext` `ENNReal.tsum_mul_right` `mul_assoc` `ENNReal.tsum_mul_left` `ENNReal.tsum_comm`
`bind_comm` 📖	mathematical	—	`bind`	—	`ext` `ENNReal.tsum_mul_left` `mul_left_comm` `ENNReal.tsum_comm`
`bind_const` 📖	mathematical	—	`bind`	—	`ext` `bind_apply` `ENNReal.tsum_mul_right` `tsum_coe` `one_mul`
`bind_pure` 📖	mathematical	—	`bind` `pure`	—	`ext` `bind_apply` `trans` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `eq_isEquiv` `tsum_eq_single` `SummationFilter.instLeAtTopUnconditional` `pure_apply_of_ne` `MulZeroClass.mul_zero` `pure_apply_self` `mul_one`
`mem_support_bindOnSupport_iff` 📖	mathematical	—	`Set` `Set.instMembership` `support` `bindOnSupport`	—	`support_bindOnSupport`
`mem_support_bind_iff` 📖	mathematical	—	`Set` `Set.instMembership` `support` `bind`	—	`support_bind`
`mem_support_pure_iff` 📖	mathematical	—	`Set` `Set.instMembership` `support` `pure`	—	`support_pure`
`pure_apply` 📖	mathematical	—	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `pure` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `instZeroENNReal`	—	—
`pure_apply_of_ne` 📖	mathematical	—	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `pure` `instZeroENNReal`	—	—
`pure_apply_self` 📖	mathematical	—	`DFunLike.coe` `PMF` `ENNReal` `instFunLike` `pure` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	—
`pure_bind` 📖	mathematical	—	`bind` `pure`	—	`ext` `ite_mul` `one_mul` `MulZeroClass.zero_mul` `tsum_ite_eq` `SummationFilter.instLeAtTopUnconditional`
`pure_bindOnSupport` 📖	mathematical	—	`bindOnSupport` `pure` `Set` `Set.instMembership` `support` `mem_support_pure_iff`	—	`ext` `mem_support_pure_iff` `trans` `IsPreorder.toIsTrans` `IsEquiv.toIsPreorder` `eq_isEquiv` `tsum_congr` `NeZero.one` `one_mul` `MulZeroClass.mul_zero` `tsum_ite_eq` `SummationFilter.instLeAtTopUnconditional`
`support_bind` 📖	mathematical	—	`support` `bind` `Set.iUnion` `Set` `Set.instMembership`	—	`Set.ext` `ENNReal.instNoZeroDivisors` `Set.iUnion_congr_Prop`
`support_bindOnSupport` 📖	mathematical	—	`support` `bindOnSupport` `Set.iUnion` `Set` `Set.instMembership`	—	`Set.ext` `ENNReal.instNoZeroDivisors` `Set.iUnion_congr_Prop`
`support_pure` 📖	mathematical	—	`support` `pure` `Set` `Set.instSingletonSet`	—	`Set.ext` `NeZero.one`
`toMeasure_bindOnSupport_apply` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure` `bindOnSupport` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `PMF` `instFunLike` `instZeroENNReal` `LinearOrder.toDecidableEq` `ENNReal.instLinearOrder` `SummationFilter.unconditional`	—	`toMeasure_apply_eq_toOuterMeasure_apply` `toOuterMeasure_bindOnSupport_apply`
`toMeasure_bind_apply` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure` `bind` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `PMF` `instFunLike` `SummationFilter.unconditional`	—	`toMeasure_apply_eq_toOuterMeasure_apply` `toOuterMeasure_bind_apply` `tsum_congr`
`toMeasure_pure` 📖	mathematical	—	`toMeasure` `pure` `MeasureTheory.Measure.dirac`	—	`MeasureTheory.Measure.ext` `toMeasure_pure_apply` `MeasureTheory.Measure.dirac_apply'`
`toMeasure_pure_apply` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `toMeasure` `pure` `Set.instMembership` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `instZeroENNReal`	—	`toMeasure_apply_eq_toOuterMeasure_apply` `toOuterMeasure_pure_apply`
`toOuterMeasure_bindOnSupport_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `MeasureTheory.OuterMeasure.instFunLikeSetENNReal` `toOuterMeasure` `bindOnSupport` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `PMF` `instFunLike` `instZeroENNReal` `LinearOrder.toDecidableEq` `ENNReal.instLinearOrder` `SummationFilter.unconditional`	—	`toOuterMeasure_apply` `tsum_congr` `tsum_zero` `ENNReal.tsum_comm` `mul_ite` `MulZeroClass.mul_zero`
`toOuterMeasure_bind_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `MeasureTheory.OuterMeasure.instFunLikeSetENNReal` `toOuterMeasure` `bind` `tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `PMF` `instFunLike` `SummationFilter.unconditional`	—	`toOuterMeasure_apply` `Set.indicator_apply` `tsum_congr` `MulZeroClass.mul_zero` `tsum_zero` `ENNReal.tsum_comm` `ENNReal.tsum_mul_left`
`toOuterMeasure_pure_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.OuterMeasure` `Set` `ENNReal` `MeasureTheory.OuterMeasure.instFunLikeSetENNReal` `toOuterMeasure` `pure` `Set.instMembership` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `instZeroENNReal`	—	`toOuterMeasure_apply` `tsum_congr` `symm` `IsEquiv.toSymm` `eq_isEquiv` `tsum_ite_eq` `SummationFilter.instLeAtTopUnconditional` `tsum_zero`
`toPMF_dirac` 📖	mathematical	—	`MeasureTheory.Measure.toPMF` `MeasureTheory.Measure.dirac` `MeasureTheory.Measure.dirac.isProbabilityMeasure` `pure`	—	`MeasureTheory.Measure.dirac.isProbabilityMeasure` `toPMF_eq_iff_toMeasure_eq` `toMeasure_pure`

---

← Back to Index