TomitaAdjointCoordinates.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The equation between the two bounded square roots determines the whole adjoint graph. Its solution uses their commuting squares summing to one.

theorem OAI.KadisonKastler.linearIsometry_inner_right line 21
theorem OAI.KadisonKastler.inner_selfAdjoint_left line 26
theorem OAI.KadisonKastler.tomitaAdjoint_graph_equation line 33
Source documentation
Membership in the adjoint graph is an equation of bounded operators.
```
theorem tomitaAdjoint_graph_equation (y z : H) :
    (y, z) ∈ (tomitaClosedLinearOperator M J Ω 1).adjoint.graph ↔
      tomitaGraphComplementRoot (M := M) J Ω
…
```
Mentions: OAI.KadisonKastler.tomitaClosedLinearOperator, OAI.KadisonKastler.tomitaGraphComplementRoot
theorem OAI.KadisonKastler.tomitaAdjoint_graph_iff line 58
Source documentation
The adjoint graph is the complementary positive column.
```
theorem tomitaAdjoint_graph_iff (y z : H) :
    (y, z) ∈ (tomitaClosedLinearOperator M J Ω 1).adjoint.graph ↔
      ∃ a : H,
        tomitaLinearPolarUnitary J Ω hsep hcyc (tomitaGraphRoot (M := M) J Ω a) = y ∧
…
```
Mentions: OAI.KadisonKastler.tomitaClosedLinearOperator, OAI.KadisonKastler.tomitaLinearPolarUnitary, OAI.KadisonKastler.tomitaGraphRoot