expLowerSimple

formal source

  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)