Hypercube edge-boundary entropy-sharp inequality #

The entropy-sharp isoperimetric inequality for the edge boundary on the Boolean cube Fin n → Bool:

|A| · (n − log₂ |A|) ≤ |∂_e A|,

which is sharper than the AM-GM form edgeBoundary_ge_AMGM.

Main statements #

• condEntropy_coord_eq — the direction-i conditional entropy on μ_A := uniformOn A equals (2 (|A| − |π_{≠i}(A)|) / |A|) · log 2.
• sum_condEntropy_le_log_card — ∑ i, H(Xᵢ | X_{≠i}) ≤ log |A|, from the chain rule and conditioning monotonicity.
• edgeBoundary_entropy_sharp — the entropy-sharp bound |A| · (n − log₂ |A|) ≤ |∂_e A|.

Implementation notes #

The conditional entropy condEntropy_coord_eq is computed via the chain rule H(X_{≠i}, Xᵢ) = H(X_{≠i}) + H(Xᵢ | X_{≠i}), evaluating H(X_{≠i}) directly from the projection fibre masses, which avoids a pointwise condDistrib Bernoulli computation.

Uniform measure on A #

The conditional entropy condEntropy_coord_eq #

The direction-i conditional entropy is computed via the chain rule H(X_{≠i}, Xᵢ) = H(X_{≠i}) + H(Xᵢ | X_{≠i}): the joint entropy is log |A|, and H(X_{≠i}) is computed directly from the projection fibre masses c_i(y) / |A|.

Chain rule and conditioning monotonicity #

Main theorem #