OAI/Analysis/KadisonKastler/ModularActionCocycle.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Unitary cocycles between represented modular actions

These are the cocycles occurring in the change-of-state theorem. The construction of a cocycle from two faithful states is a separate step.

  1. structure OAI.KadisonKastler.ModularActionCocycle line 19
  2. theorem OAI.KadisonKastler.ModularActionCocycle.star_unitaryConj line 37
  3. def OAI.KadisonKastler.ModularActionCocycle.symm line 41
  4. def OAI.KadisonKastler.ModularActionCocycle.regularField line 59
  5. theorem OAI.KadisonKastler.ModularActionCocycle.regularField_measurable line 62
  6. theorem OAI.KadisonKastler.ModularActionCocycle.regularField_star_measurable line 66
  7. theorem OAI.KadisonKastler.ModularActionCocycle.regularField_embedding line 70
  8. theorem OAI.KadisonKastler.ModularActionCocycle.regularField_translation line 80