Relabeling discrete distributions

Main results

• Cslib.Probability.PMF.map_equiv_apply: point masses after an equivalence.
• Cslib.Probability.PMF.map_congr_on_support: only supported inputs need equal outputs.
• Cslib.Probability.PMF.map_apply_toReal: finite fiber sums.
• Cslib.Probability.PMF.uniformOfFintype_map_apply: uniform image masses from fiber sizes.
• Cslib.Probability.PMF.bind_map_prodMk_apply: point masses of a pairing bind.
• Cslib.Probability.PMF.map_injective: injective encodings preserve equality of distributions.

References

Adapted from Probability/PMF.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, reusing Mathlib's support-sensitive bind congruence.

theorem Cslib.Probability.PMF.le_map_apply {α : Type u_1} {β : Type u_2} (p : PMF α) (f : α → β) (a : α) : p a ≤ (PMF.map f p) (f a)

A deterministic map preserves at least the mass of each individual preimage.

theorem Cslib.Probability.PMF.map_equiv_apply {α : Type u_1} {β : Type u_2} (p : PMF α) (e : α ≃ β) (b : β) : (PMF.map (⇑e) p) b = p (e.symm b)

Relabeling a distribution by an equivalence preserves each corresponding point mass.

theorem Cslib.Probability.PMF.map_congr_on_support {α : Type u_1} {β : Type u_2} (p : PMF α) (f g : α → β) (h : ∀ a ∈ p.support, f a = g a) : PMF.map f p = PMF.map g p

Re-encoding only needs to agree on outcomes which the distribution can produce.

theorem Cslib.Probability.PMF.map_apply_toReal {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (p : PMF α) (f : α → β) (b : β) : ((PMF.map f p) b).toReal = ∑ a : α, if b = f a then (p a).toReal else 0

The mass of a deterministic image is the sum of the masses in its fiber.

theorem Cslib.Probability.PMF.uniformOfFintype_map_apply {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] (f : α → β) (b : β) : (PMF.map f (uniformOfFintype α)) b = ↑(Nat.card { a : α // f a = b }) / ↑(Fintype.card α)

The mass of an image of a uniform input is its fiber size divided by the input size.

theorem Cslib.Probability.PMF.bind_map_prodMk_apply {α : Type u_1} {β : Type u_2} (p : PMF α) (f : α → PMF β) (pair : α × β) : (p.bind fun (a : α) => PMF.map (fun (x : β) => (a, x)) (f a)) pair = p pair.1 * (f pair.1) pair.2

Evaluating the pairing bind p.bind fun a => (f a).map (a, ·) at pair gives p pair.1 * f pair.1 pair.2.

@[simp]

theorem Cslib.Probability.PMF.map_fst_bind_pair {α : Type u_1} {β : Type u_2} (p : PMF α) (f : α → PMF β) : PMF.map Prod.fst (p.bind fun (a : α) => PMF.map (fun (x : β) => (a, x)) (f a)) = p

Marginalizing over a freshly sampled second component recovers the first distribution.

theorem Cslib.Probability.PMF.map_injective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) : Function.Injective (PMF.map f)

An injective representation of outcomes also embeds their complete probability laws.