Binomial coefficients and factorial variants

This file proves asymptotic theorems for binomial coefficients and factorial variants.

Main statements

• isEquivalent_descFactorial is the proof that n.descFactorial k ~ n^k as n → ∞.
• isEquivalent_choose is the proof that n.choose k ~ n^k / k! as n → ∞.
• isTheta_choose is the proof that n.choose k = Θ(n^k) as n → ∞.

theorem isEquivalent_descFactorial (k : ℕ) : Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => ↑(n.descFactorial k)) fun (n : ℕ) => ↑n ^ k

n.descFactorial k is asymptotically equivalent to n^k.

theorem isEquivalent_choose (k : ℕ) : Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => ↑(n.choose k)) fun (n : ℕ) => ↑n ^ k / ↑k.factorial

n.choose k is asymptotically equivalent to n^k / k!.

theorem isTheta_choose (k : ℕ) : (fun (n : ℕ) => ↑(n.choose k)) =Θ[Filter.atTop] fun (n : ℕ) => ↑n ^ k

n.choose k is big-theta n^k.