Matrix exponential

TheoremIntertwining passes to the exponential#βœ“fully proved

If A * X = X * B for a rectangular matrix X, then exp A * X = X * exp B.

theorem exp_mul_eq_mul_exp_of_mul_eq {A : Matrix m m 𝕂} {B : Matrix n n 𝕂} {X : Matrix m n 𝕂}
    (h : A * X = X * B) : NormedSpace.exp A * X = X * NormedSpace.exp B
Used by 3
Used byTime-t marginal sums to one Β· Consistency Β· The time-t marginal of the partition-valued coalescent

TheoremDeterminant of the matrix exponential#βœ“fully proved

For every complex square matrix \(A\) indexed by a finite set, \(\det(e^A) = e^{\operatorname{tr} A}\), where \(e^A\) is the matrix exponential. This identity is sometimes called Jacobi's formula.

Proof: the three cases of B. C. Hall, An Elementary Introduction to Groups and Representations, https://arxiv.org/abs/math-ph/0005032, Theorem 3.10. The Jordan-Chevalley decomposition writes \(A = N + S\) with \(N\) nilpotent, \(S\) semisimple and \(NS = SN\), so \(e^A = e^N e^S\). Diagonalizing \(S\) gives \(\det(e^S) = e^{\operatorname{tr} S}\). For the nilpotent part, where Hall uses a strictly upper-triangular form, \(e^N - I\) is nilpotent, so \(\det(e^N) = 1\), while \(\operatorname{tr} N = 0\).

theorem matrix_det_exp_eq_exp_trace (A : Matrix n n β„‚) :
    Matrix.det (NormedSpace.exp A) = Complex.exp (Matrix.trace A)
Sources
  • B. C. Hall, Lie Groups, Lie Algebras, and Representations, 2nd ed., Springer (2015), Proposition 2.23.

TheoremExponential of a nilpotent matrix#βœ“fully proved

If \(A\) is a nilpotent complex square matrix indexed by a finite set, then there is a natural number \(m\) such that \(e^A = \sum_{k=0}^{m-1} \frac{1}{k!} A^k\), where \(e^A\) is the matrix exponential.

Proof: if \(A^m = 0\), every term of the exponential series from index \(m\) on vanishes.

theorem matrix_exp_eq_sum_of_isNilpotent (A : Matrix n n β„‚) (h : IsNilpotent A) :
    βˆƒ m : β„•, NormedSpace.exp A = βˆ‘ k ∈ Finset.range m, (Nat.factorial k : β„‚)⁻¹ β€’ A ^ k
Sources
  • R. A. Horn and C. R. Johnson, Matrix Analysis, 2nd ed., Cambridge University Press (2013), Section 3.2.
3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.