cfc_map — Mathlib

English

The continuous functional calculus produces a star-normal element: cfc f a is IsStarNormal for any f and a satisfying the setup.

Русский

Непрерывное функциональное вычисление даёт звездо-нормальный элемент: cfc f a нормален относительно оператора *.

LaTeX

$$IsStarNormal (cfc f a)$$

Lean4

@[simp]
instance cfc_map (f : R → R) (a : A) : IsStarNormal (cfc f a) where
  star_comm_self := by
    rw [Commute, SemiconjBy]
    by_cases h : ContinuousOn f (spectrum R a)
    · rw [← cfc_star, ← cfc_mul .., ← cfc_mul ..]
      congr! 2
      exact mul_comm _ _
    ·
      simp [cfc_apply_of_not_continuousOn a h]
        -- The following two lemmas are just `cfc_predicate`, but specific enough for the `@[simp]` tag.

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