OAI/Analysis/KadisonKastler/StateCentralizerEquivalence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Equivalence of state and vector asymptotic centralizers

Four-unitary decomposition in the state-central sequence C-star algebra extends the quantitative unitary result to every bounded sequence.

  1. def OAI.KadisonKastler.stateSequenceVectorDefect line 24
  2. theorem OAI.KadisonKastler.StateAsymptoticallyCentral.vector line 32
  3. theorem OAI.KadisonKastler.asymptoticallyCentral_iff_state line 64
  4. theorem OAI.KadisonKastler.vectorBicentralizerMember_iff_state_sequences line 75