def
definition
piInterval
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Numerics.Interval.PiBounds on GitHub at line 32.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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]