four_pi_gt

formal source

  75/-! ## Bounds on 4π -/
  76
  77/-- 4π > 12.56 -/
  78theorem four_pi_gt : (12.56 : ℝ) < 4 * pi := by
  79  have h := Real.pi_gt_d2  -- 3.14 < π
  80  linarith
  81
  82/-- 4π < 12.6 -/
  83theorem four_pi_lt : 4 * pi < (12.6 : ℝ) := by
  84  have h := Real.pi_lt_d2  -- π < 3.15
  85  linarith
  86
  87/-- Interval containing 4π -/
  88def fourPiInterval : Interval where
  89  lo := 1256 / 100  -- 12.56
  90  hi := 126 / 10    -- 12.6
  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 < π