PApply_add

formal source

 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
 150
 151theorem PApply_sub {n : ℕ}
 152    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 153    (v w : Vec n) :
 154    PApply lam hInv β (v - w) = PApply lam hInv β v - PApply lam hInv β w := by
 155  ext i
 156  simp [sub_eq_add_neg, PApply_add, PApply_neg]
 157
 158theorem PApply_idempotent {n : ℕ}
 159    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 160    (hμ : mu lam hInv β ≠ 0) (v : Vec n) :
 161    PApply lam hInv β (PApply lam hInv β v) = PApply lam hInv β v := by
 162  ext i
 163  simp [PApply, AApply_smul, AApply_sq, hμ, mul_comm]
 164
 165theorem PApply_FApply {n : ℕ}
 166    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 167    (hμ : mu lam hInv β ≠ 0) (v : Vec n) :
 168    PApply lam hInv β (FApply lam hInv β v) = PApply lam hInv β v := by