Isometric continuous functional calculus

This file adds a class for an isometric continuous functional calculus. This is separate from the usual ContinuousFunctionalCalculus class because we prefer not to require a metric (or a norm) on the algebra for reasons discussed in the module documentation for that file.

Of course, with a metric on the algebra and an isometric continuous functional calculus, the algebra must be a C⋆-algebra already. As such, it may seem like this class is not useful. However, the main purpose is to allow for the continuous functional calculus to be an isometry for the other scalar rings ℝ and ℝ≥0 too.

Isometric continuous functional calculus for unital algebras

class IsometricContinuousFunctionalCalculus (R : Type u_1) (A : Type u_2) (p : outParam (A → Prop)) [CommSemiring R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [MetricSpace A] [Algebra R A] extends ContinuousFunctionalCalculus R A p : Prop

An extension of the ContinuousFunctionalCalculus requiring that cfcHom is an isometry.

• predicate_zero : p 0
• compactSpace_spectrum (a : A) : CompactSpace ↑(spectrum R a)
• spectrum_nonempty [Nontrivial A] (a : A) (ha : p a) : (spectrum R a).Nonempty
• exists_cfc_of_predicate (a : A) : p a → ∃ (φ : C(↑(spectrum R a), R) →⋆ₐ[R] A), Continuous ⇑φ ∧ Function.Injective ⇑φ ∧ φ (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a ∧ (∀ (f : C(↑(spectrum R a), R)), spectrum R (φ f) = Set.range ⇑f) ∧ ∀ (f : C(↑(spectrum R a), R)), p (φ f)
• isometric (a : A) (ha : p a) : Isometry ⇑(cfcHom ha)

theorem isometry_cfcHom {R : Type u_1} {A : Type u_2} {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) (ha : p a := by cfc_tac) : Isometry ⇑(cfcHom ⋯)

instance instClosedEmbeddingContinuousFunctionalCalculusOfCompleteSpace {R : Type u_1} {A : Type u_2} {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] [CompleteSpace R] : ClosedEmbeddingContinuousFunctionalCalculus R A p

theorem norm_cfcHom {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] (a : A) (f : C(↑(spectrum 𝕜 a), 𝕜)) (ha : p a := by cfc_tac) : ‖(cfcHom ⋯) f‖ = ‖f‖

theorem nnNorm_cfcHom {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] (a : A) (f : C(↑(spectrum 𝕜 a), 𝕜)) (ha : p a := by cfc_tac) : ‖(cfcHom ⋯) f‖₊ = ‖f‖₊

@[deprecated nnNorm_cfcHom (since := "2026-10-31")]

theorem nnnorm_cfcHom {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] (a : A) (f : C(↑(spectrum 𝕜 a), 𝕜)) (ha : p a := by cfc_tac) : ‖(cfcHom ⋯) f‖₊ = ‖f‖₊

Alias of nnNorm_cfcHom.

theorem IsGreatest.norm_cfc {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] [Nontrivial A] (f : 𝕜 → 𝕜) (a : A) (hf : ContinuousOn f (spectrum 𝕜 a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : IsGreatest ((fun (x : 𝕜) => ‖f x‖) '' spectrum 𝕜 a) ‖cfc f a‖

theorem IsGreatest.nnNorm_cfc {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] [Nontrivial A] (f : 𝕜 → 𝕜) (a : A) (hf : ContinuousOn f (spectrum 𝕜 a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : IsGreatest ((fun (x : 𝕜) => ‖f x‖₊) '' spectrum 𝕜 a) ‖cfc f a‖₊

@[deprecated IsGreatest.nnNorm_cfc (since := "2026-10-31")]

theorem IsGreatest.nnnorm_cfc {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] [Nontrivial A] (f : 𝕜 → 𝕜) (a : A) (hf : ContinuousOn f (spectrum 𝕜 a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : IsGreatest ((fun (x : 𝕜) => ‖f x‖₊) '' spectrum 𝕜 a) ‖cfc f a‖₊

Alias of IsGreatest.nnNorm_cfc.

theorem norm_apply_le_norm_cfc {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) ⦃x : 𝕜⦄ (hx : x ∈ spectrum 𝕜 a) (hf : ContinuousOn f (spectrum 𝕜 a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : ‖f x‖ ≤ ‖cfc f a‖

theorem nnNorm_apply_le_nnNorm_cfc {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) ⦃x : 𝕜⦄ (hx : x ∈ spectrum 𝕜 a) (hf : ContinuousOn f (spectrum 𝕜 a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : ‖f x‖₊ ≤ ‖cfc f a‖₊

@[deprecated nnNorm_apply_le_nnNorm_cfc (since := "2026-10-31")]

theorem nnnorm_apply_le_nnnorm_cfc {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) ⦃x : 𝕜⦄ (hx : x ∈ spectrum 𝕜 a) (hf : ContinuousOn f (spectrum 𝕜 a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : ‖f x‖₊ ≤ ‖cfc f a‖₊

Alias of nnNorm_apply_le_nnNorm_cfc.

theorem norm_cfc_le {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] {f : 𝕜 → 𝕜} {a : A} {c : ℝ} (hc : 0 ≤ c) (h : ∀ x ∈ spectrum 𝕜 a, ‖f x‖ ≤ c) : ‖cfc f a‖ ≤ c

theorem norm_cfc_le_iff {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) {c : ℝ} (hc : 0 ≤ c) (hf : ContinuousOn f (spectrum 𝕜 a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : ‖cfc f a‖ ≤ c ↔ ∀ x ∈ spectrum 𝕜 a, ‖f x‖ ≤ c

theorem norm_cfc_lt {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] {f : 𝕜 → 𝕜} {a : A} {c : ℝ} (hc : 0 < c) (h : ∀ x ∈ spectrum 𝕜 a, ‖f x‖ < c) : ‖cfc f a‖ < c

theorem norm_cfc_lt_iff {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) {c : ℝ} (hc : 0 < c) (hf : ContinuousOn f (spectrum 𝕜 a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : ‖cfc f a‖ < c ↔ ∀ x ∈ spectrum 𝕜 a, ‖f x‖ < c

theorem nnNorm_cfc_le {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] {f : 𝕜 → 𝕜} {a : A} (c : NNReal) (h : ∀ x ∈ spectrum 𝕜 a, ‖f x‖₊ ≤ c) : ‖cfc f a‖₊ ≤ c

@[deprecated nnNorm_cfc_le (since := "2026-10-31")]

theorem nnnorm_cfc_le {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] {f : 𝕜 → 𝕜} {a : A} (c : NNReal) (h : ∀ x ∈ spectrum 𝕜 a, ‖f x‖₊ ≤ c) : ‖cfc f a‖₊ ≤ c

Alias of nnNorm_cfc_le.

theorem nnNorm_cfc_le_iff {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) (c : NNReal) (hf : ContinuousOn f (spectrum 𝕜 a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : ‖cfc f a‖₊ ≤ c ↔ ∀ x ∈ spectrum 𝕜 a, ‖f x‖₊ ≤ c

@[deprecated nnNorm_cfc_le_iff (since := "2026-10-31")]

theorem nnnorm_cfc_le_iff {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) (c : NNReal) (hf : ContinuousOn f (spectrum 𝕜 a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : ‖cfc f a‖₊ ≤ c ↔ ∀ x ∈ spectrum 𝕜 a, ‖f x‖₊ ≤ c

Alias of nnNorm_cfc_le_iff.

theorem nnNorm_cfc_lt {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] {f : 𝕜 → 𝕜} {a : A} {c : NNReal} (hc : 0 < c) (h : ∀ x ∈ spectrum 𝕜 a, ‖f x‖₊ < c) : ‖cfc f a‖₊ < c

@[deprecated nnNorm_cfc_lt (since := "2026-10-31")]

theorem nnnorm_cfc_lt {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] {f : 𝕜 → 𝕜} {a : A} {c : NNReal} (hc : 0 < c) (h : ∀ x ∈ spectrum 𝕜 a, ‖f x‖₊ < c) : ‖cfc f a‖₊ < c

Alias of nnNorm_cfc_lt.

theorem nnNorm_cfc_lt_iff {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) {c : NNReal} (hc : 0 < c) (hf : ContinuousOn f (spectrum 𝕜 a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : ‖cfc f a‖₊ < c ↔ ∀ x ∈ spectrum 𝕜 a, ‖f x‖₊ < c

@[deprecated nnNorm_cfc_lt_iff (since := "2026-10-31")]

theorem nnnorm_cfc_lt_iff {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) {c : NNReal} (hc : 0 < c) (hf : ContinuousOn f (spectrum 𝕜 a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : ‖cfc f a‖₊ < c ↔ ∀ x ∈ spectrum 𝕜 a, ‖f x‖₊ < c

Alias of nnNorm_cfc_lt_iff.

theorem IsometricContinuousFunctionalCalculus.isGreatest_norm_spectrum {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] [Nontrivial A] (a : A) (ha : p a := by cfc_tac) : IsGreatest ((fun (x : 𝕜) => ‖x‖) '' spectrum 𝕜 a) ‖a‖

theorem IsometricContinuousFunctionalCalculus.norm_spectrum_le {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] (a : A) ⦃x : 𝕜⦄ (hx : x ∈ spectrum 𝕜 a) (ha : p a := by cfc_tac) : ‖x‖ ≤ ‖a‖

theorem IsometricContinuousFunctionalCalculus.isGreatest_nnNorm_spectrum {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] [Nontrivial A] (a : A) (ha : p a := by cfc_tac) : IsGreatest ((fun (x : 𝕜) => ‖x‖₊) '' spectrum 𝕜 a) ‖a‖₊

@[deprecated IsometricContinuousFunctionalCalculus.isGreatest_nnNorm_spectrum (since := "2026-10-31")]

theorem IsometricContinuousFunctionalCalculus.isGreatest_nnnorm_spectrum {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] [Nontrivial A] (a : A) (ha : p a := by cfc_tac) : IsGreatest ((fun (x : 𝕜) => ‖x‖₊) '' spectrum 𝕜 a) ‖a‖₊

Alias of IsometricContinuousFunctionalCalculus.isGreatest_nnNorm_spectrum.

theorem IsometricContinuousFunctionalCalculus.nnNorm_spectrum_le {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] (a : A) ⦃x : 𝕜⦄ (hx : x ∈ spectrum 𝕜 a) (ha : p a := by cfc_tac) : ‖x‖₊ ≤ ‖a‖₊

@[deprecated IsometricContinuousFunctionalCalculus.nnNorm_spectrum_le (since := "2026-10-31")]

theorem IsometricContinuousFunctionalCalculus.nnnorm_spectrum_le {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] (a : A) ⦃x : 𝕜⦄ (hx : x ∈ spectrum 𝕜 a) (ha : p a := by cfc_tac) : ‖x‖₊ ≤ ‖a‖₊

Alias of IsometricContinuousFunctionalCalculus.nnNorm_spectrum_le.

theorem CFC.norm_pow (𝕜 : Type u_1) {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] (a : A) (n : ℕ) (hn : n ≠ 0) (ha : p a := by cfc_tac) : ‖a ^ n‖ = ‖a‖ ^ n

theorem SpectrumRestricts.isometric_cfc {R : Type u_1} {S : Type u_2} {A : Type u_3} {p q : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [Semifield S] [StarRing S] [MetricSpace S] [IsTopologicalSemiring S] [ContinuousStar S] [Ring A] [StarRing A] [Algebra S A] [Algebra R S] [Algebra R A] [IsScalarTower R S A] [StarModule R S] [ContinuousSMul R S] [MetricSpace A] [IsometricContinuousFunctionalCalculus S A q] [CompleteSpace R] [ContinuousMap.UniqueHom R A] (f : C(S, R)) (halg : Isometry ⇑(algebraMap R S)) (h0 : p 0) (h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f) : IsometricContinuousFunctionalCalculus R A p

Isometric continuous functional calculus for non-unital algebras

class NonUnitalIsometricContinuousFunctionalCalculus (R : Type u_1) (A : Type u_2) (p : outParam (A → Prop)) [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [MetricSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] extends NonUnitalContinuousFunctionalCalculus R A p : Prop

An extension of the NonUnitalContinuousFunctionalCalculus requiring that cfcₙHom is an isometry.

• predicate_zero : p 0
• compactSpace_quasispectrum (a : A) : CompactSpace ↑(quasispectrum R a)
• exists_cfc_of_predicate (a : A) : p a → ∃ (φ : ContinuousMapZero (↑(quasispectrum R a)) R →⋆ₙₐ[R] A), Continuous ⇑φ ∧ Function.Injective ⇑φ ∧ φ { toContinuousMap := ContinuousMap.restrict (quasispectrum R a) (ContinuousMap.id R), map_zero' := ⋯ } = a ∧ (∀ (f : ContinuousMapZero (↑(quasispectrum R a)) R), quasispectrum R (φ f) = Set.range ⇑f) ∧ ∀ (f : ContinuousMapZero (↑(quasispectrum R a)) R), p (φ f)
• isometric (a : A) (ha : p a) : Isometry ⇑(cfcₙHom ha)

theorem isometry_cfcₙHom {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [MetricSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalIsometricContinuousFunctionalCalculus R A p] (a : A) (ha : p a := by cfc_tac) : Isometry ⇑(cfcₙHom ⋯)

instance instNonUnitalClosedEmbeddingContinuousFunctionalCalculusOfCompleteSpace {R : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [CommSemiring R] [Nontrivial R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [MetricSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [NonUnitalIsometricContinuousFunctionalCalculus R A p] [CompleteSpace R] : NonUnitalClosedEmbeddingContinuousFunctionalCalculus R A p

theorem norm_cfcₙHom {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (a : A) (f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜) (ha : p a := by cfc_tac) : ‖(cfcₙHom ⋯) f‖ = ‖f‖

theorem nnNorm_cfcₙHom {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (a : A) (f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜) (ha : p a := by cfc_tac) : ‖(cfcₙHom ⋯) f‖₊ = ‖f‖₊

@[deprecated nnNorm_cfcₙHom (since := "2026-10-31")]

theorem nnnorm_cfcₙHom {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (a : A) (f : ContinuousMapZero (↑(quasispectrum 𝕜 a)) 𝕜) (ha : p a := by cfc_tac) : ‖(cfcₙHom ⋯) f‖₊ = ‖f‖₊

Alias of nnNorm_cfcₙHom.

theorem IsGreatest.norm_cfcₙ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) (hf : ContinuousOn f (quasispectrum 𝕜 a) := by cfc_cont_tac) (hf₀ : f 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) : IsGreatest ((fun (x : 𝕜) => ‖f x‖) '' quasispectrum 𝕜 a) ‖cfcₙ f a‖

theorem IsGreatest.nnNorm_cfcₙ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) (hf : ContinuousOn f (quasispectrum 𝕜 a) := by cfc_cont_tac) (hf₀ : f 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) : IsGreatest ((fun (x : 𝕜) => ‖f x‖₊) '' quasispectrum 𝕜 a) ‖cfcₙ f a‖₊

@[deprecated IsGreatest.nnNorm_cfcₙ (since := "2026-10-31")]

theorem IsGreatest.nnnorm_cfcₙ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) (hf : ContinuousOn f (quasispectrum 𝕜 a) := by cfc_cont_tac) (hf₀ : f 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) : IsGreatest ((fun (x : 𝕜) => ‖f x‖₊) '' quasispectrum 𝕜 a) ‖cfcₙ f a‖₊

Alias of IsGreatest.nnNorm_cfcₙ.

theorem norm_apply_le_norm_cfcₙ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) ⦃x : 𝕜⦄ (hx : x ∈ quasispectrum 𝕜 a) (hf : ContinuousOn f (quasispectrum 𝕜 a) := by cfc_cont_tac) (hf₀ : f 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) : ‖f x‖ ≤ ‖cfcₙ f a‖

theorem nnNorm_apply_le_nnNorm_cfcₙ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) ⦃x : 𝕜⦄ (hx : x ∈ quasispectrum 𝕜 a) (hf : ContinuousOn f (quasispectrum 𝕜 a) := by cfc_cont_tac) (hf₀ : f 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) : ‖f x‖₊ ≤ ‖cfcₙ f a‖₊

@[deprecated nnNorm_apply_le_nnNorm_cfcₙ (since := "2026-10-31")]

theorem nnnorm_apply_le_nnnorm_cfcₙ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) ⦃x : 𝕜⦄ (hx : x ∈ quasispectrum 𝕜 a) (hf : ContinuousOn f (quasispectrum 𝕜 a) := by cfc_cont_tac) (hf₀ : f 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) : ‖f x‖₊ ≤ ‖cfcₙ f a‖₊

Alias of nnNorm_apply_le_nnNorm_cfcₙ.

theorem norm_cfcₙ_le {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] {f : 𝕜 → 𝕜} {a : A} {c : ℝ} (h : ∀ x ∈ quasispectrum 𝕜 a, ‖f x‖ ≤ c) : ‖cfcₙ f a‖ ≤ c

theorem norm_cfcₙ_le_iff {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) (c : ℝ) (hf : ContinuousOn f (quasispectrum 𝕜 a) := by cfc_cont_tac) (hf₀ : f 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) : ‖cfcₙ f a‖ ≤ c ↔ ∀ x ∈ quasispectrum 𝕜 a, ‖f x‖ ≤ c

theorem norm_cfcₙ_lt {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] {f : 𝕜 → 𝕜} {a : A} {c : ℝ} (h : ∀ x ∈ quasispectrum 𝕜 a, ‖f x‖ < c) : ‖cfcₙ f a‖ < c

theorem norm_cfcₙ_lt_iff {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) (c : ℝ) (hf : ContinuousOn f (quasispectrum 𝕜 a) := by cfc_cont_tac) (hf₀ : f 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) : ‖cfcₙ f a‖ < c ↔ ∀ x ∈ quasispectrum 𝕜 a, ‖f x‖ < c

theorem nnNorm_cfcₙ_le {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] {f : 𝕜 → 𝕜} {a : A} {c : NNReal} (h : ∀ x ∈ quasispectrum 𝕜 a, ‖f x‖₊ ≤ c) : ‖cfcₙ f a‖₊ ≤ c

@[deprecated nnNorm_cfcₙ_le (since := "2026-10-31")]

theorem nnnorm_cfcₙ_le {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] {f : 𝕜 → 𝕜} {a : A} {c : NNReal} (h : ∀ x ∈ quasispectrum 𝕜 a, ‖f x‖₊ ≤ c) : ‖cfcₙ f a‖₊ ≤ c

Alias of nnNorm_cfcₙ_le.

theorem nnNorm_cfcₙ_le_iff {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) (c : NNReal) (hf : ContinuousOn f (quasispectrum 𝕜 a) := by cfc_cont_tac) (hf₀ : f 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) : ‖cfcₙ f a‖₊ ≤ c ↔ ∀ x ∈ quasispectrum 𝕜 a, ‖f x‖₊ ≤ c

@[deprecated nnNorm_cfcₙ_le_iff (since := "2026-10-31")]

theorem nnnorm_cfcₙ_le_iff {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) (c : NNReal) (hf : ContinuousOn f (quasispectrum 𝕜 a) := by cfc_cont_tac) (hf₀ : f 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) : ‖cfcₙ f a‖₊ ≤ c ↔ ∀ x ∈ quasispectrum 𝕜 a, ‖f x‖₊ ≤ c

Alias of nnNorm_cfcₙ_le_iff.

theorem nnNorm_cfcₙ_lt {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] {f : 𝕜 → 𝕜} {a : A} {c : NNReal} (h : ∀ x ∈ quasispectrum 𝕜 a, ‖f x‖₊ < c) : ‖cfcₙ f a‖₊ < c

@[deprecated nnNorm_cfcₙ_lt (since := "2026-10-31")]

theorem nnnorm_cfcₙ_lt {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] {f : 𝕜 → 𝕜} {a : A} {c : NNReal} (h : ∀ x ∈ quasispectrum 𝕜 a, ‖f x‖₊ < c) : ‖cfcₙ f a‖₊ < c

Alias of nnNorm_cfcₙ_lt.

theorem nnNorm_cfcₙ_lt_iff {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) (c : NNReal) (hf : ContinuousOn f (quasispectrum 𝕜 a) := by cfc_cont_tac) (hf₀ : f 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) : ‖cfcₙ f a‖₊ < c ↔ ∀ x ∈ quasispectrum 𝕜 a, ‖f x‖₊ < c

@[deprecated nnNorm_cfcₙ_lt_iff (since := "2026-10-31")]

theorem nnnorm_cfcₙ_lt_iff {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) (c : NNReal) (hf : ContinuousOn f (quasispectrum 𝕜 a) := by cfc_cont_tac) (hf₀ : f 0 = 0 := by cfc_zero_tac) (ha : p a := by cfc_tac) : ‖cfcₙ f a‖₊ < c ↔ ∀ x ∈ quasispectrum 𝕜 a, ‖f x‖₊ < c

Alias of nnNorm_cfcₙ_lt_iff.

theorem NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_norm_quasispectrum {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (a : A) (ha : p a := by cfc_tac) : IsGreatest ((fun (x : 𝕜) => ‖x‖) '' quasispectrum 𝕜 a) ‖a‖

theorem NonUnitalIsometricContinuousFunctionalCalculus.norm_quasispectrum_le {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (a : A) ⦃x : 𝕜⦄ (hx : x ∈ quasispectrum 𝕜 a) (ha : p a := by cfc_tac) : ‖x‖ ≤ ‖a‖

theorem NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_nnNorm_quasispectrum {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (a : A) (ha : p a := by cfc_tac) : IsGreatest ((fun (x : 𝕜) => ‖x‖₊) '' quasispectrum 𝕜 a) ‖a‖₊

@[deprecated NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_nnNorm_quasispectrum (since := "2026-10-31")]

theorem NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_nnnorm_quasispectrum {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (a : A) (ha : p a := by cfc_tac) : IsGreatest ((fun (x : 𝕜) => ‖x‖₊) '' quasispectrum 𝕜 a) ‖a‖₊

Alias of NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_nnNorm_quasispectrum.

theorem NonUnitalIsometricContinuousFunctionalCalculus.nnNorm_quasispectrum_le {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (a : A) ⦃x : 𝕜⦄ (hx : x ∈ quasispectrum 𝕜 a) (ha : p a := by cfc_tac) : ‖x‖₊ ≤ ‖a‖₊

@[deprecated NonUnitalIsometricContinuousFunctionalCalculus.nnNorm_quasispectrum_le (since := "2026-10-31")]

theorem NonUnitalIsometricContinuousFunctionalCalculus.nnnorm_quasispectrum_le {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (a : A) ⦃x : 𝕜⦄ (hx : x ∈ quasispectrum 𝕜 a) (ha : p a := by cfc_tac) : ‖x‖₊ ≤ ‖a‖₊

Alias of NonUnitalIsometricContinuousFunctionalCalculus.nnNorm_quasispectrum_le.

theorem norm_cfcₙ_pow (𝕜 : Type u_1) {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (a : A) (n : ℕ) (hn : n ≠ 0) (ha : p a := by cfc_tac) : ‖cfcₙ (fun (x : 𝕜) => x ^ n) a‖ = ‖a‖ ^ n

theorem CFC.norm_mul_self (𝕜 : Type u_1) {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NonUnitalNormedRing A] [StarRing A] [NormedSpace 𝕜 A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p] (a : A) (ha : p a := by cfc_tac) : ‖a * a‖ = ‖a‖ ^ 2

theorem QuasispectrumRestricts.isometric_cfc {R : Type u_1} {S : Type u_2} {A : Type u_3} {p q : A → Prop} [Semifield R] [StarRing R] [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [Field S] [StarRing S] [MetricSpace S] [IsTopologicalRing S] [ContinuousStar S] [NonUnitalRing A] [StarRing A] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [Algebra R S] [Module R A] [IsScalarTower R S A] [StarModule R S] [ContinuousSMul R S] [IsScalarTower R A A] [SMulCommClass R A A] [MetricSpace A] [NonUnitalIsometricContinuousFunctionalCalculus S A q] [CompleteSpace R] [ContinuousMapZero.UniqueHom R A] (f : C(S, R)) (halg : Isometry ⇑(algebraMap R S)) (h0 : p 0) (h : ∀ (a : A), p a ↔ q a ∧ QuasispectrumRestricts a ⇑f) : NonUnitalIsometricContinuousFunctionalCalculus R A p

Instances of isometric continuous functional calculi

The instances for ℝ and ℂ can be found in Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean, as those require an actual CStarAlgebra instance on A, whereas the one for ℝ≥0 is simply inherited from an existing instance for ℝ.

instance Nonneg.instIsometricContinuousFunctionalCalculus {A : Type u_1} [NormedRing A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [NormedAlgebra ℝ A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] : IsometricContinuousFunctionalCalculus NNReal A fun (x : A) => 0 ≤ x

instance Nonneg.instNonUnitalIsometricContinuousFunctionalCalculus {A : Type u_1} [NonUnitalNormedRing A] [PartialOrder A] [StarRing A] [StarOrderedRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] : NonUnitalIsometricContinuousFunctionalCalculus NNReal A fun (x : A) => 0 ≤ x

Properties specific to ℝ≥0

theorem IsGreatest.nnNorm_cfc_nnreal {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [PartialOrder A] [StarOrderedRing A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [Nontrivial A] (f : NNReal → NNReal) (a : A) (hf : ContinuousOn f (spectrum NNReal a) := by cfc_cont_tac) (ha : 0 ≤ a := by cfc_tac) : IsGreatest (f '' spectrum NNReal a) ‖cfc f a‖₊

@[deprecated IsGreatest.nnNorm_cfc_nnreal (since := "2026-10-31")]

theorem IsGreatest.nnnorm_cfc_nnreal {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [PartialOrder A] [StarOrderedRing A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [Nontrivial A] (f : NNReal → NNReal) (a : A) (hf : ContinuousOn f (spectrum NNReal a) := by cfc_cont_tac) (ha : 0 ≤ a := by cfc_tac) : IsGreatest (f '' spectrum NNReal a) ‖cfc f a‖₊

Alias of IsGreatest.nnNorm_cfc_nnreal.

theorem apply_le_nnNorm_cfc_nnreal {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [PartialOrder A] [StarOrderedRing A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (a : A) ⦃x : NNReal⦄ (hx : x ∈ spectrum NNReal a) (hf : ContinuousOn f (spectrum NNReal a) := by cfc_cont_tac) (ha : 0 ≤ a := by cfc_tac) : f x ≤ ‖cfc f a‖₊

@[deprecated apply_le_nnNorm_cfc_nnreal (since := "2026-10-31")]

theorem apply_le_nnnorm_cfc_nnreal {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [PartialOrder A] [StarOrderedRing A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (a : A) ⦃x : NNReal⦄ (hx : x ∈ spectrum NNReal a) (hf : ContinuousOn f (spectrum NNReal a) := by cfc_cont_tac) (ha : 0 ≤ a := by cfc_tac) : f x ≤ ‖cfc f a‖₊

Alias of apply_le_nnNorm_cfc_nnreal.

theorem nnNorm_cfc_nnreal_le {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [PartialOrder A] [StarOrderedRing A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {f : NNReal → NNReal} {a : A} {c : NNReal} (h : ∀ x ∈ spectrum NNReal a, f x ≤ c) : ‖cfc f a‖₊ ≤ c

@[deprecated nnNorm_cfc_nnreal_le (since := "2026-10-31")]

theorem nnnorm_cfc_nnreal_le {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [PartialOrder A] [StarOrderedRing A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {f : NNReal → NNReal} {a : A} {c : NNReal} (h : ∀ x ∈ spectrum NNReal a, f x ≤ c) : ‖cfc f a‖₊ ≤ c

Alias of nnNorm_cfc_nnreal_le.

theorem nnNorm_cfc_nnreal_le_iff {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [PartialOrder A] [StarOrderedRing A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (a : A) (c : NNReal) (hf : ContinuousOn f (spectrum NNReal a) := by cfc_cont_tac) (ha : 0 ≤ a := by cfc_tac) : ‖cfc f a‖₊ ≤ c ↔ ∀ x ∈ spectrum NNReal a, f x ≤ c

@[deprecated nnNorm_cfc_nnreal_le_iff (since := "2026-10-31")]

theorem nnnorm_cfc_nnreal_le_iff {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [PartialOrder A] [StarOrderedRing A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (a : A) (c : NNReal) (hf : ContinuousOn f (spectrum NNReal a) := by cfc_cont_tac) (ha : 0 ≤ a := by cfc_tac) : ‖cfc f a‖₊ ≤ c ↔ ∀ x ∈ spectrum NNReal a, f x ≤ c

Alias of nnNorm_cfc_nnreal_le_iff.

theorem nnNorm_cfc_nnreal_lt {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [PartialOrder A] [StarOrderedRing A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {f : NNReal → NNReal} {a : A} {c : NNReal} (hc : 0 < c) (h : ∀ x ∈ spectrum NNReal a, f x < c) : ‖cfc f a‖₊ < c

@[deprecated nnNorm_cfc_nnreal_lt (since := "2026-10-31")]

theorem nnnorm_cfc_nnreal_lt {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [PartialOrder A] [StarOrderedRing A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {f : NNReal → NNReal} {a : A} {c : NNReal} (hc : 0 < c) (h : ∀ x ∈ spectrum NNReal a, f x < c) : ‖cfc f a‖₊ < c

Alias of nnNorm_cfc_nnreal_lt.

theorem nnNorm_cfc_nnreal_lt_iff {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [PartialOrder A] [StarOrderedRing A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (a : A) {c : NNReal} (hc : 0 < c) (hf : ContinuousOn f (spectrum NNReal a) := by cfc_cont_tac) (ha : 0 ≤ a := by cfc_tac) : ‖cfc f a‖₊ < c ↔ ∀ x ∈ spectrum NNReal a, f x < c

@[deprecated nnNorm_cfc_nnreal_lt_iff (since := "2026-10-31")]

theorem nnnorm_cfc_nnreal_lt_iff {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [PartialOrder A] [StarOrderedRing A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (a : A) {c : NNReal} (hc : 0 < c) (hf : ContinuousOn f (spectrum NNReal a) := by cfc_cont_tac) (ha : 0 ≤ a := by cfc_tac) : ‖cfc f a‖₊ < c ↔ ∀ x ∈ spectrum NNReal a, f x < c

Alias of nnNorm_cfc_nnreal_lt_iff.

theorem IsometricContinuousFunctionalCalculus.isGreatest_spectrum {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [PartialOrder A] [StarOrderedRing A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [Nontrivial A] (a : A) (ha : 0 ≤ a := by cfc_tac) : IsGreatest (spectrum NNReal a) ‖a‖₊

theorem IsometricContinuousFunctionalCalculus.spectrum_le {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [PartialOrder A] [StarOrderedRing A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : A) ⦃x : NNReal⦄ (hx : x ∈ spectrum NNReal a) (ha : 0 ≤ a := by cfc_tac) : x ≤ ‖a‖₊

theorem MonotoneOn.nnNorm_cfc {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [PartialOrder A] [StarOrderedRing A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [Nontrivial A] (f : NNReal → NNReal) (a : A) (hf : MonotoneOn f (spectrum NNReal a)) (hf₂ : ContinuousOn f (spectrum NNReal a) := by cfc_cont_tac) (ha : 0 ≤ a := by cfc_tac) : ‖cfc f a‖₊ = f ‖a‖₊

@[deprecated MonotoneOn.nnNorm_cfc (since := "2026-10-31")]

theorem MonotoneOn.nnnorm_cfc {A : Type u_1} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A] [PartialOrder A] [StarOrderedRing A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [Nontrivial A] (f : NNReal → NNReal) (a : A) (hf : MonotoneOn f (spectrum NNReal a)) (hf₂ : ContinuousOn f (spectrum NNReal a) := by cfc_cont_tac) (ha : 0 ≤ a := by cfc_tac) : ‖cfc f a‖₊ = f ‖a‖₊

Alias of MonotoneOn.nnNorm_cfc.

theorem IsGreatest.nnNorm_cfcₙ_nnreal {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (a : A) (hf : ContinuousOn f (quasispectrum NNReal a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (ha : 0 ≤ a := by cfc_tac) : IsGreatest (f '' quasispectrum NNReal a) ‖cfcₙ f a‖₊

@[deprecated IsGreatest.nnNorm_cfcₙ_nnreal (since := "2026-10-31")]

theorem IsGreatest.nnnorm_cfcₙ_nnreal {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (a : A) (hf : ContinuousOn f (quasispectrum NNReal a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (ha : 0 ≤ a := by cfc_tac) : IsGreatest (f '' quasispectrum NNReal a) ‖cfcₙ f a‖₊

Alias of IsGreatest.nnNorm_cfcₙ_nnreal.

theorem apply_le_nnNorm_cfcₙ_nnreal {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (a : A) ⦃x : NNReal⦄ (hx : x ∈ quasispectrum NNReal a) (hf : ContinuousOn f (quasispectrum NNReal a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (ha : 0 ≤ a := by cfc_tac) : f x ≤ ‖cfcₙ f a‖₊

@[deprecated apply_le_nnNorm_cfcₙ_nnreal (since := "2026-10-31")]

theorem apply_le_nnnorm_cfcₙ_nnreal {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (a : A) ⦃x : NNReal⦄ (hx : x ∈ quasispectrum NNReal a) (hf : ContinuousOn f (quasispectrum NNReal a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (ha : 0 ≤ a := by cfc_tac) : f x ≤ ‖cfcₙ f a‖₊

Alias of apply_le_nnNorm_cfcₙ_nnreal.

theorem nnNorm_cfcₙ_nnreal_le {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {f : NNReal → NNReal} {a : A} {c : NNReal} (h : ∀ x ∈ quasispectrum NNReal a, f x ≤ c) : ‖cfcₙ f a‖₊ ≤ c

@[deprecated nnNorm_cfcₙ_nnreal_le (since := "2026-10-31")]

theorem nnnorm_cfcₙ_nnreal_le {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {f : NNReal → NNReal} {a : A} {c : NNReal} (h : ∀ x ∈ quasispectrum NNReal a, f x ≤ c) : ‖cfcₙ f a‖₊ ≤ c

Alias of nnNorm_cfcₙ_nnreal_le.

theorem nnNorm_cfcₙ_nnreal_le_iff {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (a : A) (c : NNReal) (hf : ContinuousOn f (quasispectrum NNReal a) := by cfc_cont_tac) (hf₀ : f 0 = 0 := by cfc_zero_tac) (ha : 0 ≤ a := by cfc_tac) : ‖cfcₙ f a‖₊ ≤ c ↔ ∀ x ∈ quasispectrum NNReal a, f x ≤ c

@[deprecated nnNorm_cfcₙ_nnreal_le_iff (since := "2026-10-31")]

theorem nnnorm_cfcₙ_nnreal_le_iff {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (a : A) (c : NNReal) (hf : ContinuousOn f (quasispectrum NNReal a) := by cfc_cont_tac) (hf₀ : f 0 = 0 := by cfc_zero_tac) (ha : 0 ≤ a := by cfc_tac) : ‖cfcₙ f a‖₊ ≤ c ↔ ∀ x ∈ quasispectrum NNReal a, f x ≤ c

Alias of nnNorm_cfcₙ_nnreal_le_iff.

theorem nnNorm_cfcₙ_nnreal_lt {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {f : NNReal → NNReal} {a : A} {c : NNReal} (h : ∀ x ∈ quasispectrum NNReal a, f x < c) : ‖cfcₙ f a‖₊ < c

@[deprecated nnNorm_cfcₙ_nnreal_lt (since := "2026-10-31")]

theorem nnnorm_cfcₙ_nnreal_lt {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] {f : NNReal → NNReal} {a : A} {c : NNReal} (h : ∀ x ∈ quasispectrum NNReal a, f x < c) : ‖cfcₙ f a‖₊ < c

Alias of nnNorm_cfcₙ_nnreal_lt.

theorem nnNorm_cfcₙ_nnreal_lt_iff {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (a : A) (c : NNReal) (hf : ContinuousOn f (quasispectrum NNReal a) := by cfc_cont_tac) (hf₀ : f 0 = 0 := by cfc_zero_tac) (ha : 0 ≤ a := by cfc_tac) : ‖cfcₙ f a‖₊ < c ↔ ∀ x ∈ quasispectrum NNReal a, f x < c

@[deprecated nnNorm_cfcₙ_nnreal_lt_iff (since := "2026-10-31")]

theorem nnnorm_cfcₙ_nnreal_lt_iff {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (a : A) (c : NNReal) (hf : ContinuousOn f (quasispectrum NNReal a) := by cfc_cont_tac) (hf₀ : f 0 = 0 := by cfc_zero_tac) (ha : 0 ≤ a := by cfc_tac) : ‖cfcₙ f a‖₊ < c ↔ ∀ x ∈ quasispectrum NNReal a, f x < c

Alias of nnNorm_cfcₙ_nnreal_lt_iff.

theorem NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_quasispectrum {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : A) (ha : 0 ≤ a := by cfc_tac) : IsGreatest (quasispectrum NNReal a) ‖a‖₊

theorem NonUnitalIsometricContinuousFunctionalCalculus.quasispectrum_le {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : A) ⦃x : NNReal⦄ (hx : x ∈ quasispectrum NNReal a) (ha : 0 ≤ a := by cfc_tac) : x ≤ ‖a‖₊

theorem MonotoneOn.nnNorm_cfcₙ {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (a : A) (hf : MonotoneOn f (quasispectrum NNReal a)) (hf₂ : ContinuousOn f (quasispectrum NNReal a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (ha : 0 ≤ a := by cfc_tac) : ‖cfcₙ f a‖₊ = f ‖a‖₊

@[deprecated MonotoneOn.nnNorm_cfcₙ (since := "2026-10-31")]

theorem MonotoneOn.nnnorm_cfcₙ {A : Type u_1} [NonUnitalNormedRing A] [StarRing A] [NormedSpace ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] [PartialOrder A] [StarOrderedRing A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (a : A) (hf : MonotoneOn f (quasispectrum NNReal a)) (hf₂ : ContinuousOn f (quasispectrum NNReal a) := by cfc_cont_tac) (hf0 : f 0 = 0 := by cfc_zero_tac) (ha : 0 ≤ a := by cfc_tac) : ‖cfcₙ f a‖₊ = f ‖a‖₊

Alias of MonotoneOn.nnNorm_cfcₙ.

Non-unital instance for unital algebras

instance IsometricContinuousFunctionalCalculus.toNonUnital {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [RCLike 𝕜] [NormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [IsometricContinuousFunctionalCalculus 𝕜 A p] : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p

An isometric continuous functional calculus on a unital algebra yields to a non-unital one.