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]