`BookProof.ChapterAttentionOutputVariance.outputVariance_const` (p : Fin m → ℝ) (hp : ∑ j, p j = 1) (w : E) : outputVariance p (fun _ => w) = 0

Initializing...

`BookProof.ChapterAttentionOutputVariance.outputVariance_const` (p : Fin m → ℝ) (hp : ∑ j, p j = 1) (w : E) : outputVariance p (fun _ => w) = 0 · Prove2Me