Finite mixtures of probability mass functions

This opt-in probability module provides a binary PMF mixture whose parameter is the weight of the first component. General finite-selector mixtures continue to use PMF.bind directly.

noncomputable def PMF.binaryMixture {alpha : Type u} (t : NNReal) (ht : t ≤ 1) (p q : PMF alpha) : PMF alpha

The binary mixture with weight t on p and weight 1 - t on q.

Equivalently, a Bernoulli selector chooses p on true and q on false.

theorem PMF.binaryMixture_apply {alpha : Type u} (t : NNReal) (ht : t ≤ 1) (p q : PMF alpha) (a : alpha) : (binaryMixture t ht p q) a = ↑t * p a + ↑(1 - t) * q a

Pointwise mass formula for a binary PMF mixture.

@[simp]

theorem PMF.binaryMixture_zero {alpha : Type u} (h0 : 0 ≤ 1) (p q : PMF alpha) : binaryMixture 0 h0 p q = q

A binary mixture of weight zero is its second component.

@[simp]

theorem PMF.binaryMixture_one {alpha : Type u} (h1 : 1 ≤ 1) (p q : PMF alpha) : binaryMixture 1 h1 p q = p

A binary mixture of weight one is its first component.