4.3 Finite-type PMF

Definition 4.6 Real-valued fintype PMF

Lean: ProbabilityTheory.FintypePMF

For a fintype \(\alpha \), a FintypePMF \(\alpha \) is a pair \(\langle p, h_{\ge 0}, h_{\sum = 1} \rangle \) where \(p : \alpha \to \mathbb {R}\), \(p \ge 0\) pointwise, and \(\sum _{a : \alpha } p(a) = 1\). This is an \(\mathbb {R}\)-valued, linarith-compatible specialization of Mathlib’s \(\mathbb {R}_{\ge 0}^\infty \)-valued PMF [ 5 , § 4 ] .

Theorem 4.7 Bridge to Mathlib PMF

Lean: ProbabilityTheory.FintypePMF.toPMF_apply

The map \(\mathrm{toPMF} : \mathrm{FintypePMF}\, \alpha \to \mathrm{PMF}\, \alpha \) satisfies \((\mathrm{toPMF}\, p)(a) = \mathrm{ENNReal.ofReal}(p.\mathrm{prob}\, a)\), which is lossless on valid FintypePMF inputs [ 5 , § 4.1 ] .

Definition 4.8 \(L^1\) TV distance

Lean: ProbabilityTheory.FintypePMF.tvDistance

\(\mathrm{tvDistance}\, p\, q \; :=\; \sum _{a : \alpha } | p(a) - q(a) |\). This is the full \(L^1\) convention, not the half-sup TV of Definition 2.22; on discrete supports they differ by a factor of \(2\) [ 5 , § 4.1 ] , [ 24 , Ch. 1 ] .

Theorem 4.9 Non-negativity of \(\mathrm{tvDistance}\)

Lean: ProbabilityTheory.FintypePMF.tvDistance_nonneg

\(\mathrm{tvDistance}(p, q) \ge 0\) [ 5 , § 4.1 ] .

Theorem 4.10 Symmetry of \(\mathrm{tvDistance}\)

Lean: ProbabilityTheory.FintypePMF.tvDistance_comm

\(\mathrm{tvDistance}(p, q) = \mathrm{tvDistance}(q, p)\) [ 5 , § 4.1 ] .

Theorem 4.11 Self-distance is zero

Lean: ProbabilityTheory.FintypePMF.tvDistance_self

\(\mathrm{tvDistance}(p, p) = 0\) [ 5 , § 4.1 ] .

Theorem 4.12 Transfer principle

Lean: ProbabilityTheory.FintypePMF.expectation_approx_of_tv

For Boolean-valued \(f\), \(\bigl| \mathbb {E}_p[f] - \mathbb {E}_q[f] \bigr| \; \le \; \mathrm{tvDistance}(p, q)\). In the half-sup TV convention this would read \(\le 2 \cdot \mathrm{TV}(p, q)\) [ 5 , § 4.1 ] .