`BookProof.ChapterAttentionRetrieval.exp_le_denom` (beta : ℝ) (s : Fin m → ℝ) (j : Fin m) : Real.exp (beta * s j) ≤ ∑ l, Real.exp (beta * s l)

Initializing...

`BookProof.ChapterAttentionRetrieval.exp_le_denom` (beta : ℝ) (s : Fin m → ℝ) (j : Fin m) : Real.exp (beta * s j) ≤ ∑ l, Real.exp (beta * s l) · Prove2Me