def
definition
phi_pow_38_interval
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Numerics.Interval.GalacticBounds on GitHub at line 50.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
47 exact mul_pos phi_pow_32_lo_pos phi_pow_5_lo_pos
48
49/-- Interval for φ^38 = φ^37 * φ^1 -/
50def phi_pow_38_interval : Interval :=
51 mulPos phi_pow_37_interval phiInterval phi_pow_37_lo_pos phi_lo_pos
52
53lemma phi_pow_102_lo_pos : (0 : ℚ) < phi_pow_102_interval.lo := by
54 unfold phi_pow_102_interval mulPos; dsimp
55 exact mul_pos phi_pow_51_lo_pos phi_pow_51_lo_pos
56
57lemma phi_pow_38_lo_pos : (0 : ℚ) < phi_pow_38_interval.lo := by
58 unfold phi_pow_38_interval mulPos; dsimp
59 exact mul_pos phi_pow_37_lo_pos phi_lo_pos
60
61/-- Interval for φ^140 = φ^102 * φ^38 -/
62def phi_pow_140_interval : Interval :=
63 mulPos phi_pow_102_interval phi_pow_38_interval phi_pow_102_lo_pos phi_pow_38_lo_pos
64
65lemma phi_pow_140_lo_pos : (0 : ℚ) < phi_pow_140_interval.lo := by
66 unfold phi_pow_140_interval mulPos; dsimp
67 exact mul_pos phi_pow_102_lo_pos phi_pow_38_lo_pos
68
69/-- Interval for φ^145 = φ^140 * φ^5 -/
70def phi_pow_145_interval : Interval :=
71 mulPos phi_pow_140_interval phi_pow_5_interval phi_pow_140_lo_pos phi_pow_5_lo_pos
72
73theorem phi_pow_140_in_interval : phi_pow_140_interval.contains (goldenRatio ^ (140 : ℝ)) := by
74 have h_in_51 : phi_pow_51_interval.contains (goldenRatio ^ (51 : ℝ)) := phi_pow_51_in_interval
75 have h_in_102 : phi_pow_102_interval.contains (goldenRatio ^ (102 : ℝ)) := by
76 unfold phi_pow_102_interval
77 have : goldenRatio ^ (102 : ℝ) = goldenRatio ^ (51 : ℝ) * goldenRatio ^ (51 : ℝ) := by
78 rw [← Real.rpow_add goldenRatio_pos]; norm_num
79 rw [this]
80 apply mulPos_contains_mul phi_pow_51_lo_pos phi_pow_51_lo_pos h_in_51 h_in_51