Abstract Interval Interface

This file defines the abstract notion of intervals as subsets of ℝ, with semantic properties. This provides the mathematical foundation that IntervalReal will implement computationally.

Main definitions

• Lemmas about Set.Icc (closed intervals) relevant to interval arithmetic
• Convexity and integrability properties

Design notes

We primarily use Set.Icc a b from Mathlib as our semantic interval type. This file collects lemmas and abstractions useful for verified numerics.

Interval membership and operations

@[reducible, inline]

abbrev LeanCert.Core.mem_Icc (x a b : ℝ) : Prop

A real number is in the interval [a, b]

Equations

• LeanCert.Core.mem_Icc x a b = (a ≤ x ∧ x ≤ b)

theorem LeanCert.Core.mem_Icc_iff (x a b : ℝ) : mem_Icc x a b ↔ x ∈ Set.Icc a b

Interval arithmetic semantics

These lemmas establish the semantic foundation for interval arithmetic: if x ∈ [a, b] and y ∈ [c, d], then x ⊕ y ∈ [a ⊕ c, b ⊕ d] (for appropriate ⊕).

theorem LeanCert.Core.add_mem_Icc {x y a b c d : ℝ} (hx : x ∈ Set.Icc a b) (hy : y ∈ Set.Icc c d) : x + y ∈ Set.Icc (a + c) (b + d)

Addition preserves interval membership

theorem LeanCert.Core.neg_mem_Icc {x a b : ℝ} (hx : x ∈ Set.Icc a b) : -x ∈ Set.Icc (-b) (-a)

Negation reverses interval bounds

theorem LeanCert.Core.sub_mem_Icc {x y a b c d : ℝ} (hx : x ∈ Set.Icc a b) (hy : y ∈ Set.Icc c d) : x - y ∈ Set.Icc (a - d) (b - c)

Subtraction on intervals

Convexity

theorem LeanCert.Core.Icc_convex (a b : ℝ) : Convex ℝ (Set.Icc a b)

Closed intervals are convex

Compactness

theorem LeanCert.Core.Icc_compact (a b : ℝ) : IsCompact (Set.Icc a b)

Nonempty closed bounded intervals are compact

Continuous functions on intervals

theorem LeanCert.Core.continuous_Icc_bounds {f : ℝ → ℝ} {a b : ℝ} (hab : a ≤ b) (hf : Continuous f) : ∃ (lo : ℝ) (hi : ℝ), (∀ x ∈ Set.Icc a b, lo ≤ f x ∧ f x ≤ hi) ∧ (∃ x ∈ Set.Icc a b, f x = lo) ∧ ∃ x ∈ Set.Icc a b, f x = hi

A continuous function on a compact interval attains its bounds