QuantumInfo.ForMathlib.HayataGroup.TraceInequality.OperatorGeometricMean
3 declarations
The -power mean of operators and
Let be a complex Hilbert space and be the space of bounded linear operators on . For real numbers and operators , the -power mean of and is defined as the generalized perspective of the functions and . Specifically, it is the operator: where the operator powers are defined via the continuous functional calculus. This is typically applied when is a positive invertible operator and is Hermitian.
Joint Concavity of the -Power Mean for
Let be a complex inner product space and be the space of bounded linear operators on . Let denote the set of strictly positive operators (self-adjoint operators with strictly positive spectrum). For any real numbers and such that and , the operator -power mean is jointly concave on . That is, for all and any scalar , the following inequality holds in the Löwner order:
Joint Convexity of the -Power Mean for and
Let be a complex inner product space and be the space of bounded linear operators on . Let denote the set of strictly positive operators (self-adjoint operators with spectrum contained in ). For real numbers and such that and , the -power mean of , defined by is jointly convex on . That is, for all and , the following operator inequality holds:
