expUpperSimple
This definition supplies the rational expression 1/(1-x) as an upper bound for the exponential on the half-open unit interval. Interval-arithmetic routines cite it when constructing conservative enclosures for exp(x) inside [0,1). The body is a direct one-line algebraic definition implementing the known inequality exp(x) ≤ 1/(1-x).
claimFor rational $x$ satisfying $0 ≤ x < 1$, the upper-bound expression is defined by $1/(1-x)$.
background
The module supplies rigorous interval bounds for the exponential using Mathlib's exponential bounds. For an interval [lo, hi] inside [0,1), monotonicity of exp yields exp([lo, hi]) inside [exp(lo), exp(hi)]. The upper bound deploys the inequality exp(x) ≤ 1/(1-x) while the lower bound uses x + 1 ≤ exp(x).
proof idea
The definition is a one-line algebraic expression that directly encodes the upper bound 1/(1-x). It is invoked without further reduction inside the construction of the enclosing interval.
why it matters in Recognition Science
The definition is referenced by expIntervalSimple to populate the hi endpoint and by expIntervalSimple_contains_exp to certify that the enclosure contains exp(x). It completes the upper-bound component of the interval strategy for the exponential in the numerics layer.
scope and limits
- Does not prove the inequality exp(x) ≤ 1/(1-x).
- Does not apply for x outside [0,1).
- Does not accept real or floating-point inputs.
Lean usage
hi := expUpperSimple I.hiformal statement (Lean)
29def expUpperSimple (x : ℚ) : ℚ := 1 / (1 - x)
proof body
Definition body.
30
31/-- For intervals in [0, 1), compute a simple exp interval using monotonicity -/