def
definition
piPow5IntervalTight
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Numerics.Interval.PiBounds on GitHub at line 239.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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