TomitaClosedOperator.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The closed Tomita operator in linear coordinates

The fixed antiunitary in the second coordinate turns the Tomita operator into a complex-linear, densely defined closed operator. Its graph is the previously constructed closed graph, not an assumed modular object.

def OAI.KadisonKastler.tomitaProductCoordinates line 21
Source documentation
Changing only the finite product norm does not change the graph topology.
```
def tomitaProductCoordinates : TomitaGraphHilbert H ≃L[ℂ] H × H :=
…
```
Mentions: OAI.KadisonKastler.TomitaGraphHilbert

def OAI.KadisonKastler.tomitaProductGraph line 26

Source documentation

The closed graph in the ordinary product used by LinearPMap.

def tomitaProductGraph (M : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H)
    (Ω : H) (c : ℝ) : Submodule ℂ (H × H) :=
…

theorem OAI.KadisonKastler.tomitaProductGraph_closed line 30
theorem OAI.KadisonKastler.tomitaProductGraph_no_vertical line 35
def OAI.KadisonKastler.tomitaClosedLinearOperator line 44
Source documentation
The actual closed operator, expressed using a fixed conjugate copy of H.
```
def tomitaClosedLinearOperator (M : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H)
    (Ω : H) (c : ℝ) : H →ₗ.[ℂ] H :=
…
```
theorem OAI.KadisonKastler.tomitaClosedLinearOperator_graph line 48
theorem OAI.KadisonKastler.tomitaClosedLinearOperator_closed line 54
theorem OAI.KadisonKastler.tomitaClosedLinearOperator_algebraic_graph line 60
theorem OAI.KadisonKastler.tomitaClosedLinearOperator_dense line 66