Properties of the matrix logarithm

In particular, operator concavity of the matrix logarithm.

@[simp]

theorem HermitianMat.log_zero {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] : log 0 = 0

@[simp]

theorem HermitianMat.log_one {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] : log 1 = 0

theorem HermitianMat.log_smul {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] (A : HermitianMat n 𝕜) (x : ℝ) : (x • A).log = Real.log x • 1 + A.log

theorem HermitianMat.log_concave {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] {x y : HermitianMat n 𝕜} (hx : (↑x).PosDef) (hy : (↑y).PosDef) ⦃a b : ℝ⦄ (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : (a • x + b • y).log ≤ a • x.log + b • y.log

The matrix logarithm is operator concave.