pi_in_piInterval

formal source

  35  valid := by norm_num
  36
  37/-- π is contained in piInterval - PROVEN using Mathlib's bounds -/
  38theorem pi_in_piInterval : piInterval.contains pi := by
  39  simp only [contains, piInterval]
  40  constructor
  41  · -- 3.141592 ≤ π
  42    have h := Real.pi_gt_d6
  43    have h1 : ((3141592 / 1000000 : ℚ) : ℝ) < pi := by
  44      calc ((3141592 / 1000000 : ℚ) : ℝ) = (3.141592 : ℝ) := by norm_num
  45        _ < pi := h
  46    exact le_of_lt h1
  47  · -- π ≤ 3.141593
  48    have h := Real.pi_lt_d6
  49    have h1 : pi < ((3141593 / 1000000 : ℚ) : ℝ) := by
  50      calc pi < (3.141593 : ℝ) := h
  51        _ = ((3141593 / 1000000 : ℚ) : ℝ) := by norm_num
  52    exact le_of_lt h1
  53
  54/-- Wider interval for π: [3.14, 3.15] -/
  55def piIntervalWide : Interval where
  56  lo := 314 / 100  -- 3.14
  57  hi := 315 / 100  -- 3.15
  58  valid := by norm_num
  59
  60/-- π is contained in piIntervalWide - PROVEN -/
  61theorem pi_in_piIntervalWide : piIntervalWide.contains pi := by
  62  simp only [contains, piIntervalWide]
  63  constructor
  64  · have h := Real.pi_gt_d2
  65    have h1 : ((314 / 100 : ℚ) : ℝ) < pi := by
  66      calc ((314 / 100 : ℚ) : ℝ) = (3.14 : ℝ) := by norm_num
  67        _ < pi := h
  68    exact le_of_lt h1