Documentation

Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart

C⋆-algebraic facts about a⁺ and a⁻. #

A C⋆-algebra is spanned by nonnegative elements of norm at most r

A C⋆-algebra is spanned by nonnegative elements of norm less than r.

A C⋆-algebra is spanned by nonnegative contractions.

A C⋆-algebra is spanned by nonnegative strict contractions.

theorem CStarAlgebra.exists_sum_four_nonneg {A : Type u_2} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (a : A) :
∃ (x : Fin 4A), (∀ (i : Fin 4), 0 x i) (∀ (i : Fin 4), x i a) a = i : Fin 4, Complex.I ^ i x i