OAI/Analysis/KadisonKastler/CyclicAbelianExpectation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A contractive expectation for a cyclic commutative algebra

Average the conjugation action of the discrete abelian unitary group. Its fixed operators lie in the commutant, which is the original algebra by cyclicity. No normality of the expectation is asserted or needed.

  1. theorem OAI.KadisonKastler.mem_commutant_of_commute_unitaries line 25
  2. theorem OAI.KadisonKastler.isInjective_of_commutative_cyclic line 46