theorem
proved
GApply_square
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 247.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
244 unfold MetallicApply
245 rw [FApply_add, FApply_smul, FApply_smul, FApply_square _ _ _ hμ]
246
247theorem GApply_square {n : ℕ}
248 (lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
249 (hμ : mu lam hInv β ≠ 0) (v : Vec n) :
250 GApply lam hInv β (GApply lam hInv β v) = GApply lam hInv β v + v := by
251 ext i
252 have hFGi :
253 FApply lam hInv β
254 (((1 : ℝ) / 2) • v + (Real.sqrt 5 / 2) • FApply lam hInv β v) i
255 = (((1 : ℝ) / 2) • FApply lam hInv β v + (Real.sqrt 5 / 2) • v) i := by
256 simpa [GApply] using congrFun (FApply_GApply lam hInv β hμ v) i
257 have hsqrt : Real.sqrt 5 * Real.sqrt 5 = 5 := by
258 nlinarith [Real.sq_sqrt (by positivity : 0 ≤ (5 : ℝ))]
259 have hsqrtq : (Real.sqrt 5 / 2) * (Real.sqrt 5 / 2) = 5 / 4 := by
260 nlinarith [hsqrt]
261 have hFGi' :
262 FApply lam hInv β (((2 : ℝ)⁻¹) • v + (Real.sqrt 5 / 2) • FApply lam hInv β v) i
263 = (((1 : ℝ) / 2) • FApply lam hInv β v + (Real.sqrt 5 / 2) • v) i := by
264 simpa using hFGi
265 simp [GApply]
266 rw [hFGi']
267 have hmul : (Real.sqrt 5 / 2) * ((Real.sqrt 5 / 2) * v i) = (5 / 4) * v i := by
268 calc
269 (Real.sqrt 5 / 2) * ((Real.sqrt 5 / 2) * v i)
270 = ((Real.sqrt 5 / 2) * (Real.sqrt 5 / 2)) * v i := by
271 ring
272 _ = (5 / 4) * v i := by rw [hsqrtq]
273 simp
274 nlinarith [hmul]
275
276theorem MetallicApply_square {n : ℕ}
277 (p q lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)