KaplanskyTransform.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

A bounded rational transform of self-adjoint operators

The scalar map 2t/(1+t²) takes the real line into the closed unit interval. Its inverse on that interval is t/(1+sqrt(1-t²)). Resolvent continuity therefore gives bounded strong approximants to any self-adjoint contraction.

def OAI.KadisonKastler.kaplanskyTransform line 23
def OAI.KadisonKastler.kaplanskyInverse line 25
theorem OAI.KadisonKastler.continuous_kaplanskyTransform line 27
theorem OAI.KadisonKastler.continuous_kaplanskyInverse line 31
theorem OAI.KadisonKastler.abs_kaplanskyTransform_le_one line 35
theorem OAI.KadisonKastler.kaplanskyTransform_inverse line 45
theorem OAI.KadisonKastler.norm_kaplanskyTransform_le_one line 60
Source documentation
The rational transform stays in the unit ball.
```
theorem norm_kaplanskyTransform_le_one (a : H →L[ℂ] H) :
    ‖cfc kaplanskyTransform a‖ ≤ 1 := by
…
```
Mentions: OAI.KadisonKastler.kaplanskyTransform
theorem OAI.KadisonKastler.exists_kaplanskyTransform_preimage line 68
Source documentation
Every self-adjoint contraction is the rational transform of a self-adjoint operator. No spectral or density input is assumed.
```
theorem exists_kaplanskyTransform_preimage (T : H →L[ℂ] H)
    (hT : IsSelfAdjoint T) (hn : ‖T‖ ≤ 1) :
    ∃ S : H →L[ℂ] H, S = cfc kaplanskyInverse T ∧
      IsSelfAdjoint S ∧ cfc kaplanskyTransform S = T := by
…
```
Mentions: OAI.KadisonKastler.kaplanskyInverse, OAI.KadisonKastler.kaplanskyTransform