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:

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 #

References #

@[protected, instance]

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
@[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
@[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 𝔸) :
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 𝔸) :
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) 𝔸) :
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 𝔸) :
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