piFromOctagon

formal source

  54    π ≈ Perimeter/2 ≈ 3.06 (rough approximation!) -/
  55noncomputable def octagonPerimeter : ℝ := 8 * 2 * Real.sin (π / 8)
  56
  57noncomputable def piFromOctagon : ℝ := octagonPerimeter / 2
  58
  59theorem octagon_approximates_pi :
  60    -- Inscribed octagon underestimates π: piFromOctagon < π
  61    -- (Since sin(x) < x for x > 0, the inscribed polygon has perimeter < 2π)
  62    piFromOctagon < Real.pi := by
  63  unfold piFromOctagon octagonPerimeter
  64  have h_pi8_pos : (0 : ℝ) < Real.pi / 8 := by positivity
  65  have h_sin_lt : Real.sin (Real.pi / 8) < Real.pi / 8 := Real.sin_lt h_pi8_pos
  66  nlinarith [Real.sin_nonneg_of_nonneg_of_le_pi h_pi8_pos.le
  67               (by linarith [Real.pi_gt_three]), Real.pi_pos]
  68
  69/-! ## Refinement via Inscribed Polygons -/
  70
  71/-- Archimedes' method: Use n-gons to bound π.
  72
  73    Inscribed n-gon perimeter: P_n = n × 2 sin(π/n)
  74    Circumscribed n-gon perimeter: Q_n = n × 2 tan(π/n)
  75
  76    P_n/(2r) < π < Q_n/(2r)
  77
  78    As n → ∞, both converge to π. -/
  79noncomputable def inscribedPerimeter (n : ℕ) (hn : n ≥ 3) : ℝ :=
  80  n * 2 * Real.sin (π / n)
  81
  82noncomputable def circumscribedPerimeter (n : ℕ) (hn : n ≥ 3) : ℝ :=
  83  n * 2 * Real.tan (π / n)
  84
  85/-- For 8-gon (octagon):
  86    P_8 = 8 × 2 sin(π/8) ≈ 6.12
  87    Q_8 = 8 × 2 tan(π/8) ≈ 6.63