lt_ratSqrt_add_inv_prec_sq — Mathlib

English

For x ∈ ℕ and prec > 0, x < (ratSqrt(x, prec) + 1/prec)^2.

Русский

Для натурального x и prec > 0 верно x < (ratSqrt(x, prec) + 1/prec)^2.

LaTeX

$$$ x < (\operatorname{ratSqrt}(x, \operatorname{prec}) + \frac{1}{\operatorname{prec}})^2, \quad (0 < \operatorname{prec}) $$$

Lean4

theorem lt_ratSqrt_add_inv_prec_sq (x : ℕ) {prec : ℕ} (h : 0 < prec) : x < (ratSqrt x prec + 1 / prec) ^ 2 :=
  by
  unfold ratSqrt
  rw [← mul_lt_mul_iff_of_pos_right (a := (prec ^ 2 : ℚ)) (by positivity)]
  rw [← mul_pow, add_mul]
  rw [div_mul_cancel₀, div_mul_cancel₀]
  · norm_cast
    exact lt_succ_sqrt' (x * prec ^ 2)
  all_goals norm_cast; positivity

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