OAI/Analysis/KadisonKastler/CountableConjugacyAssembly.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Conjugacy on a countable Hilbert direct sum

The decomposition and reconstruction properties below describe a given block decomposition. They do not assert that an arbitrary algebra admits one. Coordinate conjugacies assemble without changing their uniform bound.

  1. def OAI.KadisonKastler.RepresentsBlockOperators line 19
  2. theorem OAI.KadisonKastler.RepresentsBlockOperators.unique line 24
  3. structure OAI.KadisonKastler.BlockAlgebraDecomposition line 33
  4. theorem OAI.KadisonKastler.l2FiberUnitary_star_apply line 41
  5. theorem OAI.KadisonKastler.blockOperator_conjugation_inclusion line 59
  6. theorem OAI.KadisonKastler.conjugates_l2FiberUnitary line 80
  7. theorem OAI.KadisonKastler.exists_bounded_conjugacy_of_block_implementers line 104