`BookProof.ChapterAttentionOutput.norm_headOutput_le` (beta : ℝ) (s : Fin m → ℝ) {v : Fin m → E} {C : ℝ} (hv : ∀ j, ‖v j‖ ≤ C) (i : Fin m) : ‖headOutput beta s v‖ ≤ C

Initializing...

`BookProof.ChapterAttentionOutput.norm_headOutput_le` (beta : ℝ) (s : Fin m → ℝ) {v : Fin m → E} {C : ℝ} (hv : ∀ j, ‖v j‖ ≤ C) (i : Fin m) : ‖headOutput beta s v‖ ≤ C · Prove2Me