Maximum entropy with a log-distance constraint is a power law

Among probability distributions on the distances 1, …, N with prescribed E[log d] = λ, the power law p_γ(d) = d^(−γ)/Σ_e e^(−γ) is the unique maximiser of Shannon entropy, and when 0 < λ < (1/N) Σ_d log d the exponent γ > 0 is unique. This corrects Theorem 6.2 of «Predicting How Transformers Attend» (Part I, v3), which omitted the condition on λ. Proof: Gibbs' inequality — Σ p log p_γ is the same for every feasible p, so H(p_γ) − H(p) is a relative entropy, nonnegative by log x ≤ x − 1 and zero only at p = p_γ; the exponent comes from the intermediate value theorem.

Main results

• MaxEntPowerLaw.maxent_power_law: corrected MaxEnt theorem: unique γ > 0, unique entropy maximiser

References

• C. Marín, «Predicting How Transformers Attend», Zenodo 20314038 (v3), Thm 6.2 (corregido).
• E. T. Jaynes, Phys. Rev. 106 (1957) 620; T. Cover, J. Thomas, Elements of Information Theory (2006), §12.

noncomputable def MaxEntPowerLaw.logMean {N : ℕ} (p : Fin N → ℝ) : ℝ

E_p[log d] for a distribution p on distances 1..N.

Equations

• MaxEntPowerLaw.logMean p = ∑ i : Fin N, p i * Real.log (↑↑i + 1)

noncomputable def MaxEntPowerLaw.entropy {N : ℕ} (p : Fin N → ℝ) : ℝ

Shannon entropy -Σ p log p.

Equations

• MaxEntPowerLaw.entropy p = -∑ i : Fin N, p i * Real.log (p i)

noncomputable def MaxEntPowerLaw.powerLaw (N : ℕ) (γ : ℝ) (i : Fin N) : ℝ

The power law p_γ(d) = d^(-γ) / Σ_e e^(-γ) on distances 1..N.

Equations

• MaxEntPowerLaw.powerLaw N γ i = (↑↑i + 1) ^ (-γ) / ∑ j : Fin N, (↑↑j + 1) ^ (-γ)

noncomputable def MaxEntPowerLaw.wt {N : ℕ} (γ : ℝ) (i : Fin N) : ℝ

Unnormalised weight d^(-γ) written with exp.

Equations

• MaxEntPowerLaw.wt γ i = Real.exp (-γ * Real.log (↑↑i + 1))

noncomputable def MaxEntPowerLaw.Z (N : ℕ) (γ : ℝ) : ℝ

Partition function.

Equations

• MaxEntPowerLaw.Z N γ = ∑ i : Fin N, MaxEntPowerLaw.wt γ i

theorem MaxEntPowerLaw.rpow_eq {N : ℕ} (γ : ℝ) (i : Fin N) : (↑↑i + 1) ^ (-γ) = wt γ i

theorem MaxEntPowerLaw.powerLaw_eq {N : ℕ} (γ : ℝ) (i : Fin N) : powerLaw N γ i = wt γ i / Z N γ

theorem MaxEntPowerLaw.Z_pos {N : ℕ} (hN : 0 < N) (γ : ℝ) : 0 < Z N γ

theorem MaxEntPowerLaw.pl_pos {N : ℕ} (hN : 0 < N) (γ : ℝ) (i : Fin N) : 0 < powerLaw N γ i

theorem MaxEntPowerLaw.pl_sum {N : ℕ} (hN : 0 < N) (γ : ℝ) : ∑ i : Fin N, powerLaw N γ i = 1

theorem MaxEntPowerLaw.log_pl {N : ℕ} (hN : 0 < N) (γ : ℝ) (i : Fin N) : Real.log (powerLaw N γ i) = -γ * Real.log (↑↑i + 1) - Real.log (Z N γ)

theorem MaxEntPowerLaw.sum_mul_log_pl {N : ℕ} (hN : 0 < N) (γ : ℝ) (p : Fin N → ℝ) (hp : ∑ i : Fin N, p i = 1) : ∑ i : Fin N, p i * Real.log (powerLaw N γ i) = -γ * logMean p - Real.log (Z N γ)

theorem MaxEntPowerLaw.term_gibbs (a b : ℝ) (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ a * (Real.log a - Real.log b) - (a - b) ∧ (a * (Real.log a - Real.log b) - (a - b) = 0 → a = b)

Termwise Gibbs inequality.

theorem MaxEntPowerLaw.gibbs_le {N : ℕ} (hN : 0 < N) (γ : ℝ) (p : Fin N → ℝ) (hp0 : ∀ (i : Fin N), 0 ≤ p i) (hp1 : ∑ i : Fin N, p i = 1) (hlm : logMean p = logMean (powerLaw N γ)) : entropy p ≤ entropy (powerLaw N γ) ∧ (entropy p = entropy (powerLaw N γ) → p = powerLaw N γ)

theorem MaxEntPowerLaw.logMean_pl {N : ℕ} (_hN : 0 < N) (γ : ℝ) : logMean (powerLaw N γ) = (∑ i : Fin N, wt γ i * Real.log (↑↑i + 1)) / Z N γ

theorem MaxEntPowerLaw.continuous_logMean {N : ℕ} (hN : 0 < N) : Continuous fun (γ : ℝ) => logMean (powerLaw N γ)

theorem MaxEntPowerLaw.logMean_zero {N : ℕ} (hN : 0 < N) : logMean (powerLaw N 0) = (∑ i : Fin N, Real.log (↑↑i + 1)) / ↑N

theorem MaxEntPowerLaw.Z_ge_one {N : ℕ} (hN : 0 < N) (γ : ℝ) : 1 ≤ Z N γ

theorem MaxEntPowerLaw.logMean_le {N : ℕ} (hN : 0 < N) (γ : ℝ) (hγ : 0 ≤ γ) : logMean (powerLaw N γ) ≤ ↑N * Real.exp (-γ * Real.log 2) * Real.log ↑N

theorem MaxEntPowerLaw.exists_gamma (N : ℕ) (hN : 2 ≤ N) (lam : ℝ) (h0 : 0 < lam) (h1 : lam < (∑ i : Fin N, Real.log (↑↑i + 1)) / ↑N) : ∃ (γ : ℝ), 0 < γ ∧ logMean (powerLaw N γ) = lam

theorem MaxEntPowerLaw.gamma_unique {N : ℕ} (hN : 2 ≤ N) (lam γ₁ γ₂ : ℝ) (h₁ : logMean (powerLaw N γ₁) = lam) (h₂ : logMean (powerLaw N γ₂) = lam) : γ₁ = γ₂

theorem MaxEntPowerLaw.maxent_power_law (N : ℕ) (hN : 2 ≤ N) (lam : ℝ) (h0 : 0 < lam) (h1 : lam < (∑ i : Fin N, Real.log (↑↑i + 1)) / ↑N) : ∃! γ : ℝ, 0 < γ ∧ logMean (powerLaw N γ) = lam ∧ ∀ (p : Fin N → ℝ), (∀ (i : Fin N), 0 ≤ p i) → ∑ i : Fin N, p i = 1 → logMean p = lam → entropy p ≤ entropy (powerLaw N γ) ∧ (entropy p = entropy (powerLaw N γ) → p = powerLaw N γ)

MaxEnt power law (corrected Theorem 6.2).