OAI/Analysis/KadisonKastler/CoreTraceScalarGauge.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Trace balance between the two scalar gauge actions

  1. theorem OAI.KadisonKastler.fourier_frequencyWindow line 16
  2. theorem OAI.KadisonKastler.fourier_character_apply line 24
  3. theorem OAI.KadisonKastler.fourier_character_star_apply line 31
  4. theorem OAI.KadisonKastler.coreTrace_scalarGauge_balance line 44