Edge-isoperimetric inequality in the discrete cube (source code)

= Edge-isoperimetric inequality in the discrete cube
{wiki}

For $A\subseteq\{0,1\}^n$,
$$
|\partial_eA|\geq|A|\log_2\frac{2^n}{|A|}.
$$
Equivalently, $A$ spans at most $\frac12|A|\log_2|A|$ cube edges. Induction on the dimension and concavity of <binary entropy function>[binary entropy] prove the inequality.