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.

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

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

theorem CFC.posPart_def {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) : a⁺ = cfcₙ (fun (x : ℝ) => x⁺) a

theorem CFC.negPart_def {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A) : a⁻ = cfcₙ (fun (x : ℝ) => x⁻) a

@[simp]

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

@[simp]

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

theorem CFC.posPart_eq_zero_of_not_isSelfAdjoint {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {a : A} (ha : ¬IsSelfAdjoint a) : a⁺ = 0

theorem CFC.negPart_eq_zero_of_not_isSelfAdjoint {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {a : A} (ha : ¬IsSelfAdjoint a) : a⁻ = 0

@[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 ℝ A IsSelfAdjoint] (a : A) : a⁺ * a⁻ = 0

@[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 ℝ A IsSelfAdjoint] (a : A) : a⁻ * a⁺ = 0

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

@[simp]

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

@[simp]

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

@[simp]

theorem CFC.posPart_smul {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A] [StarModule ℝ A] {r : NNReal} {a : A} : (r • a)⁺ = r • a⁺

@[simp]

theorem CFC.negPart_smul {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A] [StarModule ℝ A] {r : NNReal} {a : A} : (r • a)⁻ = r • a⁻

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 ℝ A IsSelfAdjoint] [T2Space A] [StarModule ℝ A] {r : ℝ} (hr : 0 ≤ r) {a : A} : (r • a)⁺ = r • a⁺

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 ℝ A IsSelfAdjoint] [T2Space A] [StarModule ℝ A] {r : ℝ} (hr : r ≤ 0) {a : A} : (r • a)⁺ = -r • a⁻

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 ℝ A IsSelfAdjoint] [T2Space A] [StarModule ℝ A] {r : ℝ} (hr : 0 ≤ r) {a : A} : (r • a)⁻ = r • a⁻

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 ℝ A IsSelfAdjoint] [T2Space A] [StarModule ℝ A] {r : ℝ} (hr : r ≤ 0) {a : A} : (r • a)⁻ = -r • a⁺

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

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

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 ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] {a b : A} (hab : a = b - a⁻) (hb : 0 ≤ b := by cfc_tac) : a⁺ = b

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 ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] {a c : A} (hac : a = a⁺ - c) (hc : 0 ≤ c := by cfc_tac) : a⁻ = c

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

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

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

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 ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] (a : A) (ha : IsSelfAdjoint a := by cfc_tac) : a⁻ = 0 ↔ 0 ≤ a

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

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 ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] (a : A) (ha : IsSelfAdjoint a := by cfc_tac) : a⁺ = 0 ↔ a ≤ 0

theorem CFC.posPart_negPart_unique {A : Type u_1} [NonUnitalRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarRing A] [TopologicalSpace A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsTopologicalRing 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⁻.

@[simp]

theorem CFC.posPart_one {A : Type u_1} [Ring A] [Algebra ℝ A] [StarRing A] [TopologicalSpace A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A] : 1⁺ = 1

@[simp]

theorem CFC.negPart_one {A : Type u_1} [Ring A] [Algebra ℝ A] [StarRing A] [TopologicalSpace A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A] : 1⁻ = 0

@[simp]

theorem CFC.posPart_algebraMap {A : Type u_1} [Ring A] [Algebra ℝ A] [StarRing A] [TopologicalSpace A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A] (r : ℝ) : ((algebraMap ℝ A) r)⁺ = (algebraMap ℝ A) r⁺

@[simp]

theorem CFC.negPart_algebraMap {A : Type u_1} [Ring A] [Algebra ℝ A] [StarRing A] [TopologicalSpace A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A] (r : ℝ) : ((algebraMap ℝ A) r)⁻ = (algebraMap ℝ A) r⁻

@[simp]

theorem CFC.posPart_algebraMap_nnreal {A : Type u_1} [Ring A] [Algebra ℝ A] [StarRing A] [TopologicalSpace A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A] (r : NNReal) : ((algebraMap NNReal A) r)⁺ = (algebraMap NNReal A) r

@[simp]

theorem CFC.posPart_natCast {A : Type u_1} [Ring A] [Algebra ℝ A] [StarRing A] [TopologicalSpace A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A] (n : ℕ) : (↑n)⁺ = ↑n

theorem CStarAlgebra.linear_combination_nonneg {A : Type u_1} [NonUnitalRing A] [Module ℂ A] [SMulCommClass ℂ A A] [IsScalarTower ℂ A A] [StarRing A] [TopologicalSpace A] [StarModule ℂ A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (x : A) : (↑(realPart x))⁺ - (↑(realPart x))⁻ + (Complex.I • (↑(imaginaryPart x))⁺ - Complex.I • (↑(imaginaryPart x))⁻) = x

theorem CStarAlgebra.span_nonneg {A : Type u_1} [NonUnitalRing A] [Module ℂ A] [SMulCommClass ℂ A A] [IsScalarTower ℂ A A] [StarRing A] [TopologicalSpace A] [StarModule ℂ A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] : Submodule.span ℂ {a : A | 0 ≤ a} = ⊤

A C⋆-algebra is spanned by its nonnegative elements.