Random subsets meet a fixed set in about its expected size

For a set U of u elements of an n-element set s and a uniformly random ℓ-subset J of s, the size X = #(U ∩ J) has a hypergeometric distribution. Double counting gives its factorial moments: n 𝔼[X] = u ℓ (card_mul_sum_card_inter_powersetCard) and n (n - 1) 𝔼[X (X - 1)] = u (u - 1) ℓ (ℓ - 1) (card_mul_sum_card_inter_mul_sub_one_powersetCard), so the variance of X is at most its mean μ = u ℓ / n (sum_card_inter_sub_sq_le). By Chebyshev's inequality X < m ≤ μ with probability at most μ / (μ - m)² (card_filter_card_inter_lt_mul_sq_le), so at most half of the ℓ-subsets meet U in fewer than μ / 2 elements once μ ≥ 8 (two_mul_card_filter_card_inter_lt_le).

Main results

• Finset.sum_card_inter_powersetCard, Finset.sum_card_inter_mul_sub_one_powersetCard: the first two factorial moments of #(U ∩ J) over the ℓ-subsets J.
• Finset.sum_card_inter_sub_sq_le: the variance is at most the mean.
• Finset.card_filter_card_inter_lt_mul_sq_le: Chebyshev's inequality.
• Finset.two_mul_card_filter_card_inter_lt_le: most ℓ-subsets meet U in at least half the expected number of elements.

theorem Finset.sum_card_inter_powersetCard {α : Type u_1} [DecidableEq α] {s U : Finset α} {ℓ : ℕ} (hU : U ⊆ s) (hℓ : 1 ≤ ℓ) : ∑ J ∈ powersetCard ℓ s, (U ∩ J).card = U.card * (s.card - 1).choose (ℓ - 1)

The first moment: summed over the ℓ-subsets J, #(U ∩ J) counts every element of U once for each ℓ-subset containing it.

theorem Finset.sum_card_inter_mul_sub_one_powersetCard {α : Type u_1} [DecidableEq α] {s U : Finset α} {ℓ : ℕ} (hU : U ⊆ s) (hℓ : 2 ≤ ℓ) : ∑ J ∈ powersetCard ℓ s, (U ∩ J).card * ((U ∩ J).card - 1) = U.card * (U.card - 1) * (s.card - 2).choose (ℓ - 2)

The second factorial moment: summed over the ℓ-subsets J, #(U ∩ J) (#(U ∩ J) - 1) counts every ordered pair of distinct elements of U once for each ℓ-subset containing both.

theorem Finset.card_mul_sum_card_inter_powersetCard {α : Type u_1} [DecidableEq α] {s U : Finset α} {ℓ : ℕ} (hU : U ⊆ s) : s.card * ∑ J ∈ powersetCard ℓ s, (U ∩ J).card = U.card * ℓ * s.card.choose ℓ

The first moment, multiplied out: n ∑_J #(U ∩ J) = #U ℓ C(n, ℓ) with n = #s.

theorem Finset.card_mul_sum_card_inter_mul_sub_one_powersetCard {α : Type u_1} [DecidableEq α] {s U : Finset α} {ℓ : ℕ} (hU : U ⊆ s) : s.card * (s.card - 1) * ∑ J ∈ powersetCard ℓ s, (U ∩ J).card * ((U ∩ J).card - 1) = U.card * (U.card - 1) * (ℓ * (ℓ - 1)) * s.card.choose ℓ

The second factorial moment, multiplied out: n (n - 1) ∑_J #(U ∩ J) (#(U ∩ J) - 1) = #U (#U - 1) ℓ (ℓ - 1) C(n, ℓ) with n = #s.

theorem Finset.sum_card_inter_sub_sq_le {α : Type u_1} [DecidableEq α] {s U : Finset α} {ℓ : ℕ} (hU : U ⊆ s) : ∑ J ∈ powersetCard ℓ s, (↑s.card * ↑(U ∩ J).card - ↑U.card * ↑ℓ) ^ 2 ≤ ↑s.card * ↑U.card * ↑ℓ * ↑(s.card.choose ℓ)

The variance of #(U ∩ J) is at most its mean: over the ℓ-subsets J of s, with n = #s, ∑_J (n #(U ∩ J) - #U ℓ)² ≤ n #U ℓ C(n, ℓ).

theorem Finset.card_filter_card_inter_lt_mul_sq_le {α : Type u_1} [DecidableEq α] {s U : Finset α} {ℓ : ℕ} (hU : U ⊆ s) {m : ℕ} (hm : s.card * m ≤ U.card * ℓ) : ↑{J ∈ powersetCard ℓ s | (U ∩ J).card < m}.card * (↑U.card * ↑ℓ - ↑s.card * ↑m) ^ 2 ≤ ↑s.card * ↑U.card * ↑ℓ * ↑(s.card.choose ℓ)

Chebyshev's inequality for #(U ∩ J): with n = #s and n m ≤ #U ℓ (so m is at most the mean), the ℓ-subsets J of s meeting U in fewer than m elements number at most n #U ℓ C(n, ℓ) / (#U ℓ - n m)².

theorem Finset.two_mul_card_filter_card_inter_lt_le {α : Type u_1} [DecidableEq α] {s U : Finset α} {ℓ : ℕ} (hU : U ⊆ s) (hs : 0 < s.card) (hμ : 8 * s.card ≤ U.card * ℓ) {m : ℕ} (hm : 2 * m * s.card ≤ U.card * ℓ) : 2 * {J ∈ powersetCard ℓ s | (U ∩ J).card < m}.card ≤ s.card.choose ℓ

Most ℓ-subsets meet U in at least half the expected number of elements: if the expected size μ = #U ℓ / #s of U ∩ J is at least 8, at most half of the ℓ-subsets J of s meet U in fewer than m ≤ μ / 2 elements.