# Documentation

Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus

# Continuous functional calculus #

In this file we construct the continuousFunctionalCalculus for a normal element a of a (unital) C⋆-algebra over ℂ. This is a star algebra equivalence C(spectrum ℂ a, ℂ) ≃⋆ₐ[ℂ] elementalStarAlgebra ℂ a which sends the (restriction of) the identity map ContinuousMap.id ℂ to the (unique) preimage of a under the coercion of elementalStarAlgebra ℂ a to A.

Being a star algebra equivalence between C⋆-algebras, this map is continuous (even an isometry), and by the Stone-Weierstrass theorem it is the unique star algebra equivalence which extends the polynomial functional calculus (i.e., Polynomial.aeval).

For any continuous function f : spectrum ℂ a → ℂ, this makes it possible to define an element f a (not valid notation) in the original algebra, which heuristically has the same eigenspaces as a and acts on eigenvector of a for an eigenvalue λ as multiplication by f λ. This description is perfectly accurate in finite dimension, but only heuristic in infinite dimension as there might be no genuine eigenvector. In particular, when f is a polynomial ∑ cᵢ Xⁱ, then f a is ∑ cᵢ aⁱ. Also, id a = a.

This file also includes a proof of the spectral permanence theorem for (unital) C⋆-algebras (see StarSubalgebra.spectrum_eq)

## Main definitions #

• continuousFunctionalCalculus : C(spectrum ℂ a, ℂ) ≃⋆ₐ[ℂ] elementalStarAlgebra ℂ a: this is the composition of the inverse of the gelfandStarTransform with the natural isomorphism induced by the homeomorphism elementalStarAlgebra.characterSpaceHomeo.
• elementalStarAlgebra.characterSpaceHomeo : characterSpace ℂ (elementalStarAlgebra ℂ a) ≃ₜ spectrum ℂ a: this homeomorphism is defined by evaluating a character φ at a, and noting that φ a ∈ spectrum ℂ a since φ is an algebra homomorphism. Moreover, this map is continuous and bijective and since the spaces involved are compact Hausdorff, it is a homeomorphism.

## Main statements #

• StarSubalgebra.coe_isUnit: for x : S in a C⋆-Subalgebra S of A, then ↑x : A is a Unit if and only if x is a unit.
• StarSubalgebra.spectrum_eq: spectral_permanence for x : S, where S is a C⋆-Subalgebra of A, spectrum ℂ x = spectrum ℂ (x : A).

The result we have established here is the strongest possible, but it is likely not the version which will be most useful in practice. Future work will include developing an appropriate API for the continuous functional calculus (including one for real-valued functions with real argument that applies to self-adjoint elements of the algebra).