Bridge: FintypePMF ↔ Mathlib.PMF (on Fintype)

Converts between the ℝ-valued FintypePMF type used by the MWU analysis and Mathlib's ℝ≥0∞-valued PMF type used by the measure-theoretic framework. The bridge is the contract that justifies the coexistence of the two types under the repository's duplicate-rule exception.

ENNReal.ofReal clamps negatives to 0, but FintypePMF.prob_nonneg rules out negatives anyway, so the clamp is invisible on valid inputs.

def ProbabilityTheory.FintypePMF.toPMF {α : Type u_1} [Fintype α] (p : FintypePMF α) : PMF α

Convert a FintypePMF to a Mathlib.PMF via ENNReal.ofReal.

Equations

• p.toPMF = PMF.ofFintype (fun (a : α) => ENNReal.ofReal (p.prob a)) ⋯

theorem ProbabilityTheory.FintypePMF.toPMF_apply {α : Type u_1} [Fintype α] (p : FintypePMF α) (a : α) : p.toPMF a = ENNReal.ofReal (p.prob a)

The PMF image of a FintypePMF evaluates to the ENNReal.ofReal coercion of the original weight.