theorem
proved
MetallicApply_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 276.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
273 simp
274 nlinarith [hmul]
275
276theorem MetallicApply_square {n : ℕ}
277 (p q lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n)
278 (hμ : mu lam hInv β ≠ 0) (hq : 0 ≤ p ^ 2 + 4 * q) (v : Vec n) :
279 MetallicApply p q lam hInv β (MetallicApply p q lam hInv β v)
280 = p • MetallicApply p q lam hInv β v + q • v := by
281 ext i
282 have hFMi :
283 FApply lam hInv β
284 ((p / 2) • v + (Real.sqrt (p ^ 2 + 4 * q) / 2) • FApply lam hInv β v) i
285 = ((p / 2) • FApply lam hInv β v
286 + (Real.sqrt (p ^ 2 + 4 * q) / 2) • v) i := by
287 simpa [MetallicApply] using congrFun (FApply_MetallicApply p q lam hInv β hμ v) i
288 have hsqrt : Real.sqrt (p ^ 2 + 4 * q) * Real.sqrt (p ^ 2 + 4 * q) = p ^ 2 + 4 * q := by
289 nlinarith [Real.sq_sqrt hq]
290 have hsqrtq :
291 (Real.sqrt (p ^ 2 + 4 * q) / 2) * (Real.sqrt (p ^ 2 + 4 * q) / 2)
292 = (p ^ 2 + 4 * q) / 4 := by
293 nlinarith [hsqrt]
294 simp [MetallicApply, hFMi]
295 have hmul :
296 (Real.sqrt (p ^ 2 + 4 * q) / 2) *
297 ((Real.sqrt (p ^ 2 + 4 * q) / 2) * v i)
298 = ((p ^ 2 + 4 * q) / 4) * v i := by
299 calc
300 (Real.sqrt (p ^ 2 + 4 * q) / 2) *
301 ((Real.sqrt (p ^ 2 + 4 * q) / 2) * v i)
302 = ((Real.sqrt (p ^ 2 + 4 * q) / 2) *
303 (Real.sqrt (p ^ 2 + 4 * q) / 2)) * v i := by
304 ring
305 _ = ((p ^ 2 + 4 * q) / 4) * v i := by rw [hsqrtq]
306 nlinarith [hmul]