OAI/Analysis/KadisonKastler/ConstructedCoreTraceSymmetry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.constructedCore_traceSymmetry line 21
2. theorem OAI.KadisonKastler.constructedCore_corner_tracial line 94

   Source documentation

   The weighted packet is tracial on its supported corner.

   theorem constructedCore_corner_tracial
       (A B : RegularCoreHilbert H →L[ℂ] RegularCoreHilbert H)
       (hA : A ∈ regularCoreAlgebra (modularStrongGroup J Ω hsep hcyc)
         (modularStrongGroup_continuous J Ω hsep hcyc) M)
       (hB : B ∈ regularCoreAlgebra (modularStrongGroup J Ω hsep hcyc)
         (modularStrongGroup_continuous J Ω hsep hcyc) M)
       (hpA : regularFrequencyWindow 0 1 * A = A)
       (hAp : A * regularFrequencyWindow 0 1 = A)
       (hpB : regularFrequencyWindow 0 1 * B = B)
       (hBp : B * regularFrequencyWindow 0 1 = B) :
       inner ℂ (coreTraceFrequencyVector Ω) ((A * B) (coreTraceFrequencyVector Ω)) =
         inner ℂ (coreTraceFrequencyVector Ω) ((B * A) (coreTraceFrequencyVector Ω)) := by
   …

   Mentions: OAI.KadisonKastler.RegularCoreHilbert, OAI.KadisonKastler.regularCoreAlgebra, OAI.KadisonKastler.modularStrongGroup, OAI.KadisonKastler.modularStrongGroup_continuous, OAI.KadisonKastler.regularFrequencyWindow, OAI.KadisonKastler.coreTraceFrequencyVector