pith. machine review for the scientific record. sign in
theorem proved term proof

embed_norm_sq

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 110theorem embed_norm_sq (s : SmallDeviationState N) :
 111    (Finset.univ.sum fun i => Complex.normSq (embed s i)) =
 112    Finset.univ.sum fun i => (s.deviations i) ^ 2 := by

proof body

Term-mode proof.

 113  apply Finset.sum_congr rfl
 114  intro i _
 115  simp [embed, Complex.normSq_ofReal]
 116  ring
 117
 118/-! ## Discrete Evolution Operator -/
 119
 120/-- The discrete evolution operator at small strain: applies R̂ in the
 121    quadratic regime, parameterized by a real "Hamiltonian matrix" H. -/

depends on (6)

Lean names referenced from this declaration's body.