# Documentation

Mathlib.Analysis.NormedSpace.MatrixExponential

# Lemmas about the matrix exponential #

In this file, we provide results about exp on Matrixs over a topological or normed algebra. Note that generic results over all topological spaces such as exp_zero can be used on matrices without issue, so are not repeated here. The topological results specific to matrices are:

• Matrix.exp_transpose
• Matrix.exp_conjTranspose
• Matrix.exp_diagonal
• Matrix.exp_blockDiagonal
• Matrix.exp_blockDiagonal'

Lemmas like exp_add_of_commute require a canonical norm on the type; while there are multiple sensible choices for the norm of a Matrix (Matrix.normedAddCommGroup, Matrix.frobeniusNormedAddCommGroup, Matrix.linftyOpNormedAddCommGroup), none of them are canonical. In an application where a particular norm is chosen using local attribute [instance], then the usual lemmas about exp are fine. When choosing a norm is undesirable, the results in this file can be used.

In this file, we copy across the lemmas about exp, but hide the requirement for a norm inside the proof.

• Matrix.exp_add_of_commute
• Matrix.exp_sum_of_commute
• Matrix.exp_nsmul
• Matrix.isUnit_exp
• Matrix.exp_units_conj
• Matrix.exp_units_conj'

Additionally, we prove some results about matrix.has_inv and matrix.div_inv_monoid, as the results for general rings are instead stated about Ring.inverse:

• Matrix.exp_neg
• Matrix.exp_zsmul
• Matrix.exp_conj
• Matrix.exp_conj'

## TODO #

• Show that Matrix.det (exp ๐ A) = exp ๐ (Matrix.trace A)

## References #

• https://en.wikipedia.org/wiki/Matrix_exponential
theorem Matrix.exp_diagonal (๐ : Type u_1) {m : Type u_2} {๐ธ : Type u_6} [] [] [Field ๐] [Ring ๐ธ] [TopologicalSpace ๐ธ] [TopologicalRing ๐ธ] [Algebra ๐ ๐ธ] [T2Space ๐ธ] (v : m โ ๐ธ) :
exp ๐ () = Matrix.diagonal (exp ๐ v)
theorem Matrix.exp_blockDiagonal (๐ : Type u_1) {m : Type u_2} {n : Type u_3} {๐ธ : Type u_6} [] [] [] [] [Field ๐] [Ring ๐ธ] [TopologicalSpace ๐ธ] [TopologicalRing ๐ธ] [Algebra ๐ ๐ธ] [T2Space ๐ธ] (v : m โ Matrix n n ๐ธ) :
exp ๐ () = Matrix.blockDiagonal (exp ๐ v)
theorem Matrix.exp_blockDiagonal' (๐ : Type u_1) {m : Type u_2} {n' : m โ Type u_5} {๐ธ : Type u_6} [] [] [(i : m) โ Fintype (n' i)] [(i : m) โ DecidableEq (n' i)] [Field ๐] [Ring ๐ธ] [TopologicalSpace ๐ธ] [TopologicalRing ๐ธ] [Algebra ๐ ๐ธ] [T2Space ๐ธ] (v : (i : m) โ Matrix (n' i) (n' i) ๐ธ) :
exp ๐ () = Matrix.blockDiagonal' (exp ๐ v)
theorem Matrix.exp_conjTranspose (๐ : Type u_1) {m : Type u_2} {๐ธ : Type u_6} [] [] [Field ๐] [Ring ๐ธ] [TopologicalSpace ๐ธ] [TopologicalRing ๐ธ] [Algebra ๐ ๐ธ] [T2Space ๐ธ] [StarRing ๐ธ] [ContinuousStar ๐ธ] (A : Matrix m m ๐ธ) :
exp ๐ () = Matrix.conjTranspose (exp ๐ A)
theorem Matrix.IsHermitian.exp (๐ : Type u_1) {m : Type u_2} {๐ธ : Type u_6} [] [] [Field ๐] [Ring ๐ธ] [TopologicalSpace ๐ธ] [TopologicalRing ๐ธ] [Algebra ๐ ๐ธ] [T2Space ๐ธ] [StarRing ๐ธ] [ContinuousStar ๐ธ] {A : Matrix m m ๐ธ} (h : ) :
Matrix.IsHermitian (exp ๐ A)
theorem Matrix.exp_transpose (๐ : Type u_1) {m : Type u_2} {๐ธ : Type u_6} [] [] [Field ๐] [CommRing ๐ธ] [TopologicalSpace ๐ธ] [TopologicalRing ๐ธ] [Algebra ๐ ๐ธ] [T2Space ๐ธ] (A : Matrix m m ๐ธ) :
exp ๐ () = Matrix.transpose (exp ๐ A)
theorem Matrix.IsSymm.exp (๐ : Type u_1) {m : Type u_2} {๐ธ : Type u_6} [] [] [Field ๐] [CommRing ๐ธ] [TopologicalSpace ๐ธ] [TopologicalRing ๐ธ] [Algebra ๐ ๐ธ] [T2Space ๐ธ] {A : Matrix m m ๐ธ} (h : ) :
Matrix.IsSymm (exp ๐ A)
theorem Matrix.exp_add_of_commute (๐ : Type u_1) {m : Type u_2} {๐ธ : Type u_6} [IsROrC ๐] [] [] [NormedRing ๐ธ] [NormedAlgebra ๐ ๐ธ] [CompleteSpace ๐ธ] (A : Matrix m m ๐ธ) (B : Matrix m m ๐ธ) (h : Commute A B) :
exp ๐ (A + B) = exp ๐ A * exp ๐ B
theorem Matrix.exp_sum_of_commute (๐ : Type u_1) {m : Type u_2} {๐ธ : Type u_6} [IsROrC ๐] [] [] [NormedRing ๐ธ] [NormedAlgebra ๐ ๐ธ] [CompleteSpace ๐ธ] {ฮน : Type u_7} (s : Finset ฮน) (f : ฮน โ Matrix m m ๐ธ) (h : Set.Pairwise โs fun i j => Commute (f i) (f j)) :
exp ๐ (Finset.sum s fun i => f i) = Finset.noncommProd s (fun i => exp ๐ (f i)) (_ : โ (i : ฮน), i โ โs โ โ (j : ฮน), j โ โs โ i โ  j โ Commute (exp ๐ (f i)) (exp ๐ (f j)))
theorem Matrix.exp_nsmul (๐ : Type u_1) {m : Type u_2} {๐ธ : Type u_6} [IsROrC ๐] [] [] [NormedRing ๐ธ] [NormedAlgebra ๐ ๐ธ] [CompleteSpace ๐ธ] (n : โ) (A : Matrix m m ๐ธ) :
exp ๐ (n โข A) = exp ๐ A ^ n
theorem Matrix.isUnit_exp (๐ : Type u_1) {m : Type u_2} {๐ธ : Type u_6} [IsROrC ๐] [] [] [NormedRing ๐ธ] [NormedAlgebra ๐ ๐ธ] [CompleteSpace ๐ธ] (A : Matrix m m ๐ธ) :
IsUnit (exp ๐ A)
theorem Matrix.exp_units_conj (๐ : Type u_1) {m : Type u_2} {๐ธ : Type u_6} [IsROrC ๐] [] [] [NormedRing ๐ธ] [NormedAlgebra ๐ ๐ธ] [CompleteSpace ๐ธ] (U : (Matrix m m ๐ธ)หฃ) (A : Matrix m m ๐ธ) :
exp ๐ (โU * A * โ) = โU * exp ๐ A * โ
theorem Matrix.exp_units_conj' (๐ : Type u_1) {m : Type u_2} {๐ธ : Type u_6} [IsROrC ๐] [] [] [NormedRing ๐ธ] [NormedAlgebra ๐ ๐ธ] [CompleteSpace ๐ธ] (U : (Matrix m m ๐ธ)หฃ) (A : Matrix m m ๐ธ) :
exp ๐ (โ * A * โU) = โ * exp ๐ A * โU
theorem Matrix.exp_neg (๐ : Type u_1) {m : Type u_2} {๐ธ : Type u_6} [IsROrC ๐] [] [] [NormedCommRing ๐ธ] [NormedAlgebra ๐ ๐ธ] [CompleteSpace ๐ธ] (A : Matrix m m ๐ธ) :
exp ๐ (-A) = (exp ๐ A)โปยน
theorem Matrix.exp_zsmul (๐ : Type u_1) {m : Type u_2} {๐ธ : Type u_6} [IsROrC ๐] [] [] [NormedCommRing ๐ธ] [NormedAlgebra ๐ ๐ธ] [CompleteSpace ๐ธ] (z : โค) (A : Matrix m m ๐ธ) :
exp ๐ (z โข A) = exp ๐ A ^ z
theorem Matrix.exp_conj (๐ : Type u_1) {m : Type u_2} {๐ธ : Type u_6} [IsROrC ๐] [] [] [NormedCommRing ๐ธ] [NormedAlgebra ๐ ๐ธ] [CompleteSpace ๐ธ] (U : Matrix m m ๐ธ) (A : Matrix m m ๐ธ) (hy : ) :
exp ๐ (U * A * ) = U * exp ๐ A *
theorem Matrix.exp_conj' (๐ : Type u_1) {m : Type u_2} {๐ธ : Type u_6} [IsROrC ๐] [] [] [NormedCommRing ๐ธ] [NormedAlgebra ๐ ๐ธ] [CompleteSpace ๐ธ] (U : Matrix m m ๐ธ) (A : Matrix m m ๐ธ) (hy : ) :
exp ๐ ( * A * U) = * exp ๐ A * U