Continuity of the continuous functional calculus in each variable #
The continuous functional calculus is a map which takes a pair a : A
(A
is a C⋆-algebra) and
a function f : C(spectrum R a, R)
where a
satisfies some predicate p
, depending on R
and
returns another element of the algebra A
. This is the map cfcHom
. The class
ContinuousFunctionalCalculus
declares that cfcHom
is a continuous map from C(spectrum R a, R)
to A
. However, users generally interact with the continuous functional calculus through cfc
,
which operates on bare functions f : R → R
instead and takes a junk value when f
is not
continuous on the spectrum of a
. In this file we provide some lemma concerning the continuity
of cfc
, subject to natural hypotheses.
However, the continuous functional calculus is also continuous in the variable a
, but there
are some conditions that must be satisfied. In particular, given a function f : R → R
the map
a ↦ cfc f a
is continuous so long as a
varies over a collection of elements satisfying the
predicate p
and their spectra are collectively contained in a compact set on which f
is
continuous. Moreover, it is required that the continuous functional calculus be the isometric
variant.
Under the assumption of IsometricContinuousFunctionalCalculus
, we show that the continuous
functional calculus is Lipschitz with constant 1 in the variable f : R →ᵤ[{spectrum R a}] R
on the set of functions which are continuous on the spectrum of a
. Combining this with the
continuity of the continuous functional calculus in the variable a
, we obtain a joint continuity
result for cfc
in both variables.
Finally, all of this is developed for both the unital and non-unital functional calculi.
The continuity results in the function variable are valid for all scalar rings, but the continuity
results in the variable a
come in two flavors: those for RCLike 𝕜
and those for ℝ≥0
.
Main results #
tendsto_cfc_fun
: IfF : X → R → R
tends tof : R → R
uniformly on the spectrum ofa
, and all these functions are continuous on the spectrum, thenfun x ↦ cfc (F x) a
tends tocfc f a
.Filter.Tendsto.cfc
: Iff : 𝕜 → 𝕜
is continuous on a compact sets
anda : X → A
tends toa₀ : A
along a filterl
(such that eventuallya x
satisfies the predicatep
associated to𝕜
and has spectrum contained ins
, as doesa₀
), thenfun x ↦ cfc f (a x)
tends tocfc f a₀
.lipschitzOnWith_cfc_fun
: The functionf ↦ cfc f a
is Lipschitz with constant with constant 1 with respect to supremum metric (onR →ᵤ[{spectrum R a}] R
) on those functions which are continuous on the spectrum.continuousOn_cfc
: Forf : 𝕜 → 𝕜
continuous on a compact sets
,cfc f
is continuous on the set ofa : A
satisfying the predicatep
(associated to𝕜
) and whose𝕜
-spectrum is contained ins
.continuousOn_cfc_setProd
: Lets : Set 𝕜
be a compact set and consider pairs(f, a) : (𝕜 → 𝕜) × A
wheref
is continuous ons
andspectrum 𝕜 a ⊆ s
anda
satisfies the predicatep a
for the continuous functional calculus. Thencfc
is jointly continuous in both variables (i.e., continuous in its uncurried form) on this set of pairs when the function space is equipped with the topology of uniform convergence ons
.- Versions of all of the above for non-unital algebras, and versions over
ℝ≥0
as well.
If F : X → R → R
tends to f : R → R
uniformly on the spectrum of a
, and all
these functions are continuous on the spectrum, then fun x ↦ cfc (F x) a
tends
to cfc f a
.
If f : X → R → R
tends to f x₀
uniformly (along 𝓝 x₀
) on the spectrum of a
,
and each f x
is continuous on the spectrum of a
, then fun x ↦ cfc (f x) a
is
continuous at x₀
.
If f : X → R → R
tends to f x₀
uniformly (along 𝓝[s] x₀
) on the spectrum of a
,
and eventually each f x
is continuous on the spectrum of a
, then fun x ↦ cfc (f x) a
is
continuous at x₀
within s
.
If f : X → R → R
is continuous on s : Set X
in the topology on
X → R →ᵤ[{spectrum R a}] → R
, and each f
is continuous on the spectrum, then x ↦ cfc (f x) a
is continuous on s
also.
If f : X → R → R
is continuous in the topology on X → R →ᵤ[{spectrum R a}] → R
,
and each f
is continuous on the spectrum, then x ↦ cfc (f x) a
is continuous.
The function f ↦ cfc f a
is Lipschitz with constant 1 with respect to
supremum metric (on R →ᵤ[{spectrum R a}] R
) on those functions which are continuous on
the spectrum.
The function f ↦ cfc f a
is Lipschitz with constant 1 with respect to
supremum metric (on R →ᵤ[{s}] R
) on those functions which are continuous on a set s
containing
the spectrum.
cfcHomSuperset
is continuous in the variable a : A
when s : Set 𝕜
is compact and a
varies over elements whose spectrum is contained in s
, all of which satisfy the predicate p
.
For f : 𝕜 → 𝕜
continuous on a compact set s
, cfc f
is continuous on the set of a : A
satisfying the predicate p
(associated to 𝕜
) and whose 𝕜
-spectrum is contained in s
.
Let s : Set 𝕜
be a compact set and consider pairs (f, a) : (𝕜 → 𝕜) × A
where f
is
continuous on s
and spectrum 𝕜 a ⊆ s
and a
satisfies the predicate p a
for the continuous
functional calculus.
Then cfc
is jointly continuous in both variables (i.e., continuous in its uncurried form) on this
set of pairs when the function space is equipped with the topology of uniform convergence on s
.
If f : 𝕜 → 𝕜
is continuous on a compact set s
and a : X → A
tends to a₀ : A
along a
filter l
(such that eventually a x
satisfies the predicate p
associated to 𝕜
and has
spectrum contained in s
, as does a₀
), then fun x ↦ cfc f (a x)
tends to cfc f a₀
.
If f : 𝕜 → 𝕜
is continuous on a compact set s
and a : X → A
is continuous at x₀
, and
eventually a x
satisfies the predicate p
associated to 𝕜
and has spectrum contained in s
),
then fun x ↦ cfc f (a x)
is continuous at x₀
.
If f : 𝕜 → 𝕜
is continuous on a compact set s
and a : X → A
is continuous at x₀
within
a set t : Set X
, and eventually a x
satisfies the predicate p
associated to 𝕜
and has
spectrum contained in s
), then fun x ↦ cfc f (a x)
is continuous at x₀
within t
.
If f : 𝕜 → 𝕜
is continuous on a compact set s
and a : X → A
is continuous on t : Set X
,
and a x
satisfies the predicate p
associated to 𝕜
and has spectrum contained in s
for all
x ∈ t
, then fun x ↦ cfc f (a x)
is continuous on t
.
cfc
is continuous in the variable a : A
when s : Set 𝕜
is compact and a
varies over
elements whose spectrum is contained in s
, all of which satisfy the predicate p
, and the
function f
is continuous on the spectrum of a
.
A version of continuousOn_cfc
over ℝ≥0
instead of RCLike 𝕜
.
Let s : Set ℝ≥0
be a compact set and consider pairs (f, a) : (ℝ≥0 → ℝ≥0) × A
where f
is
continuous on s
and spectrum ℝ≥0 a ⊆ s
and 0 ≤ a
.
Then cfc
is jointly continuous in both variables (i.e., continuous in its uncurried form) on this
set of pairs when the function space is equipped with the topology of uniform convergence on s
.
If f : ℝ≥0 → ℝ≥0
is continuous on a compact set s
and a : X → A
tends to a₀ : A
along a
filter l
(such that eventually 0 ≤ a x
and has spectrum contained in s
, as does a₀
), then
fun x ↦ cfc f (a x)
tends to cfc f a₀
.
If f : ℝ≥0 → ℝ≥0
is continuous on a compact set s
and a : X → A
is continuous at x₀
, and
eventually 0 ≤ a x
and has spectrum contained in s
), then fun x ↦ cfc f (a x)
is continuous
at x₀
.
If f : ℝ≥0 → ℝ≥0
is continuous on a compact set s
and a : X → A
is continuous at x₀
within a set t : Set X
, and eventually 0 ≤ a x
and has spectrum contained in s
), then
fun x ↦ cfc f (a x)
is continuous at x₀
within t
.
If f : ℝ≥0 → ℝ≥0
is continuous on a compact set s
and a : X → A
is continuous on
t : Set X
, and 0 ≤ a x
and has spectrum contained in s
for all x ∈ t
, then
fun x ↦ cfc f (a x)
is continuous on t
.
cfc
is continuous in the variable a : A
when s : Set ℝ≥0
is compact and a
varies over
nonnegative elements whose spectrum is contained in s
, and the function f
is
continuous on s
.
If F : X → R → R
tends to f : R → R
uniformly on the spectrum of a
, and all
these functions are continuous on the spectrum and map zero to itself, then
fun x ↦ cfcₙ (F x) a
tends to cfcₙ f a
.
If f : X → R → R
tends to f x₀
uniformly (along 𝓝 x₀
) on the spectrum of a
,
and each f x
is continuous on the spectrum of a
and maps zero to itself, then
fun x ↦ cfcₙ (f x) a
is continuous at x₀
.
If f : X → R → R
tends to f x₀
uniformly (along 𝓝[s] x₀
) on the spectrum of a
,
and eventually each f x
is continuous on the spectrum of a
and maps zero to itself, then
fun x ↦ cfcₙ (f x) a
is continuous at x₀
within s
.
If f : X → R → R
is continuous on s : Set X
in the topology on
X → R →ᵤ[{spectrum R a}] → R
, and for each x ∈ s
, f x
is continuous on the spectrum and
maps zero to itself, then x ↦ cfcₙ (f x) a
is continuous on s
also.
If f : X → R → R
is continuous in the topology on X → R →ᵤ[{spectrum R a}] → R
,
and each f
is continuous on the spectrum and maps zero to itself, then
x ↦ cfcₙ (f x) a
is continuous.
The function f ↦ cfcₙ f a
is Lipschitz with constant 1 with respect to
supremum metric (on R →ᵤ[{quasispectrum R a}] R
) on those functions which are continuous on
the quasispectrum and map zero to itself.
The function f ↦ cfcₙ f a
is Lipschitz with constant 1 with respect to
supremum metric (on R →ᵤ[{s}] R
) on those functions which are continuous on a set s
containing
the quasispectrum and map zero to itself.
cfcₙHomSuperset
is continuous in the variable a : A
when s : Set 𝕜
is compact and a
varies over elements whose spectrum is contained in s
, all of which satisfy the predicate p
.
For f : 𝕜 → 𝕜
continuous on a set s
for which f 0 = 0
, cfcₙ f
is continuous on the
set of a : A
satisfying the predicate p
(associated to 𝕜
) and whose 𝕜
-quasispectrum is
contained in s
.
Let s : Set 𝕜
be a compact set and consider pairs (f, a) : (𝕜 → 𝕜) × A
where f
is
continuous on s
, maps zero itself, and quasispectrum 𝕜 a ⊆ s
and a
satisfies the predicate
p a
for the continuous functional calculus.
Then cfcₙ
is jointly continuous in both variables (i.e., continuous in its uncurried form) on this
set of pairs when the function space is equipped with the topology of uniform convergence on s
.
If f : 𝕜 → 𝕜
is continuous on a compact set s
and f 0 = 0
and a : X → A
tends to
a₀ : A
along a filter l
(such that eventually a x
satisfies the predicate p
associated to
𝕜
and has quasispectrum contained in s
, as does a₀
), then fun x ↦ cfcₙ f (a x)
tends to
cfcₙ f a₀
.
If f : 𝕜 → 𝕜
is continuous on a compact set s
and f 0 = 0
and a : X → A
is continuous
at x₀
, and eventually a x
satisfies the predicate p
associated to 𝕜
and has quasispectrum
contained in s
), then fun x ↦ cfcₙ f (a x)
is continuous at x₀
.
If f : 𝕜 → 𝕜
is continuous on a compact set s
and f 0 = 0
and a : X → A
is continuous
at x₀
within a set t : Set X
, and eventually a x
satisfies the predicate p
associated to 𝕜
and has quasispectrum contained in s
), then fun x ↦ cfcₙ f (a x)
is continuous at x₀
within t
.
If f : 𝕜 → 𝕜
is continuous on a compact set s
and f 0 = 0
and a : X → A
is continuous
on t : Set X
, and a x
satisfies the predicate p
associated to 𝕜
and has quasispectrum
contained in s
for all x ∈ t
, then fun x ↦ cfcₙ f (a x)
is continuous on t
.
cfcₙ
is continuous in the variable a : A
when s : Set 𝕜
is compact and a
varies over
elements whose quasispectrum is contained in s
, all of which satisfy the predicate p
, and the
function f
is continuous s
and f 0 = 0
.
cfcₙ
is continuous in the variable a : A
when s : Set 𝕜
is compact and a
varies over
elements whose spectrum is contained in s
, all of which satisfy the predicate p
, and the
function f
is continuous on the spectrum of a
and maps zero to itself.
A version of continuousOn_cfcₙ
over ℝ≥0
instead of RCLike 𝕜
.
Let s : Set ℝ≥0
be a compact set and consider pairs (f, a) : (ℝ≥0 → ℝ≥0) × A
where f
is
continuous on s
, maps zero to itself, spectrum ℝ≥0 a ⊆ s
and 0 ≤ a
.
Then cfcₙ
is jointly continuous in both variables (i.e., continuous in its uncurried form) on this
set of pairs when the function space is equipped with the topology of uniform convergence on s
.
If f : ℝ≥0 → ℝ≥0
is continuous on a compact set s
and f 0 = 0
and a : X → A
tends to
a₀ : A
along a filter l
(such that eventually a x
satisfies the predicate p
associated to
ℝ≥0
and has quasispectrum contained in s
, as does a₀
), then fun x ↦ cfcₙ f (a x)
tends to
cfcₙ f a₀
.
If f : ℝ≥0 → ℝ≥0
is continuous on a compact set s
and f 0 = 0
and a : X → A
is
continuous at x₀
, and eventually a x
satisfies the predicate p
associated to ℝ≥0
and has
quasispectrum contained in s
), then fun x ↦ cfcₙ f (a x)
is continuous at x₀
.
If f : ℝ≥0 → ℝ≥0
is continuous on a compact set s
and f 0 = 0
and a : X → A
is
continuous at x₀
within a set t : Set X
, and eventually a x
satisfies the predicate p
associated to ℝ≥0
and has quasispectrum contained in s
), then fun x ↦ cfcₙ f (a x)
is
continuous at x₀
within t
.
If f : ℝ≥0 → ℝ≥0
is continuous on a compact set s
and f 0 = 0
and a : X → A
is
continuous on t : Set X
, and a x
satisfies the predicate p
associated to ℝ≥0
and has
quasispectrum contained in s
for all x ∈ t
, then fun x ↦ cfcₙ f (a x)
is continuous
on t
.
cfcₙ
is continuous in the variable a : A
when s : Set ℝ≥0
is compact and a
varies over
elements whose quasispectrum is contained in s
, all of which satisfy the predicate p
, and the
function f
is continuous s
and f 0 = 0
.