le_pow_log — Mathlib

English

If f is not bounded by 1, there exists n0>1 with f(n0)>1.

Русский

Если f не ограничено единицей, существует n0>1 с f(n0)>1.

LaTeX

$$∃ n0:ℕ, 1 < n0 ∧ 1 < f(n0)$$

Lean4

/-- Given two natural numbers `n, m` greater than 1 we have `f n ≤ f m ^ logb m n`. -/
theorem le_pow_log : f n ≤ f m ^ logb m n :=
  by
  have : Tendsto (fun k : ℕ ↦ (m * f m / (f m - 1)) ^ (k : ℝ)⁻¹ * f m ^ logb m n) atTop (𝓝 (f m ^ logb m n)) :=
    by
    nth_rw 2 [← one_mul (f ↑m ^ logb ↑m ↑n)]
    exact (tendsto_const_rpow_inv (expr_pos hm notbdd)).mul_const _
  exact
    le_of_tendsto_of_tendsto (tendsto_const_nhds (x := f ↑n)) this <|
      eventually_atTop.mpr ⟨2, fun b hb ↦ param_upperbound hm hn notbdd (ne_zero_of_lt hb)⟩

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