`BookProof.ChapterCoherentOverlapComplex.norm_coherentOverlapC` (q k : EuclideanSpace ℂ (Fin n)) : ‖coherentOverlapC q k‖ = Real.exp (-‖q‖ ^ 2 / 2 - ‖k‖ ^ 2 / 2 + (inner ℂ q k : ℂ)
ProvedBookProof.ChapterCoherentOverlapComplex.norm_coherentOverlapCtheoremstimepiece
Prove the following Lean 4 theorem from ChapterCoherentOverlapComplex.
BookProof.ChapterCoherentOverlapComplex.norm_coherentOverlapC (q k : EuclideanSpace ℂ (Fin n)) : ‖coherentOverlapC q k‖ = Real.exp (-‖q‖ ^ 2 / 2 - ‖k‖ ^ 2 / 2 + (inner ℂ q k : ℂ).re)
Formalization note: Lean 4 identifier BookProof.ChapterCoherentOverlapComplex.norm_coherentOverlapC.
Preamble
-- Generated from ChapterCoherentOverlapComplex.lean — theorem BookProof.ChapterCoherentOverlapComplex.norm_coherentOverlapC
import Mathlib
import Definitions.Def_ChapterCoherentOverlapComplex
open BookProof.ChapterCoherentOverlapComplex
open scoped BigOperators
noncomputable section
variable {n m : ℕ}Formal statement
theorem BookProof.ChapterCoherentOverlapComplex.norm_coherentOverlapC (q k : EuclideanSpace ℂ (Fin n)) :
‖coherentOverlapC q k‖
= Real.exp (-‖q‖ ^ 2 / 2 - ‖k‖ ^ 2 / 2 + (inner ℂ q k : ℂ).re) := by sorry