AApply_sq

formal source

 116    _ = mu lam hInv β * dot β v := by
 117          simp [mu, dot]
 118
 119theorem AApply_sq {n : ℕ}
 120    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β v : Vec n) :
 121    AApply lam hInv β (AApply lam hInv β v) = mu lam hInv β • AApply lam hInv β v := by
 122  funext i
 123  have hdot :
 124      dot β (fun k => lam * sharp hInv β k * dot β v) = mu lam hInv β * dot β v := by
 125    simpa [AApply] using dot_AApply lam hInv β v
 126  unfold AApply
 127  rw [hdot]
 128  simp [mu]
 129  ring
 130
 131theorem PApply_smul {n : ℕ}
 132    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 133    (c : ℝ) (v : Vec n) :
 134    PApply lam hInv β (c • v) = c • PApply lam hInv β v := by
 135  ext i
 136  simp [PApply, AApply_smul, mul_assoc, mul_comm]
 137
 138theorem PApply_add {n : ℕ}
 139    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 140    (v w : Vec n) :
 141    PApply lam hInv β (v + w) = PApply lam hInv β v + PApply lam hInv β w := by
 142  ext i
 143  simp [PApply, AApply_add]
 144  ring
 145
 146theorem PApply_neg {n : ℕ}
 147    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β w : Vec n) :
 148    PApply lam hInv β (-w) = -PApply lam hInv β w := by
 149  simpa using PApply_smul lam hInv β (-1) w