`BookProof.ChapterObservableExpectation.attention_eq_expectation` (q : EuclideanSpace ℝ (Fin n)) (k : Fin m → EuclideanSpace ℝ (Fin n)) (v : Fin m → E) (j₀ : Fin m) : (∀ j, 0 ≤ bor

Initializing...

`BookProof.ChapterObservableExpectation.attention_eq_expectation` (q : EuclideanSpace ℝ (Fin n)) (k : Fin m → EuclideanSpace ℝ (Fin n)) (v : Fin m → E) (j₀ : Fin m) : (∀ j, 0 ≤ bor · Prove2Me