OAI/Analysis/KadisonKastler/CoreFrequencyUnitWindow.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A nonzero bounded frequency window in the modular core

The unit interval supplies an explicit isometric family of vectors fixed by its frequency projection. No trace or finiteness assertion is used here.

  1. def OAI.KadisonKastler.unitFrequencyScalar line 19
  2. theorem OAI.KadisonKastler.norm_unitFrequencyScalar line 23
  3. theorem OAI.KadisonKastler.unitFrequencyScalar_fixed line 27
  4. def OAI.KadisonKastler.unitFrequencyVector line 42
  5. theorem OAI.KadisonKastler.norm_unitFrequencyVector line 45
  6. theorem OAI.KadisonKastler.unitFrequencyVector_fixed line 48
  7. theorem OAI.KadisonKastler.regularFrequencyWindow_unit_ne_zero line 52