IndisputableMonolith.Numerics.Interval.Exp

   1import IndisputableMonolith.Numerics.Interval.Basic
   2import Mathlib.Analysis.Complex.Exponential
   3import Mathlib.Analysis.SpecialFunctions.ExpDeriv
   4import Mathlib.Analysis.Complex.ExponentialBounds  -- For exp_one_gt_d9, exp_one_lt_d9
   5
   6/-!
   7# Interval Arithmetic for Exponential Function
   8
   9This module provides rigorous interval bounds for the exponential function
  10using Mathlib's bounds.
  11
  12## Strategy
  13
  14For x in [lo, hi] ⊆ [0, 1):
  151. exp is monotonically increasing, so exp([lo, hi]) ⊆ [exp(lo), exp(hi)]
  162. We use `exp_bound_div_one_sub_of_interval` for upper bounds: exp(x) ≤ 1/(1-x)
  173. We use `add_one_le_exp` for lower bounds: x + 1 ≤ exp(x)
  18-/
  19
  20namespace IndisputableMonolith.Numerics
  21
  22open Interval
  23open Real (exp)
  24
  25/-- Simple lower bound: exp(x) ≥ x + 1 for all x -/
  26def expLowerSimple (x : ℚ) : ℚ := x + 1
  27
  28/-- Simple upper bound: exp(x) ≤ 1/(1-x) for 0 ≤ x < 1 -/
  29def expUpperSimple (x : ℚ) : ℚ := 1 / (1 - x)
  30
  31/-- For intervals in [0, 1), compute a simple exp interval using monotonicity -/
  32def expIntervalSimple (I : Interval) (hI_lo : 0 ≤ I.lo) (hI_hi : I.hi < 1) : Interval where
  33  lo := expLowerSimple I.lo
  34  hi := expUpperSimple I.hi
  35  valid := by
  36    simp only [expLowerSimple, expUpperSimple]
  37    have h_denom_pos : 0 < 1 - I.hi := by linarith
  38    have h1 : I.lo + 1 ≤ I.hi + 1 := by linarith [I.valid]
  39    have h2 : I.hi + 1 ≤ 1 / (1 - I.hi) := by
  40      rw [le_div_iff₀ h_denom_pos]
  41      ring_nf
  42      nlinarith [sq_nonneg I.hi, I.valid]
  43    linarith
  44
  45theorem expIntervalSimple_contains_exp {I : Interval}
  46    (hI_lo : 0 ≤ I.lo) (hI_hi : I.hi < 1)
  47    {x : ℝ} (hx : I.contains x) :
  48    (expIntervalSimple I hI_lo hI_hi).contains (exp x) := by
  49  simp only [contains, expIntervalSimple, expLowerSimple, expUpperSimple]
  50  have hx_lo : (I.lo : ℝ) ≤ x := hx.1
  51  have hx_hi : x ≤ (I.hi : ℝ) := hx.2
  52  have hx_nonneg : 0 ≤ x := le_trans (by exact_mod_cast hI_lo) hx_lo
  53  have hx_lt_one : x < 1 := lt_of_le_of_lt hx_hi (by exact_mod_cast hI_hi)
  54  have h_hi_lt_one : (I.hi : ℝ) < 1 := by exact_mod_cast hI_hi
  55  constructor
  56  · -- Lower bound: I.lo + 1 ≤ exp(x)
  57    have h1 : (I.lo : ℝ) + 1 ≤ x + 1 := by linarith
  58    have h2 : x + 1 ≤ exp x := Real.add_one_le_exp x
  59    simp only [Rat.cast_add, Rat.cast_one]
  60    linarith
  61  · -- Upper bound: exp(x) ≤ 1/(1 - I.hi)
  62    have h1 : exp x ≤ 1 / (1 - x) := Real.exp_bound_div_one_sub_of_interval hx_nonneg hx_lt_one
  63    have h2 : 1 / (1 - x) ≤ 1 / (1 - I.hi) := by
  64      apply div_le_div_of_nonneg_left
  65      · linarith
  66      · linarith
  67      · linarith
  68    simp only [Rat.cast_div, Rat.cast_one, Rat.cast_sub]
  69    linarith
  70
  71/-- Interval containing e = exp(1) using the series bound.
  72    We know e ∈ (2.718, 2.719) -/
  73def eInterval : Interval where
  74  lo := 2718 / 1000
  75  hi := 2719 / 1000
  76  valid := by norm_num
  77
  78/-- e is contained in eInterval - PROVEN using Mathlib's exp_one_gt_d9/lt_d9 -/
  79theorem e_in_eInterval : eInterval.contains (exp 1) := by
  80  simp only [Interval.contains, eInterval]
  81  constructor
  82  · -- 2.718 ≤ exp(1)
  83    have h := Real.exp_one_gt_d9  -- 2.7182818283 < exp 1
  84    have h1 : ((2718 / 1000 : ℚ) : ℝ) = (2.718 : ℝ) := by norm_num
  85    linarith
  86  · -- exp(1) ≤ 2.719
  87    have h := Real.exp_one_lt_d9  -- exp 1 < 2.7182818286
  88    have h1 : ((2719 / 1000 : ℚ) : ℝ) = (2.719 : ℝ) := by norm_num
  89    linarith
  90
  91end IndisputableMonolith.Numerics
  92