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.
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.
To do #
- Get a version with joint continuity in both variables.
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.
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.
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 𝕜.
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.
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.
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 𝕜.
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.