Rational Endpoint Intervals - Transcendental Functions

This file provides noncomputable interval bounds for transcendental functions using floor/ceiling to obtain rational endpoints.

Main definitions

• ofRealEndpoints - Create rational interval from real bounds using floor/ceil
• expInterval - Interval bound for exponential
• logInterval - Interval bound for logarithm (positive intervals)
• atanhIntervalComputed - Interval bound for atanh (intervals in (-1, 1))
• sqrtInterval - Interval bound for square root

Main theorems

• mem_expInterval - FTIA for exp
• mem_logInterval - FTIA for log
• mem_atanhIntervalComputed - FTIA for atanh
• mem_sqrtInterval - FTIA for sqrt

Design notes

All definitions in this file are noncomputable as they use Real.exp, Real.log, etc. For computable versions, see IntervalRat.Taylor.

Rational enclosure of real intervals

noncomputable def LeanCert.Core.IntervalRat.ofRealEndpoints (lo hi : ℝ) (hle : lo ≤ hi) : IntervalRat

Coarse rational enclosure of a real interval using floor/ceil. Given a real interval [lo, hi], returns a rational interval [⌊lo⌋, ⌈hi⌉] that is guaranteed to contain all points in the original interval.

Equations

• LeanCert.Core.IntervalRat.ofRealEndpoints lo hi hle = { lo := ↑⌊lo⌋, hi := ↑⌈hi⌉, le := ⋯ }

theorem LeanCert.Core.IntervalRat.mem_ofRealEndpoints {x lo hi : ℝ} (hle : lo ≤ hi) (hx : lo ≤ x ∧ x ≤ hi) : x ∈ ofRealEndpoints lo hi hle

Any point in [lo, hi] is in the rational enclosure [⌊lo⌋, ⌈hi⌉]

Exponential interval

noncomputable def LeanCert.Core.IntervalRat.expInterval (I : IntervalRat) : IntervalRat

Interval bound for exp on rational intervals. Since exp is strictly increasing, exp([a,b]) ⊆ [⌊exp(a)⌋, ⌈exp(b)⌉]. This uses Real.exp and floor/ceil to get rational bounds.

Equations

• I.expInterval = LeanCert.Core.IntervalRat.ofRealEndpoints (Real.exp ↑I.lo) (Real.exp ↑I.hi) ⋯

theorem LeanCert.Core.IntervalRat.mem_expInterval {x : ℝ} {I : IntervalRat} (hx : x ∈ I) : Real.exp x ∈ I.expInterval

FTIA for exp: if x ∈ I, then exp(x) ∈ expInterval(I)

Positive interval check

def LeanCert.Core.IntervalRat.isPositive (I : IntervalRat) : Prop

Check if an interval is strictly positive (lo > 0)

Equations

• I.isPositive = (0 < I.lo)

instance LeanCert.Core.IntervalRat.instDecidableIsPositive (I : IntervalRat) : Decidable I.isPositive

Decidable isPositive

Equations

• I.instDecidableIsPositive = inferInstanceAs (Decidable (0 < I.lo))

structure LeanCert.Core.IntervalRat.IntervalRatPosextends LeanCert.Core.IntervalRat : Type

An interval that is guaranteed to be strictly positive

• lo : ℚ
• hi : ℚ
• le : self.lo ≤ self.hi
• lo_pos : 0 < self.lo

Logarithm interval (for positive intervals)

noncomputable def LeanCert.Core.IntervalRat.logInterval (I : IntervalRatPos) : IntervalRat

Interval bound for log on positive rational intervals. Since log is strictly increasing on (0, ∞), log([a,b]) ⊆ [⌊log(a)⌋, ⌈log(b)⌉] for a > 0. This uses Real.log and floor/ceil to get rational bounds.

Equations

• LeanCert.Core.IntervalRat.logInterval I = LeanCert.Core.IntervalRat.ofRealEndpoints (Real.log ↑I.lo) (Real.log ↑I.hi) ⋯

theorem LeanCert.Core.IntervalRat.mem_logInterval {x : ℝ} {I : IntervalRatPos} (hx : x ∈ I.toIntervalRat) : Real.log x ∈ logInterval I

FTIA for log: if x ∈ I with lo > 0, then log(x) ∈ logInterval(I)

Atanh interval (for intervals in (-1, 1))

structure LeanCert.Core.IntervalRat.IntervalRatInUnitBall : Type

An interval strictly contained in (-1, 1), suitable for atanh

• lo : ℚ
• hi : ℚ
• le : self.lo ≤ self.hi
• lo_gt : -1 < self.lo
• hi_lt : self.hi < 1

def LeanCert.Core.IntervalRat.IntervalRatInUnitBall.toIntervalRat (I : IntervalRatInUnitBall) : IntervalRat

Convert to standard interval

Equations

• I.toIntervalRat = { lo := I.lo, hi := I.hi, le := ⋯ }

instance LeanCert.Core.IntervalRat.instMembershipRealIntervalRatInUnitBall : Membership ℝ IntervalRatInUnitBall

Membership in the underlying interval

Equations

• LeanCert.Core.IntervalRat.instMembershipRealIntervalRatInUnitBall = { mem := fun (I : LeanCert.Core.IntervalRat.IntervalRatInUnitBall) (x : ℝ) => ↑I.lo ≤ x ∧ x ≤ ↑I.hi }

theorem LeanCert.Core.IntervalRat.IntervalRatInUnitBall.mem_def {x : ℝ} {I : IntervalRatInUnitBall} : x ∈ I ↔ ↑I.lo ≤ x ∧ x ≤ ↑I.hi

noncomputable def LeanCert.Core.IntervalRat.atanhIntervalComputed (I : IntervalRatInUnitBall) : IntervalRat

Interval bound for atanh on intervals strictly inside (-1, 1). Since atanh is strictly increasing on (-1, 1), atanh([a,b]) ⊆ [⌊atanh(a)⌋, ⌈atanh(b)⌉].

Equations

• LeanCert.Core.IntervalRat.atanhIntervalComputed I = LeanCert.Core.IntervalRat.ofRealEndpoints (LeanCert.Core.Real.atanh ↑I.lo) (LeanCert.Core.Real.atanh ↑I.hi) ⋯

theorem LeanCert.Core.IntervalRat.mem_atanhIntervalComputed {x : ℝ} {I : IntervalRatInUnitBall} (hx : x ∈ I) : Real.atanh x ∈ atanhIntervalComputed I

FTIA for atanh: if x ∈ I and I ⊂ (-1, 1), then atanh(x) ∈ atanhIntervalComputed(I)

Square Root Interval

def LeanCert.Core.IntervalRat.intSqrtNat (n : ℕ) : ℕ

Integer square root (floor of sqrt). Satisfies: (intSqrtNat n)^2 ≤ n < (intSqrtNat n + 1)^2

Equations

• LeanCert.Core.IntervalRat.intSqrtNat n = n.sqrt

def LeanCert.Core.IntervalRat.sqrtRatLower (q : ℚ) : ℚ

Rational lower bound for sqrt. For q ≥ 0 with q = num/den, we compute floor(sqrt(num * den)) / den. This gives: sqrtRatLower q ≤ sqrt(q).

The idea: sqrt(num/den) = sqrt(num*den)/den when properly scaled.

Equations

• LeanCert.Core.IntervalRat.sqrtRatLower q = if q ≤ 0 then 0 else have num := q.num.natAbs; have den := q.den; have s := LeanCert.Core.IntervalRat.intSqrtNat (num * den); ↑s / ↑den

def LeanCert.Core.IntervalRat.sqrtRatUpper (q : ℚ) : ℚ

Rational upper bound for sqrt. For q ≥ 0, we compute ceil(sqrt(num * den)) / den. This gives: sqrt(q) ≤ sqrtRatUpper q.

Equations

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

def LeanCert.Core.IntervalRat.sqrtRatLowerPrec (q : ℚ) (scaleBits : ℕ := LeanCert.Core.IntervalRat.sqrtScaleBits✝) : ℚ

Rational lower bound for sqrt with high precision. For q ≥ 0, we scale by 4^k, compute integer sqrt, and scale back by 2^k. This gives: sqrtRatLowerPrec q ≤ sqrt(q) with precision ~2^(-k).

Equations

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

def LeanCert.Core.IntervalRat.sqrtRatUpperPrec (q : ℚ) (scaleBits : ℕ := LeanCert.Core.IntervalRat.sqrtScaleBits✝) : ℚ

Rational upper bound for sqrt with high precision. For q ≥ 0, we scale by 4^k, compute ceil of integer sqrt, and scale back by 2^k. This gives: sqrt(q) ≤ sqrtRatUpperPrec q with precision ~2^(-k).

Equations

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

theorem LeanCert.Core.IntervalRat.sqrtRatLower_le_sqrt {q : ℚ} (hq : 0 ≤ q) : ↑(sqrtRatLower q) ≤ √↑q

Soundness of sqrtRatLower: sqrtRatLower q ≤ Real.sqrt q for q ≥ 0

theorem LeanCert.Core.IntervalRat.sqrt_le_sqrtRatUpper {q : ℚ} (hq : 0 ≤ q) : √↑q ≤ ↑(sqrtRatUpper q)

Soundness of sqrtRatUpper: Real.sqrt q ≤ sqrtRatUpper q for q ≥ 0

def LeanCert.Core.IntervalRat.sqrtInterval (I : IntervalRat) : IntervalRat

Square root interval with conservative bounds. For a non-negative interval [lo, hi], sqrt is monotone so: sqrt([lo, hi]) ⊆ [0, max(hi, 1)]

The lower bound is 0 (always sound for sqrt). The upper bound uses max(hi, 1) which satisfies sqrt(x) ≤ max(x, 1) for x ≥ 0.

Equations

• I.sqrtInterval = { lo := 0, hi := max I.hi 1, le := ⋯ }

def LeanCert.Core.IntervalRat.sqrtIntervalTight (I : IntervalRat) : IntervalRat

Improved square root interval with tight lower bounds. For a non-negative interval [lo, hi] with lo ≥ 0:

• Lower bound: sqrtRatLower(lo)
• Upper bound: sqrtRatUpper(hi)

For intervals crossing zero, we use 0 as lower bound.

Equations

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

theorem LeanCert.Core.IntervalRat.sqrtRatLowerPrec_le_sqrt {q : ℚ} (hq : 0 ≤ q) (k : ℕ) : ↑(sqrtRatLowerPrec q k) ≤ √↑q

Soundness of sqrtRatLowerPrec: sqrtRatLowerPrec q k ≤ Real.sqrt q for q ≥ 0

theorem LeanCert.Core.IntervalRat.sqrt_le_sqrtRatUpperPrec {q : ℚ} (hq : 0 ≤ q) (k : ℕ) : √↑q ≤ ↑(sqrtRatUpperPrec q k)

Soundness of sqrtRatUpperPrec: Real.sqrt q ≤ sqrtRatUpperPrec q k for q ≥ 0

def LeanCert.Core.IntervalRat.sqrtIntervalTightPrec (I : IntervalRat) : IntervalRat

High-precision square root interval. For a non-negative interval [lo, hi] with lo ≥ 0:

• Lower bound: sqrtRatLowerPrec(lo)
• Upper bound: sqrtRatUpperPrec(hi)

Uses scaling to achieve ~6 decimal digits of precision.

Equations

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

theorem LeanCert.Core.IntervalRat.mem_sqrtIntervalTightPrec' {x : ℝ} {I : IntervalRat} (hx : x ∈ I) : √x ∈ I.sqrtIntervalTightPrec

Membership theorem for sqrtIntervalTightPrec

theorem LeanCert.Core.IntervalRat.mem_sqrtInterval {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (hx_nn : 0 ≤ x) : √x ∈ I.sqrtInterval

Soundness of sqrt interval: if x ∈ I and x ≥ 0, then sqrt(x) ∈ sqrtInterval I

theorem LeanCert.Core.IntervalRat.mem_sqrtInterval' {x : ℝ} {I : IntervalRat} (hx : x ∈ I) : √x ∈ I.sqrtInterval

General soundness of sqrt interval: works for any x ∈ I (including negative). When x < 0, Real.sqrt x = 0, which is always in [0, max(hi, 1)].

theorem LeanCert.Core.IntervalRat.mem_sqrtIntervalTight {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (hx_nn : 0 ≤ x) : √x ∈ I.sqrtIntervalTight

Soundness of tight sqrt interval: if x ∈ I and x ≥ 0, then sqrt(x) ∈ sqrtIntervalTight I

theorem LeanCert.Core.IntervalRat.mem_sqrtIntervalTight' {x : ℝ} {I : IntervalRat} (hx : x ∈ I) : √x ∈ I.sqrtIntervalTight

General soundness of tight sqrt interval: works for any x ∈ I (including negative). When x < 0, Real.sqrt x = 0, which is always in the result interval.