Documentation

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Absolute value defined via the continuous functional calculus #

This file defines the absolute value via the non-unital continuous functional calculus and provides basic API.

Main declarations #

source
noncomputable def CFC.abs {A : Type u_2} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] (a : A) :
A

The absolute value defined via the non-unital continuous functional calculus.

Instances For
    source
    @[simp]
    theorem CFC.abs_neg {A : Type u_2} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] (a : A) :
    abs (-a) = abs a
    source
    @[simp]
    theorem CFC.abs_nonneg {A : Type u_2} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] (a : A) :
    0 ≤ abs a
    source
    theorem CFC.abs_star {A : Type u_2} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] (a : A) (ha : IsStarNormal a := by cfc_tac) :
    abs (star a) = abs a
    source
    @[simp]
    theorem CFC.abs_zero {A : Type u_2} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] :
    abs 0 = 0
    source
    theorem CFC.abs_mul_abs {A : Type u_2} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) :
    abs a * abs a = star a * a
    source
    theorem Commute.cfcAbs_left {A : Type u_2} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a b : A} (h₁ : Commute a b) (h₂ : Commute a (star b)) :
    Commute (CFC.abs a) b
    source
    theorem Commute.cfcAbs_right {A : Type u_2} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a b : A} (h₁ : Commute a b) (h₂ : Commute a (star b)) :
    Commute b (CFC.abs a)
    source
    theorem Commute.cfcAbs_cfcAbs {A : Type u_2} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a b : A} (h₁ : Commute a b) (h₂ : Commute a (star b)) :
    Commute (CFC.abs a) (CFC.abs b)
    source
    theorem CFC.commute_abs_self {A : Type u_2} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (ha : IsStarNormal a := by cfc_tac) :
    Commute (abs a) a

    Normal elements commute with their absolute value.

    source
    theorem Commute.cfcAbs_mul_eq {A : Type u_2} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a b : A} (h₁ : Commute a b) (h₂ : Commute a (star b)) :
    CFC.abs (a * b) = CFC.abs a * CFC.abs b
    source
    theorem CFC.abs_mul_self {A : Type u_2} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (ha : IsStarNormal a := by cfc_tac) :
    abs (a * a) = star a * a
    source
    theorem CFC.abs_nnrpow_two {A : Type u_2} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) :
    abs a ^ 2 = star a * a
    source
    theorem CFC.abs_nnrpow_two_mul {A : Type u_2} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (x : NNReal) :
    abs a ^ (2 * x) = (star a * a) ^ x
    source
    theorem CFC.abs_nnrpow {A : Type u_2} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (x : NNReal) :
    abs a ^ x = (star a * a) ^ (x / 2)
    source
    theorem CFC.abs_of_nonneg {A : Type u_2} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (ha : 0 ≤ a := by cfc_tac) :
    abs a = a
    source
    theorem CFC.abs_of_nonpos {A : Type u_2} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (ha : a ≤ 0 := by cfc_tac) :
    abs a = -a
    source
    theorem CFC.abs_eq_cfcₙ_norm {A : Type u_2} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (ha : IsSelfAdjoint a := by cfc_tac) :
    abs a = cfcₙ (fun (x : ℝ) => ‖x‖) a
    source
    theorem CFC.posPart_add_negPart {A : Type u_2} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (ha : IsSelfAdjoint a := by cfc_tac) :
    a⁺ + a⁻ = abs a
    source
    theorem CFC.abs_sub_self {A : Type u_2} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (ha : IsSelfAdjoint a := by cfc_tac) :
    abs a - a = 2 • a⁻
    source
    theorem CFC.abs_add_self {A : Type u_2} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (ha : IsSelfAdjoint a := by cfc_tac) :
    abs a + a = 2 • a⁺
    source
    @[simp]
    theorem CFC.cfcAbs_cfcAbs {A : Type u_2} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) :
    abs (abs a) = abs a
    source
    @[simp]
    theorem CFC.abs_smul_nonneg {A : Type u_2} [NonUnitalRing A] [StarRing A] [TopologicalSpace A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] [StarModule ℝ A] {R : Type u_3} [Semiring R] [SMulWithZero R NNReal] [SMul R A] [IsScalarTower R NNReal A] (r : R) (a : A) :
    abs (r • a) = r • abs a
    source
    theorem cfcₙ_norm_sq_nonneg {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [RCLike 𝕜] [NonUnitalRing A] [TopologicalSpace A] [Module 𝕜 A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) :
    0 ≤ cfcₙ (fun (z : 𝕜) => star (f z) * f z) a
    source
    theorem cfcₙ_norm_nonneg {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [RCLike 𝕜] [NonUnitalRing A] [TopologicalSpace A] [Module 𝕜 A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜) (a : A) :
    0 ≤ cfcₙ (fun (x : 𝕜) => ↑‖f x‖) a
    source
    @[simp]
    theorem CFC.abs_smul {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [NonUnitalRing A] [TopologicalSpace A] [Module 𝕜 A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [StarModule 𝕜 A] [StarModule ℝ A] [IsScalarTower ℝ 𝕜 A] (r : 𝕜) (a : A) :
    abs (r • a) = ‖r‖ • abs a
    source
    theorem CFC.abs_eq_cfcₙ_coe_norm (𝕜 : Type u_1) {A : Type u_2} {p : A → Prop} [RCLike 𝕜] [NonUnitalRing A] [TopologicalSpace A] [Module 𝕜 A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalContinuousFunctionalCalculus 𝕜 A p] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) (ha : p a := by cfc_tac) :
    abs a = cfcₙ (fun (z : 𝕜) => ↑‖z‖) a
    source
    theorem cfcₙ_comp_norm {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [RCLike 𝕜] [NonUnitalRing A] [TopologicalSpace A] [Module 𝕜 A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalContinuousFunctionalCalculus 𝕜 A p] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (f : 𝕜 → 𝕜) (a : A) (ha : p a := by cfc_tac) (hf : ContinuousOn f ((fun (z : 𝕜) => ↑‖z‖) '' quasispectrum 𝕜 a) := by cfc_cont_tac) :
    cfcₙ (fun (x : 𝕜) => f ↑‖x‖) a = cfcₙ f (CFC.abs a)
    source
    theorem CFC.quasispectrum_abs {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [RCLike 𝕜] [NonUnitalRing A] [TopologicalSpace A] [Module 𝕜 A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] [NonUnitalContinuousFunctionalCalculus 𝕜 A p] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) (ha : p a := by cfc_tac) :
    quasispectrum 𝕜 (abs a) = (fun (z : 𝕜) => ↑‖z‖) '' quasispectrum 𝕜 a
    source
    theorem CFC.abs_eq_cfc_norm {A : Type u_2} [Ring A] [StarRing A] [TopologicalSpace A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A) (ha : IsSelfAdjoint a := by cfc_tac) :
    abs a = cfc (fun (x : ℝ) => ‖x‖) a
    source
    theorem CFC.abs_coe_unitary {A : Type u_2} [Ring A] [StarRing A] [TopologicalSpace A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (U : ↥(unitary A)) :
    abs ↑U = 1
    source
    @[simp]
    theorem CFC.abs_of_mem_unitary {A : Type u_2} [Ring A] [StarRing A] [TopologicalSpace A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {U : A} (hU : U ∈ unitary A) :
    abs U = 1
    source
    theorem CFC.abs_one {A : Type u_2} [Ring A] [StarRing A] [TopologicalSpace A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] :
    abs 1 = 1
    source
    @[simp]
    theorem CFC.abs_algebraMap_nnreal {A : Type u_2} [Ring A] [StarRing A] [TopologicalSpace A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] [StarModule ℝ A] (x : NNReal) :
    abs ((algebraMap NNReal A) x) = (algebraMap NNReal A) x
    source
    @[simp]
    theorem CFC.abs_natCast {A : Type u_2} [Ring A] [StarRing A] [TopologicalSpace A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] [StarModule ℝ A] (n : ℕ) :
    abs ↑n = ↑n
    source
    @[simp]
    theorem CFC.abs_ofNat {A : Type u_2} [Ring A] [StarRing A] [TopologicalSpace A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] [StarModule ℝ A] (n : ℕ) [n.AtLeastTwo] :
    abs (OfNat.ofNat n) = OfNat.ofNat n
    source
    @[simp]
    theorem CFC.abs_intCast {A : Type u_2} [Ring A] [StarRing A] [TopologicalSpace A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] [StarModule ℝ A] (n : ℤ) :
    abs ↑n = ↑|n|
    source
    @[simp]
    theorem CFC.abs_algebraMap {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [Ring A] [TopologicalSpace A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra 𝕜 A] [Algebra ℝ A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [StarModule 𝕜 A] [StarModule ℝ A] [IsScalarTower ℝ 𝕜 A] (c : 𝕜) :
    abs ((algebraMap 𝕜 A) c) = (algebraMap ℝ A) ‖c‖
    source
    theorem cfc_comp_norm {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [RCLike 𝕜] [Ring A] [TopologicalSpace A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra 𝕜 A] [ContinuousFunctionalCalculus 𝕜 A p] [Algebra ℝ A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (f : 𝕜 → 𝕜) (a : A) (ha : p a := by cfc_tac) (hf : ContinuousOn f ((fun (z : 𝕜) => ↑‖z‖) '' spectrum 𝕜 a) := by cfc_cont_tac) :
    cfc (fun (x : 𝕜) => f ↑‖x‖) a = cfc f (CFC.abs a)
    source
    theorem CFC.abs_sq {A : Type u_2} [Ring A] [TopologicalSpace A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra ℝ A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) :
    abs a ^ 2 = star a * a
    source
    theorem CFC.spectrum_abs {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [RCLike 𝕜] [Ring A] [TopologicalSpace A] [StarRing A] [PartialOrder A] [StarOrderedRing A] [Algebra 𝕜 A] [ContinuousFunctionalCalculus 𝕜 A p] [Algebra ℝ A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) (ha : p a := by cfc_tac) :
    spectrum 𝕜 (abs a) = (fun (z : 𝕜) => ↑‖z‖) '' spectrum 𝕜 a
    source
    theorem CFC.continuous_abs {A : Type u_2} [NonUnitalNormedRing A] [StarRing A] [ContinuousStar A] [NormedSpace ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [CompleteSpace A] :
    Continuous abs
    source
    @[simp]
    theorem CFC.abs_eq_zero_iff {A : Type u_2} [NonUnitalNormedRing A] [StarRing A] [CStarRing A] [NormedSpace ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] {a : A} :
    abs a = 0 ↔ a = 0
    source
    @[simp]
    theorem CFC.norm_abs {A : Type u_2} [NonUnitalNormedRing A] [StarRing A] [CStarRing A] [NormedSpace ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] {a : A} :
    ‖abs a‖ = ‖a‖