Documentation

Mathlib.Data.Rat.NatSqrt.Defs

Rational approximations to square roots of naturals #

This file defines Nat.ratSqrt x prec, a rational approximation of the square root of a natural number x to within 1 / prec, and proves the basic bounds it satisfies.

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

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

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

Equations
Instances For
    source
    theorem Nat.ratSqrt_nonneg (x prec : ℕ) :
    0 ≤ x.ratSqrt prec
    source
    theorem Nat.ratSqrt_sq_le (x : ℕ) {prec : ℕ} (h : 0 < prec) :
    x.ratSqrt prec ^ 2 ≤ ↑x
    source
    theorem Nat.lt_ratSqrt_add_inv_prec_sq (x : ℕ) {prec : ℕ} (h : 0 < prec) :
    ↑x < (x.ratSqrt prec + 1 / ↑prec) ^ 2