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), Topology.IsClosedEmbedding ⇑φ ∧ φ (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 : outParam (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 ⋯)

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‖₊

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‖₊

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‖₊

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

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

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

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

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‖₊

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‖₊

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), Topology.IsClosedEmbedding ⇑φ ∧ φ { 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 ⋯)

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‖₊

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‖₊

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‖₊

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

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

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

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

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‖₊

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‖₊

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‖₊

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‖₊

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

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

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

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

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‖₊

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‖₊

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‖₊

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

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

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

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

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‖₊

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.