OAI/Analysis/KadisonKastler/CoreTraceDualScaling.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Dual-character rescaling of the supported trace vector

This is the local exponential rescaling needed to distinguish the semifinite core from a finite or type I factor.

  1. theorem OAI.KadisonKastler.regularTranslateApply_tensorVector line 22
  2. theorem OAI.KadisonKastler.regularCharacterStar_frequencyPacket line 35
  3. theorem OAI.KadisonKastler.regularFrequencyPacket_smul line 50
  4. theorem OAI.KadisonKastler.coreTraceFrequencyVector_dual_scaling line 55
  5. theorem OAI.KadisonKastler.coreTraceFrequencyVector_supported_scaling line 68

    Source documentation

    On the overlap of two windows the dual translate scales the trace vector.

    theorem coreTraceFrequencyVector_supported_scaling (a : ℝ) (Ω : H)
    (T : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
    (hT₀ : T * regularFrequencyWindow 0 1 = T)
    (hTₐ : T * regularFrequencyWindow (-a) (1 - a) = T) :
    T ((star (regularCharacterUnitary (H := H) (2 * Real.pi * a)) :
…

    Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularFrequencyWindow, OAI.KadisonKastler.regularCharacterUnitary