The derivative of the exponential at Hermitian matrices

In a unitary eigenbasis of a Hermitian matrix with eigenvalues d i, the derivative of the matrix exponential multiplies entry (i,j) by the positive divided difference dslope Real.exp (d i) (d j). Consequently the derivative is invertible, even on the full matrix space. This is the analytic local-inverse step for smooth logarithms on positive Hermitian matrices.

The proof uses the Duhamel integral TauCeti.expFDeriv_apply_eq_integral and Mathlib's unitary spectral theorem. The continuous linear maps use the Euclidean operator norm, whose topology is the native matrix topology.

theorem Matrix.expFDeriv_diagonal {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] (d : n → ℝ) (Y : Matrix n n 𝕜) : (TauCeti.expFDeriv 𝕜 (diagonal fun (k : n) => ↑(d k))) Y = of fun (i j : n) => ↑(dslope Real.exp (d i) (d j)) * Y i j

At a real diagonal matrix the derivative of the exponential is entrywise multiplication by the divided differences of the real exponential. This is an explicit rewrite rule: the general TauCeti.expFDeriv_apply simp rule expands the derivative into its series.

theorem Matrix.bijective_expFDeriv_diagonal {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] (d : n → ℝ) : Function.Bijective ⇑(TauCeti.expFDeriv 𝕜 (diagonal fun (k : n) => ↑(d k)))

The derivative at a real diagonal matrix is bijective. Repeated eigenvalues cause no singularity, since the corresponding divided difference is the positive exponential.

theorem Matrix.IsHermitian.expFDeriv_eigenbasis {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : A.IsHermitian) (Y : Matrix n n 𝕜) : ((Unitary.conjStarAlgAut 𝕜 (Matrix n n 𝕜)) (star hA.eigenvectorUnitary)) ((TauCeti.expFDeriv 𝕜 A) Y) = of fun (i j : n) => ↑(dslope Real.exp (hA.eigenvalues i) (hA.eigenvalues j)) * ((Unitary.conjStarAlgAut 𝕜 (Matrix n n 𝕜)) (star hA.eigenvectorUnitary)) Y i j

In a unitary eigenbasis, the derivative of the exponential is multiplication of each entry by the positive divided difference of its two eigenvalues.

theorem Matrix.IsHermitian.bijective_expFDeriv {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : A.IsHermitian) : Function.Bijective ⇑(TauCeti.expFDeriv 𝕜 A)

The derivative of the exponential at a Hermitian matrix is bijective on the full matrix space, over either the real or complex scalars.

theorem Matrix.IsHermitian.isUnit_expFDeriv {n : Type u_1} {𝕜 : Type u_2} [Fintype n] [DecidableEq n] [RCLike 𝕜] {A : Matrix n n 𝕜} (hA : A.IsHermitian) : IsUnit (TauCeti.expFDeriv 𝕜 A)

The derivative of the exponential at a Hermitian matrix is an invertible continuous linear endomorphism.