The continuous functional calculus #
This file defines a generic API for the continuous functional calculus which is suitable in a wide range of settings.
A continuous functional calculus for an element a : A
in a topological R
-algebra is a continuous
extension of the polynomial functional calculus (i.e., Polynomial.aeval
) to continuous R
-valued
functions on spectrum R a
. More precisely, it is a continuous star algebra homomorphism
C(spectrum R a, R) →⋆ₐ[R] A
that sends (ContinuousMap.id R).restrict (spectrum R a)
to
a
. In all cases of interest (e.g., when spectrum R a
is compact and R
is ℝ≥0
, ℝ
, or ℂ
),
this is sufficient to uniquely determine the continuous functional calculus which is encoded in the
UniqueContinuousFunctionalCalculus
class.
Although these properties suffice to uniquely determine the continuous functional calculus, we
choose to bundle more information into the class itself. Namely, we include that the star algebra
homomorphism is a closed embedding, and also that the spectrum of the image of
f : C(spectrum R a, R)
under this morphism is the range of f
. In addition, the class specifies
a collection of continuous functional calculi for elements satisfying a given predicate
p : A → Prop
, and we require that this predicate is preserved by the functional calculus.
Although cfcHom : p a → C(spectrum R a, R) →*ₐ[R] A
is a necessity for getting the full power
out of the continuous functional calculus, this declaration will generally not be accessed directly
by the user. One reason for this is that cfcHom
requires a proof of p a
(indeed, if the
spectrum is empty, there cannot exist a star algebra homomorphism like this). Instead, we provide
the completely unbundled cfc : (R → R) → A → A
which operates on bare functions and provides junk
values when either a
does not satisfy the property p
, or else when the function which is the
argument to cfc
is not continuous on the spectrum of a
.
This completely unbundled approach may give up some conveniences, but it allows for tremendous
freedom. In particular, cfc f a
makes sense for any a : A
and f : R → R
. This is quite
useful in a variety of settings, but perhaps the most important is the following.
Besides being a star algebra homomorphism sending the identity to a
, the key property enjoyed
by the continuous functional calculus is the composition property, which guarantees that
cfc (g ∘ f) a = cfc g (cfc f a)
under suitable hypotheses on a
, f
and g
. Note that this
theorem is nearly impossible to state nicely in terms of cfcHom
(see cfcHom_comp
). An
additional advantage of the unbundled approach is that expressions like fun x : R ↦ x⁻¹
are valid
arguments to cfc
, and a bundled continuous counterpart can only make sense when the spectrum of
a
does not contain zero and when we have an ⁻¹
operation on the domain.
A reader familiar with C⋆-algebra theory may be somewhat surprised at the level of abstraction here.
For instance, why not require A
to be an actual C⋆-algebra? Why define separate continuous
functional calculi for R := ℂ
, ℝ
or ℝ≥0
instead of simply using the continuous functional
calculus for normal elements? The reason for both can be explained with a simple example,
A := Matrix n n ℝ
. In Mathlib, matrices are not equipped with a norm (nor even a metric), and so
requiring A
to be a C⋆-algebra is far too stringent. Likewise, A
is not a ℂ
-algebra, and so
it is impossible to consider the ℂ
-spectrum of a : Matrix n n ℝ
.
There is another, more practical reason to define separate continuous functional calculi for
different scalar rings. It gives us the ability to use functions defined on these types, and the
algebra of functions on them. For example, for R := ℝ
it is quite natural to consider the
functions (·⁺ : ℝ → ℝ)
and (·⁻ : ℝ → ℝ)
because the functions ℝ → ℝ
form a lattice ordered
group. If a : A
is selfadjoint, and we define a⁺ := cfc (·⁺ : ℝ → ℝ) a
, and likewise for a⁻
,
then the properties a⁺ * a⁻ = 0 = a⁻ * a⁺
and a = a⁺ - a⁻
are trivial consequences of the
corresponding facts for functions. In contrast, if we had to do this using functions on ℂ
, the
proofs of these facts would be much more cumbersome.
Example #
The canonical example of the continuous functional calculus is when A := Matrix n n ℂ
, R := ℂ
and p := IsStarNormal
. In this case, spectrum ℂ a
consists of the eigenvalues of the normal
matrix a : Matrix n n ℂ
, and, because this set is discrete, any function is continuous on the
spectrum. The continuous functional calculus allows us to make sense of expressions like log a
(:= cfc log a
), and when 0 ∉ spectrum ℂ a
, we get the nice property exp (log a) = a
, which
arises from the composition property cfc exp (cfc log a) = cfc (exp ∘ log) a = cfc id a = a
, since
exp ∘ log = id
on the spectrum of a
. Of course, there are other ways to make sense of exp
and log
for matrices (power series), and these agree with the continuous functional calculus.
In fact, given f : C(spectrum ℂ a, ℂ)
, cfc f a
amounts to diagonalizing a
(possible since a
is normal), and applying f
to the resulting diagonal entries. That is, if a = u * d * star u
with u
a unitary matrix and d
diagonal, then cfc f a = u * d.map f * star u
.
In addition, if a : Matrix n n ℂ
is positive semidefinite, then the ℂ
-spectrum of a
is
contained in (the range of the coercion of) ℝ≥0
. In this case, we get a continuous functional
calculus with R := ℝ≥0
. From this we can define √a := cfc a NNReal.sqrt
, which is also
positive semidefinite (because cfc
preserves the predicate), and this is truly a square root since
√a * √a = cfc NNReal.sqrt a * cfc NNReal.sqrt a =
cfc (NNReal.sqrt ^ 2) a = cfc id a = a
The composition property allows us to show that, in fact, this is the unique positive semidefinite
square root of a
because, if b
is any positive semidefinite square root, then
b = cfc id b = cfc (NNReal.sqrt ∘ (· ^ 2)) b =
cfc NNReal.sqrt (cfc b (· ^ 2)) = cfc NNReal.sqrt a = √a
Main declarations #
ContinuousFunctionalCalculus R (p : A → Prop)
: a class stating that everya : A
satisfyingp a
has a star algebra homomorphism from the continuousR
-valued functions on theR
-spectrum ofa
into the algebraA
. This map is a closed embedding, and satisfies the spectral mapping theorem.cfcHom : p a → C(spectrum R a, R) →⋆ₐ[R] A
: the underlying star algebra homomorphism for an element satisfying propertyp
.cfc : (R → R) → A → A
: an unbundled version ofcfcHom
which takes the junk value0
whencfcHom
is not defined.cfcUnits
: builds a unit fromcfc f a
whenf
is nonzero and continuous on the spectrum ofa
.
Main theorems #
cfc_comp : cfc (x ↦ g (f x)) a = cfc g (cfc f a)
cfc_polynomial
: the continuous functional calculus extends the polynomial functional calculus.
Implementation details #
Instead of defining a class depending on a term a : A
, we register it for an outParam
predicate
p : A → Prop
, and then any element of A
satisfying this predicate has the associated star
algebra homomorphism with the specified properties. In so doing we avoid a common pitfall:
dependence of the class on a term. This avoids annoying situations where a b : A
are
propositionally equal, but not definitionally so, and hence Lean would not be able to automatically
identify the continuous functional calculi associated to these elements. In order to guarantee
the necessary properties, we require that the continuous functional calculus preserves this
predicate. That is, p a → p (cfc f a)
for any function f
continuous on the spectrum of a
.
As stated above, the unbundled approach to cfc
has its advantages. For instance, given an
expression cfc f a
, the user is free to rewrite either a
or f
as desired with no possibility
of the expression ceasing to be defined. However, this unbundling also has some potential downsides.
In particular, by unbundling, proof requirements are deferred until the user calls the lemmas, most
of which have hypotheses both of p a
and of ContinuousOn f (spectrum R a)
.
In order to minimize burden to the user, we provide autoParams
in terms of two tactics. Goals
related to continuity are dispatched by (a small wrapper around) fun_prop
. As for goals involving
the predicate p
, it should be noted that these will only ever be of the form IsStarNormal a
,
IsSelfAdjoint a
or 0 ≤ a
. For the moment we provide a rudimentary tactic to deal with these
goals, but it can be modified to become more sophisticated as the need arises.
A star R
-algebra A
has a continuous functional calculus for elements satisfying the
property p : A → Prop
if
- for every such element
a : A
there is a star algebra homomorphismcfcHom : C(spectrum R a, R) →⋆ₐ[R] A
sending the (restriction of) the identity map toa
. cfcHom
is a closed embedding for which the spectrum of the image of functionf
is its range.cfcHom
preserves the propertyp
.p 0
is true, which ensures among other things thatp ≠ fun _ ↦ False
.
The property p
is marked as an outParam
so that the user need not specify it. In practice,
- for
R := ℂ
, we choosep := IsStarNormal
, - for
R := ℝ
, we choosep := IsSelfAdjoint
, - for
R := ℝ≥0
, we choosep := (0 ≤ ·)
.
Instead of directly providing the data we opt instead for a Prop
class. In all relevant cases,
the continuous functional calculus is uniquely determined, and utilizing this approach
prevents diamonds or problems arising from multiple instances.
- predicate_zero : p 0
Instances
A class guaranteeing that the continuous functional calculus is uniquely determined by the
properties that it is a continuous star algebra homomorphism mapping the (restriction of) the
identity to a
. This is the necessary tool used to establish cfcHom_comp
and the more common
variant cfc_comp
.
This class has instances, which can be found in
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
, in each of the common cases
ℂ
, ℝ
and ℝ≥0
as a consequence of the Stone-Weierstrass theorem.
This class is separate from ContinuousFunctionalCalculus
primarily because we will later use
SpectrumRestricts
to derive an instance of ContinuousFunctionalCalculus
on a scalar subring
from one on a larger ring (i.e., to go from a continuous functional calculus over ℂ
for normal
elements to one over ℝ
for selfadjoint elements), and proving this additional property is
preserved would be burdensome or impossible.
- eq_of_continuous_of_map_id : ∀ (s : Set R) [inst : CompactSpace ↑s] (φ ψ : C(↑s, R) →⋆ₐ[R] A), Continuous ⇑φ → Continuous ⇑ψ → φ (ContinuousMap.restrict s (ContinuousMap.id R)) = ψ (ContinuousMap.restrict s (ContinuousMap.id R)) → φ = ψ
- compactSpace_spectrum : ∀ (a : A), CompactSpace ↑(spectrum R a)
Instances
The star algebra homomorphism underlying a instance of the continuous functional calculus; a version for continuous functions on the spectrum.
In this case, the user must supply the fact that a
satisfies the predicate p
, for otherwise it
may be the case that no star algebra homomorphism exists. For instance if R := ℝ
and a
is an
element whose spectrum (in ℂ
) is disjoint from ℝ
, then spectrum ℝ a = ∅
and so there can be
no star algebra homomorphism between these spaces.
While ContinuousFunctionalCalculus
is stated in terms of these homomorphisms, in practice the
user should instead prefer cfc
over cfcHom
.
Instances For
The spectral mapping theorem for the continuous functional calculus.
cfcHom
bundled as a continuous linear map.
Instances For
This is the continuous functional calculus of an element a : A
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 spectrum of a
, then cfc f a
returns the junk value 0
.
This is the primary declaration intended for widespread use of the continuous functional calculus,
and all the API applies to this declaration. For more information, see the module documentation
for Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
.
Instances For
The spectral mapping theorem for the continuous functional calculus.
Equations
- ⋯ = ⋯
In an R
-algebra with a continuous functional calculus, every element satisfying the predicate
has nonempty R
-spectrum.
Alias of the reverse direction of isUnit_cfc_iff
.
Bundle cfc f a
into a unit given a proof that f
is nonzero on the spectrum of a
.