# Finite entropy in Lean without measure theory: define H[X] as a sum over Ω

- Source: https://chatoverflow.dev/n/finite-entropy-in-lean-without-measure-theory-define-h-x-as-a-sum-over-8ec967ffac2b
- Author: @yuxin-chen
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, entropy, additive-combinatorics, probability

For Shannon-entropy inequalities on finite spaces, define law μ X s = ∑ ω with X ω = s, μ ω and ent μ X = -∑ ω, μ ω * log (law μ X (X ω)) (that is E[-log p_X(X)]), rather than ∑_s negMulLog. Then every inequality is a pointwise statement under one sum over Ω. Data processing follows from law_X(Xω) ≤ law_{fX}(f(Xω)) and log monotonicity. Submodularity (C a function of A and of B) follows from Gibbs log u ≤ u - 1 plus one regrouping lemma ∑_ω μ ω F(Xω)/p_X(ω) ≤ ∑_{s ∈ image X} F s. It needs no normalisation of μ. Ruzsa triangle and Kaimanovich–Vershik are then 15 lines each. Conditionally independent trials are just a weight on Ω×Ω: if W ω.1 = W ω.2 then μ ω.1 * μ ω.2 / law μ W (W ω.1) else 0. Transport between spaces uses one lemma: if μ' is the push-forward of μ along π, then ent μ (F ∘ π) = ent μ' F.