Most sets are not much larger than half

The middle binomial coefficient is at most 2 ^ n / sqrt (n + 1): C(n, ⌊n/2⌋)² (n + 1) ≤ 4 ^ n (choose_half_sq_mul_le). So the sets of at most n / 2 + t of n elements, which are those of fewer than n / 2 elements (at most half of all sets, by complementation) and those of between n / 2 and n / 2 + t elements (at most t + 1 middle binomial coefficients), are at most 6 / 10 of all sets when 100 (t + 1)² ≤ n + 1 (ten_mul_card_filter_card_le_le). This is the counting step of Smolensky's lower bound [Smo87].

Main results

• Cslib.choose_half_sq_mul_le: C(n, ⌊n/2⌋)² (n + 1) ≤ 4 ^ n.
• Cslib.ten_mul_card_filter_card_le_le: few sets are much larger than half.

References

• R. Smolensky, Algebraic methods in the theory of lower bounds for Boolean circuit complexity

theorem Cslib.centralBinom_sq_mul_le (m : ℕ) : m.centralBinom ^ 2 * (2 * m + 1) ≤ 16 ^ m

The central binomial coefficient satisfies C(2m, m)² (2m + 1) ≤ 16^m.

theorem Cslib.choose_half_sq_mul_le (n : ℕ) : n.choose (n / 2) ^ 2 * (n + 1) ≤ 4 ^ n

The middle binomial coefficient satisfies C(n, ⌊n/2⌋)² (n + 1) ≤ 4^n.

theorem Cslib.two_mul_card_small_le (n : ℕ) : 2 * {S : Finset (Fin n) | 2 * S.card < n}.card ≤ 2 ^ n

Complementation shows that at most half of all subsets have fewer than n / 2 elements.

theorem Cslib.ten_mul_card_filter_card_le_le (n t : ℕ) (h : 100 * (t + 1) ^ 2 ≤ n + 1) : 10 * {S : Finset (Fin n) | S.card ≤ n / 2 + t}.card ≤ 6 * 2 ^ n

When 100 (t + 1)² ≤ n + 1, at most 6/10 of the subsets of Fin n have at most n / 2 + t elements.