The discrete Loomis–Whitney inequality

A finite set A of points in a product of n ≥ 2 finite sets has |A| ^ (n - 1) ≤ ∏ i, |π_i(A)|, where π_i forgets the i-th coordinate Loomis and Whitney. In three dimensions: a finite set of unit cubes has volume at most the square root of the product of the areas of its three projections onto the coordinate planes. Every coordinate lies in exactly n - 1 of the sets univ.erase i, so this is Shearer's lemma for counting (card_pow_le_prod_card_image_restrict) for that family, just as Han's inequality is Shearer's lemma for entropy for it.

Main results

• Cslib.Finset.card_pow_le_prod_card_image_restrict_erase: the discrete Loomis–Whitney inequality.

References

• L. H. Loomis, H. Whitney, An inequality related to the isoperimetric inequality
• F. R. K. Chung, R. L. Graham, P. Frankl, J. B. Shearer, Some intersection theorems for ordered sets and graphs

theorem Cslib.Finset.card_pow_le_prod_card_image_restrict_erase {ι : Type u_1} {α : ι → Type u_2} [∀ (i : ι), Finite (α i)] [Fintype ι] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] (hι : 2 ≤ Fintype.card ι) (A : Finset ((i : ι) → α i)) : A.card ^ (Fintype.card ι - 1) ≤ ∏ i : ι, (Finset.image (Finset.univ.erase i).restrict A).card

Discrete Loomis–Whitney inequality: a finite set of tuples with n ≥ 2 coordinates has |A| ^ (n - 1) ≤ ∏ i, |π_i(A)|, where π_i deletes the i-th coordinate.