Documentation

Complexity.Probability.PMF

Monad notation and real-valued masses for discrete distributions #

Copies of two cslib pull requests that the pinned cslib lacks: simp lemmas turning do notation on PMF into PMF.pure/PMF.bind (cslib #1129), and real-valued probability masses (cslib #1062). The library's other lemmas about discrete distributions are split by topic: Probability/PMF/Event (event probabilities), Probability/PMF/Bind (two-stage experiments), Probability/PMF/Uniform (uniform distributions and resampling) and Probability/PMF/Map (relabeling).

Main results #

Monad notation #

Copied from cslib PR #1129 at dbe22c640c85b2e9fbcb2ec16cd3d14ccb37c4e8. Remove this block when that PR is in the base pin.

source
@[simp]
theorem Cslib.Probability.PMF.monad_pure_eq_pure {α : Type u_1} (a : α) :
pure a = PMF.pure a
source
@[simp]
theorem Cslib.Probability.PMF.monad_bind_eq_bind {α β : Type u} (p : PMF α) (f : α → PMF β) :
p >>= f = p.bind f

Real-valued probability masses #

Copied from cslib PR #1062 at b2b8dcdfe7dc7f791a146534ad2ca8eb383b51fd. Remove this block when that PR is in the base pin.

source
theorem Cslib.Probability.PMF.summable_toReal {α : Type u_1} (p : PMF α) :
Summable fun (a : α) => (p a).toReal

Real-valued probability masses are summable, even on an infinite ambient type.

source
@[simp]
theorem Cslib.Probability.PMF.tsum_toReal {α : Type u_1} (p : PMF α) :
∑' (a : α), (p a).toReal = 1

The real-valued masses of any discrete distribution sum to one.

source
theorem Cslib.Probability.PMF.sum_toReal {α : Type u_1} [Fintype α] (p : PMF α) :
∑ a : α, (p a).toReal = 1

The real-valued probabilities of a finite distribution sum to one.

source
theorem Cslib.Probability.PMF.bind_apply_toReal_tsum {α : Type u_1} {β : Type u_2} (p : PMF α) (kernel : α → PMF β) (b : β) :
((p.bind kernel) b).toReal = ∑' (a : α), (p a).toReal * ((kernel a) b).toReal

Randomized postprocessing averages the outcome probabilities over any discrete input.

source
theorem Cslib.Probability.PMF.bind_apply_toReal {α : Type u_1} {β : Type u_2} [Fintype α] (p : PMF α) (kernel : α → PMF β) (b : β) :
((p.bind kernel) b).toReal = ∑ a : α, (p a).toReal * ((kernel a) b).toReal

The probability of an outcome after a finite random choice is its weighted average.