English
The ratio n! / n^n tends to 0 as n → ∞.
Русский
Отношение n! к n^n стремится к нулю при n → ∞.
LaTeX
$$$$\\\\lim_{n \\to \\infty} \\frac{n!}{n^n} = 0.$$$$
Lean4
theorem tendsto_factorial_div_pow_self_atTop : Tendsto (fun n ↦ n ! / (n : ℝ) ^ n : ℕ → ℝ) atTop (𝓝 0) :=
tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds (tendsto_const_div_atTop_nhds_zero_nat 1)
(Eventually.of_forall fun n ↦ div_nonneg (mod_cast n.factorial_pos.le) (pow_nonneg (mod_cast n.zero_le) _))
(by
refine (eventually_gt_atTop 0).mono fun n hn ↦ ?_
rcases Nat.exists_eq_succ_of_ne_zero hn.ne.symm with ⟨k, rfl⟩
rw [factorial_eq_prod_range_add_one, pow_eq_prod_const, div_eq_mul_inv, ← inv_eq_one_div, prod_natCast,
Nat.cast_succ, ← Finset.prod_inv_distrib, ← prod_mul_distrib, Finset.prod_range_succ']
simp only [one_mul, Nat.cast_add, zero_add, Nat.cast_one]
refine mul_le_of_le_one_left (inv_nonneg.mpr <| mod_cast hn.le) (prod_le_one ?_ ?_) <;> intro x hx <;>
rw [Finset.mem_range] at hx
· positivity
· refine (div_le_one <| mod_cast hn).mpr ?_
norm_cast
cutsat)
