four_pi_in_interval

formal source

  91  valid := by norm_num
  92
  93/-- 4π is contained in fourPiInterval - PROVEN -/
  94theorem four_pi_in_interval : fourPiInterval.contains (4 * pi) := by
  95  simp only [contains, fourPiInterval]
  96  constructor
  97  · have h := four_pi_gt
  98    exact le_of_lt (by calc ((1256 / 100 : ℚ) : ℝ) = (12.56 : ℝ) := by norm_num
  99      _ < 4 * pi := h)
 100  · have h := four_pi_lt
 101    exact le_of_lt (by calc 4 * pi < (12.6 : ℝ) := h
 102      _ = ((126 / 10 : ℚ) : ℝ) := by norm_num)
 103
 104/-! ## Bounds on π² -/
 105
 106/-- π² > 9.8596 (using 3.14² = 9.8596) -/
 107theorem pi_sq_gt : (9.8596 : ℝ) < pi ^ 2 := by
 108  have h := Real.pi_gt_d2  -- 3.14 < π
 109  have hpos : 0 < pi := Real.pi_pos
 110  have h1 : (3.14 : ℝ) ^ 2 < pi ^ 2 := sq_lt_sq' (by linarith) h
 111  calc (9.8596 : ℝ) = (3.14 : ℝ) ^ 2 := by norm_num
 112    _ < pi ^ 2 := h1
 113
 114/-- π² < 9.9225 (using 3.15² = 9.9225) -/
 115theorem pi_sq_lt : pi ^ 2 < (9.9225 : ℝ) := by
 116  have h := Real.pi_lt_d2  -- π < 3.15
 117  have hpos : 0 < pi := Real.pi_pos
 118  have h1 : pi ^ 2 < (3.15 : ℝ) ^ 2 := sq_lt_sq' (by linarith) h
 119  calc pi ^ 2 < (3.15 : ℝ) ^ 2 := h1
 120    _ = (9.9225 : ℝ) := by norm_num
 121
 122/-- Interval containing π² -/
 123def piSqInterval : Interval where
 124  lo := 98596 / 10000  -- 9.8596