Finite sums for probability mass functions

This file records the summation identities for probability mass functions that need a finiteness hypothesis: the total mass on a finite type, and the finite-sum specializations of the marginal formulas of TauCeti.Probability.ProbabilityMassFunction.Marginal.

Main results

• PMF.sum_toReal_eq_one: the real values of a PMF on a finite type sum to one.
• PMF.map_fst_apply_fintype, PMF.map_snd_apply_fintype: the two marginals of a product PMF are its row and column sums whenever the factor being summed over is finite.
• PMF.map_fst_eq_iff_fintype, PMF.map_snd_eq_iff_fintype: characterizations of prescribed marginals by those finite sums.

@[simp]

theorem PMF.sum_toReal_eq_one {ι : Type u} [Fintype ι] (μ : PMF ι) : ∑ i : ι, (μ i).toReal = 1

The real values of a probability mass function on a finite type sum to one.

theorem PMF.map_fst_apply_fintype {ι : Type u} {κ : Type v} (π : PMF (ι × κ)) [Fintype κ] (i : ι) : (map Prod.fst π) i = ∑ j : κ, π (i, j)

The first marginal of a product PMF with finite second factor is obtained by summing each row of its matrix of point masses.

theorem PMF.map_fst_eq_iff_fintype {ι : Type u} {κ : Type v} (π : PMF (ι × κ)) [Fintype κ] (μ : PMF ι) : map Prod.fst π = μ ↔ ∀ (i : ι), ∑ j : κ, π (i, j) = μ i

A product PMF with finite second factor has first marginal μ exactly when its row sums are μ.

theorem PMF.map_snd_apply_fintype {ι : Type u} {κ : Type v} (π : PMF (ι × κ)) [Fintype ι] (j : κ) : (map Prod.snd π) j = ∑ i : ι, π (i, j)

The second marginal of a product PMF with finite first factor is obtained by summing each column of its matrix of point masses.

theorem PMF.map_snd_eq_iff_fintype {ι : Type u} {κ : Type v} (π : PMF (ι × κ)) [Fintype ι] (ν : PMF κ) : map Prod.snd π = ν ↔ ∀ (j : κ), ∑ i : ι, π (i, j) = ν j

A product PMF with finite first factor has second marginal ν exactly when its column sums are ν.