LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-01

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.

For fixed $k$ , $(\binom{n}{k}) / n^{k}$ tends to $1 / k!$

Statement

For each fixed $k \in N$ , $\frac{ι (\binom{n}{k})}{ι (n)^{k}} ⟶ \frac{1}{ι (k!)} (n \to \infty),$ where the expression is read for $n \geq \max {1, k}$ . For every such $n$ , one also has the uniform bound $0 \leq \frac{ι (\binom{n}{k})}{ι (n)^{k}} \leq \frac{1}{ι (k!)} .$

Facts & Assumptions

Given: A fixed $k \in N$ .

[L1]

For $n \geq k$ , $(\binom{n}{k}) k! = n^{\underline{k}}$ ( $(\binom{n}{k}) k! (n - k)! = n!$ for $k \leq n$ ; hence $(\binom{n}{k}) k! = n^{\underline{k}}$ , the quotient $n! / (k! (n - k)!)$ is a natural number, and $(\binom{n}{k}) = (\binom{n}{n - k})$ , The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ ), and the canonical embedding preserves the products involved (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field).

[L2]

Finite products and sums obey Finite sums and finite products, by recursion and Laws of finite sums and finite products, limits obey Algebra of limits: sums, scalar multiples, products and quotients, and $1 / ι (n) \to 0$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ). Canonical naturals are positive and strictly increasing (Canonical naturals are positive and strictly increasing), while multiplication by a positive real preserves order (Sign rules for products and monotonicity of multiplication, Ordered field).

Proof

technique · direct

1.1

For $n \geq \max {1, k}$ , $ι (\binom{n}{k}) / ι (n)^{k} = ι (k!)^{- 1} \prod_{j < k} (1 - ι (j) / ι (n))$ .

L1givenalgebra

2.1

For $j < k \leq n$ , strict increase and positivity give $0 \leq ι (j) / ι (n) < 1$ , so every factor in step 1.1 lies in $(0, 1]$ . Thus the finite product lies in $[0, 1]$ , proving the displayed uniform bound.

step 1.1L2

3.1

For each of the finitely many $j < k$ , $ι (j) / ι (n) \to 0$ ; finite-product limit algebra makes the product in step 1.1 tend to $1$ . Multiplication by the fixed factor $1 / ι (k!)$ yields the limit.

step 1.1L2∎

Depends on

Used by

For every real x, (1+x/n)ⁿ→exp x Theorem

Dependency tree · two levels

57 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

MIT OpenCourseWare 18.100B Real Analysis, Spring 2025 full lecture notes (standard reference, not scraped)
J. Lebl, Basic Analysis, Analytic Functions (standard reference, not scraped)
J. Lebl, Basic Analysis, Logarithm and Exponential (standard reference, not scraped)
J. K. Hunter, An Introduction to Real Analysis, Chapter 10 (standard reference, not scraped)
R. Sedgewick and P. Flajolet, Analytic Combinatorics, Asymptotic Approximations (standard reference, not scraped)

For fixed kk, (nk)/nk(kn​)/nk tends to 1/k!1/k!