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 a isometric 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] [TopologicalSemiring R] [ContinuousStar R] [Ring A] [StarRing A] [MetricSpace A] [Algebra R A] extends ContinuousFunctionalCalculus R 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] [TopologicalSemiring 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 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] [TopologicalSemiring R] [ContinuousStar R] [Semifield S] [StarRing S] [MetricSpace S] [TopologicalSemiring 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] [UniqueContinuousFunctionalCalculus 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] [TopologicalSemiring R] [ContinuousStar R] [NonUnitalRing A] [StarRing A] [MetricSpace A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] extends NonUnitalContinuousFunctionalCalculus R 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] [TopologicalSemiring 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 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] [TopologicalSemiring R] [ContinuousStar R] [Field S] [StarRing S] [MetricSpace S] [TopologicalRing 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] [UniqueNonUnitalContinuousFunctionalCalculus 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

instance IsStarNormal.instIsometricContinuousFunctionalCalculus {A : Type u_1} [CStarAlgebra A] : IsometricContinuousFunctionalCalculus ℂ A IsStarNormal

instance IsSelfAdjoint.instIsometricContinuousFunctionalCalculus {A : Type u_1} [CStarAlgebra A] : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint

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

instance IsStarNormal.instNonUnitalIsometricContinuousFunctionalCalculus {A : Type u_1} [NonUnitalCStarAlgebra A] : NonUnitalIsometricContinuousFunctionalCalculus ℂ A IsStarNormal

instance IsSelfAdjoint.instNonUnitalIsometricContinuousFunctionalCalculus {A : Type u_1} [NonUnitalCStarAlgebra A] : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint

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] [UniqueNonUnitalContinuousFunctionalCalculus ℝ 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] [UniqueContinuousFunctionalCalculus ℝ 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] [UniqueContinuousFunctionalCalculus ℝ 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] [UniqueContinuousFunctionalCalculus ℝ 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] [UniqueContinuousFunctionalCalculus ℝ 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] [UniqueContinuousFunctionalCalculus ℝ 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] [UniqueContinuousFunctionalCalculus ℝ 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 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] [UniqueNonUnitalContinuousFunctionalCalculus ℝ 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] [UniqueNonUnitalContinuousFunctionalCalculus ℝ 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] [UniqueNonUnitalContinuousFunctionalCalculus ℝ 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] [UniqueNonUnitalContinuousFunctionalCalculus ℝ 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] [UniqueNonUnitalContinuousFunctionalCalculus ℝ 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] [UniqueNonUnitalContinuousFunctionalCalculus ℝ 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