Numerics Interval Exp

Interval arithmetic for exp

Interval arithmetic is a way of doing calculations with ranges instead of single numbers. If you know a value x lies between two endpoints, you can compute a range that the result of a function must lie in. The exponential function exp(x) is monotonically increasing: a larger input always gives a larger output. So for any input interval [lo, hi] inside [0, 1), the output interval is simply [exp(lo), exp(hi)]. This approach in the machine-checked library of formal theorems proves that this simple monotonicity argument gives rigorous bounds.

The key bounds are elementary. For a lower bound, the inequality x + 1 ≤ exp(x) holds for every real x. For an upper bound, when 0 ≤ x < 1, the inequality exp(x) ≤ 1/(1 - x) holds. These are defined as interval operations, where an interval is a pair of rational numbers with a proof that the lower endpoint is at most the upper endpoint. The main theorem, expIntervalSimple_contains_exp, states that if a real number x lies in the input interval, then exp(x) lies in the computed output interval. This is a formal guarantee, checked by the machine, not an approximate claim.

The same approach applies the method to the number e = exp(1). It defines an interval with lower bound 2718/1000 and upper bound 2719/1000, and proves that e lies inside it. The proof uses known results about the exponential series: exp(1) is greater than 2.7182818283 and less than 2.7182818286. So the interval (2.718, 2.719) is certified to contain e. This is not a numerical approximation with an error bar; it is a logical statement that the true value of e falls between two exact rational numbers.

What this establishes in plain language: when the framework needs a rigorous value of the exponential function or of e itself, it does not rely on floating-point arithmetic or on unverified decimal expansions. Every bound is a theorem. The practical consequence is that any downstream calculation that uses exp or e can inherit these certified intervals, and every step of a larger proof can be checked end to end. The method is deliberately simple, using monotonicity and two elementary inequalities, which keeps the proofs short and auditable.

/-- For intervals in [0, 1), compute a simple exp interval using monotonicity -/
def expIntervalSimple (I : Interval) (hI_lo : 0 ≤ I.lo) (hI_hi : I.hi < 1) : Interval where
  lo := expLowerSimple I.lo
  hi := expUpperSimple I.hi
  valid := by
    simp only [expLowerSimple, expUpperSimple]
    have h_denom_pos : 0 < 1 - I.hi := by linarith
    have h1 : I.lo + 1 ≤ I.hi + 1 := by linarith [I.valid]
    have h2 : I.hi + 1 ≤ 1 / (1 - I.hi) := by
      rw [le_div_iff₀ h_denom_pos]
      ring_nf
      nlinarith [sq_nonneg I.hi, I.valid]
    linarith

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

This module does not provide a method for computing exp on the whole real line, only on the interval [0, 1). The interval (2.718, 2.719) is a certified container for e, not a claim about the exact decimal expansion of e. The bounds are not optimized for tightness; they are chosen for simplicity of proof.

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: