theorem ShearerCombinatorial.shannonEntropy_uniform {α : Type u_1} [Fintype α] [DecidableEq α] (F : Finset α) (hF : F.Nonempty) : ShannonEntropy.shannonEntropy (PMF.uniformOfFinset F hF) = Real.log ↑F.card

Shannon entropy of the uniform distribution on a nonempty finset $F$ equals $\log |F|$.

theorem ShearerCombinatorial.entropy_le_log_support_card {S : Type u_1} [Fintype S] [DecidableEq S] (p : PMF S) : ShannonEntropy.shannonEntropy p ≤ Real.log ↑{s : S | p s ≠ 0}.card

The Shannon entropy of a PMF is bounded by the logarithm of its support size, via Jensen's inequality applied to $-x \log x$.

theorem ShearerCombinatorial.entropy_map_uniform_le {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (F : Finset α) (hF : F.Nonempty) (f : α → β) : ShannonEntropy.shannonEntropy (PMF.map f (PMF.uniformOfFinset F hF)) ≤ Real.log ↑(Finset.image f F).card

Pushing forward the uniform distribution on $F$ by a map $f$ gives entropy at most $\log |f(F)|$.

theorem ShearerCombinatorial.shearer_set_family_inequality {n s : ℕ} (F : Finset (Fin n → Bool)) (A : Fin s → Finset (Fin n)) (k : ℕ) (hcover : ShearerEntropy.CoveringCondition A k) (hF : F.Nonempty) (hk : 0 < k) : ↑F.card ^ k ≤ ∏ j : Fin s, ↑(Finset.image (fun (x : Fin n → Bool) (i : ↥(A j)) => x ↑i) F).card

Combinatorial Shearer for set families (Corollary 10.4.7): if $\{A_j\}_{j=1}^s$ covers each index at least $k$ times, then $|F|^k \le \prod_j |F|_{A_j}|$ where $|F|_{A_j}|$ is the number of projections of $F$ onto coordinates in $A_j$.

def LoomisWhitney.coordProject {n : ℕ} {α : Type u_1} (i : Fin n) (x : Fin n → α) : ↥(Finset.univ.erase i) → α

Projection of x : Fin n → α onto all coordinates except the $i$-th one.

theorem LoomisWhitney.loomis_whitney_inequality {n : ℕ} {α : Type u_1} [Fintype α] [DecidableEq α] (S : Finset (Fin n → α)) (hne : S.Nonempty) : S.card ^ (n - 1) ≤ ∏ i : Fin n, (Finset.image (coordProject i) S).card

The Loomis-Whitney inequality (Corollary 10.4.6): for any finite set $S \subseteq A^n$, $|S|^{n-1} \le \prod_{i=1}^n |\pi_i(S)|$ where $\pi_i$ is the projection that drops coordinate $i$.