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) :
Exists fun (x : Fin 4A) => And (∀ (i : Fin 4), LE.le 0 (x i)) (And (∀ (i : Fin 4), LE.le (Norm.norm (x i)) (Norm.norm a)) (Eq a (Finset.univ.sum fun (i : Fin 4) => HSMul.hSMul (HPow.hPow Complex.I i.val) (x i))))