Finite Probability Mass Functions

FinitePMF W bundles a rational-valued mass function with non-negativity and normalization proofs, eliminating the need to thread hNN/hNorm hypotheses through probabilistic theorems.

Relationship to Other Distribution Types

Type	Number system	Normalized?	Usage
FinitePMF W	ℚ	Yes (bundled)	Probabilistic answerhood, questions, Bayesian semantics
RSAConfigData	ℚ	No	RSA unnormalized weights
RSAConfig	ℝ	No	RSA mathematical proofs
W → ℝ	ℝ	Hypothesized	Entropy / information theory

FinitePMF is the canonical type for probabilistic semantics where exact normalized distributions are needed. RSA priors are deliberately unnormalized and should NOT use FinitePMF.

structure Core.FinitePMF (W : Type u_1) [Fintype W] : Type u_1

A normalized, non-negative probability distribution over a finite type, using exact rational arithmetic.

• mass : W → ℚ

  Probability mass function

• mass_nonneg (w : W) : 0 ≤ self.mass w

  All masses are non-negative

• mass_sum_one : ∑ w : W, self.mass w = 1

  Masses sum to 1

instance Core.FinitePMF.instCoeFunForallRat {W : Type u_1} [Fintype W] : CoeFun (FinitePMF W) fun (x : FinitePMF W) => W → ℚ

Equations

• Core.FinitePMF.instCoeFunForallRat = { coe := fun (d : Core.FinitePMF W) => d.mass }

instance Core.FinitePMF.instCoeForallRat {W : Type u_1} [Fintype W] : Coe (FinitePMF W) (W → ℚ)

Coercion to bare function type, for passing to modules that take W → ℚ (e.g., DTS's condProb, bayesFactor).

Equations

• Core.FinitePMF.instCoeForallRat = { coe := fun (d : Core.FinitePMF W) => d.mass }

@[simp]

theorem Core.FinitePMF.coe_def {W : Type u_1} [Fintype W] (d : FinitePMF W) (w : W) : d.mass w = d.mass w

def Core.FinitePMF.uniform {W : Type u_1} [Fintype W] [Nonempty W] : FinitePMF W

Uniform distribution over a nonempty finite type.

Equations

• Core.FinitePMF.uniform = { mass := fun (x : W) => 1 / ↑(Fintype.card W), mass_nonneg := ⋯, mass_sum_one := ⋯ }

def Core.FinitePMF.pure {W : Type u_1} [Fintype W] [DecidableEq W] (w₀ : W) : FinitePMF W

Point mass at a single value

Equations

• Core.FinitePMF.pure w₀ = { mass := fun (w : W) => if w = w₀ then 1 else 0, mass_nonneg := ⋯, mass_sum_one := ⋯ }

def Core.FinitePMF.expect {W : Type u_1} [Fintype W] (pmf : FinitePMF W) (f : W → ℚ) : ℚ

Expected value of a function under this distribution

Equations

• pmf.expect f = ∑ w : W, pmf.mass w * f w

def Core.FinitePMF.prob {W : Type u_1} [Fintype W] (pmf : FinitePMF W) (event : W → Bool) : ℚ

Expected value of an indicator (probability of event)

Equations

• pmf.prob event = pmf.expect fun (w : W) => if event w = true then 1 else 0

theorem Core.FinitePMF.expect_pure {W : Type u_1} [Fintype W] [DecidableEq W] (w₀ : W) (f : W → ℚ) : (pure w₀).expect f = f w₀

Expected value of pure distribution is the value at that point