OAI/Analysis/KadisonKastler/CyclicGaugeKernel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The cyclic gauge as a field of scalar characters

Interchanging the time and spectral variables turns the cyclic modular gauge into ordinary character multiplication in each spectral fiber.

  1. theorem OAI.KadisonKastler.characterField_measurable line 25
  2. theorem OAI.KadisonKastler.characterField_star_measurable line 30
  3. def OAI.KadisonKastler.characterField line 46
  4. theorem OAI.KadisonKastler.characterField_apply_ae line 50
  5. theorem OAI.KadisonKastler.cyclicGauge_tensor_rows line 63
  6. theorem OAI.KadisonKastler.characterField_tensor_rows line 86
  7. theorem OAI.KadisonKastler.cyclicGauge_swap_tensor line 106