Rational approximation of the square root of a natural number.

See also Mathlib.Data.Rat.NatSqrt.Real for comparisons with the real square root.

def Nat.ratSqrt (x prec : ℕ) : ℚ

Approximate the square root of a natural number as a rational number, to within 1 / prec.

Equations

• x.ratSqrt prec = ↑(x * prec ^ 2).sqrt / ↑prec

theorem Nat.ratSqrt_nonneg (x prec : ℕ) : 0 ≤ x.ratSqrt prec

theorem Nat.ratSqrt_sq_le (x : ℕ) {prec : ℕ} (h : 0 < prec) : x.ratSqrt prec ^ 2 ≤ ↑x

theorem Nat.lt_ratSqrt_add_inv_prec_sq (x : ℕ) {prec : ℕ} (h : 0 < prec) : ↑x < (x.ratSqrt prec + 1 / ↑prec) ^ 2