`BookProof.ChapterCoherentGeometry.neg_two_mul_log_coherentOverlap` (q k : EuclideanSpace ℝ (Fin n)) : -2 * Real.log (coherentOverlap q k) = ‖q

Initializing...

`BookProof.ChapterCoherentGeometry.neg_two_mul_log_coherentOverlap` (q k : EuclideanSpace ℝ (Fin n)) : -2 * Real.log (coherentOverlap q k) = ‖q - k‖ ^ 2 · Prove2Me