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

theorem CStarAlgebra.span_nonneg_inter_closedBall {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {r : Real} (hr : LT.lt 0 r) : Eq (Submodule.span Complex (Inter.inter (setOf fun (x : A) => LE.le 0 x) (Metric.closedBall 0 r))) Top.top

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

theorem CStarAlgebra.span_nonneg_inter_ball {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {r : Real} (hr : LT.lt 0 r) : Eq (Submodule.span Complex (Inter.inter (setOf fun (x : A) => LE.le 0 x) (Metric.ball 0 r))) Top.top

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

theorem CStarAlgebra.span_nonneg_inter_unitClosedBall {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : Eq (Submodule.span Complex (Inter.inter (setOf fun (x : A) => LE.le 0 x) (Metric.closedBall 0 1))) Top.top

A C⋆-algebra is spanned by nonnegative contractions.

theorem CStarAlgebra.span_nonneg_inter_unitBall {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : Eq (Submodule.span Complex (Inter.inter (setOf fun (x : A) => LE.le 0 x) (Metric.ball 0 1))) Top.top

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 4 → A) => 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))))