mathlib3 documentation

analysis.normed_space.matrix_exponential

Lemmas about the matrix exponential #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

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.normed_add_comm_group, matrix.frobenius_normed_add_comm_group, matrix.linfty_op_normed_add_comm_group), 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.

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'

Implementation notes #

This file runs into some sharp edges on typeclass search in lean 3, especially regarding pi types. To work around this, we copy a handful of instances for when lean can't find them by itself. Hopefully we will be able to remove these in Lean 4.

TODO #

Show that matrix.det (exp 𝕂 A) = exp 𝕂 (matrix.trace A)

References #

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

@[protected, instance]

def function.topological_ring (I : Type u_1) (R : Type u_2) [non_unital_ring R] [topological_space R] [topological_ring R] :

topological_ring (I → R)

A special case of pi.topological_ring for when R is not dependently typed.

@[protected, instance]

def function.algebra_ring (I : Type u_1) {R : Type u_2} (A : Type u_3) [comm_semiring R] [ring A] [algebra R A] :

algebra R (I → A)

A special case of function.algebra for when A is a ring not a semiring

Equations

function.algebra_ring I A = pi.algebra I (λ (ᾰ : I), A)

@[protected, instance]

def pi.matrix_algebra (I : Type u_1) (R : Type u_2) (A : Type u_3) (m : I → Type u_4) [comm_semiring R] [semiring A] [algebra R A] [Π (i : I), fintype (m i)] [Π (i : I), decidable_eq (m i)] :

algebra R (Π (i : I), matrix (m i) (m i) A)

A special case of pi.algebra for when f = λ i, matrix (m i) (m i) A.

Equations

pi.matrix_algebra I R A m = pi.algebra I (λ (i : I), matrix (m i) (m i) A)

@[protected, instance]

def pi.matrix_topological_ring (I : Type u_1) (A : Type u_2) (m : I → Type u_3) [ring A] [topological_space A] [topological_ring A] [Π (i : I), fintype (m i)] :

topological_ring (Π (i : I), matrix (m i) (m i) A)

A special case of pi.topological_ring for when f = λ i, matrix (m i) (m i) A.

theorem matrix.exp_diagonal (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [fintype m] [decidable_eq m] [field 𝕂] [ring 𝔸] [topological_space 𝔸] [topological_ring 𝔸] [algebra 𝕂 𝔸] [t2_space 𝔸] (v : m → 𝔸) :

exp 𝕂 (matrix.diagonal v) = matrix.diagonal (exp 𝕂 v)

theorem matrix.exp_block_diagonal (𝕂 : Type u_1) {m : Type u_2} {n : Type u_3} {𝔸 : Type u_6} [fintype m] [decidable_eq m] [fintype n] [decidable_eq n] [field 𝕂] [ring 𝔸] [topological_space 𝔸] [topological_ring 𝔸] [algebra 𝕂 𝔸] [t2_space 𝔸] (v : m → matrix n n 𝔸) :

exp 𝕂 (matrix.block_diagonal v) = matrix.block_diagonal (exp 𝕂 v)

theorem matrix.exp_block_diagonal' (𝕂 : Type u_1) {m : Type u_2} {n' : m → Type u_5} {𝔸 : Type u_6} [fintype m] [decidable_eq m] [Π (i : m), fintype (n' i)] [Π (i : m), decidable_eq (n' i)] [field 𝕂] [ring 𝔸] [topological_space 𝔸] [topological_ring 𝔸] [algebra 𝕂 𝔸] [t2_space 𝔸] (v : Π (i : m), matrix (n' i) (n' i) 𝔸) :

exp 𝕂 (matrix.block_diagonal' v) = matrix.block_diagonal' (exp 𝕂 v)

theorem matrix.exp_conj_transpose (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [fintype m] [decidable_eq m] [field 𝕂] [ring 𝔸] [topological_space 𝔸] [topological_ring 𝔸] [algebra 𝕂 𝔸] [t2_space 𝔸] [star_ring 𝔸] [has_continuous_star 𝔸] (A : matrix m m 𝔸) :

exp 𝕂 A.conj_transpose = (exp 𝕂 A).conj_transpose

theorem matrix.is_hermitian.exp (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [fintype m] [decidable_eq m] [field 𝕂] [ring 𝔸] [topological_space 𝔸] [topological_ring 𝔸] [algebra 𝕂 𝔸] [t2_space 𝔸] [star_ring 𝔸] [has_continuous_star 𝔸] {A : matrix m m 𝔸} (h : A.is_hermitian) :

(exp 𝕂 A).is_hermitian

theorem matrix.exp_transpose (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [fintype m] [decidable_eq m] [field 𝕂] [comm_ring 𝔸] [topological_space 𝔸] [topological_ring 𝔸] [algebra 𝕂 𝔸] [t2_space 𝔸] (A : matrix m m 𝔸) :

exp 𝕂 A.transpose = (exp 𝕂 A).transpose

theorem matrix.is_symm.exp (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [fintype m] [decidable_eq m] [field 𝕂] [comm_ring 𝔸] [topological_space 𝔸] [topological_ring 𝔸] [algebra 𝕂 𝔸] [t2_space 𝔸] {A : matrix m m 𝔸} (h : A.is_symm) :

(exp 𝕂 A).is_symm

theorem matrix.exp_add_of_commute (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [is_R_or_C 𝕂] [fintype m] [decidable_eq m] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (A B : matrix m m 𝔸) (h : commute A B) :

exp 𝕂 (A + B) = (exp 𝕂 A).mul (exp 𝕂 B)

theorem matrix.exp_sum_of_commute (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [is_R_or_C 𝕂] [fintype m] [decidable_eq m] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] {ι : Type u_3} (s : finset ι) (f : ι → matrix m m 𝔸) (h : ↑s.pairwise (λ (i j : ι), commute (f i) (f j))) :

exp 𝕂 (s.sum (λ (i : ι), f i)) = s.noncomm_prod (λ (i : ι), exp 𝕂 (f i)) _

theorem matrix.exp_nsmul (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [is_R_or_C 𝕂] [fintype m] [decidable_eq m] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (n : ℕ) (A : matrix m m 𝔸) :

exp 𝕂 (n • A) = exp 𝕂 A ^ n

theorem matrix.is_unit_exp (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [is_R_or_C 𝕂] [fintype m] [decidable_eq m] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (A : matrix m m 𝔸) :

is_unit (exp 𝕂 A)

theorem matrix.exp_units_conj (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [is_R_or_C 𝕂] [fintype m] [decidable_eq m] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (U : (matrix m m 𝔸)ˣ) (A : matrix m m 𝔸) :

exp 𝕂 ((↑U.mul A).mul ↑U⁻¹) = (↑U.mul (exp 𝕂 A)).mul ↑U⁻¹

theorem matrix.exp_units_conj' (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [is_R_or_C 𝕂] [fintype m] [decidable_eq m] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (U : (matrix m m 𝔸)ˣ) (A : matrix m m 𝔸) :

exp 𝕂 ((↑U⁻¹.mul A).mul ↑U) = (↑U⁻¹.mul (exp 𝕂 A)).mul ↑U

theorem matrix.exp_neg (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [is_R_or_C 𝕂] [fintype m] [decidable_eq m] [normed_comm_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (A : matrix m m 𝔸) :

exp 𝕂 (-A) = (exp 𝕂 A)⁻¹

theorem matrix.exp_zsmul (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [is_R_or_C 𝕂] [fintype m] [decidable_eq m] [normed_comm_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (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} [is_R_or_C 𝕂] [fintype m] [decidable_eq m] [normed_comm_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (U A : matrix m m 𝔸) (hy : is_unit U) :

exp 𝕂 ((U.mul A).mul U⁻¹) = (U.mul (exp 𝕂 A)).mul U⁻¹

theorem matrix.exp_conj' (𝕂 : Type u_1) {m : Type u_2} {𝔸 : Type u_6} [is_R_or_C 𝕂] [fintype m] [decidable_eq m] [normed_comm_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] (U A : matrix m m 𝔸) (hy : is_unit U) :

exp 𝕂 ((U⁻¹.mul A).mul U) = (U⁻¹.mul (exp 𝕂 A)).mul U