realSqrt_lt_ratSqrt_add_inv_prec — Mathlib

English

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

Русский

Для x ∈ ℕ и prec > 0 верно √x < ratSqrt(x, prec) + 1/prec.

LaTeX

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

Lean4

theorem realSqrt_lt_ratSqrt_add_inv_prec (x : ℕ) {prec : ℕ} (h : 0 < prec) : √x < ratSqrt x prec + 1 / prec :=
  by
  have := lt_ratSqrt_add_inv_prec_sq (x := x) h
  have : (x : ℝ) < ↑((x.ratSqrt prec + 1 / prec) ^ 2 : ℚ) := by norm_cast
  have := Real.sqrt_lt_sqrt (by simp) this
  rw [Rat.cast_pow, Real.sqrt_sq] at this
  · push_cast at this
    exact this
  · push_cast
    exact add_nonneg (by simpa using ratSqrt_nonneg _ _) (by simp)

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