English
For m ≥ 2, the bound (1 − 1/m)^{-1} · (1 / m^{(n+1)!}) is bounded by 1 / (m^{n!})^{n} for all n ∈ ℕ.
Русский
При m ≥ 2 неравенство (1 − 1/m)^{-1} · (1 / m^{(n+1)!}) ≤ 1 / (m^{n!})^{n} выполняется для всех n ∈ ℕ.
LaTeX
$$$ \forall n \in \mathbb N,\ \forall m \in \mathbb R,\ 2 \le m \Rightarrow \left(1 - \frac{1}{m}\right)^{-1} \cdot \frac{1}{m^{(n+1)!}} \le \frac{1}{(m^{n!})^{n}}$$$
Lean4
theorem aux_calc (n : ℕ) {m : ℝ} (hm : 2 ≤ m) : (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!) ≤ 1 / (m ^ n !) ^ n :=
calc
(1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!) ≤ 2 * (1 / m ^ (n + 1)!) := by
-- the second factors coincide (and are non-negative),
-- the first factors satisfy the inequality `sub_one_div_inv_le_two`
gcongr; exact sub_one_div_inv_le_two hm
_ = 2 / m ^ (n + 1)! := (mul_one_div 2 _)
_ = 2 / m ^ (n ! * (n + 1)) := (congr_arg (2 / ·) (congr_arg (Pow.pow m) (mul_comm _ _)))
_ ≤ 1 / (m ^ n !) ^ n := by
-- Clear denominators and massage*
rw [← pow_mul, div_le_div_iff₀, one_mul, mul_add_one, pow_add, mul_comm 2]
· gcongr
-- `2 ≤ m ^ n!` is a consequence of monotonicity of exponentiation at `2 ≤ m`.
exact hm.trans <| le_self_pow₀ (one_le_two.trans hm) <| by positivity
all_goals positivity
