isTheta_choose — Mathlib

English

For each k, the sequence n ↦ n.choose k is Θ(n^k) as n → ∞.

Русский

Для каждого фиксированного k последовательность n ↦ n.choose k стремится к Θ(n^k) при n → ∞.

LaTeX

$$$ (\lambda n : \mathbb{N}) \mapsto (n.\mathrm{choose}\ k : \mathbb{R}) =_\Theta_{atTop} (\lambda n : \mathbb{N}) \mapsto (n^k : \mathbb{R}) $$$

Lean4

/-- `n.choose k` is big-theta `n^k`. -/
theorem isTheta_choose (k : ℕ) : (fun (n : ℕ) ↦ (n.choose k : ℝ)) =Θ[atTop] (fun (n : ℕ) ↦ (n ^ k : ℝ)) :=
  by
  apply (isEquivalent_choose k).trans_isTheta
  simp_rw [div_eq_mul_inv, mul_comm _ (_⁻¹)]
  exact isTheta_rfl.const_mul_left <| inv_ne_zero (mod_cast k.factorial_ne_zero)

Похожие утверждения