`BookProof.ChapterIrreversible.entropy_bornDist_pos_iff` (v : Fin n → ℂ) (hv : ∑ a, ‖v a‖ ^ 2 = 1) : 0 < entropy (bornDist v) ↔ ¬ IsDeterministicColumn v

Initializing...

`BookProof.ChapterIrreversible.entropy_bornDist_pos_iff` (v : Fin n → ℂ) (hv : ∑ a, ‖v a‖ ^ 2 = 1) : 0 < entropy (bornDist v) ↔ ¬ IsDeterministicColumn v · Prove2Me