expIntervalSimple

formal source

  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