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.eq_zero {R : Type u_1} {n₁ : Type u_2} {n₂ : Type u_3} [Zero R] (x : Matrix n₁ n₂ R) : (∀ (i : n₁) (j : n₂), x i j = 0) ↔ x = 0

theorem Matrix.mulVec_eq {R : Type u_1} {m : Type u_2} {n : Type u_3} [CommSemiring R] [Fintype n] [DecidableEq n] (a : Matrix m n R) (b : Matrix m n R) : a = b ↔ ∀ (c : n → R), a.mulVec c = b.mulVec c

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_ne_zero {R : Type u_1} {n : Type u_2} [Semiring R] (a : n → R) : (∃ (i : n), a i ≠ 0) ↔ a ≠ 0

a vector is nonzero iff one of its elements are nonzero

theorem Matrix.ext_vec {𝕜 : Type u_1} {n : Type u_2} (α : n → 𝕜) (β : n → 𝕜) : α = β ↔ ∀ (i : n), α i = β i

two vectors are equal iff their elements are equal

theorem Matrix.vecMulVec_ne_zero {R : Type u_1} {n : Type u_2} [Semiring R] [NoZeroDivisors R] [NeZero 1] {α : n → R} {β : n → R} (hα : α ≠ 0) (hβ : β ≠ 0) : Matrix.vecMulVec α β ≠ 0

the outer product of two nonzero vectors is nonzero

theorem Matrix.vecMulVec_transpose {R : Type u_1} {n : Type u_2} [CommSemiring R] (x : n → R) (y : n → R) : (Matrix.vecMulVec x y).transpose = Matrix.vecMulVec y x

the transpose of vecMul_vec x y is simply vecMul_vec y x

theorem Matrix.one_eq_sum_std_matrix {n : Type u_1} {R : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] : 1 = ∑ r : n, Matrix.stdBasisMatrix r r 1

the identity written as a sum of the standard basis

theorem Matrix.kronecker.trace {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_1} [Fintype n] (A : Matrix n n 𝕜) (B : Matrix n n 𝕜) : (Matrix.kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) A B).trace = A.trace * B.trace

$\textnormal{Tr}(A\otimes_k B)=\textnormal{Tr}(A)\textnormal{Tr}(B)$

noncomputable def Matrix.IsHermitian.eigenvectorMatrix {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) : Matrix n n 𝕜

Equations

• hA.eigenvectorMatrix = (PiLp.basisFun 2 𝕜 n).toMatrix ⇑hA.eigenvectorBasis.toBasis

theorem Matrix.IsHermitian.eigenvectorUnitary_coe_eq_eigenvectorMatrix {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) : hA.eigenvectorMatrix = ↑hA.eigenvectorUnitary

theorem Matrix.IsHermitian.eigenvalues_eq' {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) (i : n) : hA.eigenvalues i = RCLike.re (Matrix.dotProduct (star (hA.eigenvectorMatrix.transpose i)) (A.mulVec (hA.eigenvectorMatrix.transpose i)))

theorem Matrix.IsHermitian.eigenvectorMatrix_conjTranspose {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) : hA.eigenvectorMatrix.conjTranspose = hA.eigenvectorBasis.toBasis.toMatrix ⇑(PiLp.basisFun 2 𝕜 n)

theorem Matrix.IsHermitian.eigenvectorMatrix_mul_conjTranspose {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) : hA.eigenvectorMatrix * hA.eigenvectorMatrix.conjTranspose = 1

theorem Matrix.IsHermitian.trace_eq {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_1} [Fintype n] [DecidableEq n] [DecidableEq 𝕜] {A : Matrix n n 𝕜} (hA : A.IsHermitian) : A.trace = ↑(∑ i : n, hA.eigenvalues i)

the trace of a Hermitian matrix is the sum of its eigenvalues

theorem LinearMap.IsSymmetric.eigenvalue_mem_spectrum {ℍ : Type u_2} {𝕜 : Type u_1} [NormedAddCommGroup ℍ] [RCLike 𝕜] [InnerProductSpace 𝕜 ℍ] [FiniteDimensional 𝕜 ℍ] {n : Type u_3} [Fintype n] [DecidableEq 𝕜] (hn : Module.finrank 𝕜 ℍ = Fintype.card n) {A : ℍ →ₗ[𝕜] ℍ} (hA : A.IsSymmetric) (i : Fin (Fintype.card n)) : ↑(hA.eigenvalues hn i) ∈ spectrum 𝕜 A

theorem Matrix.IsHermitian.eigenvalues_hasEigenvalue {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] [DecidableEq 𝕜] {M : Matrix n n 𝕜} (hM : M.IsHermitian) (i : n) : Module.End.HasEigenvalue (Matrix.toEuclideanLin M) ↑(hM.eigenvalues i)

theorem Matrix.IsHermitian.hasEigenvector_eigenvectorBasis {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] [DecidableEq 𝕜] {M : Matrix n n 𝕜} (hM : M.IsHermitian) (i : n) : Module.End.HasEigenvector (Matrix.toEuclideanLin M) (↑(hM.eigenvalues i)) (hM.eigenvectorBasis i)

theorem Matrix.IsHermitian.apply_eigenvectorBasis {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] [DecidableEq 𝕜] {M : Matrix n n 𝕜} (hM : M.IsHermitian) (i : n) : M.mulVec (hM.eigenvectorBasis i) = hM.eigenvalues i • hM.eigenvectorBasis i

a Hermitian matrix applied to its eigenvector basis element equals the basis element scalar-ed by its respective eigenvalue

noncomputable instance instInnerForall_monlib {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] : Inner 𝕜 (n → 𝕜)

Equations

• instInnerForall_monlib = { inner := fun (x y : n → 𝕜) => inner ((EuclideanSpace.equiv n 𝕜).symm x) ((EuclideanSpace.equiv n 𝕜).symm y) }

theorem EuclideanSpace.inner_eq {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] {x : n → 𝕜} {y : n → 𝕜} : inner x y = Matrix.dotProduct (star x) y

theorem EuclideanSpace.rankOne_of_orthonormalBasis_eq_one {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] [Fintype n] (h : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)) : ∑ i : n, ((rankOne 𝕜) (h i)) (h i) = 1

theorem kmul_representation {R : Type u_1} {n₁ : Type u_2} {n₂ : Type u_3} [Fintype n₁] [Fintype n₂] [DecidableEq n₁] [DecidableEq n₂] [Semiring R] (x : Matrix (n₁ × n₂) (n₁ × n₂) R) : x = ∑ i : n₁, ∑ j : n₁, ∑ k : n₂, ∑ l : n₂, x (i, k) (j, l) • Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) (Matrix.stdBasisMatrix i j 1) (Matrix.stdBasisMatrix 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_conjTranspose {R : Type u_1} {m : Type u_2} {n : Type u_3} [CommSemiring R] [StarRing R] (x : Matrix n n R) (y : Matrix m m R) : (Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) x y).conjTranspose = Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) x.conjTranspose y.conjTranspose

$(x \otimes_k y)^* = x^* \otimes_k y^*$

theorem Matrix.kronecker.star {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_1} (x : Matrix n n 𝕜) (y : Matrix n n 𝕜) : star (Matrix.kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) x y) = Matrix.kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) (star x) (star y)

theorem Matrix.kronecker.transpose {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_1} (x : Matrix n n 𝕜) (y : Matrix n n 𝕜) : (Matrix.kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) x y).transpose = Matrix.kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) x.transpose y.transpose

theorem Matrix.kronecker.conj {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_1} (x : Matrix n n 𝕜) (y : Matrix n n 𝕜) : (Matrix.kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) x y).conj = Matrix.kroneckerMap (fun (x1 x2 : 𝕜) => x1 * x2) x.conj y.conj

theorem Matrix.unitaryGroup.coe_mk {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_1} [Fintype n] [DecidableEq n] (x : Matrix n n 𝕜) (hx : x ∈ Matrix.unitaryGroup n 𝕜) : ↑⟨x, hx⟩ = x

theorem Matrix.stdBasisMatrix_conjTranspose {R : Type u_1} {n : Type u_2} {m : Type u_3} [Semiring R] [StarAddMonoid R] [DecidableEq n] [DecidableEq m] (i : n) (j : m) (a : R) : (Matrix.stdBasisMatrix i j a).conjTranspose = Matrix.stdBasisMatrix j i (star a)

theorem Matrix.stdBasisMatrix.star_apply {R : Type u_1} {n : Type u_2} {m : Type u_3} [Semiring R] [StarAddMonoid R] [DecidableEq n] [DecidableEq m] (i : n) (k : n) (j : m) (l : m) (a : R) : star (Matrix.stdBasisMatrix i j a k l) = Matrix.stdBasisMatrix j i (star a) l k

theorem Matrix.stdBasisMatrix.star_apply' {R : Type u_3} {n : Type u_1} {m : Type u_2} [Semiring R] [StarAddMonoid R] [DecidableEq n] [DecidableEq m] (i : n) (j : m) (x : n × m) (a : R) : star (Matrix.stdBasisMatrix i j a x.1 x.2) = Matrix.stdBasisMatrix j i (star a) x.2 x.1

theorem Matrix.stdBasisMatrix.star_one {n : Type u_2} {m : Type u_3} [DecidableEq n] [DecidableEq m] {R : Type u_1} [Semiring R] [StarRing R] (i : n) (j : m) : (Matrix.stdBasisMatrix i j 1).conjTranspose = Matrix.stdBasisMatrix j i 1

$e_{ij}^*=e_{ji}$

theorem Matrix.trace_iff {R : Type u_1} {n : Type u_2} [AddCommMonoid R] [Fintype n] (x : Matrix n n R) : x.trace = ∑ k : n, x k k

theorem Matrix.stdBasisMatrix.hMul_apply_basis {n : Type u_4} {m : Type u_5} [DecidableEq n] [DecidableEq m] {R : Type u_1} {p : Type u_2} {q : Type u_3} [Semiring R] [DecidableEq p] [DecidableEq q] (i : n) (x : n) (j : m) (y : m) (k : p) (z : p) (l : q) (w : q) : Matrix.stdBasisMatrix k l (Matrix.stdBasisMatrix i j 1 x y) z w = Matrix.stdBasisMatrix i j 1 x y * Matrix.stdBasisMatrix k l 1 z w

theorem Matrix.stdBasisMatrix.mul_apply_basis' {n : Type u_4} {m : Type u_5} [DecidableEq n] [DecidableEq m] {R : Type u_1} {p : Type u_2} {q : Type u_3} [Semiring R] [DecidableEq p] [DecidableEq q] (i : n) (x : n) (j : m) (y : m) (k : p) (z : p) (l : q) (w : q) : Matrix.stdBasisMatrix k l (Matrix.stdBasisMatrix i j 1 x y) z w = if i = x ∧ j = y ∧ k = z ∧ l = w then 1 else 0

theorem Matrix.stdBasisMatrix.hMul_apply {n : Type u_2} [DecidableEq n] {R : Type u_1} [Fintype n] [Semiring R] (i : n) (j : n) (k : n) (l : n) (m : n) (p : n) : ∑ x : n × n, ∑ x_1 : n × n, ∑ x_2 : n, ∑ x_3 : n, Matrix.stdBasisMatrix l k (Matrix.stdBasisMatrix p m 1 x_1.2 x_1.1) x.2 x.1 * Matrix.stdBasisMatrix i x_2 (Matrix.stdBasisMatrix x_3 j 1 x_1.1 x_1.2) x.1 x.2 = ∑ x : n × n, ∑ x_1 : n × n, ∑ x_2 : n, ∑ x_3 : n, if p = x_1.2 ∧ m = x_1.1 ∧ l = x.2 ∧ k = x.1 ∧ x_3 = x_1.1 ∧ j = x_1.2 ∧ i = x.1 ∧ x_2 = x.2 then 1 else 0

@[simp]

theorem Matrix.stdBasisMatrix.sum_star_hMul_self {R : Type u_2} {n : Type u_1} [Semiring R] [StarAddMonoid R] [DecidableEq n] [Fintype n] (i : n) (j : n) (a : R) (b : R) : ∑ k : n, ∑ l : n, ∑ m : n, ∑ p : n, Matrix.stdBasisMatrix i j a k l * star (Matrix.stdBasisMatrix i j b) m p = a * star b

theorem Matrix.stdBasisMatrix.sum_star_hMul_self' {n : Type u_2} [DecidableEq n] {R : Type u_1} [Fintype n] [Semiring R] [StarRing R] (i : n) (j : n) : ∑ kl : n × n, ∑ mp : n × n, Matrix.stdBasisMatrix i j 1 kl.1 kl.2 * star Matrix.stdBasisMatrix i j 1 mp.1 mp.2 = 1

theorem Matrix.stdBasisMatrix.hMul_stdBasisMatrix {n : Type u_4} {m : Type u_3} [DecidableEq n] [DecidableEq m] {R : Type u_1} {p : Type u_2} [Semiring R] [DecidableEq p] [Fintype m] (i : n) (x : n) (j : m) (k : m) (l : p) (y : p) (a : R) (b : R) : (Matrix.stdBasisMatrix i j a * Matrix.stdBasisMatrix k l b) x y = if i = x ∧ j = k ∧ l = y then a * b else 0

theorem Matrix.stdBasisMatrix.hMul_stdBasis_matrix' {n : Type u_3} {m : Type u_4} [DecidableEq n] [DecidableEq m] {R : Type u_1} {p : Type u_2} [Fintype n] [DecidableEq p] [Semiring R] (i : m) (j : n) (k : n) (l : p) : Matrix.stdBasisMatrix i j 1 * Matrix.stdBasisMatrix k l 1 = (if j = k then 1 else 0) • Matrix.stdBasisMatrix i l 1

theorem LinearMap.toMatrix'_mulVec {n : Type u_1} {R : Type u_2} [Fintype n] [CommSemiring R] [DecidableEq n] (x : (n → R) →ₗ[R] n → R) (y : n → R) : (LinearMap.toMatrix' x).mulVec y = x y

def LinearEquiv.toInvertibleMatrix {n : Type u_1} {R : Type u_2} [CommSemiring R] [Fintype n] [DecidableEq n] (x : (n → R) ≃ₗ[R] n → R) : Invertible (LinearMap.toMatrix' ↑x)

Equations

• x.toInvertibleMatrix = { invOf := LinearMap.toMatrix' ↑x.symm, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }

theorem Matrix.transposeAlgEquiv_symm_op_apply {n : Type u_1} {R : Type u_2} {α : Type u_3} [CommSemiring R] [CommSemiring α] [Fintype n] [DecidableEq n] [Algebra R α] (x : Matrix n n α) : (Matrix.transposeAlgEquiv n R α).symm (MulOpposite.op x) = x.transpose

theorem Matrix.dotProduct_eq_trace {R : Type u_1} {n : Type u_2} [CommSemiring R] [StarRing R] [Fintype n] (x : n → R) (y : Matrix n n R) : Matrix.dotProduct (star x) (y.mulVec x) = ((Matrix.col (Fin 1) x * Matrix.row (Fin 1) (star x)).conjTranspose * y).trace

theorem forall_left_hMul {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [Semiring R] (x : Matrix n n R) (y : Matrix n n R) : x = y ↔ ∀ (a : Matrix n n R), a * x = a * y

theorem Matrix.smul_one_eq_one_iff {𝕜 : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [Field 𝕜] (c : 𝕜) : c • 1 = 1 ↔ c = 1 ∨ IsEmpty n