theorem
proved
tactic proof
expIntervalSimple_contains_exp
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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) -/