eInterval

formal source

  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