`log_phi_in_interval`

proved

show as: view math explainer →

module: IndisputableMonolith.Numerics.Interval.Log
domain: Numerics
line: 312 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Numerics.Interval.Log on GitHub at line 312.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 309    _ ≤ Real.exp (0.483 : ℝ) := h_lower
 310
 311/-- log(φ) is contained in logPhiInterval - PROVEN using Taylor series bounds -/
 312theorem log_phi_in_interval : logPhiInterval.contains (log ((1 + Real.sqrt 5) / 2)) := by
 313  simp only [contains, logPhiInterval]
 314  have hphi_eq : (1 + Real.sqrt 5) / 2 = Real.goldenRatio := by
 315    unfold Real.goldenRatio
 316    ring
 317  rw [hphi_eq]
 318  constructor
 319  · -- 0.48 ≤ log φ
 320    have h := log_phi_gt_048
 321    have h1 : ((48 / 100 : ℚ) : ℝ) < log Real.goldenRatio := by
 322      calc ((48 / 100 : ℚ) : ℝ) = (0.48 : ℝ) := by norm_num
 323        _ < log Real.goldenRatio := h
 324    exact le_of_lt h1
 325  · -- log φ ≤ 0.483
 326    have h := log_phi_lt_0483
 327    have h1 : log Real.goldenRatio < ((483 / 1000 : ℚ) : ℝ) := by
 328      calc log Real.goldenRatio < (0.483 : ℝ) := h
 329        _ = ((483 / 1000 : ℚ) : ℝ) := by norm_num
 330    exact le_of_lt h1
 331
 332/-- Interval containing log(2) ≈ 0.693 -/
 333def log2Interval : Interval where
 334  lo := 693 / 1000
 335  hi := 694 / 1000
 336  valid := by norm_num
 337
 338/-- log(2) is contained in log2Interval - PROVEN using Mathlib's log_two bounds -/
 339theorem log_2_in_interval : log2Interval.contains (log 2) := by
 340  simp only [contains, log2Interval]
 341  constructor
 342  · -- 0.693 ≤ log 2

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.