OAI/Analysis/KadisonKastler/ModularStripSpectralBoundary.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.modularSpectralStrip_eq_inner line 21

   Source documentation

   A scalar spectral integral is the corresponding ambient matrix coefficient.

   theorem modularSpectralStrip_eq_inner (X Y Z : H) (z : ℂ)
       (v : ResolventCyclicL2 (graphResolvent M J Ω 1)
         (graphResolvent_positive J Ω 1).isSelfAdjoint Y)
       (hv : v =ᵐ[resolventVectorMeasure (graphResolvent M J Ω 1)
         (graphResolvent_positive J Ω 1).isSelfAdjoint Y]
         fun s => modularStripKernel z s.val)
       (hZ : resolventCyclicIsometry (graphResolvent M J Ω 1)
         (graphResolvent_positive J Ω 1).isSelfAdjoint Y v = Z) :
       modularSpectralStrip (M := M) J Ω X Y z = inner ℂ X Z := by
   …

   Mentions: OAI.KadisonKastler.ResolventCyclicL2, OAI.KadisonKastler.graphResolvent, OAI.KadisonKastler.graphResolvent_positive, OAI.KadisonKastler.resolventVectorMeasure, OAI.KadisonKastler.modularStripKernel, OAI.KadisonKastler.resolventCyclicIsometry, OAI.KadisonKastler.modularSpectralStrip

2. theorem OAI.KadisonKastler.cyclic_phase_one line 44
3. theorem OAI.KadisonKastler.modularSpectralStrip_bottom line 55
4. theorem OAI.KadisonKastler.modularSpectralStrip_top line 75