TomitaPolarCoordinates.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Polar coordinates for the closed Tomita graph

The first-coordinate map has dense range and zero kernel. Extending the isometry between the ranges of its adjoint and the positive graph root identifies the graph Hilbert space with the original Hilbert space.

theorem OAI.KadisonKastler.denseRange_of_adjoint_injective line 21
def OAI.KadisonKastler.tomitaGraphFirst line 31
Source documentation
First coordinate on the graph Hilbert space.
```
def tomitaGraphFirst (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) :
    rescaledGraphSubspace M J Ω 1 →L[ℂ] H :=
…
```
Mentions: OAI.KadisonKastler.rescaledGraphSubspace
theorem OAI.KadisonKastler.tomitaGraphFirst_apply line 36
theorem OAI.KadisonKastler.tomitaGraphFirst_adjoint_apply line 44
theorem OAI.KadisonKastler.tomitaGraphFirst_mul_adjoint line 51
theorem OAI.KadisonKastler.tomitaGraphFirst_injective line 59
def OAI.KadisonKastler.tomitaGraphRoot line 66
Source documentation
The positive square root of the bounded graph resolvent.
```
def tomitaGraphRoot (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) : H →L[ℂ] H :=
…
```
theorem OAI.KadisonKastler.tomitaGraphRoot_selfAdjoint line 69
theorem OAI.KadisonKastler.tomitaGraphRoot_square line 73
theorem OAI.KadisonKastler.tomitaGraphRoot_injective line 78
theorem OAI.KadisonKastler.tomitaGraphRoot_dense line 89
theorem OAI.KadisonKastler.tomitaGraphFirst_adjoint_norm line 99
theorem OAI.KadisonKastler.tomitaGraphFirst_adjoint_dense line 111

def OAI.KadisonKastler.tomitaPolarCoordinates line 119

Source documentation

Polar identification of H with the graph Hilbert space.

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

Mentions: OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.rescaledGraphSubspace

theorem OAI.KadisonKastler.tomitaPolarCoordinates_root line 128