theorem
proved
log_phi_interval_contains
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Numerics.Interval.Tactic on GitHub at line 51.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
48 phiInterval.contains ((1 + Real.sqrt 5) / 2) := phi_in_phiInterval
49
50/-- Prove that log(φ) is in its interval -/
51theorem log_phi_interval_contains :
52 logPhiInterval.contains (Real.log ((1 + Real.sqrt 5) / 2)) := log_phi_in_interval
53
54/-- Example: Prove log(φ) > 0.48 (using interval lo = 481/1000 = 0.481) -/
55theorem log_phi_gt_048 : (0.48 : ℝ) < Real.log ((1 + Real.sqrt 5) / 2) := by
56 have h := log_phi_in_interval
57 -- logPhiInterval.lo = 481/1000 > 0.48
58 have h1 : (0.48 : ℝ) < (481 / 1000 : ℚ) := by norm_num
59 exact lt_of_lt_of_le h1 h.1
60
61/-- Example: Prove log(φ) < 0.49 (using interval hi = 482/1000 = 0.482) -/
62theorem log_phi_lt_049 : Real.log ((1 + Real.sqrt 5) / 2) < (0.49 : ℝ) := by
63 have h := log_phi_in_interval
64 -- logPhiInterval.hi = 482/1000 < 0.49
65 have h1 : ((482 / 1000 : ℚ) : ℝ) < (0.49 : ℝ) := by norm_num
66 exact lt_of_le_of_lt h.2 h1
67
68/-- Example: Prove φ > 1.61 (using interval lo = 1618/1000) -/
69theorem phi_gt_161 : (1.61 : ℝ) < (1 + Real.sqrt 5) / 2 := by
70 have h := phi_in_phiInterval
71 -- phiInterval.lo = 1618/1000 > 1.61
72 have h1 : (1.61 : ℝ) < (1618 / 1000 : ℚ) := by norm_num
73 exact lt_of_lt_of_le h1 h.1
74
75/-- Example: Prove φ < 1.62 (using interval hi = 1619/1000) -/
76theorem phi_lt_162 : (1 + Real.sqrt 5) / 2 < (1.62 : ℝ) := by
77 have h := phi_in_phiInterval
78 -- phiInterval.hi = 1619/1000 < 1.62
79 have h1 : ((1619 / 1000 : ℚ) : ℝ) < (1.62 : ℝ) := by norm_num
80 exact lt_of_le_of_lt h.2 h1
81