`BookProof.ChapterCoherentOverlap.coherentOverlap_eq_gaussian` (q k : EuclideanSpace ℝ (Fin n)) : coherentOverlap q k = Real.exp (-‖q

Initializing...

`BookProof.ChapterCoherentOverlap.coherentOverlap_eq_gaussian` (q k : EuclideanSpace ℝ (Fin n)) : coherentOverlap q k = Real.exp (-‖q - k‖ ^ 2 / 2) · Prove2Me