KaplanskyRational.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Resolvent expression and strong continuity of the bounded transform

theorem OAI.KadisonKastler.rational_transform_complex line 16
theorem OAI.KadisonKastler.kaplanskyTransform_eq_resolvents line 39
Source documentation
Two resolvents express the bounded real rational transform.
```
theorem kaplanskyTransform_eq_resolvents (a : H →L[ℂ] H) (ha : IsSelfAdjoint a) :
    cfc kaplanskyTransform a = -resolvent a Complex.I - resolvent a (-Complex.I) := by
…
```
Mentions: OAI.KadisonKastler.kaplanskyTransform

theorem OAI.KadisonKastler.tendsto_kaplanskyTransform_of_strong line 63

Source documentation

Bounded-transform strong continuity requires only self-adjointness, not a bound on the original net.

theorem tendsto_kaplanskyTransform_of_strong
    {ι : Type*} {l : Filter ι} {a : ι → H →L[ℂ] H} {T : H →L[ℂ] H}
    (ha : ∀ i, IsSelfAdjoint (a i)) (hT : IsSelfAdjoint T)
    (hlim : ∀ x, Tendsto (fun i => a i x) l (𝓝 (T x))) (x : H) :
    Tendsto (fun i => cfc kaplanskyTransform (a i) x) l
      (𝓝 (cfc kaplanskyTransform T x)) := by
…

Mentions: OAI.KadisonKastler.kaplanskyTransform