Numerics Interval Exp Exp Interval Simple

A simple interval for exp

The exponential function grows faster than a straight line but slower than a reciprocal blow-up. For any input x between 0 and 1, the two simple bounds x+1 and 1/(1-x) sandwich the true value of exp(x). The lower bound x+1 comes from the tangent line at zero; the upper bound 1/(1-x) comes from the geometric series that dominates the exponential series on that interval. Both inequalities are classical and elementary, and together they give a quick way to enclose exp(x) without computing it exactly.

The Recognition Science library, a machine-checked collection of formal theorems, packages this sandwich into a definition called expIntervalSimple. The definition takes an interval [lo, hi] inside [0, 1), and returns the interval [lo+1, 1/(1-hi)]. Because exp is monotonically increasing, the true value of exp(x) for any x in the input interval lies inside the output interval. The library proves this containment as a formal theorem, meaning the bound is verified by a computer-checked proof rather than by hand calculation.

The same library also proves a concrete interval for the number e = exp(1): it lies between 2.718 and 2.719. That result relies on deeper series bounds, not on the simple interval above, because 1 is outside the domain [0, 1). The simple interval is a building block for interval arithmetic, where rigorous enclosures replace floating-point approximations.

What expIntervalSimple does not claim: it does not give tight bounds, only valid ones. The upper bound 1/(1-x) is far from exp(x) near x=1, where it blows up while exp(x) stays finite. The definition also assumes the input interval lies in [0, 1); it says nothing about exp for negative inputs or for inputs at or above 1. These are limitations of this particular simple tool, not of the exponential function itself.

theorem expIntervalSimple_contains_exp {I : Interval}
    (hI_lo : 0 ≤ I.lo) (hI_hi : I.hi < 1)
    {x : ℝ} (hx : I.contains x) :
    (expIntervalSimple I hI_lo hI_hi).contains (exp x) := by
  simp only [contains, expIntervalSimple, expLowerSimple, expUpperSimple]
  have hx_lo : (I.lo : ℝ) ≤ x := hx.1
  have hx_hi : x ≤ (I.hi : ℝ) := hx.2
  have hx_nonneg : 0 ≤ x := le_trans (by exact_mod_cast hI_lo) hx_lo
  have hx_lt_one : x < 1 := lt_of_le_of_lt hx_hi (by exact_mod_cast hI_hi)
  have h_hi_lt_one : (I.hi : ℝ) < 1 := by exact_mod_cast hI_hi
  constructor
  · -- Lower bound: I.lo + 1 ≤ exp(x)
    have h1 : (I.lo : ℝ) + 1 ≤ x + 1 := by linarith
    have h2 : x + 1 ≤ exp x := Real.add_one_le_exp x
    simp only [Rat.cast_add, Rat.cast_one]
    linarith
  · -- Upper bound: exp(x) ≤ 1/(1 - I.hi)
    have h1 : exp x ≤ 1 / (1 - x) := Real.exp_bound_div_one_sub_of_interval hx_nonneg hx_lt_one
    have h2 : 1 / (1 - x) ≤ 1 / (1 - I.hi) := by
      apply div_le_div_of_nonneg_left
      · linarith
      · linarith
      · linarith
    simp only [Rat.cast_div, Rat.cast_one, Rat.cast_sub]
    linarith

/-- e is contained in eInterval - PROVEN using Mathlib's exp_one_gt_d9/lt_d9 -/
theorem e_in_eInterval : eInterval.contains (exp 1) := by
  simp only [Interval.contains, eInterval]
  constructor
  · -- 2.718 ≤ exp(1)
    have h := Real.exp_one_gt_d9  -- 2.7182818283 < exp 1
    have h1 : ((2718 / 1000 : ℚ) : ℝ) = (2.718 : ℝ) := by norm_num
    linarith
  · -- exp(1) ≤ 2.719
    have h := Real.exp_one_lt_d9  -- exp 1 < 2.7182818286
    have h1 : ((2719 / 1000 : ℚ) : ℝ) = (2.719 : ℝ) := by norm_num
    linarith

What this page does not claim

The simple bounds are tight; they are only valid, and the upper bound becomes poor near x=1. The interval method applies outside the domain [0, 1); it requires the input interval to lie strictly below 1. The e interval result follows from the simple interval definition; it uses a separate series bound.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Numerics/Interval/Exp.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: