Maximum entropy (Gibbs inequality) #

For a finite-alphabet random variable X : Ω → α under an arbitrary probability measure μ, entropy μ X ≤ Real.log (Fintype.card α), with equality if and only if μ.map X = uniformOn Set.univ.

Main statements #

• klDiv_uniformOn_univ_toReal_eq — KL-divergence identity: (klDiv (μ.map X) (uniformOn univ)).toReal = log |α| − entropy μ X.
• entropy_le_log_card — Shannon entropy is at most log |α|.
• entropy_eq_log_card_iff — equality holds if and only if μ.map X = uniformOn univ.

Implementation notes #

The main results follow directly from concavity of negMulLog on Set.Ici 0 via the finite-sum Jensen inequality (ConcaveOn.le_map_sum and StrictConcaveOn.map_sum_eq_iff), with uniform weights 1/N (N = |α|). No KL-divergence machinery is needed; klDiv_uniformOn_univ_toReal_eq is a secondary identity derived from the same computation.

No uniformity assumption is placed on the law of X: the bound holds for an arbitrary probability measure μ, which is what makes entropy_le_log_card usable as the log-cardinality bound on the entropy of an arbitrary encoder output. entropy_le_log_image_card (LoomisWhitney.lean) is the counterpart specialized to μ = uniformOn A, where the bound is the image cardinality #(A.image f) instead of |α|.

KL-divergence identity #

Main theorem via Jensen's inequality #

Equality condition #