OAI/Analysis/KadisonKastler/CyclicGaugeSwap.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The full cyclic gauge under the L2 variable swap

  1. abbrev OAI.KadisonKastler.modularCyclicMeasure line 22
  2. def OAI.KadisonKastler.modularCyclicGauge line 25
  3. def OAI.KadisonKastler.modularCharacterField line 30
  4. theorem OAI.KadisonKastler.cyclicGauge_swap line 36
  5. theorem OAI.KadisonKastler.cyclicGauge_star_swap line 45