 199  simp [FApply, PApply_add]
 200  ring
 201
 202theorem FApply_neg {n : ℕ}
 203    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β w : Vec n) :
 204    FApply lam hInv β (-w) = -FApply lam hInv β w := by
 205  simpa using FApply_smul lam hInv β (-1) w
 206
 207theorem FApply_sub {n : ℕ}
 208    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 209    (v w : Vec n) :
 210    FApply lam hInv β (v - w) = FApply lam hInv β v - FApply lam hInv β w := by
 211  ext i
 212  simp [sub_eq_add_neg, FApply_add, FApply_neg]
 213
 214theorem FApply_square {n : ℕ}
 215    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 216    (hμ : mu lam hInv β ≠ 0) (v : Vec n) :
 217    FApply lam hInv β (FApply lam hInv β v) = v := by
 218  ext i
 219  have hPFi : PApply lam hInv β (FApply lam hInv β v) i = PApply lam hInv β v i := by
 220    simpa using congrFun (PApply_FApply lam hInv β hμ v) i
 221  calc
 222    FApply lam hInv β (FApply lam hInv β v) i
 223        = (2 • PApply lam hInv β (FApply lam hInv β v) - FApply lam hInv β v) i := by
 224            simp [FApply]
 225    _ = (2 • PApply lam hInv β v - FApply lam hInv β v) i := by
 226          simp [hPFi]
 227    _ = v i := by
 228          simp [FApply]
 229
 230theorem FApply_GApply {n : ℕ}
 231    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 232    (hμ : mu lam hInv β ≠ 0) (v : Vec n) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.