ModularPositiveOperator.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The positive self-adjoint square root of the modular operator

Removing the linear polar unitary from the closed Tomita operator gives an unbounded operator with graph (r a, q a), where the two commuting positive roots satisfy r² + q² = 1. These coordinates prove self-adjointness directly.

def OAI.KadisonKastler.modularPositiveOperator line 24
Source documentation
The positive part of the closed Tomita operator.
```
def modularPositiveOperator : H →ₗ.[ℂ] H :=
…
```
theorem OAI.KadisonKastler.modularPositiveOperator_graph_transport line 28
theorem OAI.KadisonKastler.modularPositiveOperator_graph_iff line 45
theorem OAI.KadisonKastler.modularPositiveOperator_dense line 54
theorem OAI.KadisonKastler.modularPositiveOperator_adjoint_equation line 58
theorem OAI.KadisonKastler.modularPositiveOperator_adjoint_graph_iff line 83
Source documentation
The graph parametrization is unchanged by taking the adjoint.
```
theorem modularPositiveOperator_adjoint_graph_iff (y z : H) :
    (y, z) ∈ (modularPositiveOperator J Ω hsep hcyc).adjoint.graph ↔
      ∃ a : H, tomitaGraphRoot (M := M) J Ω a = y ∧
…
```
Mentions: OAI.KadisonKastler.modularPositiveOperator, OAI.KadisonKastler.tomitaGraphRoot
theorem OAI.KadisonKastler.modularPositiveOperator_selfAdjoint line 110
theorem OAI.KadisonKastler.modularPositiveOperator_closed line 117
theorem OAI.KadisonKastler.modularPositiveOperator_inner_nonneg line 122
Source documentation
Positivity on the whole domain, not only the algebraic core.
```
theorem modularPositiveOperator_inner_nonneg (x : (modularPositiveOperator J Ω hsep hcyc).domain) :
    0 ≤ inner ℂ (modularPositiveOperator J Ω hsep hcyc x) (x : H) := by
…
```
Mentions: OAI.KadisonKastler.modularPositiveOperator