PApply_FApply

formal source

 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
 182  rw [hsubi, hsmuli]
 183  simp [hidi]
 184  ring
 185
 186theorem FApply_smul {n : ℕ}
 187    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 188    (c : ℝ) (v : Vec n) :
 189    FApply lam hInv β (c • v) = c • FApply lam hInv β v := by
 190  ext i
 191  simp [FApply, PApply_smul, mul_comm]
 192  ring
 193
 194theorem FApply_add {n : ℕ}
 195    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)