OAI/Analysis/KadisonKastler/RectangularFunctionalCalculus.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Continuous functional calculus through a rectangular intertwiner

  1. theorem OAI.KadisonKastler.cfc_rectangular_intertwines line 20

    Source documentation

    Functional calculus preserves a bounded intertwiner of selfadjoint operators, even when the two operators act on different Hilbert spaces.

    theorem cfc_rectangular_intertwines
    (a : K →L[ℂ] K) (b : H →L[ℂ] H) (T : H →L[ℂ] K)
    (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b)
    (hT : a.comp T = T.comp b) (f : ℂ → ℂ)
    (hfa : ContinuousOn f (spectrum ℂ a)) (hfb : ContinuousOn f (spectrum ℂ b)) :
    (cfc f a).comp T = T.comp (cfc f b) := by
…