mathlib documentation

analysis.normed_space.matrix_exponential

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 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]
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
@[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 β†’ 𝔸) :
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 𝔸) :
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 𝔸) :
exp 𝕂 A.conj_transpose = (exp 𝕂 A).conj_transpose
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.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 : βˆ€ (i : ΞΉ), i ∈ s β†’ βˆ€ (j : ΞΉ), j ∈ s β†’ 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