four_pi_lt_d6

formal source

 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
 201  hi := 12566372 / 1000000  -- 12.566372
 202  valid := by norm_num
 203
 204/-- 4π is contained in fourPiIntervalTight - PROVEN -/
 205theorem four_pi_in_interval_tight : fourPiIntervalTight.contains (4 * pi) := by
 206  simp only [contains, fourPiIntervalTight]
 207  constructor
 208  · have h := four_pi_gt_d6
 209    exact le_of_lt (by calc ((12566368 / 1000000 : ℚ) : ℝ) = (12.566368 : ℝ) := by norm_num
 210      _ < 4 * pi := h)
 211  · have h := four_pi_lt_d6
 212    exact le_of_lt (by calc 4 * pi < (12.566372 : ℝ) := h
 213      _ = ((12566372 / 1000000 : ℚ) : ℝ) := by norm_num)
 214
 215/-- π⁵ > 306.0193 (using π > 3.141592) -/
 216theorem pi_pow5_gt_d6 : (306.0193 : ℝ) < pi ^ 5 := by
 217  have h := Real.pi_gt_d6  -- 3.141592 < π
 218  have hpos : 0 < pi := Real.pi_pos
 219  have h1 : (3.141592 : ℝ) ^ 5 < pi ^ 5 := by
 220    have hle : (3.141592 : ℝ) ≤ pi := le_of_lt h
 221    have hlo : (0 : ℝ) < 3.141592 := by norm_num
 222    nlinarith [sq_nonneg pi, sq_nonneg (pi - 3.141592), mul_self_nonneg pi,
 223               mul_self_nonneg (pi ^ 2), mul_self_nonneg (pi ^ 2 - 3.141592 ^ 2)]
 224  calc (306.0193 : ℝ) < (3.141592 : ℝ) ^ 5 := by norm_num