Two-block extremisers for the cross-Sperner inequality (source code)

= Two-block extremisers for the cross-Sperner inequality

Choose disjoint <subsets> $K_1,K_2\subseteq[n]$ of size $k\geq1$ with $2k\leq n$. Let $\mathcal A$ consist of <subsets> containing all of $K_1$ and none of $K_2$; let $\mathcal B$ consist of <subsets> omitting at least one point of $K_1$ and containing at least one point of $K_2$. These form a <cross-Sperner family> pair, with sizes $2^{n-2k}$ and $(2^k-1)^2 2^{n-2k}$. Their square roots sum to $2^{n/2}$, proving sharpness of the <Cross-Sperner inequality>. The free coordinates outside the two blocks account for the factor $2^{n-2k}$.