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 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 #

References #

theorem Matrix.exp_diagonal (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [Fintype m] [DecidableEq m] [Field 𝕂] [Ring 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] [Algebra 𝕂 𝔸] [T2Space 𝔸] (v : m β†’ 𝔸) :
theorem Matrix.exp_blockDiagonal (𝕂 : Type u_1) {m : Type u_2} {n : Type u_3} {𝔸 : Type u_6} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] [Field 𝕂] [Ring 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] [Algebra 𝕂 𝔸] [T2Space 𝔸] (v : m β†’ Matrix n n 𝔸) :
theorem Matrix.exp_blockDiagonal' (𝕂 : Type u_1) {m : Type u_2} {n' : m β†’ Type u_5} {𝔸 : Type u_6} [Fintype m] [DecidableEq m] [(i : m) β†’ Fintype (n' i)] [(i : m) β†’ DecidableEq (n' i)] [Field 𝕂] [Ring 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] [Algebra 𝕂 𝔸] [T2Space 𝔸] (v : (i : m) β†’ Matrix (n' i) (n' i) 𝔸) :
theorem Matrix.exp_conjTranspose (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [Fintype m] [DecidableEq m] [Field 𝕂] [Ring 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] [Algebra 𝕂 𝔸] [T2Space 𝔸] [StarRing 𝔸] [ContinuousStar 𝔸] (A : Matrix m m 𝔸) :
NormedSpace.exp 𝕂 A.conjTranspose = (NormedSpace.exp 𝕂 A).conjTranspose
theorem Matrix.IsHermitian.exp (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [Fintype m] [DecidableEq m] [Field 𝕂] [Ring 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] [Algebra 𝕂 𝔸] [T2Space 𝔸] [StarRing 𝔸] [ContinuousStar 𝔸] {A : Matrix m m 𝔸} (h : A.IsHermitian) :
(NormedSpace.exp 𝕂 A).IsHermitian
theorem Matrix.exp_transpose (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [Fintype m] [DecidableEq m] [Field 𝕂] [CommRing 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] [Algebra 𝕂 𝔸] [T2Space 𝔸] (A : Matrix m m 𝔸) :
NormedSpace.exp 𝕂 A.transpose = (NormedSpace.exp 𝕂 A).transpose
theorem Matrix.IsSymm.exp (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [Fintype m] [DecidableEq m] [Field 𝕂] [CommRing 𝔸] [TopologicalSpace 𝔸] [TopologicalRing 𝔸] [Algebra 𝕂 𝔸] [T2Space 𝔸] {A : Matrix m m 𝔸} (h : A.IsSymm) :
(NormedSpace.exp 𝕂 A).IsSymm
theorem Matrix.exp_add_of_commute (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [RCLike 𝕂] [Fintype m] [DecidableEq m] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (A : Matrix m m 𝔸) (B : Matrix m m 𝔸) (h : Commute A B) :
NormedSpace.exp 𝕂 (A + B) = NormedSpace.exp 𝕂 A * NormedSpace.exp 𝕂 B
theorem Matrix.exp_sum_of_commute (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [RCLike 𝕂] [Fintype m] [DecidableEq m] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] {ΞΉ : Type u_7} (s : Finset ΞΉ) (f : ΞΉ β†’ Matrix m m 𝔸) (h : (↑s).Pairwise fun (i j : ΞΉ) => Commute (f i) (f j)) :
NormedSpace.exp 𝕂 (βˆ‘ i ∈ s, f i) = s.noncommProd (fun (i : ΞΉ) => NormedSpace.exp 𝕂 (f i)) β‹―
theorem Matrix.exp_nsmul (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [RCLike 𝕂] [Fintype m] [DecidableEq m] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (n : β„•) (A : Matrix m m 𝔸) :
NormedSpace.exp 𝕂 (n β€’ A) = NormedSpace.exp 𝕂 A ^ n
theorem Matrix.isUnit_exp (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [RCLike 𝕂] [Fintype m] [DecidableEq m] [NormedRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (A : Matrix m m 𝔸) :
IsUnit (NormedSpace.exp 𝕂 A)
theorem Matrix.exp_units_conj (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [RCLike 𝕂] [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' (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [RCLike 𝕂] [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 (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [RCLike 𝕂] [Fintype m] [DecidableEq m] [NormedCommRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (A : Matrix m m 𝔸) :
NormedSpace.exp 𝕂 (-A) = (NormedSpace.exp 𝕂 A)⁻¹
theorem Matrix.exp_zsmul (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [RCLike 𝕂] [Fintype m] [DecidableEq m] [NormedCommRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (z : β„€) (A : Matrix m m 𝔸) :
NormedSpace.exp 𝕂 (z β€’ A) = NormedSpace.exp 𝕂 A ^ z
theorem Matrix.exp_conj (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [RCLike 𝕂] [Fintype m] [DecidableEq m] [NormedCommRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (U : Matrix m m 𝔸) (A : Matrix m m 𝔸) (hy : IsUnit U) :
NormedSpace.exp 𝕂 (U * A * U⁻¹) = U * NormedSpace.exp 𝕂 A * U⁻¹
theorem Matrix.exp_conj' (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [RCLike 𝕂] [Fintype m] [DecidableEq m] [NormedCommRing 𝔸] [NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (U : Matrix m m 𝔸) (A : Matrix m m 𝔸) (hy : IsUnit U) :
NormedSpace.exp 𝕂 (U⁻¹ * A * U) = U⁻¹ * NormedSpace.exp 𝕂 A * U