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 #

CFC.abs: The absolute value as abs a := CFC.sqrt (star a * a).

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) :

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

Equations

CFC.abs a = CFC.sqrt (star a * a)

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

@[simp]

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

@[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‖

Documentation

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs

Absolute value defined via the continuous functional calculus #

Main declarations #