Operator monotonicity of logarithm (source code)

= Operator monotonicity of logarithm

For positive-definite <Hermitian operator>[Hermitian operators],
$$
0<A\leq B\quad\Longrightarrow\quad\log A\leq\log B.
$$
The same statement on supports follows by regularizing with a positive multiple of the identity and taking a <limit>.