Papers With

← All papers
First page of A generalization of Boppana's entropy inequality

A generalization of Boppana's entropy inequality

Boon Suan Ho

math.CO Jan 27, 2026 · v1
formalization combinatorics
Read PDF arXiv abstract Code
TL;DR
Formalizes in Lean 4 a generalized Boppana entropy inequality relevant to the union-closed sets conjecture.
Abstract
In recent progress on the union-closed sets conjecture, a key lemma has been Boppana's entropy inequality: $h(x^2)\geφxh(x)$, where $φ=(1+\sqrt5)/2$ and $h(x)=-x\log x-(1-x)\log(1-x)$. In this note, we prove that the generalized inequality $α_kh(x^k)\ge x^{k-1}h(x)$, first conjectured by Yuster, holds for real $k>1$, where $α_k$ is the unique positive solution to $x(1+x)^{k-1}=1$. This implies an analogue of the union-closed sets conjecture for approximate $k$-union closed set systems. We also formalize our proof in Lean 4.
Problem

In progress on the union-closed sets conjecture, Boppana's entropy inequality h(x^2) >= phi*x*h(x) served as a key lemma. Yuster conjectured a generalization to arbitrary real exponents k > 1, which remained unproven.

Approach

The authors prove that the generalized inequality alpha_k * h(x^k) >= x^(k-1) * h(x) holds for real k > 1, where alpha_k is the unique positive solution to x(1+x)^(k-1) = 1. The proof analyzes the function q(x) = x^(k-1)*h(x)/h(x^k), showing it attains its maximum at x = 1/(1+alpha) where q equals alpha. The proof is formalized in Lean 4.

Results

The generalized inequality is proved for all real k > 1, implying an analogue of the union-closed sets conjecture for approximate k-union closed set systems. The proof is fully formalized in Lean 4.