theorem
proved
PApply_smul
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Cost.Ndim.Projector on GitHub at line 131.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
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