CoveringBinomialBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Counting bounded-size subsets

Subsets of cardinality at most r are counted by a partial binomial sum. The elementary bound by (1 + B.card)^r includes r = 0 and empty B.

theorem OAI.TalagrandDiscreteConvexity.Covering.card_subsets_card_le line 19

Source documentation

Partition the subsets of B of size at most r by their cardinality.

theorem card_subsets_card_le {V : Type*} [DecidableEq V] (B : Finset V) (r : ℕ) :
    (B.powerset.filter (fun I => I.card ≤ r)).card =
      ∑ i ∈ Finset.range (r + 1), Nat.choose B.card i := by
…

theorem OAI.TalagrandDiscreteConvexity.Covering.sum_choose_range_le_pow line 29
Source documentation
A partial binomial sum is bounded by the number of length-r words over an alphabet with n + 1 letters.
```
theorem sum_choose_range_le_pow (n r : ℕ) :
    (∑ i ∈ Finset.range (r + 1), Nat.choose n i) ≤ (1 + n) ^ r := by
…
```

theorem OAI.TalagrandDiscreteConvexity.Covering.card_subsets_card_le_pow line 45

Source documentation

The number of subsets of B of size at most r is at most (1 + B.card)^r.

theorem card_subsets_card_le_pow {V : Type*} [DecidableEq V]
    (B : Finset V) (r : ℕ) :
    (B.powerset.filter (fun I => I.card ≤ r)).card ≤ (1 + B.card) ^ r := by
…