instNonUnitalIsometricContinuousFunctionalCalculus

English

There is a nonunital isometric continuous functional calculus for NNReal values on A, i.e., NonUnitalIsometricContinuousCalculus 𝕜 A p with q = IsSelfAdjoint and spectrum compatibility.

Русский

Существует неединичный изометрический непрерывный функциональный калькулятор для NNReal на A.

LaTeX

$$Nonneg.instNonUnitalIsometricContinuousCalculus : NonUnitalIsometricContinuousFunctionalCalculus NNReal A (0 ≤ ·)$$

Lean4

instance instNonUnitalIsometricContinuousFunctionalCalculus :
    NonUnitalIsometricContinuousFunctionalCalculus ℝ≥0 A (0 ≤ ·) :=
  QuasispectrumRestricts.isometric_cfc (q := IsSelfAdjoint) ContinuousMap.realToNNReal isometry_subtype_coe le_rfl
    (fun _ ↦ nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts)

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