theorem
proved
FApply_sub
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 207.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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) :
217 FApply lam hInv β (FApply lam hInv β v) = v := by
218 ext i
219 have hPFi : PApply lam hInv β (FApply lam hInv β v) i = PApply lam hInv β v i := by
220 simpa using congrFun (PApply_FApply lam hInv β hμ v) i
221 calc
222 FApply lam hInv β (FApply lam hInv β v) i
223 = (2 • PApply lam hInv β (FApply lam hInv β v) - FApply lam hInv β v) i := by
224 simp [FApply]
225 _ = (2 • PApply lam hInv β v - FApply lam hInv β v) i := by
226 simp [hPFi]
227 _ = v i := by
228 simp [FApply]
229
230theorem FApply_GApply {n : ℕ}
231 (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
232 (hμ : mu lam hInv β ≠ 0) (v : Vec n) :
233 FApply lam hInv β (GApply lam hInv β v)
234 = ((1 : ℝ) / 2) • FApply lam hInv β v + (Real.sqrt 5 / 2) • v := by
235 unfold GApply
236 rw [FApply_add, FApply_smul, FApply_smul, FApply_square _ _ _ hμ]
237