Disjoint subcube packing inequality (source code)

= Disjoint subcube packing inequality

Pairwise disjoint subcubes of $\{0,1\}^m$ fixing $d_1,\ldots,d_n$ coordinates satisfy $\sum_{x=1}^n2^{-d_x}\leq1$. By <Jensen inequality>, their average codimension is at least $\log_2n$. Consequently a <separating family of disjoint set pairs> of total incidence at most $\lambda mn$, with $\lambda>0$, has $m\geq\lceil\log_2n/\lambda\rceil$.