Matrix basics

Basic matrix lemmas used by the monlib4 automorphism-of-matrix-algebras formalization.

@[reducible, inline]

abbrev Matrix.stdBasisMatrix {R : Type u_1} {n : Type u_2} {m : Type u_3} [Zero R] [DecidableEq n] [DecidableEq m] (i : n) (j : m) (a : R) : Matrix n m R

Compatibility name for the old Monlib/mathlib3 matrix unit API.

Equations

• Matrix.stdBasisMatrix i j a = Matrix.single i j a

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_stdBasis {R : Type u_1} {m : Type u_2} {n : Type u_3} [Semiring R] [Fintype n] (a : Matrix m n R) (i : m) (j : n) : a.mulVec ((Pi.basisFun R n) j) i = a i j

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

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 at least one entry is nonzero.

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

Two vectors are equal iff their entries are equal.

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

The transpose of vecMulVec x y is vecMulVec y x.

theorem Matrix.smul_mulVec_assoc {R : Type u_1} {m : Type u_2} {n : Type u_3} [Semiring R] [Fintype n] (r : R) (x : Matrix m n R) (y : n → R) : (r • x).mulVec y = r • x.mulVec y

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

The identity matrix as a sum of standard matrix units.

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

The trace of a Kronecker product is the product of traces.

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

@[reducible, inline]

noncomputable abbrev 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 𝕜

The unitary eigenvector matrix associated to a Hermitian matrix.

Equations

• hA.eigenvectorMatrix = ↑hA.eigenvectorUnitary

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 (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.eigenvectorUnitary).conjTranspose

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_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) : A.trace = ↑(∑ i : n, hA.eigenvalues i)

theorem LinearMap.IsSymmetric.eigenvalue_mem_spectrum {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {A : E →ₗ[𝕜] E} (hn : Module.finrank 𝕜 E = Fintype.card n) (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] {M : Matrix n n 𝕜} (hM : M.IsHermitian) (i : n) : Module.End.HasEigenvalue (toEuclideanLin M) ↑(hM.eigenvalues i)

theorem Matrix.IsHermitian.hasEigenvector_eigenvectorBasis {𝕜 : Type u_1} {n : Type u_2} [RCLike 𝕜] [Fintype n] [DecidableEq n] {M : Matrix n n 𝕜} (hM : M.IsHermitian) (i : n) : Module.End.HasEigenvector (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] {M : Matrix n n 𝕜} (hM : M.IsHermitian) (i : n) : M.mulVec (hM.eigenvectorBasis i).ofLp = hM.eigenvalues i • (hM.eigenvectorBasis i).ofLp

theorem Matrix.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) • kroneckerMap (fun (x1 x2 : R) => x1 * x2) (single i j 1) (single k l 1)

Expand a square matrix indexed by a product as a sum of Kronecker products of matrix units.

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) : (kroneckerMap (fun (x1 x2 : R) => x1 * x2) x y).conjTranspose = kroneckerMap (fun (x1 x2 : R) => x1 * x2) x.conjTranspose y.conjTranspose

theorem Matrix.kronecker_star {R : Type u_1} {n : Type u_2} [CommSemiring R] [StarRing R] (x y : Matrix n n R) : star (kroneckerMap (fun (x1 x2 : R) => x1 * x2) x y) = kroneckerMap (fun (x1 x2 : R) => x1 * x2) (star x) (star y)

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

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

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

theorem Matrix.kronecker_conj {R : Type u_1} {n : Type u_2} [CommSemiring R] [StarRing R] (x y : Matrix n n R) : (kroneckerMap (fun (x1 x2 : R) => x1 * x2) x y).conj = kroneckerMap (fun (x1 x2 : R) => x1 * x2) x.conj y.conj

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

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

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.single i j 1) (Matrix.single k l 1)

@[implicit_reducible]

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

Equations

• EuclideanSpace.instInnerPi = { 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 y : n → 𝕜} : inner 𝕜 x y = 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 Matrix.single_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) : (single i j a).conjTranspose = single j i (star a)

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

theorem Matrix.single.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 (single i j a x.1 x.2) = single j i (star a) x.2 x.1

theorem Matrix.single.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) : (single i j 1).conjTranspose = single j i 1

The conjugate transpose of a standard matrix unit.

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.single.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 x : n) (j y : m) (k z : p) (l w : q) : single k l (single i j 1 x y) z w = single i j 1 x y * single k l 1 z w

theorem Matrix.single.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 x : n) (j y : m) (k z : p) (l w : q) : single k l (single i j 1 x y) z w = if i = x ∧ j = y ∧ k = z ∧ l = w then 1 else 0

theorem Matrix.single.hMul_apply {n : Type u_2} [DecidableEq n] {R : Type u_1} [Fintype n] [Semiring R] (i j k l m p : n) : ∑ x : n × n, ∑ x_1 : n × n, ∑ x_2 : n, ∑ x_3 : n, single l k (single p m 1 x_1.2 x_1.1) x.2 x.1 * single i x_2 (single 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

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

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

theorem Matrix.single.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 x : n) (j k : m) (l y : p) (a b : R) : (single i j a * single k l b) x y = if i = x ∧ j = k ∧ l = y then a * b else 0

theorem Matrix.single.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 k : n) (l : p) : single i j 1 * single k l 1 = (if j = k then 1 else 0) • single i l 1

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 α) : (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) : star x ⬝ᵥ y.mulVec x = ((replicateCol (Fin 1) x * replicateRow (Fin 1) (star x)).conjTranspose * y).trace

theorem forall_left_hMul {n : Type u_1} {R : Type u_2} [Fintype n] [Semiring R] (x 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} [DecidableEq n] [Field 𝕜] (c : 𝕜) : c • 1 = 1 ↔ c = 1 ∨ IsEmpty n

@[reducible]

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)

A linear equivalence of R^n gives an invertible matrix.

Equations

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