A generalization of Boppana's entropy inequality

TL;DR

This paper generalizes Boppana's entropy inequality for real exponents, proving a conjecture by Yuster, and explores implications for union-closed set systems, with formal proof in Lean 4.

Contribution

The paper extends Boppana's entropy inequality to real values of k, confirming Yuster's conjecture and applying it to approximate union-closed set systems.

Findings

Proved the generalized entropy inequality for real k>1.

Established an analogue of the union-closed sets conjecture for approximate systems.

Provided a formal proof in Lean 4.

Abstract

In recent progress on the union-closed sets conjecture, a key lemma has been Boppana's entropy inequality: $h(x^2)\ge\phi xh(x)$, where $\phi=(1+\sqrt5)/2$ and $h(x)=-x\log x-(1-x)\log(1-x)$. In this note, we prove that the generalized inequality $\alpha_kh(x^k)\ge x^{k-1}h(x)$, first conjectured by Yuster, holds for real $k>1$, where $\alpha_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.