`BookProof.ChapterAttentionCoarseGrain.le_mergeWeights` {f : Fin m → Fin r} {p : Fin m → ℝ} (hp : ∀ x, 0 ≤ p x) (x : Fin m) : p x ≤ mergeWeights f p (f x)

Initializing...

`BookProof.ChapterAttentionCoarseGrain.le_mergeWeights` {f : Fin m → Fin r} {p : Fin m → ℝ} (hp : ∀ x, 0 ≤ p x) (x : Fin m) : p x ≤ mergeWeights f p (f x) · Prove2Me