LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A binomial-sum bound for compression sample sizes

Statement

For natural numbers $m, d$ with $1 \leq d \leq m$ , $\sum_{i = 0}^{d} (\binom{m}{i}) \leq {(\frac{e m}{d})}^{d},$ where $(\binom{m}{i})$ is the number of $i$ -element subsets of an $m$ -element set, natural numbers and binomial counts in real expressions denote their canonical real images, and $e = \exp (1)$ .

Statement references

Finite sums and finite products, by recursion: defines the real finite sums in the displayed inequality.

Laws of finite sums and finite products: real finite sums preserve inequalities between corresponding terms.

The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ : $(\binom{m}{i})$ counts the $i$ -element subsets of an $m$ -element set.

The canonical natural $ι (n) = n \cdot 1_{F}$ of a field: $n$ is the canonical real associated with the natural number $n$ .

Canonical naturals are positive and strictly increasing: $n > 0$ whenever $n \geq 1$ .

Integer powers $a^{m}$ : the exponent $d$ denotes a natural power in the real field.

The real exponential function and the number $e$ by a power series: $e = \exp (1)$ .

Floyd and Warmuth, Sample Compression, Learnability, and the Vapnik–Chervonenkis Dimension, §5 and Appendix: their compression sample-size derivation uses the same binomial sum; this item proves the estimate below directly.

Facts & Assumptions

Given: Natural numbers $m, d$ satisfying $1 \leq d \leq m$ .

[F1]

The binomial theorem gives $\sum_{i = 0}^{m} (\binom{m}{i}) x^{i} = (1 + x)^{m}$ for real $x$ . The binomial theorem in $R$ : $(x + y)^{n} = \sum_{k < n + 1} ι ⁣ (\binom{n}{k}) x^{k} y^{n - k}$

[F2]

If $0 < x \leq 1$ and $i \leq d$ , then $x^{d} \leq x^{i}$ , by monotonicity of natural powers in the exponent on $(0, 1]$ . Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$

[F3]

$1 + x \leq \exp (x)$ for every real $x$ . $1 + x \leq \exp (x)$ for every real $x$ , hence $(1 - p)^{m} \leq \exp (- m p)$

[F4]

Natural powers use the recursive field-power convention; they preserve order on nonnegative bases, and repeated use of the exponential addition law gives $(\exp (x))^{m} = \exp (m x)$ and $(\exp (1))^{d} = \exp (d)$ , where $e = \exp (1)$ . Integer powers $a^{m}$ , Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ , The real exponential function and the number $e$ by a power series, The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$

[F5]

The displayed expressions are real finite sums, and if each term of one such sum is at most the corresponding term of another, then the first sum is at most the second. Finite sums and finite products, by recursion, Laws of finite sums and finite products

[F6]

The indices $m, d, i$ are natural numbers, each $(\binom{m}{i})$ is a natural count, so its canonical real is nonnegative; $m$ and $d$ are positive because $m, d \geq 1$ . The natural numbers $N$ (von Neumann), The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ , The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, Canonical naturals are positive and strictly increasing

Proof

Given: Natural numbers $m, d$ satisfying $1 \leq d \leq m$ .

1.1givenF1F2F5F6algebra

Put $x = d / m$ , so $0 < x \leq 1$ by [F6] and $d \leq m$ . For every $0 \leq i \leq d$ , [F2] gives $x^{d} \leq x^{i}$ ; multiplying by the nonnegative $(\binom{m}{i})$ , using [F5] to sum, and extending the sum by nonnegative terms from [F6], then applying [F1], yields $x^{d} \sum_{i = 0}^{d} (\binom{m}{i}) \leq \sum_{i = 0}^{d} (\binom{m}{i}) x^{i} \leq \sum_{i = 0}^{m} (\binom{m}{i}) x^{i} = (1 + x)^{m}$ .

2.1givenF3F4F6step 1.1algebra∎

By [F3], $1 + x \leq \exp (x)$ ; both sides are nonnegative, so [F4] gives $(1 + x)^{m} \leq (\exp (x))^{m} = \exp (m x) = \exp (d) = e^{d}$ . Since $x^{d} = (d / m)^{d} > 0$ by [F6], divide step 1.1 by this quantity to obtain the stated bound.

Depends on

Used by

A sample-size consequence for compression schemes Corollary

Dependency tree · two levels

62 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Sally Floyd and Manfred Warmuth, Sample Compression, Learnability, and the Vapnik–Chervonenkis Dimension, §5 and Appendix (standard reference, not scraped)