Complementary-layer bound for biased measure (source code)

= Complementary-layer bound for biased measure
{title2=$\mu_p(\mathcal F)\ge p\quad(p\ge1/2)$}

Suppose a <self-dual set family> has level proportions $a_j\le j/n$ for $j<n/2$. Subtract the binomial identity $p=\sum_j\binom nj(j/n)p^j(1-p)^{n-j}$ from its <biased measure of a set family> and pair levels $j,n-j$. The difference is
$$
\mu_p(\mathcal F)-p=\sum_{j<n/2}\binom nj(j/n-a_j)[p^{n-j}(1-p)^j-p^j(1-p)^{n-j}].
$$
Every term is nonnegative for $p\ge1/2$. A self-dual <intersecting family> has the required level bounds by the <Erdős-Ko-Rado theorem>.