`BookProof.ChapterAttentionSparse.one_sub_attendedMass_eq` (beta : ℝ) (s : Fin m → ℝ) (S : Finset (Fin m)) (i : Fin m) : 1 - attendedMass beta s S = ∑ l ∈ Sᶜ, scoreSoftmax beta s l

Initializing...

`BookProof.ChapterAttentionSparse.one_sub_attendedMass_eq` (beta : ℝ) (s : Fin m → ℝ) (S : Finset (Fin m)) (i : Fin m) : 1 - attendedMass beta s S = ∑ l ∈ Sᶜ, scoreSoftmax beta s l · Prove2Me