Numerics Interval Exp Exp Lower Simple

A simple lower bound

The exponential function exp(x) grows faster than any straight line, but for every real number x it stays at or above the specific line x + 1. This is the inequality exp(x) ≥ x + 1, a classical result that follows from the function's defining series or from its convexity. The framework's machine-checked library of formal theorems records this as a definition named expLowerSimple, which takes a rational number x and returns x + 1. The declaration itself is just that arithmetic expression; the mathematical content lives in the surrounding theorem that the interval containing exp(x) respects this lower bound.

The library uses this bound as one half of a rigorous interval enclosure for exp on inputs from 0 up to but not including 1. For such an input interval [lo, hi], the lower endpoint of the output interval is expLowerSimple lo, namely lo + 1, and the upper endpoint comes from the companion bound exp(x) ≤ 1/(1 − x). Because exp is monotonically increasing on this range, the true value exp(x) for any x inside [lo, hi] must lie between these two endpoints. The theorem expIntervalSimple_contains_exp states exactly this containment, and its proof is checked by the machine, not by hand calculation.

What this does not claim is any precision or tightness. The bound x + 1 is deliberately crude: it is the tangent line at zero, so it is exact only at x = 0 and becomes progressively looser as x grows. The library also carries a sharper interval for e = exp(1), pinning it between 2.718 and 2.719 using a series bound, but expLowerSimple plays no part in that tighter result. The simple bound exists to make other proofs cheap and reliable, not to compete with refined estimates.

The practical payoff is that any later proof needing a lower bound on exp can call this fact without rederiving it, and the machine guarantees the inequality holds for every real input, not just for the rational points where the definition is written. That separation, between the simple rational expression and the universally quantified real theorem, is what makes the library a tool rather than a collection of examples.

/-- Simple lower bound: exp(x) ≥ x + 1 for all x -/
def expLowerSimple (x : ℚ) : ℚ := x + 1

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 bound x + 1 is not tight except at x = 0, and the declaration makes no claim about precision. The simple lower bound does not contribute to the sharper interval for e, which uses a separate series argument. The declaration does not itself prove the inequality exp(x) ≥ x + 1; that content lives in the surrounding theorem.

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: