OAI/Analysis/KadisonKastler/AbelianDerivationAveraging.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Abelian averaging of a spatial derivation implementer

A spatial derivation preserving a von Neumann algebra also preserves its commutant. Averaging over any commuting unitary subgroup of the commutant keeps the same derivation, preserves the norm bound, and makes the implementer commute with that subgroup. This is the abelian averaging step in the spatial splitting argument.

  1. theorem OAI.KadisonKastler.commutator_mem_commutant_of_preserves line 21
  2. theorem OAI.KadisonKastler.unitaryConj_sub_mem_commutant_of_preserves line 39
  3. theorem OAI.KadisonKastler.exists_abelian_averaged_implementer line 53