Counting small subsets

The number of subsets of a finite set of size at most d is the corresponding truncated sum of binomial coefficients. This identity holds for any threshold, including those above the size of the ground set.

Weighting a subset t of s by z ^ (#s - #t) gives total weight (z + 1) ^ #s. When z ≥ 1, every subset of size at most d has weight at least z ^ (#s - d). This gives a small-subset bound with a freely chosen integer weight.

Choosing z = 2 and d = #s / 3 gives the exact integral inequality M ^ 3 * 4 ^ #s ≤ 27 ^ #s, where M counts subsets of size at most #s / 3. Equivalently, the exponential base is (27 / 4) ^ (1 / 3), strictly below 2. The integral form needs neither real powers nor an asymptotic convention.

Main results

• Finset.card_filter_powerset_card_le_eq_sum_choose: count bounded-size subsets of a finset.
• Finset.card_filter_card_le_eq_sum_choose: the specialization to a finite type.
• Finset.card_filter_card_le_mul_pow_le: the weighted bound for any size threshold.
• Finset.card_filter_card_le_third_pow_three_mul_four_pow_le: the one-third bound.

theorem Finset.card_filter_powerset_card_le_eq_sum_choose {α : Type u_1} (s : Finset α) (D : ℕ) : {S ∈ s.powerset | S.card ≤ D}.card = ∑ j ∈ range (D + 1), s.card.choose j

Counting subsets of s by their cardinality gives a truncated binomial sum. Terms above the cardinality of s vanish, so the threshold D need not be bounded by #s.

theorem Finset.card_filter_card_le_eq_sum_choose {α : Type u_1} [Fintype α] (D : ℕ) : {S : Finset α | S.card ≤ D}.card = ∑ j ∈ range (D + 1), (Fintype.card α).choose j

Counting subsets of a finite type by cardinality gives a truncated binomial sum, including thresholds above the size of the type.

theorem Finset.card_filter_card_le_mul_pow_le {α : Type u_1} (s : Finset α) (d z : ℕ) (hz : 1 ≤ z) : {t ∈ s.powerset | t.card ≤ d}.card * z ^ (s.card - d) ≤ (z + 1) ^ s.card

The number of subsets of s of size at most d, multiplied by the minimum weight z ^ (#s - d) of such a subset, is at most the total weight (z + 1) ^ #s.

theorem Finset.card_filter_card_le_third_pow_three_mul_four_pow_le {α : Type u_1} (s : Finset α) : {t ∈ s.powerset | t.card ≤ s.card / 3}.card ^ 3 * 4 ^ s.card ≤ 27 ^ s.card

The subsets of size at most one third of the ground set have exponential base (27 / 4) ^ (1 / 3). This is an exact integer inequality, including the empty ground set.