PApply_sub

formal source

 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
 169  ext i
 170  have hsubi :
 171      PApply lam hInv β (FApply lam hInv β v) i
 172        = PApply lam hInv β (2 • PApply lam hInv β v) i - PApply lam hInv β v i := by
 173    unfold FApply
 174    rw [PApply_sub]
 175    rfl
 176  have hsmuli :
 177      PApply lam hInv β (2 • PApply lam hInv β v) i
 178        = (2 • PApply lam hInv β (PApply lam hInv β v)) i := by
 179    simpa using congrFun (PApply_smul lam hInv β 2 (PApply lam hInv β v)) i
 180  have hidi : PApply lam hInv β (PApply lam hInv β v) i = PApply lam hInv β v i := by
 181    simpa using congrFun (PApply_idempotent lam hInv β hμ v) i