def
definition
phi_pow_37_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 42.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
39 exact mul_pos phi_pow_16_lo_pos phi_pow_16_lo_pos
40
41/-- Interval for φ^37 = φ^32 * φ^5 -/
42def phi_pow_37_interval : Interval :=
43 mulPos phi_pow_32_interval phi_pow_5_interval phi_pow_32_lo_pos phi_pow_5_lo_pos
44
45lemma phi_pow_37_lo_pos : (0 : ℚ) < phi_pow_37_interval.lo := by
46 unfold phi_pow_37_interval mulPos; dsimp
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