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.