OAI/Analysis/KadisonKastler/CoreFrequencyCuts.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Frequency windows in the concrete modular core

The translation generators and the proved real spectral commutant theorem put the Fourier interval projections inside the actual generated core.

  1. theorem OAI.KadisonKastler.regularFourierIndicator_mem_core line 25
  2. theorem OAI.KadisonKastler.regularFrequencyProjection_mem_core line 58
  3. def OAI.KadisonKastler.regularFrequencyWindow line 63

    Source documentation

    A bounded frequency interval, used for the finite-weight core corners.

    def regularFrequencyWindow (a b : ℝ) : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H :=
…

    Mentions: OAI.KadisonKastler.RegularCoreHilbert

  4. theorem OAI.KadisonKastler.regularFrequencyWindow_mem_core line 67
  5. theorem OAI.KadisonKastler.regularFrequencyWindow_isStarProjection line 71