phi_pow_2_interval

formal source

 135  exact lt_of_lt_of_le (by exact_mod_cast h_lo) h_in_145.1
 136
 137/-- Interval for φ^2 = φ + 1 -/
 138def phi_pow_2_interval : Interval :=
 139  phiInterval.add (Interval.point 1)
 140
 141lemma phi_pow_2_lo_pos : (0 : ℚ) < phi_pow_2_interval.lo := by
 142  unfold phi_pow_2_interval phiInterval; norm_num
 143
 144/-- Interval for φ^142 = φ^140 * φ^2 -/
 145def phi_pow_142_interval : Interval :=
 146  mulPos phi_pow_140_interval phi_pow_2_interval phi_pow_140_lo_pos phi_pow_2_lo_pos
 147
 148theorem phi_pow_142_in_interval : phi_pow_142_interval.contains (goldenRatio ^ (142 : ℝ)) := by
 149  have h_in_140 := phi_pow_140_in_interval
 150  have h_in_2 : phi_pow_2_interval.contains (goldenRatio ^ (2 : ℝ)) := by
 151    unfold phi_pow_2_interval
 152    have h_sq : goldenRatio ^ (2 : ℝ) = goldenRatio + 1 := goldenRatio_sq
 153    rw [h_sq]
 154    apply add_contains_add (phi_in_phiInterval) (contains_point 1)
 155  unfold phi_pow_142_interval
 156  have : goldenRatio ^ (142 : ℝ) = goldenRatio ^ (140 : ℝ) * goldenRatio ^ (2 : ℝ) := by
 157    rw [← Real.rpow_add goldenRatio_pos]; norm_num
 158  rw [this]
 159  apply mulPos_contains_mul phi_pow_140_lo_pos phi_pow_2_lo_pos h_in_140 h_in_2
 160
 161theorem phi_pow_142_lt_ratio_1_3 : phi_pow_142_interval.hi < 13/10 * galactic_ratio_rational := by
 162  unfold phi_pow_142_interval phi_pow_2_interval phi_pow_140_interval phi_pow_102_interval phi_pow_38_interval phi_pow_37_interval phi_pow_32_interval phi_pow_51_interval phi_pow_16_interval phi_pow_5_interval phiInterval mulPos Interval.add Interval.point
 163  norm_num
 164
 165theorem ratio_0_7_lt_phi_pow_142 : 7/10 * galactic_ratio_rational < phi_pow_142_interval.lo := by
 166  unfold phi_pow_142_interval phi_pow_2_interval phi_pow_140_interval phi_pow_102_interval phi_pow_38_interval phi_pow_37_interval phi_pow_32_interval phi_pow_51_interval phi_pow_16_interval phi_pow_5_interval phiInterval mulPos Interval.add Interval.point
 167  norm_num
 168