expUpperSimple
plain-language theorem explainer
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).
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.