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

theorem CStarAlgebra.span_nonneg_inter_closedBall {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {r : ℝ} (hr : 0 < r) : Submodule.span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 r) = ⊤

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 : ℝ} (hr : 0 < r) : Submodule.span ℂ ({x : A | 0 ≤ x} ∩ Metric.ball 0 r) = ⊤

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] : Submodule.span ℂ ({x : A | 0 ≤ x} ∩ Metric.closedBall 0 1) = ⊤

A C⋆-algebra is spanned by nonnegative contractions.

theorem CStarAlgebra.span_nonneg_inter_unitBall {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : Submodule.span ℂ ({x : A | 0 ≤ x} ∩ Metric.ball 0 1) = ⊤

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 4 → A), (∀ (i : Fin 4), 0 ≤ x i) ∧ (∀ (i : Fin 4), ‖x i‖ ≤ ‖a‖) ∧ a = ∑ i : Fin 4, Complex.I ^ ↑i • x i