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

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.