Binomial estimates for Smolensky's bound

The number of subsets of Fin n of size at most n / 2 + t is at most 2^{n-1} + (t + 1) · C(n, ⌊n/2⌋), and C(n, ⌊n/2⌋)² · (n + 1) ≤ 4^n. Hence, when 100 (t + 1)² ≤ n + 1, at most 6/10 of all subsets have size at most n / 2 + t.

theorem Complexity.Smolensky.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 Complexity.Smolensky.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 Complexity.Smolensky.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 Complexity.Smolensky.card_middle_le (n t : ℕ) : {S : Finset (Fin n) | n ≤ 2 * S.card ∧ S.card ≤ n / 2 + t}.card ≤ (t + 1) * n.choose (n / 2)

Subsets of size between n / 2 and n / 2 + t number at most (t + 1) · C(n, ⌊n/2⌋).

theorem Complexity.Smolensky.ten_mul_card_le_internal (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.