 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
 146  have h := Real.pi_gt_d2  -- 3.14 < π
 147  have hpos : 0 < pi := Real.pi_pos
 148  -- π > 3.14 implies π⁵ > 3.14⁵ = 305.2447...
 149  have h1 : (3.14 : ℝ) ^ 5 < pi ^ 5 := by
 150    have hle : (3.14 : ℝ) ≤ pi := le_of_lt h
 151    have hlo : (0 : ℝ) < 3.14 := by norm_num
 152    nlinarith [sq_nonneg pi, sq_nonneg (pi - 3.14), mul_self_nonneg pi,
 153               mul_self_nonneg (pi ^ 2), mul_self_nonneg (pi ^ 2 - 3.14 ^ 2)]

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.