 100  ext i
 101  simp [sub_eq_add_neg, AApply_add, AApply_neg]
 102
 103theorem dot_AApply {n : ℕ}
 104    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β v : Vec n) :
 105    dot β (AApply lam hInv β v) = mu lam hInv β * dot β v := by
 106  unfold dot AApply mu
 107  calc
 108    ∑ i : Fin n, β i * (lam * sharp hInv β i * dot β v)
 109        = (lam * dot β v) * ∑ i : Fin n, β i * sharp hInv β i := by
 110            rw [Finset.mul_sum]
 111            apply Finset.sum_congr rfl
 112            intro i hi
 113            ring
 114    _ = (lam * ∑ i : Fin n, β i * sharp hInv β i) * dot β v := by
 115          ring
 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) :

papers checked against this theorem

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