ProbDist
plain-language theorem explainer
A structure encoding a strictly positive real-valued function on a finite type that sums to one defines a discrete probability distribution. Information theorists deriving entropy from the Recognition Composition Law and statistical physicists computing variational free energy cite this construction. Non-negativity of the probabilities follows directly from the positivity condition via the ordering on the reals.
Claim. Let $ι$ be a finite type. A probability distribution on $ι$ is a function $p : ι → ℝ$ such that $p(i) > 0$ for all $i$ and $∑_i p(i) = 1$.
background
The module derives variational free energy from the Recognition Composition Law on finite recognition partitions. It implements the Friston VFE as expected energy plus KL divergence to a prior, which for a Boltzmann reference reduces to expected energy minus temperature times entropy. This structure supplies the probability measures required for those calculations.
proof idea
The definition directly records the positivity and normalization axioms. The accompanying non-negativity result is a one-line wrapper applying le_of_lt to the positivity axiom.
why it matters
This supplies the discrete probability space for entropy and free-energy results throughout the module. It feeds theorems such as deterministic_has_zero_entropy and shannon_entropy_equals_expected_jcost in InformationIsLedger, plus entropy_is_expected_surprisal in ShannonEntropy. The construction closes the finite case needed to equate Shannon entropy with expected J-cost and to identify the variational free energy minimum with the Helmholtz free energy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.