OAI/Analysis/KadisonKastler/TomitaPolarResolventSymmetry.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.tomitaPolarCoordinates_first line 14
2. theorem OAI.KadisonKastler.tomitaPolarCoordinates_conjugation line 29
3. theorem OAI.KadisonKastler.tomitaPolarCoordinates_second line 38
4. theorem OAI.KadisonKastler.inner_tomitaGraphRoot line 50
5. theorem OAI.KadisonKastler.tomitaPolarResolvent_inner line 60
6. theorem OAI.KadisonKastler.tomitaPolarConjugation_resolvent line 78

   Source documentation

   The polar conjugation exchanges the two endpoints of the graph spectrum.

   theorem tomitaPolarConjugation_resolvent (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H)
       (hsep : Function.Injective (algebraVectorMap M Ω))
       (hcyc : DenseRange (algebraVectorMap M Ω)) :
       conjugationOperator (tomitaPolarConjugation J Ω hsep hcyc) (graphResolvent M J Ω 1) =
         1 - graphResolvent M J Ω 1 := by
   …

   Mentions: OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.conjugationOperator, OAI.KadisonKastler.tomitaPolarConjugation, OAI.KadisonKastler.graphResolvent