expIntervalSimple_contains_exp

formal source

  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