theorem
proved
FApply_square
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Cost.Ndim.Projector on GitHub at line 214.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
238theorem FApply_MetallicApply {n : ℕ}
239 (p q lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
240 (hμ : mu lam hInv β ≠ 0) (v : Vec n) :
241 FApply lam hInv β (MetallicApply p q lam hInv β v)
242 = (p / 2) • FApply lam hInv β v
243 + (Real.sqrt (p ^ 2 + 4 * q) / 2) • v := by
244 unfold MetallicApply