pi_sq_lt

formal source

 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
 125  hi := 99225 / 10000  -- 9.9225
 126  valid := by norm_num
 127
 128/-- π² is contained in piSqInterval - PROVEN -/
 129theorem pi_sq_in_interval : piSqInterval.contains (pi ^ 2) := by
 130  simp only [contains, piSqInterval]
 131  constructor
 132  · have h := pi_sq_gt
 133    exact le_of_lt (by calc ((98596 / 10000 : ℚ) : ℝ) = (9.8596 : ℝ) := by norm_num
 134      _ < pi ^ 2 := h)
 135  · have h := pi_sq_lt
 136    exact le_of_lt (by calc pi ^ 2 < (9.9225 : ℝ) := h
 137      _ = ((99225 / 10000 : ℚ) : ℝ) := by norm_num)
 138
 139/-! ## Bounds on π⁵ -/
 140
 141/-- π⁵ = π² · π² · π -/
 142theorem pi_pow5_eq : pi ^ 5 = pi ^ 2 * pi ^ 2 * pi := by ring
 143
 144/-- π⁵ > 305 (using π > 3.14) -/
 145theorem pi_pow5_gt : (305 : ℝ) < pi ^ 5 := by