phi_pow_8_upper

formal source

  67  linarith
  68
  69/-- `φ^8 < 47.03` (from `φ < 1.62`). -/
  70theorem phi_pow_8_upper : phi ^ (8 : ℕ) < 47.03 := by
  71  rw [phi_pow_8_fib]
  72  have hphi : phi < 1.62 := phi_lt_onePointSixTwo
  73  linarith
  74
  75/-! ## φ^(−8) bounds -/
  76
  77private lemma phi_zpow_neg8_eq_inv : phi ^ (-8 : ℤ) = (phi ^ (8 : ℕ))⁻¹ := by
  78  rw [show ((-8 : ℤ)) = -((8 : ℕ) : ℤ) from by norm_num, zpow_neg, zpow_natCast]
  79
  80theorem phi_zpow_neg8_lower : phi ^ (-8 : ℤ) > 0.02126 := by
  81  rw [phi_zpow_neg8_eq_inv]
  82  have hupper : phi ^ (8 : ℕ) < 47.03 := phi_pow_8_upper
  83  have hpos : (0 : ℝ) < phi ^ (8 : ℕ) := pow_pos phi_pos 8
  84  have h1 : (phi ^ (8 : ℕ))⁻¹ > (47.03 : ℝ)⁻¹ := by
  85    rw [gt_iff_lt, inv_lt_inv₀ (by norm_num : (0:ℝ) < 47.03) hpos]
  86    exact hupper
  87  have h2 : (47.03 : ℝ)⁻¹ ≥ 0.02126 := by norm_num
  88  linarith
  89
  90theorem phi_zpow_neg8_upper : phi ^ (-8 : ℤ) < 0.02137 := by
  91  rw [phi_zpow_neg8_eq_inv]
  92  have hlower : phi ^ (8 : ℕ) > 46.81 := phi_pow_8_lower
  93  have hpos : (0 : ℝ) < phi ^ (8 : ℕ) := pow_pos phi_pos 8
  94  have h1 : (phi ^ (8 : ℕ))⁻¹ < (46.81 : ℝ)⁻¹ := by
  95    rw [inv_lt_inv₀ hpos (by norm_num : (0:ℝ) < 46.81)]
  96    exact hlower
  97  have h2 : (46.81 : ℝ)⁻¹ ≤ 0.02137 := by norm_num
  98  linarith
  99
 100/-! ## The two-sided washout prefactor -/