Documentation

Mathlib.Analysis.Normed.Algebra.MatrixExponential

Lemmas about the matrix exponential #

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

Lemmas like NormedSpace.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 attribute [local instance], then the usual lemmas about NormedSpace.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 NormedSpace.exp, but hide the requirement for a norm inside the proof.

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:

TODO #

Show that Matrix.det (NormedSpace.exp A) = NormedSpace.exp (Matrix.trace A)

References #

https://en.wikipedia.org/wiki/Matrix_exponential

theorem Matrix.exp_diagonal {m : Type u_1} {𝔸 : Type u_4} [Fintype m] [DecidableEq m] [Ring 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] [T2Space 𝔸] [Algebra ℚ 𝔸] (v : m → 𝔸) :

NormedSpace.exp (diagonal v) = diagonal (NormedSpace.exp v)

theorem Matrix.exp_blockDiagonal {m : Type u_1} {n : Type u_2} {𝔸 : Type u_4} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] [Ring 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] [T2Space 𝔸] [Algebra ℚ 𝔸] (v : m → Matrix n n 𝔸) :

NormedSpace.exp (blockDiagonal v) = blockDiagonal (NormedSpace.exp v)

theorem Matrix.exp_blockDiagonal' {m : Type u_1} {n' : m → Type u_3} {𝔸 : Type u_4} [Fintype m] [DecidableEq m] [(i : m) → Fintype (n' i)] [(i : m) → DecidableEq (n' i)] [Ring 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] [T2Space 𝔸] [Algebra ℚ 𝔸] (v : (i : m) → Matrix (n' i) (n' i) 𝔸) :

NormedSpace.exp (blockDiagonal' v) = blockDiagonal' (NormedSpace.exp v)

theorem Matrix.exp_conjTranspose {m : Type u_1} {𝔸 : Type u_4} [Fintype m] [DecidableEq m] [Ring 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] [T2Space 𝔸] [StarRing 𝔸] [ContinuousStar 𝔸] (A : Matrix m m 𝔸) :

NormedSpace.exp A.conjTranspose = (NormedSpace.exp A).conjTranspose

theorem Matrix.IsHermitian.exp {m : Type u_1} {𝔸 : Type u_4} [Fintype m] [DecidableEq m] [Ring 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] [T2Space 𝔸] [StarRing 𝔸] [ContinuousStar 𝔸] {A : Matrix m m 𝔸} (h : A.IsHermitian) :

(NormedSpace.exp A).IsHermitian

theorem Matrix.exp_transpose {m : Type u_1} {𝔸 : Type u_4} [Fintype m] [DecidableEq m] [CommRing 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] [Algebra ℚ 𝔸] [T2Space 𝔸] (A : Matrix m m 𝔸) :

NormedSpace.exp A.transpose = (NormedSpace.exp A).transpose

theorem Matrix.IsSymm.exp {m : Type u_1} {𝔸 : Type u_4} [Fintype m] [DecidableEq m] [CommRing 𝔸] [TopologicalSpace 𝔸] [IsTopologicalRing 𝔸] [Algebra ℚ 𝔸] [T2Space 𝔸] {A : Matrix m m 𝔸} (h : A.IsSymm) :

(NormedSpace.exp A).IsSymm

theorem Matrix.exp_add_of_commute {m : Type u_1} {𝔸 : Type u_4} [Fintype m] [DecidableEq m] [NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (A B : Matrix m m 𝔸) (h : Commute A B) :

NormedSpace.exp (A + B) = NormedSpace.exp A * NormedSpace.exp B

theorem Matrix.exp_sum_of_commute {m : Type u_1} {𝔸 : Type u_4} [Fintype m] [DecidableEq m] [NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] {ι : Type u_5} (s : Finset ι) (f : ι → Matrix m m 𝔸) (h : (↑s).Pairwise (Function.onFun Commute f)) :

NormedSpace.exp (∑ i ∈ s, f i) = s.noncommProd (fun (i : ι) => NormedSpace.exp (f i)) ⋯

theorem Matrix.exp_nsmul {m : Type u_1} {𝔸 : Type u_4} [Fintype m] [DecidableEq m] [NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (n : ℕ) (A : Matrix m m 𝔸) :

NormedSpace.exp (n • A) = NormedSpace.exp A ^ n

theorem Matrix.isUnit_exp {m : Type u_1} {𝔸 : Type u_4} [Fintype m] [DecidableEq m] [NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (A : Matrix m m 𝔸) :

IsUnit (NormedSpace.exp A)

theorem Matrix.exp_units_conj {m : Type u_1} {𝔸 : Type u_4} [Fintype m] [DecidableEq m] [NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (U : (Matrix m m 𝔸)ˣ) (A : Matrix m m 𝔸) :

NormedSpace.exp (↑U * A * ↑U⁻¹) = ↑U * NormedSpace.exp A * ↑U⁻¹

theorem Matrix.exp_units_conj' {m : Type u_1} {𝔸 : Type u_4} [Fintype m] [DecidableEq m] [NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (U : (Matrix m m 𝔸)ˣ) (A : Matrix m m 𝔸) :

NormedSpace.exp (↑U⁻¹ * A * ↑U) = ↑U⁻¹ * NormedSpace.exp A * ↑U

theorem Matrix.exp_neg {m : Type u_1} {𝔸 : Type u_4} [Fintype m] [DecidableEq m] [NormedCommRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (A : Matrix m m 𝔸) :

NormedSpace.exp (-A) = (NormedSpace.exp A)⁻¹

theorem Matrix.exp_zsmul {m : Type u_1} {𝔸 : Type u_4} [Fintype m] [DecidableEq m] [NormedCommRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (z : ℤ) (A : Matrix m m 𝔸) :

NormedSpace.exp (z • A) = NormedSpace.exp A ^ z

theorem Matrix.exp_conj {m : Type u_1} {𝔸 : Type u_4} [Fintype m] [DecidableEq m] [NormedCommRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (U A : Matrix m m 𝔸) (hy : IsUnit U) :

NormedSpace.exp (U * A * U⁻¹) = U * NormedSpace.exp A * U⁻¹

theorem Matrix.exp_conj' {m : Type u_1} {𝔸 : Type u_4} [Fintype m] [DecidableEq m] [NormedCommRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (U A : Matrix m m 𝔸) (hy : IsUnit U) :

NormedSpace.exp (U⁻¹ * A * U) = U⁻¹ * NormedSpace.exp A * U