Intervals with Real Endpoints

This file defines IntervalReal, an interval type with real (ℝ) endpoints. Unlike IntervalRat (which has rational endpoints and is suitable for computation), IntervalReal allows us to represent intervals involving transcendental values like [1, Real.exp 1] or [Real.log 2, π].

Main definitions

• IntervalReal - Intervals with real endpoints
• expInterval - Interval bound for exp
• logInterval - Interval bound for log (on positive intervals)

Main theorems

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

Design notes

This type complements IntervalRat for proving facts about transcendental functions. While IntervalRat is used for numerical computation (since rationals are computable), IntervalReal is used for correctness proofs involving exp, log, etc.

Typical workflow:

1. Use IntervalRat for actual interval arithmetic computations
2. Convert to IntervalReal when proving facts about transcendental functions
3. Use mathlib's analysis lemmas directly on real intervals

structure LeanCert.Core.IntervalReal : Type

An interval with real endpoints

• lo : ℝ
• hi : ℝ
• le : self.lo ≤ self.hi

def LeanCert.Core.IntervalReal.toSet (I : IntervalReal) : Set ℝ

The set of reals contained in this interval

Equations

• I.toSet = Set.Icc I.lo I.hi

instance LeanCert.Core.IntervalReal.instMembershipReal : Membership ℝ IntervalReal

Membership in an interval

Equations

• LeanCert.Core.IntervalReal.instMembershipReal = { mem := fun (I : LeanCert.Core.IntervalReal) (x : ℝ) => I.lo ≤ x ∧ x ≤ I.hi }

@[simp]

theorem LeanCert.Core.IntervalReal.mem_def (x : ℝ) (I : IntervalReal) : x ∈ I ↔ I.lo ≤ x ∧ x ≤ I.hi

theorem LeanCert.Core.IntervalReal.mem_toSet_iff (x : ℝ) (I : IntervalReal) : x ∈ I.toSet ↔ x ∈ I

def LeanCert.Core.IntervalReal.singleton (r : ℝ) : IntervalReal

Create an interval from a single real

Equations

• LeanCert.Core.IntervalReal.singleton r = { lo := r, hi := r, le := ⋯ }

theorem LeanCert.Core.IntervalReal.mem_singleton (r : ℝ) : r ∈ singleton r

def LeanCert.Core.IntervalReal.ofRat (I : IntervalRat) : IntervalReal

Convert from IntervalRat to IntervalReal

Equations

• LeanCert.Core.IntervalReal.ofRat I = { lo := ↑I.lo, hi := ↑I.hi, le := ⋯ }

theorem LeanCert.Core.IntervalReal.mem_ofRat {x : ℝ} {I : IntervalRat} (hx : x ∈ I) : x ∈ ofRat I

Interval addition

def LeanCert.Core.IntervalReal.add (I J : IntervalReal) : IntervalReal

Add two intervals

Equations

• I.add J = { lo := I.lo + J.lo, hi := I.hi + J.hi, le := ⋯ }

theorem LeanCert.Core.IntervalReal.mem_add {x y : ℝ} {I J : IntervalReal} (hx : x ∈ I) (hy : y ∈ J) : x + y ∈ I.add J

FTIA for addition

Interval negation

def LeanCert.Core.IntervalReal.neg (I : IntervalReal) : IntervalReal

Negate an interval

Equations

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

theorem LeanCert.Core.IntervalReal.mem_neg {x : ℝ} {I : IntervalReal} (hx : x ∈ I) : -x ∈ I.neg

FTIA for negation

Interval multiplication

def LeanCert.Core.IntervalReal.mul (I J : IntervalReal) : IntervalReal

Multiply two intervals

Equations

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

Exponential interval

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

Interval bound for exp. Since exp is strictly increasing, exp([a,b]) = [exp(a), exp(b)].

Equations

• I.expInterval = { lo := Real.exp I.lo, hi := Real.exp I.hi, le := ⋯ }

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

FTIA for exp: if x ∈ [a,b], then exp(x) ∈ [exp(a), exp(b)]. This is FULLY PROVED - no sorry, no axioms.

Logarithm interval (for positive intervals)

structure LeanCert.Core.IntervalReal.IntervalRealPosextends LeanCert.Core.IntervalReal : Type

An interval that is strictly positive

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

noncomputable def LeanCert.Core.IntervalReal.logInterval (I : IntervalRealPos) : IntervalReal

Interval bound for log on positive intervals. Since log is strictly increasing on (0, ∞), log([a,b]) = [log(a), log(b)] for a > 0.

Equations

• LeanCert.Core.IntervalReal.logInterval I = { lo := Real.log I.lo, hi := Real.log I.hi, le := ⋯ }

theorem LeanCert.Core.IntervalReal.mem_logInterval {x : ℝ} {I : IntervalRealPos} (hx : x ∈ I.toIntervalReal) : Real.log x ∈ logInterval I

FTIA for log: if x ∈ [a,b] with a > 0, then log(x) ∈ [log(a), log(b)]. This is FULLY PROVED - no sorry, no axioms.

Trigonometric intervals (global bounds)

def LeanCert.Core.IntervalReal.sinInterval (_I : IntervalReal) : IntervalReal

Interval bound for sin. Since |sin x| ≤ 1 for all x, we use [-1, 1].

Equations

• _I.sinInterval = { lo := -1, hi := 1, le := LeanCert.Core.IntervalReal.sinInterval._proof_1 }

theorem LeanCert.Core.IntervalReal.mem_sinInterval {x : ℝ} {I : IntervalReal} (_hx : x ∈ I) : Real.sin x ∈ I.sinInterval

FTIA for sin

def LeanCert.Core.IntervalReal.cosInterval (_I : IntervalReal) : IntervalReal

Interval bound for cos. Since |cos x| ≤ 1 for all x, we use [-1, 1].

Equations

• _I.cosInterval = { lo := -1, hi := 1, le := LeanCert.Core.IntervalReal.sinInterval._proof_1 }

theorem LeanCert.Core.IntervalReal.mem_cosInterval {x : ℝ} {I : IntervalReal} (_hx : x ∈ I) : Real.cos x ∈ I.cosInterval

FTIA for cos

def LeanCert.Core.IntervalReal.atanInterval (_I : IntervalReal) : IntervalReal

Interval bound for atan. Since arctan x ∈ (-π/2, π/2) ⊂ [-2, 2] for all x.

Equations

• _I.atanInterval = { lo := -2, hi := 2, le := LeanCert.Core.IntervalReal.atanInterval._proof_2 }

theorem LeanCert.Core.IntervalReal.mem_atanInterval {x : ℝ} {I : IntervalReal} (_hx : x ∈ I) : Real.arctan x ∈ I.atanInterval

FTIA for atan

theorem LeanCert.Core.IntervalReal.abs_arsinh_le_abs (x : ℝ) : |Real.arsinh x| ≤ |x|

|arsinh x| ≤ |x| for all x. This follows from MVT and |arsinh'| ≤ 1.

def LeanCert.Core.IntervalReal.arsinhInterval (I : IntervalReal) : IntervalReal

Interval bound for arsinh. Uses a conservative bound based on input interval.

Equations

• I.arsinhInterval = { lo := -(max |I.lo| |I.hi| + 1), hi := max |I.lo| |I.hi| + 1, le := ⋯ }

theorem LeanCert.Core.IntervalReal.mem_arsinhInterval {x : ℝ} {I : IntervalReal} (hx : x ∈ I) : Real.arsinh x ∈ I.arsinhInterval

FTIA for arsinh

Hyperbolic function intervals

noncomputable def LeanCert.Core.IntervalReal.sinhInterval (I : IntervalReal) : IntervalReal

Interval bound for sinh. Since sinh is strictly monotonic increasing, sinh([a,b]) = [sinh(a), sinh(b)].

Equations

• I.sinhInterval = { lo := Real.sinh I.lo, hi := Real.sinh I.hi, le := ⋯ }

theorem LeanCert.Core.IntervalReal.mem_sinhInterval {x : ℝ} {I : IntervalReal} (hx : x ∈ I) : Real.sinh x ∈ I.sinhInterval

FTIA for sinh: if x ∈ [a,b], then sinh(x) ∈ [sinh(a), sinh(b)]. This is FULLY PROVED - no sorry, no axioms.

noncomputable def LeanCert.Core.IntervalReal.coshInterval (I : IntervalReal) : IntervalReal

Interval bound for cosh. cosh is convex with minimum at 0:

• If interval is all non-negative: cosh is increasing
• If interval is all non-positive: cosh is decreasing
• If interval contains 0: minimum is cosh(0) = 1, max is at endpoints

Equations

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

theorem LeanCert.Core.IntervalReal.mem_coshInterval {x : ℝ} {I : IntervalReal} (hx : x ∈ I) : Real.cosh x ∈ I.coshInterval

FTIA for cosh: if x ∈ [a,b], then cosh(x) ∈ coshInterval([a,b]). This is FULLY PROVED - no sorry, no axioms.

Square root interval

noncomputable def LeanCert.Core.IntervalReal.sqrtInterval (I : IntervalReal) : IntervalReal

Interval bound for sqrt. For any interval I, sqrt(x) ∈ [0, max(hi, 1)] for x ∈ I. This is always sound because:

• sqrt(x) ≥ 0 for all x (Mathlib convention: sqrt(negative) = 0)
• sqrt(x) ≤ max(x, 1) for x ≥ 0, so sqrt(x) ≤ max(hi, 1)

Equations

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

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

FTIA for sqrt: if x ∈ I, then sqrt(x) ∈ sqrtInterval(I). Works for all x including negative (where sqrt returns 0 by Mathlib convention).