`BookProof.ChapterTrajectory.jointProb_nonneg` (U V : Matrix (Fin n) (Fin n) ℂ) (psi : Fin n → ℂ) (f a : Fin n) : 0 ≤ jointProb U V psi f a

Initializing...

`BookProof.ChapterTrajectory.jointProb_nonneg` (U V : Matrix (Fin n) (Fin n) ℂ) (psi : Fin n → ℂ) (f a : Fin n) : 0 ≤ jointProb U V psi f a · Prove2Me