feat: convenience lemmas for continuity of the continuous functional calculus in the operator variable (leanprover-community#33628)

If `a : X → A` is continuous and `A` is a C⋆-algebra and `f` is continuous on a neighborhood of the union of the spectra of `a x`, then `fun x ↦ cfc f (a x)` is continuous (assuming that `a x` satisfies the relevant predicate for the continuous functional calculus).

This is slightly weaker than our existing theorems for the continuity of the continuous functional calculus (compare with `Continuous.cfc`), but it is often easier to apply in practice. In particular, it uses upper hemicontinuity of the spectrum to automatically satisfy some of the hypotheses in `Continuous.cfc` at the cost of requiring a *neighborhood* (instead of just compact sets containing the spectra).

Indeed, in leanprover-community#33617 we use this to establish continuity of common functions defined in terms of the continuous functional calculus, such as `CFC.log`, `CFC.nnrpow`, `CFC.rpow`, `CFC.sqrt` and `CFC.abs`.

- [ ] depends on: leanprover-community#33623
- [ ] depends on: leanprover-community#33624
- [ ] depends on: leanprover-community#33625
- [ ] depends on: leanprover-community#33626
- [ ] depends on: leanprover-community#33627

Author: j-loreaux

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Continuity.lean

@@ -314,6 +314,35 @@ theorem ContinuousOn.cfc' [TopologicalSpace X] {s : Set 𝕜} (hs : IsCompact s)
   filter_upwards [self_mem_nhdsWithin] with x hx
   exact ha x hx
 
+/-- 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 ContinuousOn.cfc_of_mem_nhdsSet [CompleteSpace A] [TopologicalSpace X] {s : Set 𝕜}
+    (f : 𝕜 → 𝕜) {a : X → A} {t : Set X} (hs : s ∈ 𝓝ˢ (⋃ 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 ↦ cfc f (a x)) t := by
+  have hs' := hs
+  simp only [nhdsSet_iUnion, mem_iSup] at hs'
+  have (x : t) : ∃ S, IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a x), spectrum 𝕜 x' ⊆ S) ∧ S ⊆ s:= by
+    obtain ⟨S, ⟨hS₁, hS₂⟩, hS₃⟩ :=
+      spectrum.isCompact (𝕜 := 𝕜) (a x) |>.nhdsSet_basis_isCompact.mem_iff.mp (hs' x x.2)
+    refine ⟨S, hS₂, ?_, hS₃⟩
+    exact upperHemicontinuous_spectrum 𝕜 A |>.upperHemicontinuousAt (a x) _ hS₁ |>.mono
+      fun _ ↦ subset_of_mem_nhdsSet
+  choose S hS₁ hS₂ hS₃ using this
+  classical
+  refine ha_cont.cfc (s := fun x : X ↦ if hx : x ∈ t then S ⟨x, hx⟩ else ∅) f
+    (by simpa +contextual using hS₁) ?_ ha' ?_
+  all_goals simp +contextual only [↓reduceDIte]
+  · exact fun x₀ hx₀ ↦ ha_cont.continuousWithinAt hx₀ |>.eventually <| hS₂ ⟨x₀, hx₀⟩
+  · exact fun x hx ↦ hf.mono <| hS₃ ⟨x, hx⟩
+
 /-- 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
@@ -336,6 +365,21 @@ theorem Continuous.cfc' [TopologicalSpace X] {s : Set 𝕜} (hs : IsCompact s) (
   rw [← continuousOn_univ] at ha_cont ⊢
   exact ha_cont.cfc' hs f (fun x _ ↦ ha x) (fun x _ ↦ ha' 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 Continuous.cfc_of_mem_nhdsSet [CompleteSpace A] [TopologicalSpace X] {s : Set 𝕜}
+    (f : 𝕜 → 𝕜) {a : X → A} (hs : s ∈ 𝓝ˢ (⋃ x, spectrum 𝕜 (a x))) (ha_cont : Continuous a)
+    (ha' : ∀ x, p (a x) := by cfc_tac) (hf : ContinuousOn f s := by cfc_cont_tac) :
+    Continuous (fun x ↦ cfc f (a x)) := by
+  rw [← continuousOn_univ] at ha_cont ⊢
+  exact ha_cont.cfc_of_mem_nhdsSet f (by simpa) (by simpa)
+
 end RCLike
 
 section NNReal
@@ -437,6 +481,36 @@ theorem ContinuousOn.cfc_nnreal' [TopologicalSpace X] {s : Set ℝ≥0} (hs : Is
   filter_upwards [self_mem_nhdsWithin] with x hx
   exact ha x hx
 
+/-- 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 ContinuousOn.cfc_nnreal_of_mem_nhdsSet [CompleteSpace A] [TopologicalSpace X] {s : Set ℝ≥0}
+    (f : ℝ≥0 → ℝ≥0) {a : X → A} {t : Set X} (hs : s ∈ 𝓝ˢ (⋃ x ∈ t, spectrum ℝ≥0 (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 ↦ cfc f (a x)) t := by
+  have hs' := hs
+  simp only [nhdsSet_iUnion, mem_iSup] at hs'
+  have (x : t) : ∃ S, IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a x), spectrum ℝ≥0 x' ⊆ S) ∧ S ⊆ s:= by
+    obtain ⟨S, ⟨hS₁, hS₂⟩, hS₃⟩ :=
+      spectrum.isCompact_nnreal (a x) |>.nhdsSet_basis_isCompact.mem_iff.mp (hs' x x.2)
+    refine ⟨S, hS₂, ?_, hS₃⟩
+    exact upperHemicontinuous_spectrum_nnreal A |>.upperHemicontinuousAt (a x) _ hS₁ |>.mono
+      fun _ ↦ subset_of_mem_nhdsSet
+  choose S hS₁ hS₂ hS₃ using this
+  classical
+  refine ha_cont.cfc_nnreal (s := fun x : X ↦ if hx : x ∈ t then S ⟨x, hx⟩ else ∅) f
+    (by simpa +contextual using hS₁) ?_ ha' ?_
+  all_goals simp +contextual only [↓reduceDIte]
+  · exact fun x₀ hx₀ ↦ ha_cont.continuousWithinAt hx₀ |>.eventually <| hS₂ ⟨x₀, hx₀⟩
+  · exact fun x hx ↦ hf.mono <| hS₃ ⟨x, hx⟩
+
 /-- 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`,
@@ -459,6 +533,22 @@ theorem Continuous.cfc_nnreal' [TopologicalSpace X] {s : Set ℝ≥0} (hs : IsCo
   rw [← continuousOn_univ] at ha_cont ⊢
   exact ha_cont.cfc_nnreal' hs f (fun x _ ↦ ha x) (fun x _ ↦ ha' 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 Continuous.cfc_nnreal_of_mem_nhdsSet [CompleteSpace A] [TopologicalSpace X] {s : Set ℝ≥0}
+    (f : ℝ≥0 → ℝ≥0) {a : X → A} (hs : s ∈ 𝓝ˢ (⋃ x, spectrum ℝ≥0 (a x))) (ha_cont : Continuous a)
+    (ha' : ∀ x, 0 ≤ a x := by cfc_tac) (hf : ContinuousOn f s := by cfc_cont_tac) :
+    Continuous (fun x ↦ cfc f (a x)) := by
+  rw [← continuousOn_univ] at ha_cont ⊢
+  exact ha_cont.cfc_nnreal_of_mem_nhdsSet f (by simpa) (by simpa)
+
 end NNReal
 
 end Right
@@ -731,6 +821,36 @@ theorem ContinuousOn.cfcₙ' [TopologicalSpace X] {s : Set 𝕜} (hs : IsCompact
   filter_upwards [self_mem_nhdsWithin] with x hx
   exact ha x hx
 
+/-- 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 ContinuousOn.cfcₙ_of_mem_nhdsSet [CompleteSpace A] [TopologicalSpace X] {s : Set 𝕜}
+    (f : 𝕜 → 𝕜) {a : X → A} {t : Set X} (hs : s ∈ 𝓝ˢ (⋃ 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 ↦ cfcₙ f (a x)) t := by
+  have hs' := hs
+  simp only [nhdsSet_iUnion, mem_iSup] at hs'
+  have (x : t) : ∃ S, IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a x), quasispectrum 𝕜 x' ⊆ S) ∧ S ⊆ s := by
+    obtain ⟨S, ⟨hS₁, hS₂⟩, hS₃⟩ :=
+      quasispectrum.isCompact (𝕜 := 𝕜) (a x) |>.nhdsSet_basis_isCompact.mem_iff.mp (hs' x x.2)
+    refine ⟨S, hS₂, ?_, hS₃⟩
+    exact upperHemicontinuous_quasispectrum 𝕜 A |>.upperHemicontinuousAt (a x) _ hS₁ |>.mono
+      fun _ ↦ subset_of_mem_nhdsSet
+  choose S hS₁ hS₂ hS₃ using this
+  classical
+  refine ha_cont.cfcₙ (s := fun x : X ↦ if hx : x ∈ t then S ⟨x, hx⟩ else ∅) f
+    (by simpa +contextual using hS₁) ?_ ha' ?_
+  all_goals simp +contextual only [↓reduceDIte]
+  · exact fun x₀ hx₀ ↦ ha_cont.continuousWithinAt hx₀ |>.eventually <| hS₂ ⟨x₀, hx₀⟩
+  · exact fun x hx ↦ hf.mono <| hS₃ ⟨x, hx⟩
+
 /-- 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
@@ -755,6 +875,23 @@ theorem Continuous.cfcₙ' [TopologicalSpace X] {s : Set 𝕜} (hs : IsCompact s
   rw [← continuousOn_univ] at ha_cont ⊢
   exact ha_cont.cfcₙ' hs f (fun x _ ↦ ha x) (fun x _ ↦ ha' 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 Continuous.cfcₙ_of_mem_nhdsSet [CompleteSpace A] [TopologicalSpace X] {s : Set 𝕜}
+    (f : 𝕜 → 𝕜) {a : X → A} (hs : s ∈ 𝓝ˢ (⋃ x, quasispectrum 𝕜 (a x))) (ha_cont : Continuous a)
+    (ha' : ∀ 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 ↦ cfcₙ f (a x)) := by
+  rw [← continuousOn_univ] at ha_cont ⊢
+  exact ha_cont.cfcₙ_of_mem_nhdsSet f (by simpa) (by simpa)
+
 end RCLike
 
 section NNReal
@@ -859,6 +996,36 @@ theorem ContinuousOn.cfcₙ_nnreal' [TopologicalSpace X] {s : Set ℝ≥0} (hs :
   filter_upwards [self_mem_nhdsWithin] with x hx
   exact ha x hx
 
+/-- 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 ContinuousOn.cfcₙ_nnreal_of_mem_nhdsSet [CompleteSpace A] [TopologicalSpace X] {s : Set ℝ≥0}
+    (f : ℝ≥0 → ℝ≥0) {a : X → A} {t : Set X} (hs : s ∈ 𝓝ˢ (⋃ x ∈ t, quasispectrum ℝ≥0 (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 ↦ cfcₙ f (a x)) t := by
+  have hs' := hs
+  simp only [nhdsSet_iUnion, mem_iSup] at hs'
+  have (x : t) : ∃ S, IsCompact S ∧ (∀ᶠ (x' : A) in 𝓝 (a x), quasispectrum ℝ≥0 x' ⊆ S) ∧ S ⊆ s:= by
+    obtain ⟨S, ⟨hS₁, hS₂⟩, hS₃⟩ :=
+      quasispectrum.isCompact_nnreal (a x) |>.nhdsSet_basis_isCompact.mem_iff.mp (hs' x x.2)
+    refine ⟨S, hS₂, ?_, hS₃⟩
+    exact upperHemicontinuous_quasispectrum_nnreal A |>.upperHemicontinuousAt (a x) _ hS₁ |>.mono
+      fun _ ↦ subset_of_mem_nhdsSet
+  choose S hS₁ hS₂ hS₃ using this
+  classical
+  refine ha_cont.cfcₙ_nnreal (s := fun x : X ↦ if hx : x ∈ t then S ⟨x, hx⟩ else ∅) f
+    (by simpa +contextual using hS₁) ?_ ha' ?_
+  all_goals simp +contextual only [↓reduceDIte]
+  · exact fun x₀ hx₀ ↦ ha_cont.continuousWithinAt hx₀ |>.eventually <| hS₂ ⟨x₀, hx₀⟩
+  · exact fun x hx ↦ hf.mono <| hS₃ ⟨x, hx⟩
+
 /-- 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`
@@ -883,6 +1050,23 @@ theorem Continuous.cfcₙ_nnreal' [TopologicalSpace X] {s : Set ℝ≥0} (hs : I
   rw [← continuousOn_univ] at ha_cont ⊢
   exact ha_cont.cfcₙ_nnreal' hs f (fun x _ ↦ ha x) (fun x _ ↦ ha' 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. -/
+theorem Continuous.cfcₙ_nnreal_of_mem_nhdsSet [CompleteSpace A] [TopologicalSpace X] {s : Set ℝ≥0}
+    (f : ℝ≥0 → ℝ≥0) {a : X → A} (hs : s ∈ 𝓝ˢ (⋃ x, quasispectrum ℝ≥0 (a x)))
+    (ha_cont : Continuous a) (ha' : ∀ 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 ↦ cfcₙ f (a x)) := by
+  rw [← continuousOn_univ] at ha_cont ⊢
+  exact ha_cont.cfcₙ_nnreal_of_mem_nhdsSet f (by simpa) (by simpa)
+
 end NNReal
 
 end Right