Verified rational bounds for square roots

Rational lower and upper bounds for Real.sqrt of a rational interval are built via integer square roots (boundedSqrt/sqrtq), shown to converge, and assembled into ComputableℝSeq.Sqrt.sqrt. This yields an IsComputable instance for Real.sqrt and the golden ratio constants. The bound functions are executable; the packaged sequence mentions Real.sqrt itself as its reference value, so sqrt and the instances are noncomputable Lean terms.

theorem ComputableℝSeq.Sqrt.boundedSqrt_le_rsqrt (y : ℚ) (n b : ℕ) (hb : 0 < b) : ↑(mkRat (Int.sqrt (y.num * ↑b ^ n)) ((y.den * b ^ n).sqrt + 1)) ≤ √↑y

theorem ComputableℝSeq.Sqrt.rsqrt_le_boundedSqrt (y : ℚ) (n b : ℕ) (hb : 0 < b) : √↑y ≤ ↑(mkRat (Int.sqrt (y.num * ↑b ^ n) + 1) (y.den * b ^ n).sqrt)

def ComputableℝSeq.Sqrt.boundedSqrt (x : NonemptyInterval ℚ) (n b : ℕ) (hb : 0 < b) : NonemptyInterval ℚ

A version of square roots for rational intervals, that give an interval containing the actual square root, that are at most b^-n wider than the true interval.

Equations

• One or more equations did not get rendered due to their size.

def ComputableℝSeq.Sqrt.sqrtq (x : NonemptyInterval ℚ) (n : ℕ) : NonemptyInterval ℚ

Definition of sqrtq.

Equations

• ComputableℝSeq.Sqrt.sqrtq x n = if x.toProd.2 ≤ 0 then 0 else ComputableℝSeq.Sqrt.boundedSqrt x n 4 ComputableℝSeq.Sqrt.sqrtq._proof_1

theorem ComputableℝSeq.Sqrt.sqrt_lb_def (q : NonemptyInterval ℚ) (n : ℕ) : (sqrtq q n).toProd.1 = if q.toProd.2 ≤ 0 then 0 else mkRat (Int.sqrt (q.toProd.1.num * 4 ^ n)) ((q.toProd.1.den * 4 ^ n).sqrt + 1)

theorem ComputableℝSeq.Sqrt.sqrt_ub_def (q : NonemptyInterval ℚ) (n : ℕ) : (sqrtq q n).toProd.2 = if q.toProd.2 ≤ 0 then 0 else mkRat (Int.sqrt (q.toProd.2.num * 4 ^ n) + 1) (q.toProd.2.den * 4 ^ n).sqrt

theorem ComputableℝSeq.Sqrt.sqrtq_nonneg (q : NonemptyInterval ℚ) (n : ℕ) : 0 ≤ (sqrtq q n).toProd.1

theorem ComputableℝSeq.Sqrt.lb_le_sqrt_lb (q : NonemptyInterval ℚ) (n : ℕ) : ↑(sqrtq q n).toProd.1 ≤ √↑q.toProd.1

theorem ComputableℝSeq.Sqrt.sqrt_ub_le_ub (q : NonemptyInterval ℚ) (n : ℕ) : √↑q.toProd.2 ≤ ↑(sqrtq q n).toProd.2

theorem ComputableℝSeq.Sqrt.denom_err (x y ε : ℝ) (hy : y ≠ 0) (hyε : y + ε ≠ 0) : x / (y + ε) = x / y - x / y * ε / (y + ε)

This equality is a generally true way to "split a denominator", but is particularly useful as an approximation when ε is small compared to y, and we wish to approximate x / (y + ε) with x / y.

theorem ComputableℝSeq.Sqrt.sqrt_le_mkRat_add (q : ℚ) (n : ℕ) : √↑q ≤ ↑(mkRat (Int.sqrt (q.num * 4 ^ n)) ((q.den * 4 ^ n).sqrt + 1)) + 2 * √↑q / 2 ^ n

theorem ComputableℝSeq.Sqrt.mkRat_sub_le_sqrt (q : ℚ) (n : ℕ) : ↑(if q ≤ 0 then 0 else mkRat (Int.sqrt (q.num * 4 ^ n) + 1) (q.den * 4 ^ n).sqrt) - 7 * √↑q / 2 ^ n ≤ √↑q

theorem ComputableℝSeq.Sqrt.sqrt_le_sqrtq_add (r : ℝ) (x : NonemptyInterval ℚ) (n : ℕ) (hq : ↑x.toProd.1 ≤ r ∧ r ≤ ↑x.toProd.2) (hx : 0 < x.toProd.1) : √r ≤ ↑(sqrtq x n).toProd.1 + 2 * √r / 2 ^ n + (↑x.toProd.2 - ↑x.toProd.1) / (2 * √↑x.toProd.1)

The square root lower bound has an error that can be composed into one part 2 * √r / 2^n that decays with n, but depends on the value; and one part (x.snd - x.fst) / √r, that is proportional to width of the input interval.

theorem ComputableℝSeq.Sqrt.sqrt_le_sqrtq_add' (r : ℝ) (x : NonemptyInterval ℚ) (n : ℕ) (hq : ↑x.toProd.1 ≤ r ∧ r ≤ ↑x.toProd.2) (hr : 0 < r) : √r ≤ ↑(sqrtq x n).toProd.1 + 2 * √r / 2 ^ n + (↑x.toProd.2 - ↑x.toProd.1) / √r

Similar to sqrt_le_sqrtq_add, but doesn't require 0 < x.fst.

theorem ComputableℝSeq.Sqrt.sqrtq_sub_le_sqrt (r : ℝ) (x : NonemptyInterval ℚ) (n : ℕ) (hq : ↑x.toProd.1 ≤ r ∧ r ≤ ↑x.toProd.2) (hx : 0 < x.toProd.1) (hn : 3 ≤ n) : ↑(sqrtq x n).toProd.2 - 7 * √r / 2 ^ n - (↑x.toProd.2 - ↑x.toProd.1) / √↑x.toProd.1 ≤ √r

theorem ComputableℝSeq.Sqrt.sqrtq_sub_le_sqrt' (r : ℝ) (x : NonemptyInterval ℚ) (n : ℕ) (hq : ↑x.toProd.1 ≤ r ∧ r ≤ ↑x.toProd.2) (hr : 0 < r) (hn : 3 ≤ n) : ↑(sqrtq x n).toProd.2 - 7 * √r / 2 ^ n - (↑x.toProd.2 - ↑x.toProd.1) / √r ≤ √r

theorem ComputableℝSeq.Sqrt.TLUW_lower : TendstoLocallyUniformlyWithout (fun (n : ℕ) (x : ℚ) => (fun (n : ℕ) (q : ℚ) => mkRat (Int.sqrt (q.num * 4 ^ n)) ((q.den * 4 ^ n).sqrt + 1)) n x) fun (q : ℝ) => √q

theorem ComputableℝSeq.Sqrt.TLUW_upper : TendstoLocallyUniformlyWithout (fun (n : ℕ) (x : ℚ) => (fun (n : ℕ) (q : ℚ) => if q ≤ 0 then 0 else mkRat (Int.sqrt (q.num * 4 ^ n) + 1) (q.den * 4 ^ n).sqrt) n x) fun (q : ℝ) => √q

noncomputable def ComputableℝSeq.Sqrt.sqrt : ComputableℝSeq → ComputableℝSeq

Definition of sqrt.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

noncomputable instance IsComputable.instComputableSqrt (x : ℝ) [hx : IsComputable x] : IsComputable √x

Equations

• IsComputable.instComputableSqrt x = IsComputable.lift Real.sqrt ComputableℝSeq.Sqrt.sqrt IsComputable.instComputableSqrt._proof_1 hx

@[implicit_reducible]

noncomputable instance IsComputable.instComputableGoldenRatio : IsComputable Real.goldenRatio

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

noncomputable instance IsComputable.instComputableGoldenConj : IsComputable Real.goldenConj

Equations

• One or more equations did not get rendered due to their size.