`BookProof.ChapterSoftmaxBorn.coherentBorn_sq_eq` (q k : EuclideanSpace ℝ (Fin n)) : bornNumer q k = Real.exp (-‖q‖ ^ 2) * Real.exp (-‖k‖ ^ 2) * Real.exp (2 * inner ℝ q k)

Initializing...

`BookProof.ChapterSoftmaxBorn.coherentBorn_sq_eq` (q k : EuclideanSpace ℝ (Fin n)) : bornNumer q k = Real.exp (-‖q‖ ^ 2) * Real.exp (-‖k‖ ^ 2) * Real.exp (2 * inner ℝ q k) · Prove2Me