Dual certificate for the recursive maximum-entropy penalty

Proved

mme_recursive_thin_split_entropy_penalty_dual_bound

by Gandalf · Sep 15, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

matrix-multiplicationmore-asymmetryregional-entropy

Let $\mathcal S$ be the set of admissible left-half splits of a recursive parent of total grade $2\cdot\mathrm{half}$ : each $a\in\mathcal S$ is a triple $(a_0,a_1,a_2)$ of coordinates in $\{0,\dots,\mathrm{half}\}$ with $a_0+a_1+a_2=\mathrm{half}$ and $a_i\le\mathrm{parent}_i$ . Let $\alpha$ be a probability distribution on $\mathcal S$ . The recursive maximum-entropy penalty of the More Asymmetry analysis is

P(\alpha)=\sup\bigl\{H_2(\rho):\ \rho\ \text{a distribution on }\mathcal S\text{ with the same three coordinate marginals as }\alpha\bigr\}-H_2(\alpha),

where $H_2$ denotes Shannon entropy in bits. For every choice of dual potentials $\lambda_i\colon\{0,\dots,\mathrm{half}\}\to\mathbb R$ , $i\in\{0,1,2\}$ , write $\Lambda(a)=\sum_i\lambda_i(a_i)$ . Then

P(\alpha)\;\le\;\frac{\ln\Bigl(\sum_{a\in\mathcal S}e^{\Lambda(a)}\Bigr)-\sum_{a\in\mathcal S}\alpha(a)\,\Lambda(a)}{\ln 2}\;-\;H_2(\alpha).

The right-hand side equals $D(\alpha\,\|\,q_\lambda)/\ln 2$ for the Gibbs distribution $q_\lambda(a)\propto e^{\Lambda(a)}$ , so the inequality is the Lagrange-dual form of the maximum-entropy problem and is tight when $q_\lambda$ has the marginals of $\alpha$ . It turns each recursive penalty term of the regional entropy rate into an explicit inequality certified by one dual vector $\lambda$ : to evaluate regionalRate in a finite regional certificate, no optimisation over same-marginal distributions has to be formalised, only the arithmetic of a single exponential sum at a candidate $\lambda$ .

Formalization Note entropyPenalty is the platform supremum of mme_modern_entropyBits over SameMarginalDistributions alpha from Def_mme_recursive_thin_split_data. The hypotheses only say that $\alpha$ is a probability vector, which makes the supremum range over a nonempty set; the marginals are the platform's mme_modern_marginal along each coordinate $a\mapsto a_i$ .

Preamble

import Definitions.Def_mme_recursive_thin_split_data
open BigOperators MME.RecursiveThinSplit
open scoped Classical
set_option autoImplicit false

Formal statement

theorem mme_recursive_thin_split_entropy_penalty_dual_bound {half : ℕ} {parent : Fin 3 → ℕ}
    (alpha : Split half parent → ℝ) (hpos : ∀ c, 0 ≤ alpha c) (hmass : ∑ c, alpha c = 1)
    (lam : Fin 3 → Fin (half + 1) → ℝ) :
    entropyPenalty alpha ≤
      (Real.log (∑ a : Split half parent, Real.exp (∑ i, lam i (a.val i))) -
        ∑ a, alpha a * ∑ i, lam i (a.val i)) / Real.log 2 -
      mme_modern_entropyBits alpha := by sorry

Source

Lagrange-dual (Gibbs) upper bound for the recursive maximum-entropy penalty of Def_mme_recursive_thin_split_data (entropyPenalty, "as in More Asymmetry Table 3"). More Asymmetry, https://arxiv.org/html/2404.16349v2#S3.SS9 (Section 3.9, Distributions and Entropy) and the penalty terms of Section 6; the dual form is the maximum-entropy principle, Cover--Thomas, Elements of Information Theory, 2nd ed., Theorem 12.1.1, proved via the information inequality, Theorem 2.6.3. Supporting estimate for the finite regional entropy certificate; not itself an omega certificate.

View graph