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)
: