OAI/Analysis/KadisonKastler/CoreWindowDualComparison.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Dual translation changes the trace of every nonzero sub-half-window

  1. def OAI.KadisonKastler.coreFrequencyProjection line 20
  2. theorem OAI.KadisonKastler.coreFrequencyProjection_le line 31
  3. def OAI.KadisonKastler.constructedCoreDualEquiv line 47
  4. theorem OAI.KadisonKastler.constructedCore_subhalf_not_equivalent_dual line 55