eventually_pow_one_div_le — Mathlib

English

For x ≥ 0 and y > 1, there exists N such that for all n ≥ N, x^(1/n) ≤ y.

Русский

Для x ≥ 0 и y > 1 существует N such that для всех n ≥ N выполняется x^{1/n} ≤ y.

LaTeX

$$$$\forall x\in\mathbb{R}_{\ge 0},\forall y>1,\ \exists N\in\mathbb{N},\forall n\ge N: x^{1/n} \le y.$$$$

Lean4

theorem eventually_pow_one_div_le (x : ℝ≥0) {y : ℝ≥0} (hy : 1 < y) : ∀ᶠ n : ℕ in atTop, x ^ (1 / n : ℝ) ≤ y :=
  by
  obtain ⟨m, hm⟩ := add_one_pow_unbounded_of_pos x (tsub_pos_of_lt hy)
  rw [tsub_add_cancel_of_le hy.le] at hm
  refine eventually_atTop.2 ⟨m + 1, fun n hn => ?_⟩
  simp only [one_div]
  simpa only [NNReal.rpow_inv_le_iff (Nat.cast_pos.2 <| m.succ_pos.trans_le hn), NNReal.rpow_natCast] using
    hm.le.trans (pow_right_mono₀ hy.le (m.le_succ.trans hn))

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