Lie's Trace Formula

This file proves the formula det (exp A) = exp (tr A) for matrices, also known as Lie's trace formula.

The proof proceeds by first showing the formula for upper-triangular matrices and then leveraging Schur triangulation to generalize to any matrix. An upper-triangular matrix A is defined in mathlib as Matrix.BlockTriangular A id.

Main results

• Matrix.det_exp: The determinant of the exponential of a matrix is the exponential of its trace.

instance Matrix.instUniformSpace_physLean {𝕂 : Type u_1} {m : Type u_2} {n : Type u_3} [UniformSpace 𝕂] : UniformSpace (Matrix m n 𝕂)

Equations

• Matrix.instUniformSpace_physLean = id inferInstance

theorem Matrix.tsum_eq_zero {β : Type u_4} [TopologicalSpace β] [AddCommMonoid β] {f : ℕ → β} (h : ∀ (n : ℕ), f n = 0) : ∑' (n : ℕ), f n = 0

If every term of a series is zero, then its sum is zero.

The determinant of the matrix exponential

theorem Matrix.matrix_tsum_apply {𝕂 : Type u_1} {m : Type u_2} [RCLike 𝕂] {f : ℕ → Matrix m m 𝕂} (hf : Summable f) (i j : m) : (∑' (n : ℕ), f n) i j = ∑' (n : ℕ), f n i j

Apply a matrix tsum to a given entry.

theorem Matrix.diag_mul_of_blockTriangular_id {𝕂 : Type u_1} {m : Type u_2} [RCLike 𝕂] [Fintype m] [LinearOrder m] {A B : Matrix m m 𝕂} (hA : A.BlockTriangular id) (hB : B.BlockTriangular id) : (A * B).diag = A.diag * B.diag

For upper-triangular matrices, the diagonal of a product is the product of the diagonals. This is a specific case of a more general property for block-triangular matrices.

theorem Matrix.blockTriangular.pow {𝕂 : Type u_1} {m : Type u_2} [RCLike 𝕂] [Fintype m] [LinearOrder m] {A : Matrix m m 𝕂} (hA : A.BlockTriangular id) (k : ℕ) : (A ^ k).BlockTriangular id

Powers of block triangular matrices are block triangular.

theorem Matrix.diag_pow_of_blockTriangular_id {𝕂 : Type u_1} {m : Type u_2} [RCLike 𝕂] [Fintype m] [LinearOrder m] {A : Matrix m m 𝕂} (hA : A.BlockTriangular id) (k : ℕ) : (A ^ k).diag = A.diag ^ k

For an upper-triangular matrix, the diagonal of a power is the power of the diagonal.

theorem Matrix.blockTriangular_exp_of_blockTriangular_id {𝕂 : Type u_1} {m : Type u_2} [RCLike 𝕂] [Fintype m] [LinearOrder m] {A : Matrix m m 𝕂} (hA : A.BlockTriangular id) : (NormedSpace.exp 𝕂 A).BlockTriangular id

The exponential of an upper-triangular matrix is upper-triangular.

theorem Matrix.diag_pow_entry_eq_pow_diag_entry {𝕂 : Type u_1} {m : Type u_2} [RCLike 𝕂] [Fintype m] [LinearOrder m] {A : Matrix m m 𝕂} (hA : A.BlockTriangular id) (n : ℕ) (i : m) : (A ^ n) i i = A i i ^ n

For an upper–triangular matrix A, the (i,i) entry of the power A ^ n is simply the n-th power of the original diagonal entry.

theorem Matrix.exp_series_diag_term_eq {𝕂 : Type u_1} {m : Type u_2} [RCLike 𝕂] [Fintype m] [LinearOrder m] {A : Matrix m m 𝕂} (hA : A.BlockTriangular id) (n : ℕ) (i : m) : ((↑n.factorial)⁻¹ • A ^ n) i i = (↑n.factorial)⁻¹ • A i i ^ n

Each term in the matrix exponential series equals the corresponding scalar term on the diagonal

theorem Matrix.matrix_exp_series_diag_eq_scalar_series {𝕂 : Type u_1} {m : Type u_2} [RCLike 𝕂] [Fintype m] [LinearOrder m] {A : Matrix m m 𝕂} (hA : A.BlockTriangular id) (i : m) : ∑' (n : ℕ), ((↑n.factorial)⁻¹ • A ^ n) i i = ∑' (n : ℕ), (↑n.factorial)⁻¹ • A i i ^ n

The diagonal of the matrix exponential series equals the scalar exponential series

theorem Matrix.diag_exp_of_blockTriangular_id {𝕂 : Type u_1} {m : Type u_2} [RCLike 𝕂] [Fintype m] [LinearOrder m] {A : Matrix m m 𝕂} (hA : A.BlockTriangular id) : (NormedSpace.exp 𝕂 A).diag = fun (i : m) => NormedSpace.exp 𝕂 (A i i)

The diagonal of the exponential of an upper-triangular matrix A consists of the exponentials of the diagonal entries of A.

theorem Matrix.det_exp_of_blockTriangular_id {𝕂 : Type u_1} {m : Type u_2} [RCLike 𝕂] [Fintype m] [LinearOrder m] {A : Matrix m m 𝕂} (hA : A.BlockTriangular id) : (NormedSpace.exp 𝕂 A).det = NormedSpace.exp 𝕂 A.trace

Lie's trace formula for upper triangular matrices.

theorem Matrix.trace_unitary_conj {𝕂 : Type u_1} {m : Type u_2} [RCLike 𝕂] [Fintype m] [LinearOrder m] (A : Matrix m m 𝕂) (U : ↥(unitaryGroup m 𝕂)) : (↑U * A * star ↑U).trace = A.trace

The trace is invariant under unitary conjugation.

theorem Matrix.det_unitary_conj {𝕂 : Type u_1} {m : Type u_2} [RCLike 𝕂] [Fintype m] [LinearOrder m] (A : Matrix m m 𝕂) (U : ↥(unitaryGroup m 𝕂)) : (↑U * A * star ↑U).det = A.det

The determinant is invariant under unitary conjugation.

theorem Matrix.exp_unitary_conj {𝕂 : Type u_1} {m : Type u_2} [RCLike 𝕂] [Fintype m] [LinearOrder m] (A : Matrix m m 𝕂) (U : ↥(unitaryGroup m 𝕂)) : NormedSpace.exp 𝕂 (↑U * A * star ↑U) = ↑U * NormedSpace.exp 𝕂 A * star ↑U

The exponential of a matrix commutes with unitary conjugation.

theorem Matrix.det_exp_unitary_conj {𝕂 : Type u_1} {m : Type u_2} [RCLike 𝕂] [Fintype m] [LinearOrder m] (A : Matrix m m 𝕂) (U : ↥(unitaryGroup m 𝕂)) : (NormedSpace.exp 𝕂 (↑U * A * star ↑U)).det = (NormedSpace.exp 𝕂 A).det

theorem Matrix.det_exp {𝕂 : Type u_4} {m : Type u_5} [RCLike 𝕂] [IsAlgClosed 𝕂] [Fintype m] [LinearOrder m] (A : Matrix m m 𝕂) : (NormedSpace.exp 𝕂 A).det = NormedSpace.exp 𝕂 A.trace

The determinant of the exponential of a matrix is the exponential of its trace. This is also known as Lie's trace formula.

theorem Matrix.map_tsum {α : Type u_4} {β : Type u_5} {m : Type u_6} {n : Type u_7} [AddCommMonoid α] [AddCommMonoid β] [TopologicalSpace α] [TopologicalSpace β] [T2Space β] (f : α →+ β) (hf : Continuous ⇑f) {s : ℕ → Matrix m n α} (hs : Summable s) : (∑' (k : ℕ), s k).map ⇑f = ∑' (k : ℕ), (s k).map ⇑f

theorem Matrix.map_pow {α : Type u_4} {β : Type u_5} {m : Type u_6} [Fintype m] [DecidableEq m] [Semiring α] [Semiring β] (f : α →+* β) (A : Matrix m m α) (k : ℕ) : (A ^ k).map ⇑f = A.map ⇑f ^ k

theorem NormedSpace.exp_map_algebraMap {n : Type u_1} [Fintype n] [DecidableEq n] (A : Matrix n n ℝ) : (exp ℝ A).map ⇑(algebraMap ℝ ℂ) = exp ℂ (A.map ⇑(algebraMap ℝ ℂ))

theorem Matrix.det_exp_real {n : Type u_1} [Fintype n] [LinearOrder n] (A : Matrix n n ℝ) : (NormedSpace.exp ℝ A).det = Real.exp A.trace

Lie's trace formula over ℝ: det(exp(A)) = exp(tr(A)) for any real matrix A. This is proved by transferring the result from ℂ using the naturality of polynomial identities.