Hitting a spread family with a random set

Let x₀, x₁, … be subsets of a finite type U, and let y be a uniformly random subset of U. The events xₖ ⊆ y are increasing, and two of them are independent when the sets are disjoint. Janson's inequality bounds the probability that y contains no xₖ Alon and Spencer, Chapter 8. We prove a deterministic, greedy form of it. Suppose each xₖ overlaps the earlier sets only a little: ∑_{j < k, xⱼ ∩ xₖ ≠ ∅} 2 ^ (-#(xⱼ \ xₖ)) ≤ 1 / 2. Then the fraction of subsets that contain no xₖ is at most ∏ₖ (1 - 2 ^ (-#xₖ - 1)) (Cslib.card_filter_forall_not_subset_le). The proof conditions on the sets that are disjoint from xₖ, which are independent of the event xₖ ⊆ y. It bounds the other overlaps with the Harris–Kleitman inequality, since the family of subsets avoiding the earlier sets is a lower set.

Forbidding arbitrary patterns, rather than the all-ones pattern, leaves at most as many subsets: Cslib.card_filter_avoidsPatterns_le turns the forbidden patterns y ∩ xₖ = βₖ into xₖ ⊆ y, one element at a time Mertz and Pitassi, Claim 2.3.

A family X of N-element sets is r-spread when every nonempty T lies in at most #X / r ^ #T of its members. A greedy choice finds K members of such a family with small overlaps whenever K ((1 + 2 / r) ^ N - 1) ≤ 2 ^ N / 2 (Cslib.exists_seq_overlap_le_of_spread). So few subsets avoid every pattern on a spread family (Cslib.card_filter_avoidsPatterns_le_of_spread). This replaces the spread (robust sunflower) lemma in the proof of the full-range lemma of query-to-communication lifting Mertz and Pitassi, Lemma 3.2, at the cost of a larger spread. The greedy form and its use there are original to this library.

Main results

• Cslib.card_filter_forall_not_subset_le: the greedy Janson bound.
• Cslib.card_filter_avoidsPatterns_le: forbidding the all-ones patterns is the worst case.
• Cslib.exists_seq_overlap_le_of_spread: spread families contain long sequences with small overlaps.
• Cslib.card_filter_avoidsPatterns_le_of_spread: few subsets avoid every pattern on a spread family.

References

• N. Alon and J. H. Spencer, The Probabilistic Method
• I. Mertz and T. Pitassi, Lifting: As Easy As 1, 2, 3

Independence from the elements of a set

theorem Cslib.card_filter_subset_mul_two_pow {U : Type u_1} [DecidableEq U] {s : Finset U} {D : Finset (Finset U)} (hD : ∀ (y : Finset U), y ∈ D ↔ y \ s ∈ D) : {x ∈ D | s ⊆ x}.card * 2 ^ s.card = D.card

If membership in D ignores the elements of s, then exactly a 2 ^ (-#s) fraction of D contains s.

theorem Cslib.card_filter_subset_univ_mul_two_pow {U : Type u_1} [DecidableEq U] [Fintype U] (s : Finset U) : {x : Finset U | s ⊆ x}.card * 2 ^ s.card = 2 ^ Fintype.card U

Exactly 2 ^ (#U - #s) subsets of U contain s.

The greedy Janson bound

@[reducible, inline]

noncomputable abbrev Cslib.avoiders {U : Type u_1} [DecidableEq U] [Fintype U] (x : ℕ → Finset U) (K : ℕ) : Finset (Finset U)

The subsets of U that contain none of x 0, …, x (K - 1).

theorem Cslib.card_avoiders_mul_le_card_filter {U : Type u_1} [DecidableEq U] [Fintype U] (x : ℕ → Finset U) (K : ℕ) (hK : ∑ j ∈ Finset.range K with ¬Disjoint (x j) (x K), (1 / 2) ^ (x j \ x K).card ≤ 1 / 2) : ↑(avoiders x K).card * (1 / 2) ^ ((x K).card + 1) ≤ ↑{x_1 ∈ avoiders x K | x K ⊆ x_1}.card

The step of the greedy Janson bound: if x K overlaps the earlier sets only a little, then at least a 2 ^ (-#(x K) - 1) fraction of the subsets avoiding the earlier sets contain x K.

theorem Cslib.card_filter_forall_not_subset_le {U : Type u_1} [DecidableEq U] [Fintype U] (x : ℕ → Finset U) (K : ℕ) (hx : ∀ k < K, ∑ j ∈ Finset.range k with ¬Disjoint (x j) (x k), (1 / 2) ^ (x j \ x k).card ≤ 1 / 2) : ↑{y : Finset U | ∀ k < K, ¬x k ⊆ y}.card ≤ 2 ^ Fintype.card U * ∏ k ∈ Finset.range K, (1 - (1 / 2) ^ ((x k).card + 1))

The greedy Janson bound. If each x k overlaps the earlier sets only a little, at most a ∏ₖ (1 - 2 ^ (-#(x k) - 1)) fraction of the subsets of U contain none of x 0, …, x (K - 1).

Forbidding arbitrary patterns

def Cslib.AvoidsPatterns {U : Type u_1} [DecidableEq U] {ι : Type u_2} (I : Finset ι) (s : ι → Finset U) (β : ι → U → Bool) (y : Finset U) : Prop

y avoids the pattern β i on s i for every i ∈ I: each s i has an element whose membership in y differs from β i.

@[instance_reducible]

instance Cslib.instDecidablePredFinsetAvoidsPatterns {U : Type u_1} [DecidableEq U] {ι : Type u_2} (I : Finset ι) (s : ι → Finset U) (β : ι → U → Bool) : DecidablePred (AvoidsPatterns I s β)

theorem Cslib.card_filter_eq_add_card_filter_insert {U : Type u_1} [DecidableEq U] [Fintype U] (u : U) (P : Finset U → Prop) [DecidablePred P] : (Finset.filter P Finset.univ).card = {y : Finset U | u ∉ y ∧ P y}.card + {y : Finset U | u ∉ y ∧ P (insert u y)}.card

Splitting the subsets of U by whether they contain u.

theorem Cslib.card_filter_avoidsPatterns_le_update {U : Type u_1} [DecidableEq U] [Fintype U] {ι : Type u_2} (I : Finset ι) (s : ι → Finset U) (β : ι → U → Bool) (u : U) : (Finset.filter (AvoidsPatterns I s β) Finset.univ).card ≤ (Finset.filter (AvoidsPatterns I s fun (i : ι) (v : U) => if v = u then true else β i v) Finset.univ).card

Changing every pattern to true at one element does not decrease the number of subsets avoiding the patterns Mertz and Pitassi, Claim 2.3.

theorem Cslib.card_filter_avoidsPatterns_le {U : Type u_1} [DecidableEq U] [Fintype U] {ι : Type u_2} (I : Finset ι) (s : ι → Finset U) (β : ι → U → Bool) : (Finset.filter (AvoidsPatterns I s β) Finset.univ).card ≤ {y : Finset U | ∀ i ∈ I, ¬s i ⊆ y}.card

Monotonization. Forbidding the all-ones patterns is the worst case: at most as many subsets of U avoid arbitrary patterns β i on the sets s i as contain none of the s i Mertz and Pitassi, Claim 2.3.

Spread families

theorem Cslib.sum_filter_not_disjoint_le_of_spread {U : Type u_1} [DecidableEq U] {X : Finset (Finset U)} {N : ℕ} {r : ℝ} (hr : 0 < r) (hspread : ∀ (T : Finset U), T.Nonempty → ↑{x ∈ X | T ⊆ x}.card * r ^ T.card ≤ ↑X.card) {t : Finset U} (ht : t.card = N) : ∑ y ∈ X with ¬Disjoint t y, (1 / 2) ^ (t \ y).card ≤ ↑X.card * (1 / 2) ^ N * ((1 + 2 / r) ^ N - 1)

A spread family of N-element sets overlaps a fixed N-element set t only a little: the members meeting t have total weight ∑ 2 ^ (-#(t \ y)) ≤ #X 2 ^ (-N) ((1 + 2 / r) ^ N - 1).

theorem Cslib.exists_seq_overlap_le_of_spread {U : Type u_1} [DecidableEq U] {X : Finset (Finset U)} {N : ℕ} {r : ℝ} (hr : 0 < r) (hspread : ∀ (T : Finset U), T.Nonempty → ↑{x ∈ X | T ⊆ x}.card * r ^ T.card ≤ ↑X.card) (hN : ∀ x ∈ X, x.card = N) (hX : X.Nonempty) {K : ℕ} (hK : ↑K * ((1 + 2 / r) ^ N - 1) ≤ 2 ^ N / 2) : ∃ (x : ℕ → Finset U), (∀ k < K, x k ∈ X) ∧ ∀ k < K, ∑ j ∈ Finset.range k with ¬Disjoint (x j) (x k), (1 / 2) ^ (x j \ x k).card ≤ 1 / 2

Greedy choice. An r-spread family of N-element sets contains K members with small overlaps whenever K ((1 + 2 / r) ^ N - 1) ≤ 2 ^ N / 2.

theorem Cslib.card_filter_avoidsPatterns_le_of_spread {U : Type u_1} [DecidableEq U] [Fintype U] {X : Finset (Finset U)} {N : ℕ} {r : ℝ} (hr : 0 < r) (hspread : ∀ (T : Finset U), T.Nonempty → ↑{x ∈ X | T ⊆ x}.card * r ^ T.card ≤ ↑X.card) (hN : ∀ x ∈ X, x.card = N) (hX : X.Nonempty) {K : ℕ} (hK : ↑K * ((1 + 2 / r) ^ N - 1) ≤ 2 ^ N / 2) (β : Finset U → U → Bool) : ↑(Finset.filter (AvoidsPatterns X id β) Finset.univ).card ≤ 2 ^ Fintype.card U * (1 - (1 / 2) ^ (N + 1)) ^ K

Few subsets avoid every pattern on a spread family. If X is an r-spread family of N-element sets and K ((1 + 2 / r) ^ N - 1) ≤ 2 ^ N / 2, then at most a (1 - 2 ^ (-N - 1)) ^ K fraction of the subsets y of U avoid the pattern β x on every x ∈ X.

theorem Cslib.one_add_pow_le_one_add_two_mul {a : ℝ} (ha : 0 ≤ a) {N : ℕ} (h : a * ↑N ≤ 1 / 2) : (1 + a) ^ N ≤ 1 + 2 * a * ↑N

(1 + a) ^ N ≤ 1 + 2 a N when 0 ≤ a and a N ≤ 1 / 2.

theorem Cslib.card_filter_avoidsPatterns_mul_two_pow_le_of_spread {U : Type u_1} [DecidableEq U] [Fintype U] {X : Finset (Finset U)} {N : ℕ} {r : ℝ} (hr : 0 < r) (hspread : ∀ (T : Finset U), T.Nonempty → ↑{x ∈ X | T ⊆ x}.card * r ^ T.card ≤ ↑X.card) (hN : ∀ x ∈ X, x.card = N) (hX : X.Nonempty) {D : ℕ} (hD : 16 * ↑N * (↑D + 1) ≤ r) (β : Finset U → U → Bool) : ↑(Finset.filter (AvoidsPatterns X id β) Finset.univ).card * 2 ^ (D + 1) ≤ 2 ^ Fintype.card U

Few subsets avoid every pattern on a spread family, in exponential form: if X is an r-spread family of N-element sets with 16 N (D + 1) ≤ r, then at most a 2 ^ (-D - 1) fraction of the subsets of U avoid the pattern β x on every x ∈ X.