`BookProof.ChapterAttentionRetrieval.norm_headOutput_sub_le_of_margin` {beta delta C : ℝ} (hb : 0 ≤ beta) (s : Fin m → ℝ) (v : Fin m → E) (j : Fin m) (hmargin : ∀ l, l ≠ j → s l +

Initializing...

`BookProof.ChapterAttentionRetrieval.norm_headOutput_sub_le_of_margin` {beta delta C : ℝ} (hb : 0 ≤ beta) (s : Fin m → ℝ) (v : Fin m → E) (j : Fin m) (hmargin : ∀ l, l ≠ j → s l + · Prove2Me