OAI/Analysis/KadisonKastler/PositiveConeOrbitUniqueness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniqueness on the commutant-unitary orbit of the reference vector

A vector in the generated positive cone which is obtained from the reference vector by a commutant unitary must be the reference vector. The proof uses the centralizer identity and positivity of the quadratic operator attached to 1 - J u J.

  1. theorem OAI.KadisonKastler.positiveCone_commutant_unitary_fixed line 24