IndisputableMonolith.Numerics.Interval.PiBounds

   1import IndisputableMonolith.Numerics.Interval.Basic
   2import Mathlib.Analysis.Real.Pi.Bounds
   3
   4/-!
   5# Rigorous Bounds on π
   6
   7This module provides interval bounds on π using Mathlib's proven bounds.
   8
   9## Mathlib Resources
  10
  11Mathlib provides very precise bounds on π:
  12- `Real.pi_gt_three`: 3 < π
  13- `Real.pi_lt_four`: π < 4
  14- `Real.pi_gt_d2`: 3.14 < π
  15- `Real.pi_lt_d2`: π < 3.15
  16- `Real.pi_gt_d4`: 3.1415 < π
  17- `Real.pi_lt_d4`: π < 3.1416
  18- `Real.pi_gt_d6`: 3.141592 < π
  19- `Real.pi_lt_d6`: π < 3.141593
  20- `Real.pi_gt_d20`: 3.14159265358979323846 < π
  21- `Real.pi_lt_d20`: π < 3.14159265358979323847
  22
  23We use these to build interval bounds for π and powers of π.
  24-/
  25
  26namespace IndisputableMonolith.Numerics
  27
  28open Interval
  29open Real (pi)
  30
  31/-- Interval containing π with 6 decimal places of precision -/
  32def piInterval : Interval where
  33  lo := 3141592 / 1000000  -- 3.141592
  34  hi := 3141593 / 1000000  -- 3.141593
  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
  69  · have h := Real.pi_lt_d2
  70    have h1 : pi < ((315 / 100 : ℚ) : ℝ) := by
  71      calc pi < (3.15 : ℝ) := h
  72        _ = ((315 / 100 : ℚ) : ℝ) := by norm_num
  73    exact le_of_lt h1
  74
  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 < π
 109  have hpos : 0 < pi := Real.pi_pos
 110  have h1 : (3.14 : ℝ) ^ 2 < pi ^ 2 := sq_lt_sq' (by linarith) h
 111  calc (9.8596 : ℝ) = (3.14 : ℝ) ^ 2 := by norm_num
 112    _ < pi ^ 2 := h1
 113
 114/-- π² < 9.9225 (using 3.15² = 9.9225) -/
 115theorem pi_sq_lt : pi ^ 2 < (9.9225 : ℝ) := by
 116  have h := Real.pi_lt_d2  -- π < 3.15
 117  have hpos : 0 < pi := Real.pi_pos
 118  have h1 : pi ^ 2 < (3.15 : ℝ) ^ 2 := sq_lt_sq' (by linarith) h
 119  calc pi ^ 2 < (3.15 : ℝ) ^ 2 := h1
 120    _ = (9.9225 : ℝ) := by norm_num
 121
 122/-- Interval containing π² -/
 123def piSqInterval : Interval where
 124  lo := 98596 / 10000  -- 9.8596
 125  hi := 99225 / 10000  -- 9.9225
 126  valid := by norm_num
 127
 128/-- π² is contained in piSqInterval - PROVEN -/
 129theorem pi_sq_in_interval : piSqInterval.contains (pi ^ 2) := by
 130  simp only [contains, piSqInterval]
 131  constructor
 132  · have h := pi_sq_gt
 133    exact le_of_lt (by calc ((98596 / 10000 : ℚ) : ℝ) = (9.8596 : ℝ) := by norm_num
 134      _ < pi ^ 2 := h)
 135  · have h := pi_sq_lt
 136    exact le_of_lt (by calc pi ^ 2 < (9.9225 : ℝ) := h
 137      _ = ((99225 / 10000 : ℚ) : ℝ) := by norm_num)
 138
 139/-! ## Bounds on π⁵ -/
 140
 141/-- π⁵ = π² · π² · π -/
 142theorem pi_pow5_eq : pi ^ 5 = pi ^ 2 * pi ^ 2 * pi := by ring
 143
 144/-- π⁵ > 305 (using π > 3.14) -/
 145theorem pi_pow5_gt : (305 : ℝ) < pi ^ 5 := by
 146  have h := Real.pi_gt_d2  -- 3.14 < π
 147  have hpos : 0 < pi := Real.pi_pos
 148  -- π > 3.14 implies π⁵ > 3.14⁵ = 305.2447...
 149  have h1 : (3.14 : ℝ) ^ 5 < pi ^ 5 := by
 150    have hle : (3.14 : ℝ) ≤ pi := le_of_lt h
 151    have hlo : (0 : ℝ) < 3.14 := by norm_num
 152    nlinarith [sq_nonneg pi, sq_nonneg (pi - 3.14), mul_self_nonneg pi,
 153               mul_self_nonneg (pi ^ 2), mul_self_nonneg (pi ^ 2 - 3.14 ^ 2)]
 154  calc (305 : ℝ) < (3.14 : ℝ) ^ 5 := by norm_num
 155    _ < pi ^ 5 := h1
 156
 157/-- π⁵ < 312 (using π < 3.15) -/
 158theorem pi_pow5_lt : pi ^ 5 < (312 : ℝ) := by
 159  have h := Real.pi_lt_d2  -- π < 3.15
 160  have hpos : 0 < pi := Real.pi_pos
 161  -- π < 3.15 implies π⁵ < 3.15⁵ = 311.6...
 162  have h1 : pi ^ 5 < (3.15 : ℝ) ^ 5 := by
 163    have hle : pi ≤ (3.15 : ℝ) := le_of_lt h
 164    nlinarith [sq_nonneg pi, sq_nonneg (3.15 - pi), mul_self_nonneg pi,
 165               mul_self_nonneg (pi ^ 2), mul_self_nonneg (3.15 ^ 2 - pi ^ 2)]
 166  calc pi ^ 5 < (3.15 : ℝ) ^ 5 := h1
 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
 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
 225    _ < pi ^ 5 := h1
 226
 227/-- π⁵ < 306.0199 (using π < 3.141593) -/
 228theorem pi_pow5_lt_d6 : pi ^ 5 < (306.0199 : ℝ) := by
 229  have h := Real.pi_lt_d6  -- π < 3.141593
 230  have hpos : 0 < pi := Real.pi_pos
 231  have h1 : pi ^ 5 < (3.141593 : ℝ) ^ 5 := by
 232    have hle : pi ≤ (3.141593 : ℝ) := le_of_lt h
 233    nlinarith [sq_nonneg pi, sq_nonneg (3.141593 - pi), mul_self_nonneg pi,
 234               mul_self_nonneg (pi ^ 2), mul_self_nonneg (3.141593 ^ 2 - pi ^ 2)]
 235  calc pi ^ 5 < (3.141593 : ℝ) ^ 5 := h1
 236    _ < (306.0199 : ℝ) := by norm_num
 237
 238/-- Tight interval for π⁵ -/
 239def piPow5IntervalTight : Interval where
 240  lo := 3060193 / 10000  -- 306.0193
 241  hi := 3060199 / 10000  -- 306.0199
 242  valid := by norm_num
 243
 244/-- π⁵ is contained in piPow5IntervalTight - PROVEN -/
 245theorem pi_pow5_in_interval_tight : piPow5IntervalTight.contains (pi ^ 5) := by
 246  simp only [contains, piPow5IntervalTight]
 247  constructor
 248  · have h := pi_pow5_gt_d6
 249    exact le_of_lt (by calc ((3060193 / 10000 : ℚ) : ℝ) = (306.0193 : ℝ) := by norm_num
 250      _ < pi ^ 5 := h)
 251  · have h := pi_pow5_lt_d6
 252    exact le_of_lt (by calc pi ^ 5 < (306.0199 : ℝ) := h
 253      _ = ((3060199 / 10000 : ℚ) : ℝ) := by norm_num)
 254
 255end IndisputableMonolith.Numerics
 256