`FApply_smul`

proved

show as: view math explainer →

module: IndisputableMonolith.Cost.Ndim.Projector
domain: Cost
line: 186 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Cost.Ndim.Projector on GitHub at line 186.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 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)
 196    (v w : Vec n) :
 197    FApply lam hInv β (v + w) = FApply lam hInv β v + FApply lam hInv β w := by
 198  ext i
 199  simp [FApply, PApply_add]
 200  ring
 201
 202theorem FApply_neg {n : ℕ}
 203    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β w : Vec n) :
 204    FApply lam hInv β (-w) = -FApply lam hInv β w := by
 205  simpa using FApply_smul lam hInv β (-1) w
 206
 207theorem FApply_sub {n : ℕ}
 208    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 209    (v w : Vec n) :
 210    FApply lam hInv β (v - w) = FApply lam hInv β v - FApply lam hInv β w := by
 211  ext i
 212  simp [sub_eq_add_neg, FApply_add, FApply_neg]
 213
 214theorem FApply_square {n : ℕ}
 215    (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
 216    (hμ : mu lam hInv β ≠ 0) (v : Vec n) :

papers checked against this theorem

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