`BookProof.ChapterAttentionSink.sink_denom` (beta s0 : ℝ) (s : Fin m → ℝ) : ∑ l, Real.exp (beta * (Fin.cons s0 s : Fin (m + 1) → ℝ) l) = Real.exp (beta * s0) + ∑ l, Real.exp (beta

Initializing...

`BookProof.ChapterAttentionSink.sink_denom` (beta s0 : ℝ) (s : Fin m → ℝ) : ∑ l, Real.exp (beta * (Fin.cons s0 s : Fin (m + 1) → ℝ) l) = Real.exp (beta * s0) + ∑ l, Real.exp (beta · Prove2Me