OAI/Analysis/KadisonKastler/CocycleCoreTransport.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Concrete core isomorphisms from unitary cocycles

  1. def OAI.KadisonKastler.ModularActionCocycle.gauge line 22
  2. theorem OAI.KadisonKastler.ModularActionCocycle.gauge_apply_ae line 25
  3. theorem OAI.KadisonKastler.ModularActionCocycle.gauge_symm_eq_star line 30
  4. theorem OAI.KadisonKastler.ModularActionCocycle.conj_of_intertwines line 46
  5. theorem OAI.KadisonKastler.ModularActionCocycle.gauge_embedding line 58
  6. theorem OAI.KadisonKastler.ModularActionCocycle.gauge_translation line 77
  7. theorem OAI.KadisonKastler.ModularActionCocycle.gauge_core_le line 112
  8. theorem OAI.KadisonKastler.ModularActionCocycle.gauge_conjugates_core line 129
  9. theorem OAI.KadisonKastler.ModularActionCocycle.core_equiv line 143