PolarPartialIsometry.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Concrete right supports in a finite tracial von Neumann algebra

The partial isometry is constructed by extending the isometry sqrt(x* x) ξ ↦ x ξ from its dense range and setting it to zero on the orthogonal complement. Bicommutant closure keeps that operator in the algebra.

def OAI.KadisonSimilarity.rangeIntoClosure line 21
Source documentation
The range map, with its codomain restricted to the closed range.
```
def rangeIntoClosure (B : H →L[ℂ] H) : H →ₗ[ℂ] operatorRangeClosure B :=
…
```
Mentions: OAI.KadisonSimilarity.operatorRangeClosure
theorem OAI.KadisonSimilarity.rangeIntoClosure_dense line 26
def OAI.KadisonSimilarity.polarModulus line 32
Source documentation
Positive square root used only for this polar factor.
```
def polarModulus (x : H →L[ℂ] H) : H →L[ℂ] H := CFC.sqrt (star x * x)
```
theorem OAI.KadisonSimilarity.polarModulus_selfAdjoint line 34
theorem OAI.KadisonSimilarity.polarModulus_square line 37
theorem OAI.KadisonSimilarity.polarModulus_norm_apply line 40
def OAI.KadisonSimilarity.polarRangeIsometry line 51
Source documentation
Isometry from the initial closed range to the ambient Hilbert space.
```
def polarRangeIsometry (x : H →L[ℂ] H) : operatorRangeClosure (polarModulus x) →ₗᵢ[ℂ] H :=
…
```
Mentions: OAI.KadisonSimilarity.operatorRangeClosure, OAI.KadisonSimilarity.polarModulus
theorem OAI.KadisonSimilarity.polarRangeIsometry_apply line 55
def OAI.KadisonSimilarity.polarPartialIsometry line 60
Source documentation
The actual partial isometry, extended by zero.
```
def polarPartialIsometry (x : H →L[ℂ] H) : H →L[ℂ] H :=
…
```
theorem OAI.KadisonSimilarity.polarPartialIsometry_mul_modulus line 64
theorem OAI.KadisonSimilarity.polarPartialIsometry_initial line 76
theorem OAI.KadisonSimilarity.polarPartialIsometry_mul_initial line 91
theorem OAI.KadisonSimilarity.polarPartialIsometry_final line 103
theorem OAI.KadisonSimilarity.leftSupport_polarPartialIsometry line 117
Source documentation
A left support of x is also a left support of its polar partial isometry.
```
theorem leftSupport_polarPartialIsometry (x q : H →L[ℂ] H) (hqx : q * x = x) :
    q * polarPartialIsometry x = polarPartialIsometry x := by
…
```
Mentions: OAI.KadisonSimilarity.polarPartialIsometry
theorem OAI.KadisonSimilarity.polarPartialIsometry_commutes line 132
Source documentation
Commutation on the two dense range maps extends to the polar isometry.
```
theorem polarPartialIsometry_commutes (x T : H →L[ℂ] H)
    (hx : Commute x T) (hS : Commute (polarModulus x) T)
    (hSstar : Commute (polarModulus x) (star T)) :
    Commute (polarPartialIsometry x) T := by
…
```
Mentions: OAI.KadisonSimilarity.polarModulus, OAI.KadisonSimilarity.polarPartialIsometry
theorem OAI.KadisonSimilarity.polarModulus_mem line 159
theorem OAI.KadisonSimilarity.polarPartialIsometry_mem line 170