phi_lt_1_7

formal source

  87  linarith
  88
  89/-- Upper bound for φ. -/
  90lemma phi_lt_1_7 : phi < 1.7 := by
  91  unfold phi
  92  norm_num
  93  have : Real.sqrt 5 < 2.4 := by
  94    rw [← Real.sqrt_sq (by norm_num : (0:ℝ)≤2.4)]
  95    apply Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
  96  linarith
  97
  98/-- φ¹⁰ > 100. -/
  99theorem phi_10_bounds : phi_power 10 > 100 := by
 100  unfold phi_power
 101  have h : phi > 1.6 := phi_gt_1_6
 102  have h10 : phi ^ 10 > 1.6 ^ 10 := pow_lt_pow_left h (by norm_num) (by norm_num)
 103  have : (1.6 : ℝ) ^ 10 > 100 := by norm_num
 104  exact gt_of_gt_of_gt h10 this
 105
 106/-- φ¹³ < 550. -/
 107theorem phi_13_bounds : phi_power 13 < 550 := by
 108  unfold phi_power
 109  have h : phi < 1.62 := by
 110    unfold phi
 111    norm_num
 112    have : Real.sqrt 5 < 2.24 := by
 113      rw [← Real.sqrt_sq (by norm_num : (0:ℝ)≤2.24)]
 114      apply Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
 115    linarith
 116  have h13 : phi ^ 13 < 1.62 ^ 13 := pow_lt_pow_left h (by norm_num) (by norm_num)
 117  have : (1.62 : ℝ) ^ 13 < 550 := by norm_num
 118  exact lt_trans h13 this
 119
 120/-! ## Recognition Cost Derivation -/