Few subsets meet a fixed set in few points

A uniformly random subset x of a finite set S meets a fixed K ⊆ S in about #K / 2 points. Weighting each subset x by 2 ^ #(K \ x) gives total weight 3 ^ #K 2 ^ #(S \ K) (Finset.sum_powerset_two_pow_card_sdiff), and every subset meeting K in at most j points has weight at least 2 ^ (#K - j). So at most a (3 / 4) ^ #K 2 ^ j fraction of the subsets of S meet K in at most j points (Finset.two_pow_mul_card_filter_card_inter_le); for instance at most a (27 / 32) ^ r / 2 fraction meet a set of 3 r points in fewer than r points. Weighting by 2 ^ #x instead bounds the subsets missing at most j points of S (Finset.two_pow_mul_card_filter_card_sdiff_le). This is the exponential-moment (Chernoff) bound with the single weight 2 Alon and Spencer, Appendix A, stated by counting; for the subsets of K itself, Hoeffding's bound for fair coins (Cslib.BitString.card_filter_le_card_filter_sub_half_le) is sharper.

A family of sets for which many points of S are avoided by most of its members inside S is therefore small (Finset.four_mul_sum_card_filter_notMem_le): by Markov's inequality, many of its members meet the avoided points in few points, or miss few points of S. This is the counting step of Razborov's corruption bound for disjointness [Raz92].

Main results

• Finset.two_pow_mul_card_filter_card_inter_le: few subsets of S meet K in few points.
• Finset.two_pow_mul_card_filter_card_sdiff_le: few subsets of S miss few of its points.
• Finset.four_mul_sum_card_filter_notMem_le: families avoiding many points are small.

References

• N. Alon and J. H. Spencer, The Probabilistic Method
• A. A. Razborov, On the distributional complexity of disjointness

theorem Finset.sum_powerset_two_pow_card_sdiff {U : Type u_1} [DecidableEq U] {K S : Finset U} (hKS : K ⊆ S) : ∑ x ∈ S.powerset, 2 ^ (K \ x).card = 3 ^ K.card * 2 ^ (S.card - K.card)

Weighting each subset x of S by 2 ^ #(K \ x) gives total weight 3 ^ #K 2 ^ #(S \ K).

theorem Finset.two_pow_mul_card_filter_card_inter_le {U : Type u_1} [DecidableEq U] {K S : Finset U} (hKS : K ⊆ S) (j : ℕ) : 2 ^ (K.card - j) * {x ∈ S.powerset | (K ∩ x).card ≤ j}.card ≤ 3 ^ K.card * 2 ^ (S.card - K.card)

Few subsets of S meet K ⊆ S in at most j points: 2 ^ (#K - j) times their number is at most 3 ^ #K 2 ^ #(S \ K).

theorem Finset.two_pow_mul_card_filter_card_sdiff_le {U : Type u_1} [DecidableEq U] (S : Finset U) (j : ℕ) : 2 ^ (S.card - j) * {x ∈ S.powerset | (S \ x).card ≤ j}.card ≤ 3 ^ S.card

Few subsets of S miss at most j of its points: 2 ^ (#S - j) times their number is at most 3 ^ #S.

Families of sets that avoid many points

theorem Finset.four_mul_sum_card_filter_notMem_le {U : Type u_1} [DecidableEq U] (A : Finset (Finset U)) (S : Finset U) {r j : ℕ} (hrj : 12 * r ≤ j + 1) : 4 * ∑ i ∈ S with 3 * {x ∈ A | i ∈ x ∧ x ⊆ S}.card < {x ∈ A | x ⊆ S ∧ i ∉ x}.card, ↑{x ∈ A | x ⊆ S ∧ i ∉ x}.card ≤ ∑ i ∈ S, ↑{x ∈ A | x ⊆ S ∧ i ∉ x}.card + 2 ^ S.card * (8 * ↑S.card * (27 / 32) ^ r + (↑j + 1) * 2 ^ j * (3 / 4) ^ S.card)

A family of sets that avoid many points is small. Let A be a family of sets and S a finite set, and call a point i ∈ S bad if the members of A inside S containing i are fewer than a third of those avoiding it. Then the pairs of a member of A inside S and a bad point it avoids are at most a quarter of the pairs of a member inside S and a point of S it avoids, up to 2 ^ #S (8 #S (27 / 32) ^ r + (j + 1) 2 ^ j (3 / 4) ^ #S), which is a small fraction of #S 2 ^ #S when #S ≥ 48 r and j = 12 r. If at least 3 r points are bad, at least a quarter of the members of A inside S meet a set K of 3 r bad points in fewer than r points, by Markov's inequality, and few subsets of S do (two_pow_mul_card_filter_card_inter_le). Otherwise, the bad points are fewer than (j + 1) / 4 and most members inside S avoid more than j points, unless few subsets of S miss at most j points (two_pow_mul_card_filter_card_sdiff_le). This is the key counting step of the corruption bound for disjointness (Cslib.Communication.Disjointness.corrupted_hardDist) [Raz92].