Some obvious lemmas on matrices #
This file includes some necessary and obvious results for matrices,
such as matrix.mul_vec_eq.
We also show that the trace of a symmetric matrix is equal to the sum of its eigenvalues.
theorem
matrix.mul_vec_eq
{R : Type u_1}
{m : Type u_2}
{n : Type u_3}
[comm_semiring R]
[fintype n]
[decidable_eq n]
(a b : matrix m n R) :
two matrices $a,b \in M_n$ are equal iff for all vectors $c \in \mathbb{k}^n$ we have $a c = b c$, essentially, treat them as linear maps on $\mathbb{k}^n$ so you can have extentionality with vectors
theorem
matrix.vec_mul_vec_ne_zero
{R : Type u_1}
{n : Type u_2}
[semiring R]
[no_zero_divisors R]
{α β : n → R}
(hα : α ≠ 0)
(hβ : β ≠ 0) :
matrix.vec_mul_vec α β ≠ 0
the outer product of two nonzero vectors is nonzero
theorem
matrix.vec_mul_vec_transpose
{R : Type u_1}
{n : Type u_2}
[comm_semiring R]
(x y : n → R) :
(matrix.vec_mul_vec x y).transpose = matrix.vec_mul_vec y x
the transpose of vec_mul_vec x y is simply vec_mul_vec y x
theorem
matrix.one_eq_sum_std_matrix
{n : Type u_1}
{R : Type u_2}
[comm_semiring R]
[fintype n]
[decidable_eq n] :
1 = finset.univ.sum (λ (r : n), matrix.std_basis_matrix r r 1)
the identity written as a sum of the standard basis
theorem
matrix.kronecker.trace
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{n : Type u_4}
[fintype n]
(A B : matrix n n 𝕜) :
(matrix.kronecker_map has_mul.mul A B).trace = A.trace * B.trace
$\textnormal{Tr}(A\otimes_k B)=\textnormal{Tr}(A)\textnormal{Tr}(B)$
theorem
matrix.is_hermitian.trace_eq
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{n : Type u_4}
[fintype n]
[decidable_eq n]
[decidable_eq 𝕜]
{A : matrix n n 𝕜}
(hA : A.is_hermitian) :
A.trace = finset.univ.sum (λ (i : n), ↑(hA.eigenvalues i))
the trace of a Hermitian matrix is the sum of its eigenvalues
theorem
linear_map.is_symmetric.eigenvalue_mem_spectrum
{ℍ : Type u_1}
{𝕜 : Type u_3}
[normed_add_comm_group ℍ]
[is_R_or_C 𝕜]
[inner_product_space 𝕜 ℍ]
[finite_dimensional 𝕜 ℍ]
{n : Type u_4}
[fintype n]
[decidable_eq 𝕜]
(hn : finite_dimensional.finrank 𝕜 ℍ = fintype.card n)
{A : ℍ →ₗ[𝕜] ℍ}
(hA : A.is_symmetric)
(i : fin (fintype.card n)) :
↑(hA.eigenvalues hn i) ∈ spectrum 𝕜 A
theorem
matrix.is_hermitian.eigenvalues_has_eigenvalue
{𝕜 : Type u_1}
{n : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
[decidable_eq 𝕜]
{M : matrix n n 𝕜}
(hM : M.is_hermitian)
(i : n) :
theorem
matrix.is_hermitian.has_eigenvector_eigenvector_basis
{𝕜 : Type u_1}
{n : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
[decidable_eq 𝕜]
{M : matrix n n 𝕜}
(hM : M.is_hermitian)
(i : n) :
module.End.has_eigenvector (⇑matrix.to_euclidean_lin M) ↑(hM.eigenvalues i) (⇑(hM.eigenvector_basis) i)
theorem
matrix.is_hermitian.apply_eigenvector_basis
{𝕜 : Type u_1}
{n : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
[decidable_eq n]
[decidable_eq 𝕜]
{M : matrix n n 𝕜}
(hM : M.is_hermitian)
(i : n) :
M.mul_vec (⇑(hM.eigenvector_basis) i) = hM.eigenvalues i • ⇑(hM.eigenvector_basis) i
a Hermitian matrix applied to its eigenvector basis element equals the basis element scalar-ed by its respective eigenvalue
theorem
euclidean_space.inner_eq
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
{x y : n → 𝕜} :
has_inner.inner x y = matrix.dot_product (has_star.star x) y
theorem
euclidean_space.rank_one_of_orthonormal_basis_eq_one
{n : Type u_1}
{𝕜 : Type u_2}
[is_R_or_C 𝕜]
[fintype n]
(h : orthonormal_basis n 𝕜 (euclidean_space 𝕜 n)) :
theorem
kmul_representation
{R : Type u_1}
{n₁ : Type u_2}
{n₂ : Type u_3}
[fintype n₁]
[fintype n₂]
[decidable_eq n₁]
[decidable_eq n₂]
[semiring R]
(x : matrix (n₁ × n₂) (n₁ × n₂) R) :
x = finset.univ.sum (λ (i : n₁), finset.univ.sum (λ (j : n₁), finset.univ.sum (λ (k : n₂), finset.univ.sum (λ (l : n₂), x (i, k) (j, l) • matrix.kronecker_map has_mul.mul (matrix.std_basis_matrix i j 1) (matrix.std_basis_matrix k l 1)))))
for any matrix $x\in M_{n_1 \times n_2}$, we have $$x=\sum_{i,j,k,l}x_{ik}^{jl}(e_{ij} \otimes_k e_{kl}) $$
theorem
matrix.kronecker_conj_transpose
{R : Type u_1}
{m : Type u_2}
{n : Type u_3}
[comm_semiring R]
[star_ring R]
(x : matrix n n R)
(y : matrix m m R) :
$(x \otimes_k y)^* = x^* \otimes_k y^*$
theorem
matrix.kronecker.transpose
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{n : Type u_1}
(x y : matrix n n 𝕜) :
theorem
matrix.is_hermitian.eigenvector_matrix_mem_unitary_group
{n : Type u_4}
[fintype n]
{𝕜 : Type u_1}
[is_R_or_C 𝕜]
[decidable_eq 𝕜]
[decidable_eq n]
{x : matrix n n 𝕜}
(hx : x.is_hermitian) :
theorem
matrix.unitary_group.coe_mk
{𝕜 : Type u_3}
[is_R_or_C 𝕜]
{n : Type u_4}
[fintype n]
[decidable_eq n]
(x : matrix n n 𝕜)
(hx : x ∈ matrix.unitary_group n 𝕜) :
theorem
matrix.std_basis_matrix_conj_transpose
{R : Type u_1}
{n : Type u_2}
{m : Type u_3}
[semiring R]
[star_add_monoid R]
[decidable_eq n]
[decidable_eq m]
(i : n)
(j : m)
(a : R) :
(matrix.std_basis_matrix i j a).conj_transpose = matrix.std_basis_matrix j i (has_star.star a)
theorem
matrix.std_basis_matrix.star_apply
{R : Type u_1}
{n : Type u_2}
{m : Type u_3}
[semiring R]
[star_add_monoid R]
[decidable_eq n]
[decidable_eq m]
(i k : n)
(j l : m)
(a : R) :
has_star.star (matrix.std_basis_matrix i j a k l) = matrix.std_basis_matrix j i (has_star.star a) l k
theorem
matrix.std_basis_matrix.star_apply'
{R : Type u_1}
{n : Type u_2}
{m : Type u_3}
[semiring R]
[star_add_monoid R]
[decidable_eq n]
[decidable_eq m]
(i : n)
(j : m)
(x : n × m)
(a : R) :
has_star.star (matrix.std_basis_matrix i j a x.fst x.snd) = matrix.std_basis_matrix j i (has_star.star a) x.snd x.fst
theorem
matrix.std_basis_matrix.star_one
{n : Type u_2}
{m : Type u_3}
[decidable_eq n]
[decidable_eq m]
{R : Type u_1}
[semiring R]
[star_ring R]
(i : n)
(j : m) :
(matrix.std_basis_matrix i j 1).conj_transpose = matrix.std_basis_matrix j i 1
$e_{ij}^*=e_{ji}$
theorem
matrix.trace_iff
{R : Type u_1}
{n : Type u_2}
[add_comm_monoid R]
[fintype n]
(x : matrix n n R) :
x.trace = finset.univ.sum (λ (k : n), x k k)
theorem
matrix.std_basis_matrix.mul_apply_basis
{n : Type u_2}
{m : Type u_3}
[decidable_eq n]
[decidable_eq m]
{R : Type u_1}
{p : Type u_4}
{q : Type u_5}
[semiring R]
[decidable_eq p]
[decidable_eq q]
(i x : n)
(j y : m)
(k z : p)
(l w : q) :
matrix.std_basis_matrix k l (matrix.std_basis_matrix i j 1 x y) z w = matrix.std_basis_matrix i j 1 x y * matrix.std_basis_matrix k l 1 z w
theorem
matrix.std_basis_matrix.mul_apply_basis'
{n : Type u_2}
{m : Type u_3}
[decidable_eq n]
[decidable_eq m]
{R : Type u_1}
{p : Type u_4}
{q : Type u_5}
[semiring R]
[decidable_eq p]
[decidable_eq q]
(i x : n)
(j y : m)
(k z : p)
(l w : q) :
theorem
matrix.std_basis_matrix.mul_apply
{n : Type u_2}
[decidable_eq n]
{R : Type u_1}
[fintype n]
[semiring R]
(i j k l m p : n) :
finset.univ.sum (λ (x : n × n), finset.univ.sum (λ (x_1 : n × n), finset.univ.sum (λ (x_2 : n), finset.univ.sum (λ (x_3 : n), matrix.std_basis_matrix l k (matrix.std_basis_matrix p m 1 x_1.snd x_1.fst) x.snd x.fst * matrix.std_basis_matrix i x_2 (matrix.std_basis_matrix x_3 j 1 x_1.fst x_1.snd) x.fst x.snd)))) = finset.univ.sum (λ (x : n × n), finset.univ.sum (λ (x_1 : n × n), finset.univ.sum (λ (x_2 : n), finset.univ.sum (λ (x_3 : n), ite (p = x_1.snd ∧ m = x_1.fst ∧ l = x.snd ∧ k = x.fst ∧ x_3 = x_1.fst ∧ j = x_1.snd ∧ i = x.fst ∧ x_2 = x.snd) 1 0))))
@[simp]
theorem
matrix.std_basis_matrix.sum_star_mul_self
{R : Type u_1}
{n : Type u_2}
[semiring R]
[star_add_monoid R]
[decidable_eq n]
[fintype n]
(i j : n)
(a b : R) :
finset.univ.sum (λ (k : n), finset.univ.sum (λ (l : n), finset.univ.sum (λ (m : n), finset.univ.sum (λ (p : n), matrix.std_basis_matrix i j a k l * has_star.star (matrix.std_basis_matrix i j b) m p)))) = a * has_star.star b
theorem
matrix.std_basis_matrix.sum_star_mul_self'
{n : Type u_2}
[decidable_eq n]
{R : Type u_1}
[fintype n]
[semiring R]
[star_ring R]
(i j : n) :
finset.univ.sum (λ (kl : n × n), finset.univ.sum (λ (mp : n × n), matrix.std_basis_matrix i j 1 kl.fst kl.snd * has_star.star matrix.std_basis_matrix i j 1 mp.fst mp.snd)) = 1
theorem
matrix.std_basis_matrix.mul_std_basis_matrix
{n : Type u_2}
{m : Type u_3}
[decidable_eq n]
[decidable_eq m]
{R : Type u_1}
{p : Type u_4}
[semiring R]
[decidable_eq p]
[fintype m]
(i x : n)
(j k : m)
(l y : p)
(a b : R) :
theorem
matrix.std_basis_matrix.mul_std_basis_matrix'
{n : Type u_2}
{m : Type u_3}
[decidable_eq n]
[decidable_eq m]
{R : Type u_1}
{p : Type u_4}
[fintype n]
[decidable_eq p]
[semiring R]
(i : m)
(j k : n)
(l : p) :
(matrix.std_basis_matrix i j 1).mul (matrix.std_basis_matrix k l 1) = ite (j = k) 1 0 • matrix.std_basis_matrix i l 1
theorem
linear_map.to_matrix'_mul_vec
{n : Type u_1}
{R : Type u_2}
[fintype n]
[comm_semiring R]
[decidable_eq n]
(x : (n → R) →ₗ[R] n → R)
(y : n → R) :
(⇑linear_map.to_matrix' x).mul_vec y = ⇑x y
def
linear_equiv.to_invertible_matrix
{n : Type u_1}
{R : Type u_2}
[comm_semiring R]
[fintype n]
[decidable_eq n]
(x : (n → R) ≃ₗ[R] n → R) :
Equations
- x.to_invertible_matrix = {inv_of := ⇑linear_map.to_matrix' ↑(x.symm), inv_of_mul_self := _, mul_inv_of_self := _}
theorem
matrix.transpose_alg_equiv_symm_op_apply
{n : Type u_1}
{R : Type u_2}
{α : Type u_3}
[comm_semiring R]
[comm_semiring α]
[fintype n]
[decidable_eq n]
[algebra R α]
(x : matrix n n α) :
⇑((matrix.transpose_alg_equiv n R α).symm) (mul_opposite.op x) = x.transpose
theorem
matrix.dot_product_eq_trace
{R : Type u_1}
{n : Type u_2}
[comm_semiring R]
[star_ring R]
[fintype n]
(x : n → R)
(y : matrix n n R) :
matrix.dot_product (has_star.star x) (y.mul_vec x) = (((matrix.col x).mul (matrix.row (has_star.star x))).conj_transpose.mul y).trace