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: 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.
• Filter.Tendsto.cfc: 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₀.
• lipschitzOnWith_cfc_fun: The function f ↦ cfc f a is Lipschitz with constant with constant 1 with respect to supremum metric (on R →ᵤ[{spectrum R a}] R) on those functions which are continuous on the spectrum.
• continuousOn_cfc: 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.
• continuousOn_cfc_setProd: 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.
• Versions of all of the above for non-unital algebras, and versions over ℝ≥0 as well.

theorem tendsto_cfc_fun {X : Type u_1} {R : Type u_2} {A : Type u_3} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [ContinuousFunctionalCalculus R A p] {l : Filter X} {F : X → R → R} {f : R → R} {a : A} (h_tendsto : TendstoUniformlyOn F f l (spectrum R a)) (hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (spectrum R a)) : Filter.Tendsto (fun (x : X) => cfc (F x) a) l (nhds (cfc f a))

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.

theorem continuousAt_cfc_fun {X : Type u_1} {R : Type u_2} {A : Type u_3} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [ContinuousFunctionalCalculus R A p] [TopologicalSpace X] {f : X → R → R} {a : A} {x₀ : X} (h_tendsto : TendstoUniformlyOn f (f x₀) (nhds x₀) (spectrum R a)) (hf : ∀ᶠ (x : X) in nhds x₀, ContinuousOn (f x) (spectrum R a)) : ContinuousAt (fun (x : X) => cfc (f x) a) x₀

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₀.

theorem continuousWithinAt_cfc_fun {X : Type u_1} {R : Type u_2} {A : Type u_3} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [ContinuousFunctionalCalculus R A p] [TopologicalSpace X] {f : X → R → R} {a : A} {x₀ : X} {s : Set X} (h_tendsto : TendstoUniformlyOn f (f x₀) (nhdsWithin x₀ s) (spectrum R a)) (hf : ∀ᶠ (x : X) in nhdsWithin x₀ s, ContinuousOn (f x) (spectrum R a)) : ContinuousWithinAt (fun (x : X) => cfc (f x) a) s 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.

theorem ContinuousOn.cfc_fun {X : Type u_1} {R : Type u_2} {A : Type u_3} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [ContinuousFunctionalCalculus R A p] [TopologicalSpace X] {f : X → R → R} {a : A} {s : Set X} (h_cont : ContinuousOn (fun (x : X) => (UniformOnFun.ofFun {spectrum R a}) (f x)) s) (hf : ∀ x ∈ s, ContinuousOn (f x) (spectrum R a) := by cfc_cont_tac) : ContinuousOn (fun (x : X) => cfc (f x) a) 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.

theorem Continuous.cfc_fun {X : Type u_1} {R : Type u_2} {A : Type u_3} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [TopologicalSpace A] [Algebra R A] [ContinuousFunctionalCalculus R A p] [TopologicalSpace X] (f : X → R → R) (a : A) (h_cont : Continuous fun (x : X) => (UniformOnFun.ofFun {spectrum R a}) (f x)) (hf : ∀ (x : X), ContinuousOn (f x) (spectrum R a) := by cfc_cont_tac) : Continuous fun (x : X) => cfc (f x) a

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.

theorem lipschitzOnWith_cfc_fun (R : Type u_2) {A : Type u_3} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [MetricSpace A] [Algebra R A] [IsometricContinuousFunctionalCalculus R A p] (a : A) : LipschitzOnWith 1 (fun (f : UniformOnFun R R {spectrum R a}) => cfc ((UniformOnFun.toFun {spectrum R a}) f) a) {f : UniformOnFun R R {spectrum R a} | ContinuousOn ((UniformOnFun.toFun {spectrum R a}) f) (spectrum R a)}

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.

theorem lipschitzOnWith_cfc_fun_of_subset {R : Type u_2} {A : Type u_3} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [MetricSpace A] [Algebra R A] [IsometricContinuousFunctionalCalculus R A p] (a : A) {s : Set R} (hs : spectrum R a ⊆ s) : LipschitzOnWith 1 (fun (f : UniformOnFun R R {s}) => cfc ((UniformOnFun.toFun {s}) f) a) {f : UniformOnFun R R {s} | ContinuousOn ((UniformOnFun.toFun {s}) f) s}

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.

theorem continuous_cfcHomSuperset_left {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] [ContinuousStar A] [TopologicalSpace X] {s : Set 𝕜} (hs : IsCompact s) (f : C(↑s, 𝕜)) (a : X → A) (ha_cont : Continuous a) (ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s) (ha' : ∀ (x : X), p (a x) := by cfc_tac) : Continuous fun (x : X) => (cfcHomSuperset ⋯ ⋯) f

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.

theorem continuousOn_cfc {𝕜 : Type u_2} (A : Type u_3) {p : A → Prop} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] [ContinuousStar A] {s : Set 𝕜} (hs : IsCompact s) (f : 𝕜 → 𝕜) (hf : ContinuousOn f s := by cfc_cont_tac) : ContinuousOn (cfc f) {a : A | p a ∧ spectrum 𝕜 a ⊆ s}

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.

theorem continuousOn_cfc_setProd {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] [ContinuousStar A] {s : Set 𝕜} (hs : IsCompact s) : ContinuousOn (fun (fa : UniformOnFun 𝕜 𝕜 {s} × A) => cfc ((UniformOnFun.toFun {s}) fa.1) fa.2) ({f : UniformOnFun 𝕜 𝕜 {s} | ContinuousOn ((UniformOnFun.toFun {s}) f) s} ×ˢ {a : A | p a ∧ spectrum 𝕜 a ⊆ 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.

theorem Filter.Tendsto.cfc {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] [ContinuousStar A] {s : Set 𝕜} (hs : IsCompact s) (f : 𝕜 → 𝕜) {a : X → A} {a₀ : A} {l : Filter X} (ha_tendsto : Tendsto a l (nhds a₀)) (ha : ∀ᶠ (x : X) in l, spectrum 𝕜 (a x) ⊆ s) (ha' : ∀ᶠ (x : X) in l, p (a x)) (ha₀ : spectrum 𝕜 a₀ ⊆ s) (ha₀' : p a₀) (hf : ContinuousOn f s := by cfc_cont_tac) : Tendsto (fun (x : X) => cfc f (a x)) l (nhds (cfc f a₀))

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₀.

theorem ContinuousAt.cfc {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] [ContinuousStar A] [TopologicalSpace X] {s : Set 𝕜} (hs : IsCompact s) (f : 𝕜 → 𝕜) {a : X → A} {x₀ : X} (ha_cont : ContinuousAt a x₀) (ha : ∀ᶠ (x : X) in nhds x₀, spectrum 𝕜 (a x) ⊆ s) (ha' : ∀ᶠ (x : X) in nhds x₀, p (a x)) (hf : ContinuousOn f s := by cfc_cont_tac) : ContinuousAt (fun (x : X) => cfc f (a x)) x₀

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₀.

theorem ContinuousWithinAt.cfc {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] [ContinuousStar A] [TopologicalSpace X] {s : Set 𝕜} (hs : IsCompact s) (f : 𝕜 → 𝕜) {a : X → A} {x₀ : X} {t : Set X} (hx₀ : x₀ ∈ t) (ha_cont : ContinuousWithinAt a t x₀) (ha : ∀ᶠ (x : X) in nhdsWithin x₀ t, spectrum 𝕜 (a x) ⊆ s) (ha' : ∀ᶠ (x : X) in nhdsWithin x₀ t, p (a x)) (hf : ContinuousOn f s := by cfc_cont_tac) : ContinuousWithinAt (fun (x : X) => cfc f (a x)) t 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.

theorem ContinuousOn.cfc {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] [ContinuousStar A] [TopologicalSpace X] {s : X → Set 𝕜} (f : 𝕜 → 𝕜) {a : X → A} {t : Set X} (hs : ∀ x ∈ t, IsCompact (s x)) (ha_cont : ContinuousOn a t) (ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in nhdsWithin x₀ t, spectrum 𝕜 (a x) ⊆ s x₀) (ha' : ∀ x ∈ t, p (a x)) (hf : ∀ x ∈ t, ContinuousOn f (s x) := by cfc_cont_tac) : ContinuousOn (fun (x : X) => cfc f (a x)) t

Suppose a : X → Set A is continuous on t : Set X and a x satisfies the predicate p for all x ∈ t. Suppose further that s : X → Set 𝕜 is a family of sets with s x compact when x ∈ t such that s x₀ contains the spectrum of a x for all sufficiently close x ∈ t. If f : 𝕜 → 𝕜 is continuous on s x, for each x ∈ t, then fun x ↦ cfc f (a x) is continuous on t.

theorem ContinuousOn.cfc' {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] [ContinuousStar A] [TopologicalSpace X] {s : Set 𝕜} (hs : IsCompact s) (f : 𝕜 → 𝕜) {a : X → A} {t : Set X} (ha_cont : ContinuousOn a t) (ha : ∀ x ∈ t, spectrum 𝕜 (a x) ⊆ s) (ha' : ∀ x ∈ t, p (a x)) (hf : ContinuousOn f s := by cfc_cont_tac) : ContinuousOn (fun (x : X) => cfc f (a x)) 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.

theorem ContinuousOn.cfc_of_mem_nhdsSet {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] [ContinuousStar A] [CompleteSpace A] [TopologicalSpace X] {s : Set 𝕜} (f : 𝕜 → 𝕜) {a : X → A} {t : Set X} (hs : s ∈ nhdsSet (⋃ x ∈ t, spectrum 𝕜 (a x))) (ha_cont : ContinuousOn a t) (ha' : ∀ x ∈ t, p (a x) := by cfc_tac) (hf : ContinuousOn f s := by cfc_cont_tac) : ContinuousOn (fun (x : X) => cfc f (a x)) t

If f : 𝕜 → 𝕜 is continuous on s and a : X → A is continuous on t : Set X, and a x satisfies the predicate p associated to 𝕜 and s is a common neighborhood of the spectra of a x for all x ∈ t, then fun x ↦ cfc f (a x) is continuous on t.

This is weaker than ContinuousOn.cfc since it requires f to be continuous on a neighborhood of the spectra, but in practice it is often easier to apply because s is not required to be compact, nor does it require an indexed family of compact sets. This is proven using ContinuousOn.cfc and upperHemicontinuous_spectrum to produce the necessary family of compact sets.

theorem Continuous.cfc {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] [ContinuousStar A] [TopologicalSpace X] {s : X → Set 𝕜} (f : 𝕜 → 𝕜) {a : X → A} (ha_cont : Continuous a) (hs : ∀ (x : X), IsCompact (s x)) (ha : ∀ (x₀ : X), ∀ᶠ (x : X) in nhds x₀, spectrum 𝕜 (a x) ⊆ s x₀) (hf : ∀ (x : X), ContinuousOn f (s x) := by cfc_cont_tac) (ha' : ∀ (x : X), p (a x) := by cfc_tac) : Continuous fun (x : X) => cfc f (a x)

Suppose a : X → Set A is continuous and a x satisfies the predicate p for all x. Suppose further that s : X → Set 𝕜 is a family of compact sets s x₀ contains the spectrum of a x for all sufficiently close x. If f : 𝕜 → 𝕜 is continuous on each s x, then fun x ↦ cfc f (a x) is continuous.

theorem Continuous.cfc' {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] [ContinuousStar A] [TopologicalSpace X] {s : Set 𝕜} (hs : IsCompact s) (f : 𝕜 → 𝕜) {a : X → A} (ha_cont : Continuous a) (ha : ∀ (x : X), spectrum 𝕜 (a x) ⊆ s) (hf : ContinuousOn f s := by cfc_cont_tac) (ha' : ∀ (x : X), p (a x) := by cfc_tac) : Continuous fun (x : X) => cfc f (a x)

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.

theorem Continuous.cfc_of_mem_nhdsSet {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] [ContinuousStar A] [CompleteSpace A] [TopologicalSpace X] {s : Set 𝕜} (f : 𝕜 → 𝕜) {a : X → A} (hs : s ∈ nhdsSet (⋃ (x : X), spectrum 𝕜 (a x))) (ha_cont : Continuous a) (ha' : ∀ (x : X), p (a x) := by cfc_tac) (hf : ContinuousOn f s := by cfc_cont_tac) : Continuous fun (x : X) => cfc f (a x)

If f : 𝕜 → 𝕜 is continuous on s and a : X → A is continuous and a x satisfies the predicate p associated to 𝕜 and s is a common neighborhood of the spectra of a x for all x, then fun x ↦ cfc f (a x) is continuous.

This is weaker than Continuous.cfc since it requires f to be continuous on a neighborhood of the spectra, but in practice it is often easier to apply because s is not required to be compact, nor does it require an indexed family of compact sets. This is proven using Continuous.cfc and upperHemicontinuous_spectrum to produce the necessary family of compact sets.

theorem continuousOn_cfc_nnreal (A : Type u_2) [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] {s : Set NNReal} (hs : IsCompact s) (f : NNReal → NNReal) (hf : ContinuousOn f s := by cfc_cont_tac) : ContinuousOn (cfc f) {a : A | 0 ≤ a ∧ spectrum NNReal a ⊆ s}

A version of continuousOn_cfc over ℝ≥0 instead of RCLike 𝕜.

theorem continuousOn_cfc_nnreal_setProd {A : Type u_2} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] {s : Set NNReal} (hs : IsCompact s) : ContinuousOn (fun (fa : UniformOnFun NNReal NNReal {s} × A) => cfc ((UniformOnFun.toFun {s}) fa.1) fa.2) ({f : UniformOnFun NNReal NNReal {s} | ContinuousOn ((UniformOnFun.toFun {s}) f) s} ×ˢ {a : A | 0 ≤ a ∧ spectrum NNReal a ⊆ s})

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.

theorem Filter.Tendsto.cfc_nnreal {X : Type u_1} {A : Type u_2} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] {s : Set NNReal} (hs : IsCompact s) (f : NNReal → NNReal) {a : X → A} {a₀ : A} {l : Filter X} (ha_tendsto : Tendsto a l (nhds a₀)) (ha : ∀ᶠ (x : X) in l, spectrum NNReal (a x) ⊆ s) (ha' : ∀ᶠ (x : X) in l, 0 ≤ a x) (ha₀ : spectrum NNReal a₀ ⊆ s) (ha₀' : 0 ≤ a₀) (hf : ContinuousOn f s := by cfc_cont_tac) : Tendsto (fun (x : X) => cfc f (a x)) l (nhds (cfc f a₀))

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₀.

theorem ContinuousAt.cfc_nnreal {X : Type u_1} {A : Type u_2} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] [TopologicalSpace X] {s : Set NNReal} (hs : IsCompact s) (f : NNReal → NNReal) {a : X → A} {x₀ : X} (ha_cont : ContinuousAt a x₀) (ha : ∀ᶠ (x : X) in nhds x₀, spectrum NNReal (a x) ⊆ s) (ha' : ∀ᶠ (x : X) in nhds x₀, 0 ≤ a x) (hf : ContinuousOn f s := by cfc_cont_tac) : ContinuousAt (fun (x : X) => cfc f (a x)) x₀

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₀.

theorem ContinuousWithinAt.cfc_nnreal {X : Type u_1} {A : Type u_2} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] [TopologicalSpace X] {s : Set NNReal} (hs : IsCompact s) (f : NNReal → NNReal) {a : X → A} {x₀ : X} {t : Set X} (hx₀ : x₀ ∈ t) (ha_cont : ContinuousWithinAt a t x₀) (ha : ∀ᶠ (x : X) in nhdsWithin x₀ t, spectrum NNReal (a x) ⊆ s) (ha' : ∀ᶠ (x : X) in nhdsWithin x₀ t, 0 ≤ a x) (hf : ContinuousOn f s := by cfc_cont_tac) : ContinuousWithinAt (fun (x : X) => cfc f (a x)) t 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.

theorem ContinuousOn.cfc_nnreal {X : Type u_1} {A : Type u_2} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] [TopologicalSpace X] {s : X → Set NNReal} (f : NNReal → NNReal) {a : X → A} {t : Set X} (hs : ∀ x ∈ t, IsCompact (s x)) (ha_cont : ContinuousOn a t) (ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in nhdsWithin x₀ t, spectrum NNReal (a x) ⊆ s x₀) (ha' : ∀ x ∈ t, 0 ≤ a x) (hf : ∀ x ∈ t, ContinuousOn f (s x) := by cfc_cont_tac) : ContinuousOn (fun (x : X) => cfc f (a x)) t

Suppose a : X → Set A is continuous on t : Set X and 0 ≤ a x for all x ∈ t. Suppose further that s : X → Set ℝ≥0 is a family of sets with s x compact when x ∈ t such that s x₀ contains the spectrum of a x for all sufficiently close x ∈ t. If f : ℝ≥0 → ℝ≥0 is continuous on s x, for each x ∈ t, then fun x ↦ cfc f (a x) is continuous on t.

theorem ContinuousOn.cfc_nnreal' {X : Type u_1} {A : Type u_2} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] [TopologicalSpace X] {s : Set NNReal} (hs : IsCompact s) (f : NNReal → NNReal) {a : X → A} {t : Set X} (ha_cont : ContinuousOn a t) (ha : ∀ x ∈ t, spectrum NNReal (a x) ⊆ s) (ha' : ∀ x ∈ t, 0 ≤ a x) (hf : ContinuousOn f s := by cfc_cont_tac) : ContinuousOn (fun (x : X) => cfc f (a x)) 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.

theorem ContinuousOn.cfc_nnreal_of_mem_nhdsSet {X : Type u_1} {A : Type u_2} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] [CompleteSpace A] [TopologicalSpace X] {s : Set NNReal} (f : NNReal → NNReal) {a : X → A} {t : Set X} (hs : s ∈ nhdsSet (⋃ x ∈ t, spectrum NNReal (a x))) (ha_cont : ContinuousOn a t) (ha' : ∀ x ∈ t, 0 ≤ a x := by cfc_tac) (hf : ContinuousOn f s := by cfc_cont_tac) : ContinuousOn (fun (x : X) => cfc f (a x)) t

If f : ℝ≥0 → ℝ≥0 is continuous on s and a : X → A is continuous on t : Set X, and a x is nonnegative for all x ∈ t and s is a common neighborhood of the spectra of a x for all x ∈ t, then fun x ↦ cfc f (a x) is continuous on t.

This is weaker than ContinuousOn.cfc_nnreal since it requires f to be continuous on a neighborhood of the spectra, but in practice it is often easier to apply because s is not required to be compact, nor does it require an indexed family of compact sets. This is proven using ContinuousOn.cfc_nnreal and upperHemicontinuous_spectrum_nnreal to produce the necessary family of compact sets.

theorem Continuous.cfc_nnreal {X : Type u_1} {A : Type u_2} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] [TopologicalSpace X] {s : X → Set NNReal} (f : NNReal → NNReal) {a : X → A} (ha_cont : Continuous a) (hs : ∀ (x : X), IsCompact (s x)) (ha : ∀ (x₀ : X), ∀ᶠ (x : X) in nhds x₀, spectrum NNReal (a x) ⊆ s x₀) (hf : ∀ (x : X), ContinuousOn f (s x) := by cfc_cont_tac) (ha' : ∀ (x : X), 0 ≤ a x := by cfc_tac) : Continuous fun (x : X) => cfc f (a x)

Suppose a : X → Set A is a continuous family of nonnegative elements. Suppose further that s : X → Set ℝ≥0 is a family of compact sets such that s x₀ contains the spectrum of a x for all sufficiently close x. If f : ℝ≥0 → ℝ≥0 is continuous on each s x, then fun x ↦ cfc f (a x) is continuous.

theorem Continuous.cfc_nnreal' {X : Type u_1} {A : Type u_2} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] [TopologicalSpace X] {s : Set NNReal} (hs : IsCompact s) (f : NNReal → NNReal) {a : X → A} (ha_cont : Continuous a) (ha : ∀ (x : X), spectrum NNReal (a x) ⊆ s) (hf : ContinuousOn f s := by cfc_cont_tac) (ha' : ∀ (x : X), 0 ≤ a x := by cfc_tac) : Continuous fun (x : X) => cfc f (a x)

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.

theorem Continuous.cfc_nnreal_of_mem_nhdsSet {X : Type u_1} {A : Type u_2} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] [CompleteSpace A] [TopologicalSpace X] {s : Set NNReal} (f : NNReal → NNReal) {a : X → A} (hs : s ∈ nhdsSet (⋃ (x : X), spectrum NNReal (a x))) (ha_cont : Continuous a) (ha' : ∀ (x : X), 0 ≤ a x := by cfc_tac) (hf : ContinuousOn f s := by cfc_cont_tac) : Continuous fun (x : X) => cfc f (a x)

If f : ℝ≥0 → ℝ≥0 is continuous on s and a : X → A is continuous and a x is nonnegative for all x and s is a common neighborhood of the spectra of a x for all x, then fun x ↦ cfc f (a x) is continuous.

This is weaker than Continuous.cfc_nnreal since it requires f to be continuous on a neighborhood of the spectra, but in practice it is often easier to apply because s is not required to be compact, nor does it require an indexed family of compact sets. This is proven using Continuous.cfc_nnreal and upperHemicontinuous_spectrum_nnreal to produce the necessary family of compact sets.

theorem tendsto_cfcₙ_fun {X : Type u_1} {R : Type u_2} {A : Type u_3} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [Nontrivial R] [IsTopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalContinuousFunctionalCalculus R A p] {l : Filter X} {F : X → R → R} {f : R → R} {a : A} (h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)) (hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)) (hF0 : ∀ᶠ (x : X) in l, F x 0 = 0) : Filter.Tendsto (fun (x : X) => cfcₙ (F x) a) l (nhds (cfcₙ f a))

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.

theorem continuousAt_cfcₙ_fun {X : Type u_1} {R : Type u_2} {A : Type u_3} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [Nontrivial R] [IsTopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalContinuousFunctionalCalculus R A p] [TopologicalSpace X] {f : X → R → R} {a : A} {x₀ : X} (h_tendsto : TendstoUniformlyOn f (f x₀) (nhds x₀) (quasispectrum R a)) (hf : ∀ᶠ (x : X) in nhds x₀, ContinuousOn (f x) (quasispectrum R a)) (hf0 : ∀ᶠ (x : X) in nhds x₀, f x 0 = 0) : ContinuousAt (fun (x : X) => cfcₙ (f x) a) x₀

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₀.

theorem continuousWithinAt_cfcₙ_fun {X : Type u_1} {R : Type u_2} {A : Type u_3} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [Nontrivial R] [IsTopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalContinuousFunctionalCalculus R A p] [TopologicalSpace X] {f : X → R → R} {a : A} {x₀ : X} {s : Set X} (h_tendsto : TendstoUniformlyOn f (f x₀) (nhdsWithin x₀ s) (quasispectrum R a)) (hf : ∀ᶠ (x : X) in nhdsWithin x₀ s, ContinuousOn (f x) (quasispectrum R a)) (hf0 : ∀ᶠ (x : X) in nhdsWithin x₀ s, f x 0 = 0 := by cfc_zero_tac) : ContinuousWithinAt (fun (x : X) => cfcₙ (f x) a) s 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.

theorem ContinuousOn.cfcₙ_fun {X : Type u_1} {R : Type u_2} {A : Type u_3} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [Nontrivial R] [IsTopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalContinuousFunctionalCalculus R A p] [TopologicalSpace X] {f : X → R → R} {a : A} {s : Set X} (h_cont : ContinuousOn (fun (x : X) => (UniformOnFun.ofFun {quasispectrum R a}) (f x)) s) (hf : ∀ x ∈ s, ContinuousOn (f x) (quasispectrum R a)) (hf0 : ∀ x ∈ s, f x 0 = 0) : ContinuousOn (fun (x : X) => cfcₙ (f x) a) 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.

theorem Continuous.cfcₙ_fun {X : Type u_1} {R : Type u_2} {A : Type u_3} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [Nontrivial R] [IsTopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalContinuousFunctionalCalculus R A p] [TopologicalSpace X] (f : X → R → R) (a : A) (h_cont : Continuous fun (x : X) => (UniformOnFun.ofFun {quasispectrum R a}) (f x)) (hf : ∀ (x : X), ContinuousOn (f x) (quasispectrum R a) := by cfc_cont_tac) (hf0 : ∀ (x : X), f x 0 = 0 := by cfc_zero_tac) : Continuous fun (x : X) => cfcₙ (f x) a

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.

theorem lipschitzOnWith_cfcₙ_fun (R : Type u_2) {A : Type u_3} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [Nontrivial R] [IsTopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [MetricSpace A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalIsometricContinuousFunctionalCalculus R A p] (a : A) : LipschitzOnWith 1 (fun (f : UniformOnFun R R {quasispectrum R a}) => cfcₙ ((UniformOnFun.toFun {quasispectrum R a}) f) a) {f : UniformOnFun R R {quasispectrum R a} | ContinuousOn ((UniformOnFun.toFun {quasispectrum R a}) f) (quasispectrum R a) ∧ f 0 = 0}

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.

theorem lipschitzOnWith_cfcₙ_fun_of_subset {R : Type u_2} {A : Type u_3} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R] [Nontrivial R] [IsTopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [MetricSpace A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalIsometricContinuousFunctionalCalculus R A p] (a : A) {s : Set R} (hs : quasispectrum R a ⊆ s) : LipschitzOnWith 1 (fun (f : UniformOnFun R R {s}) => cfcₙ ((UniformOnFun.toFun {s}) f) a) {f : UniformOnFun R R {s} | ContinuousOn ((UniformOnFun.toFun {s}) f) s ∧ f 0 = 0}

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.

theorem continuous_cfcₙHomSuperset_left {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] [TopologicalSpace X] {s : Set 𝕜} (hs : IsCompact s) [hs0 : Fact (0 ∈ s)] (f : ContinuousMapZero (↑s) 𝕜) {a : X → A} (ha_cont : Continuous a) (ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s) (ha' : ∀ (x : X), p (a x) := by cfc_tac) : Continuous fun (x : X) => (cfcₙHomSuperset ⋯ ⋯) f

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.

theorem continuousOn_cfcₙ {𝕜 : Type u_2} (A : Type u_3) {p : A → Prop} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] {s : Set 𝕜} (hs : IsCompact s) (f : 𝕜 → 𝕜) (hf : ContinuousOn f s := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) : ContinuousOn (fun (x : A) => cfcₙ f x) {a : A | p a ∧ quasispectrum 𝕜 a ⊆ s}

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.

theorem continuousOn_cfcₙ_setProd {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] {s : Set 𝕜} (hs : IsCompact s) : ContinuousOn (fun (fa : UniformOnFun 𝕜 𝕜 {s} × A) => cfcₙ ((UniformOnFun.toFun {s}) fa.1) fa.2) ({f : UniformOnFun 𝕜 𝕜 {s} | ContinuousOn ((UniformOnFun.toFun {s}) f) s ∧ f 0 = 0} ×ˢ {a : A | p a ∧ quasispectrum 𝕜 a ⊆ 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.

theorem Filter.Tendsto.cfcₙ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] {s : Set 𝕜} (hs : IsCompact s) (f : 𝕜 → 𝕜) {a : X → A} {a₀ : A} {l : Filter X} (ha_tendsto : Tendsto a l (nhds a₀)) (ha : ∀ᶠ (x : X) in l, quasispectrum 𝕜 (a x) ⊆ s) (ha' : ∀ᶠ (x : X) in l, p (a x)) (ha₀ : quasispectrum 𝕜 a₀ ⊆ s) (ha₀' : p a₀) (hf : ContinuousOn f s := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) : Tendsto (fun (x : X) => cfcₙ f (a x)) l (nhds (cfcₙ f a₀))

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₀.

theorem ContinuousAt.cfcₙ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] [TopologicalSpace X] {s : Set 𝕜} (hs : IsCompact s) (f : 𝕜 → 𝕜) {a : X → A} {x₀ : X} (ha_cont : ContinuousAt a x₀) (ha : ∀ᶠ (x : X) in nhds x₀, quasispectrum 𝕜 (a x) ⊆ s) (ha' : ∀ᶠ (x : X) in nhds x₀, p (a x)) (hf : ContinuousOn f s := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) : ContinuousAt (fun (x : X) => cfcₙ f (a x)) x₀

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₀.

theorem ContinuousWithinAt.cfcₙ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] [TopologicalSpace X] {s : Set 𝕜} (hs : IsCompact s) (f : 𝕜 → 𝕜) {a : X → A} {x₀ : X} {t : Set X} (hx₀ : x₀ ∈ t) (ha_cont : ContinuousWithinAt a t x₀) (ha : ∀ᶠ (x : X) in nhdsWithin x₀ t, quasispectrum 𝕜 (a x) ⊆ s) (ha' : ∀ᶠ (x : X) in nhdsWithin x₀ t, p (a x)) (hf : ContinuousOn f s := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) : ContinuousWithinAt (fun (x : X) => cfcₙ f (a x)) t 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.

theorem ContinuousOn.cfcₙ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] [TopologicalSpace X] {s : X → Set 𝕜} (f : 𝕜 → 𝕜) {a : X → A} {t : Set X} (hs : ∀ x ∈ t, IsCompact (s x)) (ha_cont : ContinuousOn a t) (ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in nhdsWithin x₀ t, quasispectrum 𝕜 (a x) ⊆ s x₀) (ha' : ∀ x ∈ t, p (a x)) (hf : ∀ x ∈ t, ContinuousOn f (s x) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) : ContinuousOn (fun (x : X) => cfcₙ f (a x)) t

Suppose a : X → Set A is continuous on t : Set X and a x satisfies the predicate p for all x ∈ t. Suppose further that s : X → Set 𝕜 is a family of sets with s x compact when x ∈ t such that s x₀ contains the spectrum of a x for all sufficiently close x ∈ t. If f : 𝕜 → 𝕜 is continuous on s x for each x ∈ t, and f 0 = 0 then fun x ↦ cfcₙ f (a x) is continuous on t.

theorem ContinuousOn.cfcₙ' {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] [TopologicalSpace X] {s : Set 𝕜} (hs : IsCompact s) (f : 𝕜 → 𝕜) {a : X → A} {t : Set X} (ha_cont : ContinuousOn a t) (ha : ∀ x ∈ t, quasispectrum 𝕜 (a x) ⊆ s) (ha' : ∀ x ∈ t, p (a x)) (hf : ContinuousOn f s := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) : ContinuousOn (fun (x : X) => cfcₙ f (a x)) 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.

theorem ContinuousOn.cfcₙ_of_mem_nhdsSet {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] [CompleteSpace A] [TopologicalSpace X] {s : Set 𝕜} (f : 𝕜 → 𝕜) {a : X → A} {t : Set X} (hs : s ∈ nhdsSet (⋃ x ∈ t, quasispectrum 𝕜 (a x))) (ha_cont : ContinuousOn a t) (ha' : ∀ x ∈ t, p (a x) := by cfc_tac) (hf : ContinuousOn f s := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) : ContinuousOn (fun (x : X) => cfcₙ f (a x)) t

If f : 𝕜 → 𝕜 is continuous on 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 s is a common neighborhood of the quasispectra of a x for all x ∈ t, then fun x ↦ cfcₙ f (a x) is continuous on t.

This is weaker than ContinuousOn.cfcₙ since it requires f to be continuous on a neighborhood of the quasispectra, but in practice it is often easier to apply because s is not required to be compact, nor does it require an indexed family of compact sets. This is proven using ContinuousOn.cfcₙ and upperHemicontinuous_quasispectrum to produce the necessary family of compact sets.

theorem Continuous.cfcₙ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] [TopologicalSpace X] {s : X → Set 𝕜} (f : 𝕜 → 𝕜) {a : X → A} (ha_cont : Continuous a) (hs : ∀ (x : X), IsCompact (s x)) (ha : ∀ (x₀ : X), ∀ᶠ (x : X) in nhds x₀, quasispectrum 𝕜 (a x) ⊆ s x₀) (hf : ∀ (x : X), ContinuousOn f (s x) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (ha' : ∀ (x : X), p (a x) := by cfc_tac) : Continuous fun (x : X) => cfcₙ f (a x)

Suppose a : X → Set A is continuous and a x satisfies the predicate p for all x. Suppose further that s : X → Set 𝕜 is a family of compact sets s x₀ contains the spectrum of a x for all sufficiently close x. If f : 𝕜 → 𝕜 is continuous on each s x and f 0 = 0, then fun x ↦ cfc f (a x) is continuous.

theorem Continuous.cfcₙ' {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] [TopologicalSpace X] {s : Set 𝕜} (hs : IsCompact s) (f : 𝕜 → 𝕜) {a : X → A} (ha_cont : Continuous a) (ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s) (hf : ContinuousOn f s := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (ha' : ∀ (x : X), p (a x) := by cfc_tac) : Continuous fun (x : X) => cfcₙ f (a x)

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.

theorem Continuous.cfcₙ_of_mem_nhdsSet {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] [CompleteSpace A] [TopologicalSpace X] {s : Set 𝕜} (f : 𝕜 → 𝕜) {a : X → A} (hs : s ∈ nhdsSet (⋃ (x : X), quasispectrum 𝕜 (a x))) (ha_cont : Continuous a) (ha' : ∀ (x : X), p (a x) := by cfc_tac) (hf : ContinuousOn f s := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) : Continuous fun (x : X) => cfcₙ f (a x)

If f : 𝕜 → 𝕜 is continuous on s and f 0 = 0 and a : X → A is continuous and a x satisfies the predicate p associated to 𝕜 and s is a common neighborhood of the quasispectra of a x for all x, then fun x ↦ cfcₙ f (a x) is continuous.

This is weaker than Continuous.cfcₙ since it requires f to be continuous on a neighborhood of the quasispectra, but in practice it is often easier to apply because s is not required to be compact, nor does it require an indexed family of compact sets. This is proven using Continuous.cfcₙ and upperHemicontinuous_quasispectrum to produce the necessary family of compact sets.

theorem continuousOn_cfcₙ_nnreal (A : Type u_2) [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] {s : Set NNReal} (hs : IsCompact s) (f : NNReal → NNReal) (hf : ContinuousOn f s := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) : ContinuousOn (fun (x : A) => cfcₙ f x) {a : A | 0 ≤ a ∧ quasispectrum NNReal a ⊆ s}

A version of continuousOn_cfcₙ over ℝ≥0 instead of RCLike 𝕜.

theorem continuousOn_cfcₙ_nnreal_setProd {A : Type u_2} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] {s : Set NNReal} (hs : IsCompact s) : ContinuousOn (fun (fa : UniformOnFun NNReal NNReal {s} × A) => cfcₙ ((UniformOnFun.toFun {s}) fa.1) fa.2) ({f : UniformOnFun NNReal NNReal {s} | ContinuousOn ((UniformOnFun.toFun {s}) f) s ∧ f 0 = 0} ×ˢ {a : A | 0 ≤ a ∧ quasispectrum NNReal a ⊆ s})

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.

theorem Filter.Tendsto.cfcₙ_nnreal {X : Type u_1} {A : Type u_2} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] {s : Set NNReal} (hs : IsCompact s) (f : NNReal → NNReal) {a : X → A} {a₀ : A} {l : Filter X} (ha_tendsto : Tendsto a l (nhds a₀)) (ha : ∀ᶠ (x : X) in l, quasispectrum NNReal (a x) ⊆ s) (ha' : ∀ᶠ (x : X) in l, 0 ≤ a x) (ha₀ : quasispectrum NNReal a₀ ⊆ s) (ha₀' : 0 ≤ a₀) (hf : ContinuousOn f s := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) : Tendsto (fun (x : X) => cfcₙ f (a x)) l (nhds (cfcₙ f a₀))

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 0 ≤ a x and has quasispectrum contained in s, as does a₀), then fun x ↦ cfcₙ f (a x) tends to cfcₙ f a₀.

theorem ContinuousAt.cfcₙ_nnreal {X : Type u_1} {A : Type u_2} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] [TopologicalSpace X] {s : Set NNReal} (hs : IsCompact s) (f : NNReal → NNReal) {a : X → A} {x₀ : X} (ha_cont : ContinuousAt a x₀) (ha : ∀ᶠ (x : X) in nhds x₀, quasispectrum NNReal (a x) ⊆ s) (ha' : ∀ᶠ (x : X) in nhds x₀, 0 ≤ a x) (hf : ContinuousOn f s := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) : ContinuousAt (fun (x : X) => cfcₙ f (a x)) x₀

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 0 ≤ a x and has quasispectrum contained in s, then fun x ↦ cfcₙ f (a x) is continuous at x₀.

theorem ContinuousWithinAt.cfcₙ_nnreal {X : Type u_1} {A : Type u_2} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] [TopologicalSpace X] {s : Set NNReal} (hs : IsCompact s) (f : NNReal → NNReal) {a : X → A} {x₀ : X} {t : Set X} (hx₀ : x₀ ∈ t) (ha_cont : ContinuousWithinAt a t x₀) (ha : ∀ᶠ (x : X) in nhdsWithin x₀ t, quasispectrum NNReal (a x) ⊆ s) (ha' : ∀ᶠ (x : X) in nhdsWithin x₀ t, 0 ≤ a x) (hf : ContinuousOn f s := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) : ContinuousWithinAt (fun (x : X) => cfcₙ f (a x)) t 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 0 ≤ a x and has quasispectrum contained in s, then fun x ↦ cfcₙ f (a x) is continuous at x₀ within t.

theorem ContinuousOn.cfcₙ_nnreal {X : Type u_1} {A : Type u_2} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] [TopologicalSpace X] {s : X → Set NNReal} (f : NNReal → NNReal) {a : X → A} {t : Set X} (hs : ∀ x ∈ t, IsCompact (s x)) (ha_cont : ContinuousOn a t) (ha : ∀ x₀ ∈ t, ∀ᶠ (x : X) in nhdsWithin x₀ t, quasispectrum NNReal (a x) ⊆ s x₀) (ha' : ∀ x ∈ t, 0 ≤ a x) (hf : ∀ x ∈ t, ContinuousOn f (s x) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) : ContinuousOn (fun (x : X) => cfcₙ f (a x)) t

Suppose a : X → Set A is continuous on t : Set X and 0 ≤ a x for all x ∈ t. Suppose further that s : X → Set ℝ≥0 is a family of sets with s x compact when x ∈ t such that s x₀ contains the spectrum of a x for all sufficiently close x ∈ t. If f : ℝ≥0 → ℝ≥0 is continuous on s x for each x ∈ t and f 0 = 0, then fun x ↦ cfc f (a x) is continuous on t.

theorem ContinuousOn.cfcₙ_nnreal' {X : Type u_1} {A : Type u_2} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] [TopologicalSpace X] {s : Set NNReal} (hs : IsCompact s) (f : NNReal → NNReal) {a : X → A} {t : Set X} (ha_cont : ContinuousOn a t) (ha : ∀ x ∈ t, quasispectrum NNReal (a x) ⊆ s) (ha' : ∀ x ∈ t, 0 ≤ a x) (hf : ContinuousOn f s := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) : ContinuousOn (fun (x : X) => cfcₙ f (a x)) 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 0 ≤ a x and has quasispectrum contained in s for all x ∈ t, then fun x ↦ cfcₙ f (a x) is continuous on t.

theorem ContinuousOn.cfcₙ_nnreal_of_mem_nhdsSet {X : Type u_1} {A : Type u_2} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] [CompleteSpace A] [TopologicalSpace X] {s : Set NNReal} (f : NNReal → NNReal) {a : X → A} {t : Set X} (hs : s ∈ nhdsSet (⋃ x ∈ t, quasispectrum NNReal (a x))) (ha_cont : ContinuousOn a t) (ha' : ∀ x ∈ t, 0 ≤ a x := by cfc_tac) (hf : ContinuousOn f s := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) : ContinuousOn (fun (x : X) => cfcₙ f (a x)) t

If f : ℝ≥0 → ℝ≥0 is continuous on s and f 0 = 0 and a : X → A is continuous on t : Set X, and a x is nonnegative for all x ∈ t and s is a common neighborhood of the quasispectra of a x for all x ∈ t, then fun x ↦ cfcₙ f (a x) is continuous on t.

This is weaker than ContinuousOn.cfcₙ_nnreal since it requires f to be continuous on a neighborhood of the quasispectra, but in practice it is often easier to apply because s is not required to be compact, nor does it require an indexed family of compact sets. This is proven using ContinuousOn.cfcₙ_nnreal and upperHemicontinuous_quasispectrum_nnreal to produce the necessary family of compact sets.

theorem Continuous.cfcₙ_nnreal {X : Type u_1} {A : Type u_2} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] [TopologicalSpace X] {s : X → Set NNReal} (f : NNReal → NNReal) {a : X → A} (ha_cont : Continuous a) (hs : ∀ (x : X), IsCompact (s x)) (ha : ∀ (x₀ : X), ∀ᶠ (x : X) in nhds x₀, quasispectrum NNReal (a x) ⊆ s x₀) (hf : ∀ (x : X), ContinuousOn f (s x) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (ha' : ∀ (x : X), 0 ≤ a x := by cfc_tac) : Continuous fun (x : X) => cfcₙ f (a x)

Suppose a : X → Set A is a continuous family of nonnegative elements. Suppose further that s : X → Set ℝ≥0 is a family of compact sets such that s x₀ contains the spectrum of a x for all sufficiently close x. If f : ℝ≥0 → ℝ≥0 is continuous on each s x and f 0 = 0, then fun x ↦ cfc f (a x) is continuous.

theorem Continuous.cfcₙ_nnreal' {X : Type u_1} {A : Type u_2} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] [TopologicalSpace X] {s : Set NNReal} (hs : IsCompact s) (f : NNReal → NNReal) {a : X → A} (ha_cont : Continuous a) (ha : ∀ (x : X), quasispectrum NNReal (a x) ⊆ s) (hf : ContinuousOn f s := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (ha' : ∀ (x : X), 0 ≤ a x := by cfc_tac) : Continuous fun (x : X) => cfcₙ f (a x)

cfcₙ is continuous in the variable a : A when s : Set ℝ≥0 is compact and a varies over nonnegative elements whose quasispectrum is contained in s, and the function f is continuous on s and f 0 = 0.

theorem Continuous.cfcₙ_nnreal_of_mem_nhdsSet {X : Type u_1} {A : Type u_2} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [ContinuousStar A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [T2Space A] [IsTopologicalRing A] [CompleteSpace A] [TopologicalSpace X] {s : Set NNReal} (f : NNReal → NNReal) {a : X → A} (hs : s ∈ nhdsSet (⋃ (x : X), quasispectrum NNReal (a x))) (ha_cont : Continuous a) (ha' : ∀ (x : X), 0 ≤ a x := by cfc_tac) (hf : ContinuousOn f s := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) : Continuous fun (x : X) => cfcₙ f (a x)

If f : ℝ≥0 → ℝ≥0 is continuous on s and f 0 = 0 and a : X → A is continuous and a x is nonnegative for all x and s is a common neighborhood of the quasispectra of a x for all x, then fun x ↦ cfcₙ f (a x) is continuous.

This is weaker than Continuous.cfcₙ_nnreal since it requires f to be continuous on a neighborhood of the quasispectra, but in practice it is often easier to apply because s is not required to be compact, nor does it require an indexed family of compact sets. This is proven using Continuous.cfcₙ_nnreal and upperHemicontinuous_quasispectrum_nnreal to produce the necessary family of compact sets.