Documentation

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

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
@[instance_reducible]
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
source
@[instance_reducible]
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
source
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
source
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
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 ℝ A 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 ℝ A IsSelfAdjoint] :
0⁻ = 0
source
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
source
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
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 ℝ A 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 ℝ A 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 ℝ A 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 ℝ A IsSelfAdjoint] [T2Space 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 ℝ A IsSelfAdjoint] [T2Space 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 ℝ A IsSelfAdjoint] [T2Space 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 ℝ A IsSelfAdjoint] [T2Space 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 ℝ A IsSelfAdjoint] [T2Space 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 ℝ A IsSelfAdjoint] [T2Space 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 ℝ A IsSelfAdjoint] [T2Space 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 ℝ A IsSelfAdjoint] [T2Space 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 ℝ A 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 ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] (a : A) :
0 ≤ a⁻
source
instance CFC.instSelfAdjointDecompose {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] :
SelfAdjointDecompose 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 ℝ A 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 ℝ A 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 ℝ A 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 ℝ A 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 ℝ A 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 ℝ A 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 ℝ A 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 ℝ A 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 ℝ A IsSelfAdjoint] [PartialOrder A] [StarOrderedRing A] [NonnegSpectrumClass ℝ A] [IsSemitopologicalRing 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]
theorem CFC.posPart_one {A : Type u_1} [Ring A] [Algebra ℝ A] [StarRing A] [TopologicalSpace A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A] :
1⁺ = 1
source
@[simp]
theorem CFC.negPart_one {A : Type u_1} [Ring A] [Algebra ℝ A] [StarRing A] [TopologicalSpace A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A] :
1⁻ = 0
source
@[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⁺
source
@[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⁻
source
@[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
source
@[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
source
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
source
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.