KaplanskyResolvent.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Bounded resolvents for the Kaplansky argument

Off-real resolvents are uniformly bounded on all self-adjoint operators. Their strong continuity therefore does not require a norm bound on the approximating self-adjoint net. This is the bounded-transform step used in Kaplansky's proof (Pacific J. Math. 1 (1951), Lemma 4, pp.229--230).

theorem OAI.KadisonKastler.spectral_im_eq_zero line 26
theorem OAI.KadisonKastler.nonreal_mem_resolventSet line 32
Source documentation
Every nonreal point belongs to the resolvent set of a self-adjoint operator.
```
theorem nonreal_mem_resolventSet {a : H →L[ℂ] H} (ha : IsSelfAdjoint a)
    {z : ℂ} (hz : z.im ≠ 0) : z ∈ resolventSet ℂ a := by
…
```
theorem OAI.KadisonKastler.resolvent_eq_cfc_of_selfAdjoint line 39

theorem OAI.KadisonKastler.norm_resolvent_le_inv_abs_im line 55

Source documentation

The resolvent norm bound is independent of the self-adjoint operator.

theorem norm_resolvent_le_inv_abs_im {a : H →L[ℂ] H} (ha : IsSelfAdjoint a)
    {z : ℂ} (hz : z.im ≠ 0) : ‖resolvent a z‖ ≤ |z.im|⁻¹ := by
…

theorem OAI.KadisonKastler.tendsto_resolvent_of_selfAdjoint_strong line 67

Source documentation

Strong continuity of off-real resolvents, including unbounded nets.

theorem tendsto_resolvent_of_selfAdjoint_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)))
    {z : ℂ} (hz : z.im ≠ 0) (x : H) :
    Tendsto (fun i => resolvent (a i) z x) l (𝓝 (resolvent T z x)) := by
…