The positive (and negative) parts of a selfadjoint element in a C⋆-algebra #

This file defines the positive and negative parts of a selfadjoint element in a C⋆-algebra via the continuous functional calculus and develops the basic API, including the uniqueness of the positive and negative parts.

source

noncomputable instance CStarAlgebra.instPosPart {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] :

PosPart A

Equations

CStarAlgebra.instPosPart = { posPart := cfcₙ fun (x : ℝ) => x⁺ }

source

noncomputable instance CStarAlgebra.instNegPart {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] :

NegPart A

Equations

CStarAlgebra.instNegPart = { negPart := cfcₙ fun (x : ℝ) => x⁻ }

source

theorem CFC.posPart_def {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] (a : A) :

a⁺ = cfcₙ (fun (x : ℝ) => x⁺) a

source

theorem CFC.negPart_def {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] (a : A) :

a⁻ = cfcₙ (fun (x : ℝ) => x⁻) a

source

@[simp]

theorem CFC.posPart_zero {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] :

0⁺ = 0

source

@[simp]

theorem CFC.negPart_zero {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] :

0⁻ = 0

source

@[simp]

theorem CFC.posPart_mul_negPart {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] (a : A) :

a⁺ * a⁻ = 0

source

@[simp]

theorem CFC.negPart_mul_posPart {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] (a : A) :

a⁻ * a⁺ = 0

source

theorem CFC.posPart_sub_negPart {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] (a : A) (ha : IsSelfAdjoint a := by cfc_tac) :

a⁺ - a⁻ = a

source

@[simp]

theorem CFC.posPart_neg {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] [UniqueNonUnitalContinuousFunctionalCalculus ℝ A] (a : A) :

(-a)⁺ = a⁻

source

@[simp]

theorem CFC.negPart_neg {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] [UniqueNonUnitalContinuousFunctionalCalculus ℝ A] (a : A) :

(-a)⁻ = a⁺

source

@[simp]

theorem CFC.posPart_smul {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] [UniqueNonUnitalContinuousFunctionalCalculus ℝ A] [StarModule ℝ A] {r : NNReal} {a : A} :

(r • a)⁺ = r • a⁺

source

@[simp]

theorem CFC.negPart_smul {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] [UniqueNonUnitalContinuousFunctionalCalculus ℝ A] [StarModule ℝ A] {r : NNReal} {a : A} :

(r • a)⁻ = r • a⁻

source

theorem CFC.posPart_smul_of_nonneg {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] [UniqueNonUnitalContinuousFunctionalCalculus ℝ A] [StarModule ℝ A] {r : ℝ} (hr : 0 ≤ r) {a : A} :

(r • a)⁺ = r • a⁺

source

theorem CFC.posPart_smul_of_nonpos {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] [UniqueNonUnitalContinuousFunctionalCalculus ℝ A] [StarModule ℝ A] {r : ℝ} (hr : r ≤ 0) {a : A} :

(r • a)⁺ = -r • a⁻

source

theorem CFC.negPart_smul_of_nonneg {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] [UniqueNonUnitalContinuousFunctionalCalculus ℝ A] [StarModule ℝ A] {r : ℝ} (hr : 0 ≤ r) {a : A} :

(r • a)⁻ = r • a⁻

source

theorem CFC.negPart_smul_of_nonpos {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] [UniqueNonUnitalContinuousFunctionalCalculus ℝ A] [StarModule ℝ A] {r : ℝ} (hr : r ≤ 0) {a : A} :

(r • a)⁻ = -r • a⁺

source

theorem CFC.posPart_nonneg {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] (a : A) :

0 ≤ a⁺

source

theorem CFC.negPart_nonneg {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] (a : A) :

0 ≤ a⁻

source

theorem CFC.posPart_eq_of_eq_sub_negPart {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] {a b : A} (hab : a = b - a⁻) (hb : 0 ≤ b := by cfc_tac) :

a⁺ = b

source

theorem CFC.negPart_eq_of_eq_PosPart_sub {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] {a c : A} (hac : a = a⁺ - c) (hc : 0 ≤ c := by cfc_tac) :

a⁻ = c

source

theorem CFC.le_posPart {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] {a : A} (ha : IsSelfAdjoint a := by cfc_tac) :

a ≤ a⁺

source

theorem CFC.neg_negPart_le {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] {a : A} (ha : IsSelfAdjoint a := by cfc_tac) :

-a⁻ ≤ a

source

theorem CFC.posPart_eq_self {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] (a : A) :

a⁺ = a ↔ 0 ≤ a

source

@[deprecated CFC.posPart_eq_self]

theorem CFC.eq_posPart_iff {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] (a : A) :

a = a⁺ ↔ 0 ≤ a

source

theorem CFC.negPart_eq_zero_iff {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] (a : A) (ha : IsSelfAdjoint a := by cfc_tac) :

a⁻ = 0 ↔ 0 ≤ a

source

theorem CFC.negPart_eq_neg {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] (a : A) :

a⁻ = -a ↔ a ≤ 0

source

@[deprecated CFC.negPart_eq_neg]

theorem CFC.eq_negPart_iff {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] (a : A) :

a = -a⁻ ↔ a ≤ 0

source

theorem CFC.posPart_eq_zero_iff {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] (a : A) (ha : IsSelfAdjoint a := by cfc_tac) :

a⁺ = 0 ↔ a ≤ 0

source

theorem CFC.posPart_negPart_unique {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [UniqueNonUnitalContinuousFunctionalCalculus ℝ A] [TopologicalRing A] [T2Space A] {a b c : A} (habc : a = b - c) (hbc : b * c = 0) (hb : 0 ≤ b := by cfc_tac) (hc : 0 ≤ c := by cfc_tac) :

a⁺ = b ∧ a⁻ = c

The positive and negative parts of a selfadjoint element a are unique. That is, if a = b - c is the difference of nonnegative elements whose product is zero, then these are precisely a⁺ and a⁻.

source

@[simp]