TomitaPolarConjugation.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The antiunitary obtained from the polar graph coordinates

Transporting adjoint on the closed graph yields an involutive antiunitary on the original Hilbert space. The commutant identity is a subsequent step.

theorem OAI.KadisonKastler.tomitaGraphFlip_involutive line 19
def OAI.KadisonKastler.tomitaGraphAntiunitary line 26
Source documentation
Adjoint restricts to an antiunitary involution on the closed graph.
```
def tomitaGraphAntiunitary (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) :
    rescaledGraphSubspace M J Ω 1 ≃ₗᵢ⋆[ℂ] rescaledGraphSubspace M J Ω 1 where
…
```
Mentions: OAI.KadisonKastler.rescaledGraphSubspace
theorem OAI.KadisonKastler.tomitaGraphAntiunitary_involutive line 36

def OAI.KadisonKastler.tomitaPolarConjugation line 41

Source documentation

The polar conjugation constructed on the original represented Hilbert space.

def tomitaPolarConjugation (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H)
    (hsep : Function.Injective (algebraVectorMap M Ω))
    (hcyc : DenseRange (algebraVectorMap M Ω)) : H ≃ₗᵢ⋆[ℂ] H :=
…

Mentions: OAI.KadisonKastler.algebraVectorMap

theorem OAI.KadisonKastler.tomitaPolarConjugation_involutive line 47