`BookProof.ChapterAttentionOutputVariance.sum_dist_sq_expand` {p : Fin m → ℝ} (hp : ∑ j, p j = 1) (v : Fin m → E) (c : E) : ∑ j, p j * ‖v j - c‖ ^ 2 = (∑ j, p j * ‖v j‖ ^ 2)

Initializing...

`BookProof.ChapterAttentionOutputVariance.sum_dist_sq_expand` {p : Fin m → ℝ} (hp : ∑ j, p j = 1) (v : Fin m → E) (c : E) : ∑ j, p j * ‖v j - c‖ ^ 2 = (∑ j, p j * ‖v j‖ ^ 2) - 2 * · Prove2Me