Documentation

Complexity.Probability.Shearer

Shearer's lemma and Han's inequality #

Let P be the law of a tuple X = (X_i)_{i ∈ ι} of random variables with finite alphabets, and for a finite set s of coordinates write X_s for the restriction to s, whose law is P.map s.restrict. For a family S j, j ∈ J, of coordinate sets covering every coordinate at least k times, Shearer's lemma states k H(X) ≤ ∑ j, H(X_{S j}). Taking the sets univ.erase i gives Han's inequality (n - 1) H(X) ≤ ∑ i, H(X_{-i}), and taking singletons gives the subadditivity H(X) ≤ ∑ i, H(X_i). The form of Han's inequality proved here compares only subsets of sizes n - 1 and n; it is the last step of the monotone chain of averages in [CT06], Theorem 17.6.1, not the full chain.

The proof orders the coordinates and uses the chain rule H(X_s) = ∑ i ∈ s, H(X_i | X_{j ∈ s, j < i}) together with the fact that conditioning on more coordinates cannot increase entropy (conditionalEntropy_map_fst_ge).

Applied to the uniform distribution on a finite set of tuples, Shearer's lemma bounds its size by the sizes of its projections: |A| ^ k ≤ ∏ j, |A restricted to S j|. For α i = Bool this is the original statement of Chung, Graham, Frankl and Shearer about families of sets.

Main results #

References #

source
theorem Cslib.Probability.PMF.entropy_map_restrict_eq_sum {ι : Type u_1} {α : ι → Type u_2} [∀ (i : ι), Finite (α i)] [LinearOrder ι] (P : PMF ((i : ι) → α i)) (s : Finset ι) :
entropy (PMF.map s.restrict P) = ∑ i ∈ s, conditionalEntropy (PMF.map (fun (x : (i : ι) → α i) => ({x ∈ s | x < i}.restrict x, x i)) P)

The chain rule over linearly ordered coordinates ([CT06], Theorem 2.5.1): the entropy of the restriction to s is the sum, over i ∈ s, of the entropy of X_i given the earlier coordinates of s.

source
theorem Cslib.Probability.PMF.mul_entropy_le_sum_entropy_map_restrict {ι : Type u_1} {α : ι → Type u_2} [∀ (i : ι), Finite (α i)] [Finite ι] [DecidableEq ι] {J : Type u_3} [Fintype J] (P : PMF ((i : ι) → α i)) (S : J → Finset ι) {k : ℕ} (hk : ∀ (i : ι), k ≤ {j : J | i ∈ S j}.card) :
↑k * entropy P ≤ ∑ j : J, entropy (PMF.map (S j).restrict P)

Shearer's lemma: if every coordinate lies in at least k of the sets S j, then k times the entropy of the tuple is at most the sum of the entropies of its restrictions to the sets S j.

source
theorem Cslib.Probability.PMF.sub_one_mul_entropy_le_sum_entropy_map_restrict_erase {ι : Type u_1} {α : ι → Type u_2} [∀ (i : ι), Finite (α i)] [Fintype ι] [DecidableEq ι] (P : PMF ((i : ι) → α i)) :
(↑(Fintype.card ι) - 1) * entropy P ≤ ∑ i : ι, entropy (PMF.map (Finset.univ.erase i).restrict P)

Han's inequality: for n coordinates, n - 1 times the entropy of the tuple is at most the sum of the entropies of the tuples with one coordinate deleted. This is the comparison of the averages over subsets of sizes n - 1 and n in [CT06], Theorem 17.6.1; the comparison of smaller sizes is not formalized.

source
theorem Cslib.Probability.PMF.entropy_le_sum_entropy_map_eval {ι : Type u_1} {α : ι → Type u_2} [∀ (i : ι), Finite (α i)] [Fintype ι] (P : PMF ((i : ι) → α i)) :
entropy P ≤ ∑ i : ι, entropy (PMF.map (fun (x : (i : ι) → α i) => x i) P)

Subadditivity of entropy: the entropy of a tuple is at most the sum of the entropies of its coordinates ([CT06], Theorem 2.6.6).

source
theorem Cslib.Finset.card_pow_le_prod_card_image_restrict {ι : Type u_1} {α : ι → Type u_2} [∀ (i : ι), Finite (α i)] [Finite ι] [DecidableEq ι] [(i : ι) → DecidableEq (α i)] {J : Type u_3} [Fintype J] (A : Finset ((i : ι) → α i)) (S : J → Finset ι) {k : ℕ} (hk0 : 0 < k) (hk : ∀ (i : ι), k ≤ {j : J | i ∈ S j}.card) :
A.card ^ k ≤ ∏ j : J, (Finset.image (S j).restrict A).card

Shearer's lemma for counting: if every coordinate lies in at least k ≥ 1 of the sets S j, the k-th power of the size of a finite set of tuples is at most the product of the sizes of its restrictions to the sets S j. For Boolean coordinates this bounds a family of sets by its traces.