expIntervalSimple
plain-language theorem explainer
expIntervalSimple assembles a rational interval enclosing exp(x) for any x inside a given input interval I subset of [0,1) by taking the lower bound I.lo + 1 and upper bound 1/(1 - I.hi). Numerics routines in Recognition Science cite it when they need machine-checkable exponential bounds that stay inside rational arithmetic. The definition is a direct constructor that applies the two simple bounds and discharges the validity obligation with linear arithmetic.
Claim. For a closed interval $I = [a, b]$ with rational endpoints satisfying $0 ≤ a ≤ b < 1$, the interval $[a + 1, 1/(1 - b)]$.
background
The Interval structure is a closed interval with rational endpoints lo and hi obeying lo ≤ hi. The module supplies interval arithmetic for the exponential function over subintervals of [0,1) by exploiting monotonicity together with the elementary inequalities x + 1 ≤ exp(x) and exp(x) ≤ 1/(1 - x). These bounds are realized by the sibling definitions expLowerSimple and expUpperSimple, which are then combined inside expIntervalSimple.
proof idea
The definition directly sets lo to expLowerSimple I.lo and hi to expUpperSimple I.hi. The embedded valid proof unfolds the two bound definitions by simp, then applies linarith and nlinarith (after a short ring_nf step) to confirm that the constructed lower endpoint is at most the upper endpoint under the given hypotheses.
why it matters
This definition supplies the concrete interval object consumed by the downstream theorem expIntervalSimple_contains_exp, which certifies that the constructed interval contains exp(x) whenever x lies in I. It implements the simple monotonicity strategy described in the module documentation and thereby supports certified exponential bounds inside the numerics layer without requiring the full strength of Mathlib's real-analysis machinery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.