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 ๐”ธ) :
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) :
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) :