instIsometricContinuousFunctionalCalculus

English

There is an instance of an isometric continuous functional calculus for NNReal on A with p a tthe predicate IsSelfAdjoint, given NonnegSpectrumClass.

Русский

Существует экземпляр изометрического непрерывного функционального калькулятора для NNReal на A, если p(a) означает IsSelfAdjoint и существует соответствующий Nonneg спектр.

LaTeX

$$Nonneg.instIsometricContinuousFunctionalCalculus : IsometricContinuousFunctionalCalculus NNReal A (0 ≤ ·)$$

Lean4

instance instIsometricContinuousFunctionalCalculus : IsometricContinuousFunctionalCalculus ℝ≥0 A (0 ≤ ·) :=
  SpectrumRestricts.isometric_cfc (q := IsSelfAdjoint) ContinuousMap.realToNNReal isometry_subtype_coe le_rfl
    (fun _ ↦ nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts)

Похожие утверждения