OAI/Analysis/KadisonKastler/SignedCyclicFunctional.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A cyclic signed-vector model for a Hermitian functional

The norm-additive positive parts give a two-summand GNS representation. Equality in the coefficient norm bound makes its sign preserve the cyclic subspace. Restricting there gives the precise model used in the separation argument, with no polar-decomposition hypothesis.

  1. theorem OAI.KadisonKastler.exists_signed_cyclic_functional line 25