cfc_apply_mkD — Mathlib

English

There is a version of cfc f a expressed using mkD with the restriction of f to the spectrum. If f is continuous on the spectrum, use mkD; otherwise use mkD of the zero function, yielding the same cfc value.

Русский

Существует версия cfc f a через mkD с ограничением функции f на спектр; если f непрерывна на спектре, используем mkD; иначе — mkD нулевой функции.

LaTeX

$$$ cfc f a = cfcHom ha (mkD ((spectrum R a).restrict f) 0) $$$

Lean4

/-- A version of `cfc_apply` in terms of `ContinuousMap.mkD` -/
theorem cfc_apply_mkD : cfc f a = cfcHom (a := a) ha (mkD ((spectrum R a).restrict f) 0) :=
  by
  by_cases hf : ContinuousOn f (spectrum R a)
  · rw [cfc_apply f a, mkD_of_continuousOn hf]
  · rw [cfc_apply_of_not_continuousOn a hf, mkD_of_not_continuousOn hf, map_zero]

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