Shannon entropy on N points is at most log N, with equality iff uniform

Formalizes part (i) of the positional entropy area law: for a probability vector p on a finite nonempty type of cardinality N, -sum p log p <= log N, with equality iff p is uniform. Proved from Mathlib's strict concavity of negMulLog via Jensen with uniform weights. Convention: Real.log, natural logarithm, 0 log 0 = 0. Implicit hypotheses made explicit: p nonnegative, summing to 1. The paper states (i) for p(d) ∝ d^(−γ) with γ > 0 and "equality iff γ = 0", which is not consistent as written (and at N = 1 equality holds for every γ); what is formalized is the Gibbs-inequality form its proof uses. Not formalized: the power-law specialization p(d) proportional to d^(-gamma), and parts (ii) and (iii) (Euler-Maclaurin asymptotics, zeta limit).

Main results

• TransformerAttention.EntropyBound.entropy_le_log_card: entropy of a probability vector on N points is at most log N
• TransformerAttention.EntropyBound.entropy_eq_log_card_iff: equality iff the distribution is uniform

References

• C. Marín, Predicting How Transformers Attend Analytic Power-Law Theory, Phase Transitions, and Practical Compression Tools, Zenodo (2026), doi:10.5281/zenodo.20314038, thm:area_law.

theorem TransformerAttention.EntropyBound.entropy_le_log_card {ι : Type u_1} [Fintype ι] [Nonempty ι] (p : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (hsum : ∑ i : ι, p i = 1) : -∑ i : ι, p i * Real.log (p i) ≤ Real.log ↑(Fintype.card ι)

Part (i), inequality: the entropy of a probability distribution on N points is ≤ log N (Jensen for the concave negMulLog with uniform weights).

theorem TransformerAttention.EntropyBound.entropy_eq_log_card_iff {ι : Type u_1} [Fintype ι] [Nonempty ι] (p : ι → ℝ) (hp : ∀ (i : ι), 0 ≤ p i) (hsum : ∑ i : ι, p i = 1) : -∑ i : ι, p i * Real.log (p i) = Real.log ↑(Fintype.card ι) ↔ ∀ (i : ι), p i = 1 / ↑(Fintype.card ι)

Part (i), equality case: equality holds iff p is uniform (strict Jensen).