theorem
proved
tactic proof
MetallicApply_square
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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]
307
308end Ndim
309end Cost
310end IndisputableMonolith