Limits of binomial coefficients along proportional sequences #
For fixed k, the leading term of a.choose k is a ^ k / k!. This file records the
corresponding limit when a and the normalizing denominator vary together: if a i / b i
converges to x and b i⁻¹ converges to zero, then
(a i).choose k / (b i) ^ k → x ^ k / k!.
The statement includes boundary limits such as x = 0; no divergence hypothesis on a is
needed. It is useful for finite-population limits, where one of a population and its complement
may stay bounded.
Main result #
TauCeti.tendsto_choose_div_pow_of_tendsto_div— the normalized fixed-order binomial coefficient along an asymptotically proportional sequence.
theorem
TauCeti.tendsto_choose_div_pow_of_tendsto_div
{α : Type u_1}
{l : Filter α}
{a : α → ℕ}
{b : α → ℝ}
{x : ℝ}
(hab : Filter.Tendsto (fun (i : α) => ↑(a i) / b i) l (nhds x))
(hb : Filter.Tendsto (fun (i : α) => (b i)⁻¹) l (nhds 0))
(k : ℕ)
:
A fixed-order binomial coefficient has its expected leading-term limit along any sequence whose ratio to a common denominator converges.
The separate hypothesis that the inverse denominator tends to zero makes the statement applicable to denominators other than the natural index.