Exact rational interval arithmetic

The intervals in this file have rational endpoints, while their semantics is over the real numbers. The operations provide the enclosure primitives used by the radical-expression evaluator, with soundness checked by the kernel.

structure LeanPool.Besicovitch.RationalInterval : Type

A nonempty closed interval with rational endpoints.

• lower : ℚ

  The lower rational endpoint.

• upper : ℚ

  The upper rational endpoint.

• lower_le_upper : self.lower ≤ self.upper

def LeanPool.Besicovitch.RationalInterval.Contains (I : RationalInterval) (x : ℝ) : Prop

A real number belongs to a rational interval.

Equations

• I.Contains x = (↑I.lower ≤ x ∧ x ≤ ↑I.upper)

def LeanPool.Besicovitch.RationalInterval.singleton (q : ℚ) : RationalInterval

The degenerate interval containing one rational number.

Equations

• LeanPool.Besicovitch.RationalInterval.singleton q = { lower := q, upper := q, lower_le_upper := ⋯ }

def LeanPool.Besicovitch.RationalInterval.add (I J : RationalInterval) : RationalInterval

The interval sum.

Equations

• I.add J = { lower := I.lower + J.lower, upper := I.upper + J.upper, lower_le_upper := ⋯ }

def LeanPool.Besicovitch.RationalInterval.neg (I : RationalInterval) : RationalInterval

The additive inverse of an interval.

Equations

• I.neg = { lower := -I.upper, upper := -I.lower, lower_le_upper := ⋯ }

def LeanPool.Besicovitch.RationalInterval.mul (I J : RationalInterval) : RationalInterval

The smallest interval whose endpoints include all four endpoint products.

Equations

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

def LeanPool.Besicovitch.RationalInterval.pow (I : RationalInterval) : ℕ → RationalInterval

Natural powers of a rational interval.

Equations

• I.pow 0 = LeanPool.Besicovitch.RationalInterval.singleton 1
• I.pow n.succ = (I.pow n).mul I

def LeanPool.Besicovitch.RationalInterval.inv (I : RationalInterval) (h : 0 < I.lower ∨ I.upper < 0) : RationalInterval

An interval which avoids zero has a well-defined reciprocal interval.

Equations

• I.inv h = { lower := 1 / I.upper, upper := 1 / I.lower, lower_le_upper := ⋯ }

theorem LeanPool.Besicovitch.RationalInterval.singleton_contains (q : ℚ) : (singleton q).Contains ↑q

theorem LeanPool.Besicovitch.RationalInterval.add_contains {I J : RationalInterval} {x y : ℝ} (hx : I.Contains x) (hy : J.Contains y) : (I.add J).Contains (x + y)

theorem LeanPool.Besicovitch.RationalInterval.neg_contains {I : RationalInterval} {x : ℝ} (hx : I.Contains x) : I.neg.Contains (-x)

theorem LeanPool.Besicovitch.RationalInterval.mul_contains {I J : RationalInterval} {x y : ℝ} (hx : I.Contains x) (hy : J.Contains y) : (I.mul J).Contains (x * y)

theorem LeanPool.Besicovitch.RationalInterval.pow_contains {I : RationalInterval} {x : ℝ} (hx : I.Contains x) (n : ℕ) : (I.pow n).Contains (x ^ n)

Interval powers contain the corresponding real powers.

theorem LeanPool.Besicovitch.RationalInterval.inv_contains {I : RationalInterval} {x : ℝ} (hx : I.Contains x) (h : 0 < I.lower ∨ I.upper < 0) : (I.inv h).Contains x⁻¹