Rational Utility

Helper functions and lemmas for constructing rational numbers with prescribed square bounds.

def findRationalWithSquareBetween (lower upper : ℚ) (_h0 : 0 ≤ lower) (_hlt : lower < upper) : ℚ

Helper function to find a positive rational number whose square is between two given rationals. Assumes 0 ≤ lower and lower < upper.

Construction: Let N = ⌈(upper+1)/(upper-lower)⌉ + 1 and m = Nat.sqrt ⌊N²·lower⌋ + 1. Return m / N. The choice of N ensures N·(√upper − √lower) ≥ 1, which bounds m above by N·√upper, so (m/N)² ≤ upper. The floor construction ensures (m/N)² > lower.

Equations

• findRationalWithSquareBetween lower upper _h0 _hlt = (↑⌊lower * ↑(⌈(upper + 1) / (upper - lower)⌉.toNat + 1) ^ 2⌋.toNat.sqrt + 1) / ↑(⌈(upper + 1) / (upper - lower)⌉.toNat + 1)

theorem findRationalWithSquareBetween_positive (lower upper : ℚ) (h0 : 0 ≤ lower) (hlt : lower < upper) : 0 < findRationalWithSquareBetween lower upper h0 hlt

theorem findRationalWithSquareBetween_spec (lower upper : ℚ) (h0 : 0 ≤ lower) (hlt : lower < upper) : have r := findRationalWithSquareBetween lower upper h0 hlt; lower ≤ r * r ∧ r * r ≤ upper