 167    _ < (312 : ℝ) := by norm_num
 168
 169/-- Interval containing π⁵ -/
 170def piPow5Interval : Interval where
 171  lo := 305
 172  hi := 312
 173  valid := by norm_num
 174
 175/-- π⁵ is contained in piPow5Interval - PROVEN -/
 176theorem pi_pow5_in_interval : piPow5Interval.contains (pi ^ 5) := by
 177  simp only [contains, piPow5Interval]
 178  constructor
 179  · have h := pi_pow5_gt
 180    exact le_of_lt (by calc ((305 : ℚ) : ℝ) = (305 : ℝ) := by norm_num
 181      _ < pi ^ 5 := h)
 182  · have h := pi_pow5_lt
 183    exact le_of_lt (by calc pi ^ 5 < (312 : ℝ) := h
 184      _ = ((312 : ℚ) : ℝ) := by norm_num)
 185
 186/-! ## Tighter bounds using d6 precision -/
 187
 188/-- 4π > 12.566368 (using π > 3.141592) -/
 189theorem four_pi_gt_d6 : (12.566368 : ℝ) < 4 * pi := by
 190  have h := Real.pi_gt_d6  -- 3.141592 < π
 191  linarith
 192
 193/-- 4π < 12.566372 (using π < 3.141593) -/
 194theorem four_pi_lt_d6 : 4 * pi < (12.566372 : ℝ) := by
 195  have h := Real.pi_lt_d6  -- π < 3.141593
 196  linarith
 197
 198/-- Tight interval for 4π -/
 199def fourPiIntervalTight : Interval where
 200  lo := 12566368 / 1000000  -- 12.566368

papers checked against this theorem

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