OAI/Analysis/KadisonKastler/CoreFrequencyFinite.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The finite-window reduction for the modular core

The frequency window is nonzero, and the weighted packet gives a faithful vector on its corner. Equality of the vector norms for an operator and its adjoint makes this corner finite.

  1. def OAI.KadisonKastler.unitCoreFrequencyProjection line 24
  2. theorem OAI.KadisonKastler.unitCoreFrequencyProjection_ne_zero line 32
  3. theorem OAI.KadisonKastler.unitCoreFrequencyProjection_finite_of_norm line 37
  4. theorem OAI.KadisonKastler.core_projectionSemifinite_of_window_norm line 52