PhyslibAlpha.AlgebraicFramework.CStarAlgebra.JordanDecomposition

The Jordan decomposition of a self-adjoint element

Every self-adjoint element `a` of a C⋆-algebra splits canonically as `a = a⁺ - a⁻`, a difference of two *orthogonal* positive elements (`a⁺ * a⁻ = 0`) — the noncommutative analogue of splitting a real-valued function into its positive and negative parts, or a signed measure into its positive and negative variation (Camille Jordan's decomposition theorem, 1881/1892). This is not the same "Jordan" as `StarAlgebra/Jordan.lean`'s Jordan *product* `a ∘ b := a * b + b * a` — that one is named for Pascual Jordan, no relation, and the shared name is an unfortunate but standard clash in the operator-algebra literature.

Mathlib already builds `a⁺`, `a⁻` from the continuous functional calculus (`cfcₙ` applied to the functions `t ↦ max t 0` and `t ↦ max (-t) 0`) and proves the decomposition, orthogonality, and uniqueness facts at the level of a bare C⋆-algebra element. This file packages exactly those facts one level up, at the level of `Observable A := selfAdjoint A` and `PositiveObservable A`, so that "take the positive/negative part" is available as an operation *on observables*, landing in `PositiveObservable A` rather than requiring the caller to separately track self-adjointness and nonnegativity of a bare element of `A` after the fact.

Genuinely needing a full C⋆-algebra here (rather than a bare order-unit space) is not a corner that was cut: the continuous functional calculus behind `a⁺`, `a⁻` needs completeness and the C⋆-identity to exist at all, so `[CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]` is the correct, load-bearing hypothesis, not one to weaken.

Main definitions

- `Observable.posPart`, `Observable.negPart` : the positive and negative parts of an observable, as `PositiveObservable A`. - `Observable.posPart_sub_negPart` : `a⁺ - a⁻ = a`. - `Observable.posPart_mul_negPart`, `Observable.negPart_mul_posPart` : the two parts are orthogonal. - `Observable.posPart_negPart_unique` : this is the *only* decomposition of `a` into a difference of orthogonal positive observables.

A. Positive observables

B. Positive and negative parts

7 declarations

theorem

An observable $a \ge 0$ iff $a = b^2$ for some observable $b$

#nonneg_iff_exists_observable_sq

Let $A$ be a $C^*$ -algebra. For any observable $a \in A$ , $a \ge 0$ if and only if there exists an observable $b \in A$ such that $a = b^2$ .

definition

Positive part $a^+$ of an observable $a$

#posPart

For a self-adjoint element $a$ of a $C^*$ -algebra $A$ (referred to as an observable), its positive part $a^+$ is the positive observable defined via the continuous functional calculus as $f(a)$ where $f(t) = \max(t, 0)$ . The result is returned as a `PositiveObservable`, which is a structure containing an element $x \in A$ along with proofs that $x$ is self-adjoint and $x \geq 0$ .

definition

Negative part $a^-$ of an observable $a$

#negPart

For an observable $a$ (a self-adjoint element) in a $C^*$ -algebra $A$ , its negative part $a^-$ is the positive element defined via the continuous functional calculus by the function $f(t) = \max(-t, 0)$ . It is one of the two components in the Jordan decomposition $a = a^+ - a^-$ .

theorem

$a = a^+ - a^-$

#posPart_sub_negPart

Let $A$ be a $C^*$ -algebra and $a \in A$ be an observable (a self-adjoint element). Let $a^+$ and $a^-$ denote the positive part and negative part of $a$ , respectively. Then $a$ is the difference of these two parts: $a^+ - a^- = a$

theorem

$a^+ a^- = 0$ for an observable $a$

#posPart_mul_negPart

Let $A$ be a $C^*$ -algebra and $a$ be an observable (a self-adjoint element) in $A$ . Let $a^+$ and $a^-$ denote the positive part (`posPart a`) and the negative part (`negPart a`) of $a$ as defined by the continuous functional calculus. Then their product is zero, i.e., $a^+ a^- = 0$ .

theorem

$a^- a^+ = 0$ for an observable $a$

#negPart_mul_posPart

For any observable $a$ in a $C^*$ -algebra $A$ , the product of its negative part $a^-$ and its positive part $a^+$ is zero: $a^- a^+ = 0$ This signifies that the negative and positive parts of the Jordan decomposition are orthogonal.

theorem

Uniqueness of the Jordan decomposition $a = a^+ - a^-$

#posPart_negPart_unique

Let $A$ be a $C^*$ -algebra and $a$ be an observable (a self-adjoint element of $A$ ). Suppose there exist two positive observables $b$ and $c$ (self-adjoint elements such that $b, c \ge 0$ ) that satisfy the decomposition $a = b - c$ and the orthogonality condition $bc = 0$ . Then $b$ is the positive part of $a$ (denoted $a^+$ ) and $c$ is the negative part of $a$ (denoted $a^-$ ).

PhyslibAlpha.AlgebraicFramework.CStarAlgebra.JordanDecomposition

The Jordan decomposition of a self-adjoint element

Main definitions

A. Positive observables

B. Positive and negative parts

An observable a≥0a \ge 0a≥0 iff a=b2a = b^2a=b2 for some observable bbb

Positive part a+a^+a+ of an observable aaa

Negative part a−a^-a− of an observable aaa

a=a+−a−a = a^+ - a^-a=a+−a−

a+a−=0a^+ a^- = 0a+a−=0 for an observable aaa

a−a+=0a^- a^+ = 0a−a+=0 for an observable aaa

Uniqueness of the Jordan decomposition a=a+−a−a = a^+ - a^-a=a+−a−

An observable $a \ge 0$ iff $a = b^2$ for some observable $b$

Positive part $a^+$ of an observable $a$

Negative part $a^-$ of an observable $a$

$a = a^+ - a^-$

$a^+ a^- = 0$ for an observable $a$

$a^- a^+ = 0$ for an observable $a$

Uniqueness of the Jordan decomposition $a = a^+ - a^-$