OAI/Analysis/KadisonKastler/ScalarGaugeWindowBalance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Scalar-field and gauge lifting of the finite-window trace identity

  1. theorem OAI.KadisonKastler.regularFrequencyWindow_tensor line 18
  2. theorem OAI.KadisonKastler.l2ScalarSwap_frequencyWindow line 29
  3. theorem OAI.KadisonKastler.characterField_window_balance line 39
  4. theorem OAI.KadisonKastler.scalarGaugeWindowBalance line 81