OAI/Analysis/KadisonKastler/ModularCyclicGroup.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The scalar cyclic modular group

The phase multipliers form a strongly continuous unitary group. The cyclic isometry intertwines this group with the constructed original group, so its laws require no additional modular-theory input.

  1. abbrev OAI.KadisonKastler.ModularCyclicSpace line 22
  2. def OAI.KadisonKastler.modularCyclicPhaseOperator line 25
  3. theorem OAI.KadisonKastler.modularCyclicPhaseOperator_intertwines line 38
  4. theorem OAI.KadisonKastler.modularCyclicPhaseOperator_norm line 45
  5. theorem OAI.KadisonKastler.modularCyclicPhaseOperator_zero line 51
  6. theorem OAI.KadisonKastler.modularCyclicPhaseOperator_add line 58
  7. def OAI.KadisonKastler.modularCyclicUnitary line 69
  8. def OAI.KadisonKastler.modularCyclicGroup line 84
  9. theorem OAI.KadisonKastler.modularCyclicGroup_continuous line 94
  10. theorem OAI.KadisonKastler.modularCyclicGroup_apply_ae line 103