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

Initializing...

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