Documentation

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart

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_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
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.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) :
a⁻ = 0 ↔ 0 ≤ a
source
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) :
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) :
b = a⁺ ∧ c = a⁻

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⁻.