English
The nonunital continuous functional calculus assigns to each element a ∈ A a rule that sends a suitable function f to an element cfcₙ f a ∈ A, behaving like evaluation whenever its hypotheses hold and giving zero otherwise.
Русский
Неприводимый непрерывный функциональный калькулятор сопоставляет каждому элементу a∈A правило, отправляющее подходящую функцию f в элемент cfcₙ f a ∈ A, ведущее себя как оценка при выполнении условий и равное нулю в противном случае.
LaTeX
$$$cfc_n f a = 0$ if not (appropriate conditions), otherwise equals the evaluation map$$
Lean4
/-- This is the *continuous functional calculus* of an element `a : A` in a non-unital algebra
applied to bare functions. When either `a` does not satisfy the predicate `p` (i.e., `a` is not
`IsStarNormal`, `IsSelfAdjoint`, or `0 ≤ a` when `R` is `ℂ`, `ℝ`, or `ℝ≥0`, respectively), or when
`f : R → R` is not continuous on the quasispectrum of `a` or `f 0 ≠ 0`, then `cfcₙ f a` returns the
junk value `0`.
This is the primary declaration intended for widespread use of the continuous functional calculus
for non-unital algebras, and all the API applies to this declaration. For more information, see the
module documentation for `Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital`. -/
noncomputable def cfcₙ :=
val_proj @wrapped✝.{}
