FApply_MetallicApply

formal source

 235  unfold GApply
 236  rw [FApply_add, FApply_smul, FApply_smul, FApply_square _ _ _ hμ]
 237
 238theorem FApply_MetallicApply {n : ℕ}
 239    (p q lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 240    (hμ : mu lam hInv β ≠ 0) (v : Vec n) :
 241    FApply lam hInv β (MetallicApply p q lam hInv β v)
 242      = (p / 2) • FApply lam hInv β v
 243        + (Real.sqrt (p ^ 2 + 4 * q) / 2) • v := by
 244  unfold MetallicApply
 245  rw [FApply_add, FApply_smul, FApply_smul, FApply_square _ _ _ hμ]
 246
 247theorem GApply_square {n : ℕ}
 248    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 249    (hμ : mu lam hInv β ≠ 0) (v : Vec n) :
 250    GApply lam hInv β (GApply lam hInv β v) = GApply lam hInv β v + v := by
 251  ext i
 252  have hFGi :
 253      FApply lam hInv β
 254          (((1 : ℝ) / 2) • v + (Real.sqrt 5 / 2) • FApply lam hInv β v) i
 255        = (((1 : ℝ) / 2) • FApply lam hInv β v + (Real.sqrt 5 / 2) • v) i := by
 256    simpa [GApply] using congrFun (FApply_GApply lam hInv β hμ v) i
 257  have hsqrt : Real.sqrt 5 * Real.sqrt 5 = 5 := by
 258    nlinarith [Real.sq_sqrt (by positivity : 0 ≤ (5 : ℝ))]
 259  have hsqrtq : (Real.sqrt 5 / 2) * (Real.sqrt 5 / 2) = 5 / 4 := by
 260    nlinarith [hsqrt]
 261  have hFGi' :
 262      FApply lam hInv β (((2 : ℝ)⁻¹) • v + (Real.sqrt 5 / 2) • FApply lam hInv β v) i
 263        = (((1 : ℝ) / 2) • FApply lam hInv β v + (Real.sqrt 5 / 2) • v) i := by
 264    simpa using hFGi
 265  simp [GApply]
 266  rw [hFGi']
 267  have hmul : (Real.sqrt 5 / 2) * ((Real.sqrt 5 / 2) * v i) = (5 / 4) * v i := by
 268    calc