def
definition
phi_pow_32_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 34.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
31 unfold phiInterval; norm_num
32
33/-- Interval for φ^32 = (φ^16)^2 -/
34def phi_pow_32_interval : Interval :=
35 mulPos phi_pow_16_interval phi_pow_16_interval phi_pow_16_lo_pos phi_pow_16_lo_pos
36
37lemma phi_pow_32_lo_pos : (0 : ℚ) < phi_pow_32_interval.lo := by
38 unfold phi_pow_32_interval mulPos; dsimp
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