Order properties of Ring.inverse in C⋆-algebras

This file shows that Ring.inverse is convex on strictly positive operators.

Main declarations

• convexOn_ringInverse: Ring.inverse is convex on strictly positive operators, i.e. the inverse is operator convex.

theorem CStarAlgebra.convexOn_ringInverse {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : ConvexOn ℝ {a : A | IsStrictlyPositive a} Ring.inverse

theorem CStarAlgebra.convexOn_ringInverse_algebraMap_add {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {t : ℝ} (ht : 0 < t) : ConvexOn ℝ (Set.Ici 0) fun (x : A) => Ring.inverse ((algebraMap ℝ A) t + x)