A generalization of Boppana's entropy inequality

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+\sqrt{5})\mathrm{/}2$ and $h(x)=-x\log x-(1-x)\log (1-x)$. In this note, we prove that the generalized inequality ${\alpha }_{k}h(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.