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