Commit 2023-05-11 10:01 1a5bf78b

View on Github →

feat: port Probability.ProbabilityMassFunction.Monad (#3876)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/ProbabilityMassFunction/Monad.lean

added def Pmf.bind

added def Pmf.bindOnSupport

added theorem Pmf.bindOnSupport_apply

added theorem Pmf.bindOnSupport_bindOnSupport

added theorem Pmf.bindOnSupport_comm

added theorem Pmf.bindOnSupport_eq_bind

added theorem Pmf.bindOnSupport_eq_zero_iff

added theorem Pmf.bindOnSupport_pure

added theorem Pmf.bind_apply

added theorem Pmf.bind_bind

added theorem Pmf.bind_comm

added theorem Pmf.bind_const

added theorem Pmf.bind_pure

added theorem Pmf.mem_support_bindOnSupport_iff

added theorem Pmf.mem_support_bind_iff

added theorem Pmf.mem_support_pure_iff

added def Pmf.pure

added theorem Pmf.pure_apply

added theorem Pmf.pure_apply_of_ne

added theorem Pmf.pure_apply_self

added theorem Pmf.pure_bind

added theorem Pmf.pure_bindOnSupport

added theorem Pmf.support_bind

added theorem Pmf.support_bindOnSupport

added theorem Pmf.support_pure

added theorem Pmf.toMeasure_bindOnSupport_apply

added theorem Pmf.toMeasure_bind_apply

added theorem Pmf.toMeasure_pure

added theorem Pmf.toMeasure_pure_apply

added theorem Pmf.toOuterMeasure_bindOnSupport_apply

added theorem Pmf.toOuterMeasure_bind_apply

added theorem Pmf.toOuterMeasure_pure_apply

added theorem Pmf.toPmf_dirac