IndisputableMonolith.Numerics.Interval.Exp
The Numerics.Interval.Exp module supplies simple verified bounds for the real exponential using rational endpoints. It is imported by the power and tactic modules to enclose expressions involving exp and log. The content rests on the inequality exp(x) ≥ x + 1 together with the interval primitives from the Basic module.
claim$e^x ≥ x + 1$ for all real $x$, with simple interval enclosures $e^{[a,b]} ⊆ [L,U]$ for rational $a ≤ b$.
background
The module sits inside the verified interval arithmetic framework of Numerics.Interval.Basic. That framework computes exact bounds on real functions by propagating rational endpoints through arithmetic operations. The supplied doc-comment states: 'This module provides rigorous interval arithmetic for computing bounds on transcendental functions. The key insight is that we use rational endpoints (which Lean can compute exactly) to bound real values.' It introduces the elementary lower bound exp(x) ≥ x + 1 as the seed for exponential enclosures.
proof idea
This is a definition module, no proofs. The declarations establish direct bounds derived from the convexity of exp and the interval operations imported from Basic.
why it matters in Recognition Science
The module feeds the power-function bounds in Numerics.Interval.Pow, which relies on the identity x^y = exp(y log x) for positive x. It also supports the interval_bound tactic in Numerics.Interval.Tactic for proving inequalities on transcendental expressions. The downstream Pow doc-comment notes that the strategy for x in [lo_x, hi_x] uses the exponential to obtain rigorous enclosures.
scope and limits
- Does not extend to complex exponentials.
- Does not implement Taylor series of arbitrary order.
- Does not refine intervals adaptively or to arbitrary precision.
- Does not address bases outside the positive reals for related functions.