`BookProof.ChapterTrajectory.finalProb_total` (U V : Matrix (Fin n) (Fin n) ℂ) (psi : Fin n → ℂ) (hU : Uᴴ * U = 1) (hV : Vᴴ * V = 1) (hpsi : ∑ a, ‖psi a‖ ^ 2 = 1) : ∑ f, finalProb

Initializing...

`BookProof.ChapterTrajectory.finalProb_total` (U V : Matrix (Fin n) (Fin n) ℂ) (psi : Fin n → ℂ) (hU : Uᴴ * U = 1) (hV : Vᴴ * V = 1) (hpsi : ∑ a, ‖psi a‖ ^ 2 = 1) : ∑ f, finalProb · Prove2Me