`BookProof.ChapterAttentionOutputVariance.headOutput_minimizes` (beta : ℝ) (s : Fin m → ℝ) (v : Fin m → E) (i : Fin m) (c : E) : ∑ j, scoreSoftmax beta s j * ‖v j

Initializing...

`BookProof.ChapterAttentionOutputVariance.headOutput_minimizes` (beta : ℝ) (s : Fin m → ℝ) (v : Fin m → E) (i : Fin m) (c : E) : ∑ j, scoreSoftmax beta s j * ‖v j - headOutput beta · Prove2Me