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.

翻译：在并封闭集猜想的最新进展中，一个关键引理是Boppana熵不等式：$h(x^2)\geφxh(x)$，其中$φ=(1+\sqrt5)/2$，$h(x)=-x\log x-(1-x)\log(1-x)$。本文证明了Yuster首先猜想的一般化不等式$α_kh(x^k)\ge x^{k-1}h(x)$对所有实数$k>1$成立，其中$α_k$是方程$x(1+x)^{k-1}=1$的唯一正解。该结果蕴含了近似$k$-并封闭集系统对应的并封闭集猜想类比。我们还在Lean 4中形式化了证明过程。