The logarithm and real powers of positive definite matrices

Over 𝕜 = ℝ or ℂ, the matrix exponential maps the Hermitian matrices onto the positive definite ones, with inverse the logarithm cfc Real.log of the continuous functional calculus. This file proves both inverse identities and that the logarithm is C^n on the positive definite matrices for every n : ℕ∞ω, including the analytic case n = ω, over 𝕜 itself. Near each positive definite matrix it agrees with the analytic local inverse of exp on the full matrix space, which the inverse function theorem provides because the derivative of exp at a Hermitian matrix is invertible (Matrix.IsHermitian.isUnit_expFDeriv). The real powers P ^ s = exp (s • log P) and the square root inherit this smoothness.

The logarithm is written cfc Real.log, which is CFC.log whenever the latter is defined; CFC.log needs a normed ℝ-algebra structure, which complex matrices do not carry by default. The smoothness statements use the scoped Euclidean operator norm Matrix.Norms.L2Operator, whose topology is the native matrix topology.

Main results

• Matrix.IsHermitian.posDef_exp: the exponential of a Hermitian matrix is positive definite.
• Matrix.IsHermitian.cfc_log_exp, Matrix.PosDef.exp_cfc_log: the logarithm inverts the exponential on the Hermitian matrices, and the exponential inverts the logarithm on the positive definite matrices.
• Matrix.PosDef.rpow_eq_exp_smul_cfc_log: P ^ s = exp (s • log P) for positive definite P.
• Matrix.contDiffOn_cfc_log, Matrix.contDiffOn_rpow, Matrix.contDiffOn_sqrt: the logarithm, every real power and the square root are C^n on the positive definite matrices.

References

• Brian C. Hall, Lie Groups, Lie Algebras, and Representations, second edition, Graduate Texts in Mathematics 222, Springer, 2015, Sections 2.3 and 2.5.

theorem Matrix.IsHermitian.posDef_exp {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] {X : Matrix n n 𝕜} (hX : X.IsHermitian) : (NormedSpace.exp X).PosDef

The exponential of a Hermitian matrix is positive definite.

@[simp]

theorem Matrix.IsHermitian.cfc_log_exp {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] {X : Matrix n n 𝕜} (hX : X.IsHermitian) : cfc Real.log (NormedSpace.exp X) = X

The logarithm of the exponential of a Hermitian matrix is the matrix itself.

@[simp]

theorem Matrix.PosDef.exp_cfc_log {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] {P : Matrix n n 𝕜} (hP : P.PosDef) : NormedSpace.exp (cfc Real.log P) = P

The exponential of the logarithm of a positive definite matrix is the matrix itself.

theorem Matrix.contDiffOn_cfc_log {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] {k : WithTop ℕ∞} : ContDiffOn 𝕜 k (cfc Real.log) {P : Matrix n n 𝕜 | P.PosDef}

Smoothness of the matrix logarithm. The logarithm is C^n on the positive definite matrices for every n : ℕ∞ω, including n = ω, over either the real or the complex scalars.

theorem Matrix.PosDef.rpow_eq_exp_smul_cfc_log {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] {P : Matrix n n 𝕜} (hP : P.PosDef) (s : ℝ) : P ^ s = NormedSpace.exp (s • cfc Real.log P)

A real power of a positive definite matrix is the exponential of its rescaled logarithm.

theorem Matrix.contDiffOn_rpow {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] (s : ℝ) {k : WithTop ℕ∞} : ContDiffOn 𝕜 k (fun (P : Matrix n n 𝕜) => P ^ s) {P : Matrix n n 𝕜 | P.PosDef}

Every real power P ↦ P ^ s is C^n on the positive definite matrices, for every n : ℕ∞ω.

theorem Matrix.contDiffOn_sqrt {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] {k : WithTop ℕ∞} : ContDiffOn 𝕜 k CFC.sqrt {P : Matrix n n 𝕜 | P.PosDef}

The square root is C^n on the positive definite matrices, for every n : ℕ∞ω.