OAI/Analysis/KadisonKastler/CoreTraceScalarBalance.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The trace balance on scalar L2 frequency packets

  1. theorem OAI.KadisonKastler.unitWindow_translate_conjugate line 13
  2. theorem OAI.KadisonKastler.coreTraceFrequencyScalar_spectral_balance line 42