Marginals of a probability mass function on a product

This file records the two marginals of a probability mass function on an arbitrary product as the infinite row and column sums of its matrix of point masses, together with the resulting characterizations of a prescribed marginal.

Main results

• PMF.map_fst_apply, PMF.map_snd_apply: the two marginals of a product PMF are its infinite row and column sums.
• PMF.map_fst_eq_iff, PMF.map_snd_eq_iff: characterizations of prescribed marginals by those sums.

theorem PMF.map_fst_apply {ι : Type u} {κ : Type v} (π : PMF (ι × κ)) (i : ι) : (map Prod.fst π) i = ∑' (j : κ), π (i, j)

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

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

A product PMF has first marginal μ exactly when its infinite row sums are μ.

theorem PMF.map_snd_apply {ι : Type u} {κ : Type v} (π : PMF (ι × κ)) (j : κ) : (map Prod.snd π) j = ∑' (i : ι), π (i, j)

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

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

A product PMF has second marginal ν exactly when its infinite column sums are ν.