Matrix.IsHermitian.det_eq_prod_eigenvalues
theorem Matrix.IsHermitian.det_eq_prod_eigenvalues :
โ {๐ : Type u_1} [inst : RCLike ๐] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n ๐} [inst_2 : DecidableEq n]
(hA : A.IsHermitian), A.det = Finset.univ.prod fun i => โ(hA.eigenvalues i)
This theorem states that for any field `๐` (having algebraic structure similar to real or complex numbers), with a finite type `n` (which could be seen as indices), and a hermitian matrix `A` of type `๐` with indices from `n`, assuming that the equality in `n` is decidable, the determinant of `A` is equal to the product of its eigenvalues. Here, the eigenvalues are obtained over all indices in the universal set implied by the finiteness of type `n`. In simpler terms, this theorem is asserting that the determinant of a hermitian matrix is the product of all its eigenvalues.
More concisely: For any finite-type field `๐` and hermitian matrix `A` of size `n x n` over `๐`, the determinant equals the product of its eigenvalues.
|
Matrix.IsHermitian.rank_eq_rank_diagonal
theorem Matrix.IsHermitian.rank_eq_rank_diagonal :
โ {๐ : Type u_1} [inst : RCLike ๐] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n ๐} [inst_2 : DecidableEq n]
(hA : A.IsHermitian), A.rank = (Matrix.diagonal hA.eigenvalues).rank
This theorem states that for any hermitian matrix `A` of type `๐` and indexed by type `n`, the rank of `A` is equal to the rank of its diagonalized form. Here, the diagonalized form is represented by the matrix whose elements are the eigenvalues of `A` on the diagonal and zeros elsewhere. The index type `n` is finite and has decidable equality. The type `๐` is required to have a structure compatible with a ring or a field, indicated by `RCLike ๐`. In mathematical terms, if $A$ is a Hermitian matrix, then the rank of $A$ is equal to the rank of its diagonal matrix formed by its eigenvalues.
More concisely: The rank of a Hermitian matrix is equal to the rank of its diagonal matrix formed by its eigenvalues.
|
Matrix.IsHermitian.mulVec_eigenvectorBasis
theorem Matrix.IsHermitian.mulVec_eigenvectorBasis :
โ {๐ : Type u_1} [inst : RCLike ๐] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n ๐} [inst_2 : DecidableEq n]
(hA : A.IsHermitian) (i : n), A.mulVec (hA.eigenvectorBasis i) = hA.eigenvalues i โข hA.eigenvectorBasis i
The theorem `Matrix.IsHermitian.mulVec_eigenvectorBasis` states that for any field `๐` (in the context of rings and linear algebra), for any type `n` that is a finite type (i.e., there are finitely many instances of `n`), and for any matrix `A` of type `Matrix n n ๐` (i.e., a square matrix with elements in `๐` and both rows and columns indexed by `n`), if `A` is Hermitian (i.e., equal to its own conjugate transpose), then for every instance `i` of `n`, the result of multiplying `A` by the `i`-th eigenvector from the basis of eigenvectors of `A` is equal to the `i`-th eigenvalue times the `i`-th eigenvector. This means that the entries of the `eigenvectorBasis` are indeed eigenvectors of the matrix `A`.
More concisely: For any Hermitian matrix `A` of size `n x n` over a field `๐`, the `i`-th eigenvector in the eigenvector basis is an eigenvector of `A` with eigenvalue `A`'s `i`-th eigenvalue.
|
Matrix.IsHermitian.transpose_eigenvectorMatrix_apply
theorem Matrix.IsHermitian.transpose_eigenvectorMatrix_apply :
โ {๐ : Type u_1} [inst : RCLike ๐] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n ๐} [inst_2 : DecidableEq n]
(hA : A.IsHermitian) (i : n), hA.eigenvectorMatrix.transpose i = hA.eigenvectorBasis i
This theorem states that for any scalar field `๐` and any type `n` (which is finite and has decidable equality), given a Hermitian matrix `A` of type `Matrix n n ๐` and an index `i` of type `n`, the i-th column of the transpose of the matrix generated by the eigenvectors of `A` (as obtained by the method `A.IsHermitian.eigenvectorMatrix.transpose`) is equal to the i-th basis vector of the eigenvector basis of `A` (as obtained by the method `hA.eigenvectorBasis`). In mathematical terms, this theorem asserts that the eigenvectors of a Hermitian matrix, when arranged column-wise to form a new matrix and then transposed, form a basis for the space on which the matrix operates. This is a fundamental result in linear algebra, especially in the study of Hermitian matrices.
More concisely: The columns of the matrix formed by the eigenvectors of a Hermitian matrix, when transposed, form the eigenvector basis of the matrix.
|
Matrix.IsHermitian.exists_eigenvector_of_ne_zero
theorem Matrix.IsHermitian.exists_eigenvector_of_ne_zero :
โ {๐ : Type u_1} [inst : RCLike ๐] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n ๐},
A.IsHermitian โ A โ 0 โ โ v t, t โ 0 โง v โ 0 โง A.mulVec v = t โข v
The theorem states that for any non-zero Hermitian matrix `A` with entries in a ring `๐` and indexed by a finite type `n`, there exists a non-zero vector `v` and a non-zero scalar `t` such that the multiplication of the matrix `A` with the vector `v` equals the scalar multiplication of `t` and `v`. This vector `v` is an eigenvector of the matrix `A` and `t` is its corresponding non-zero eigenvalue.
More concisely: For any non-zero Hermitian matrix `A` over a ring `๐` of size `n x n`, there exists a non-zero eigenvector `v` and a non-zero complex eigenvalue `t` such that `Av = tv`.
|
Matrix.IsHermitian.eigenvectorMatrix_mul_inv
theorem Matrix.IsHermitian.eigenvectorMatrix_mul_inv :
โ {๐ : Type u_1} [inst : RCLike ๐] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n ๐} [inst_2 : DecidableEq n]
(hA : A.IsHermitian), hA.eigenvectorMatrix * hA.eigenvectorMatrixInv = 1
This theorem states that if you have a Hermitian matrix `A` over a ring `๐`, where `๐` has a structure of a ring with conjugation (i.e., it is an instance of `RCLike`), and the indices `n` of the matrix form a finite type (i.e., there are finitely many indices), with a decidable equality, then the product of `A`'s eigenvector matrix and the inverse of this eigenvector matrix is equal to the identity matrix.
In simpler terms, for a Hermitian matrix (which is a matrix that is equal to its own conjugate transpose, and includes as a special case symmetric matrices over the real numbers), there exists a matrix of eigenvectors such that when it is multiplied by its inverse, the result is the identity matrix. This is an important property in linear algebra as it shows that Hermitian matrices can be diagonalized using a basis of their eigenvectors.
More concisely: For a finite-sized Hermitian matrix `A` over a ring `๐` with a decidable equality and conjugation structure, the product of its eigenvector matrix and the inverse of its eigenvector matrix equals the identity matrix.
|
Matrix.IsHermitian.spectral_theorem
theorem Matrix.IsHermitian.spectral_theorem :
โ {๐ : Type u_1} [inst : RCLike ๐] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n ๐} [inst_2 : DecidableEq n]
(hA : A.IsHermitian),
hA.eigenvectorMatrixInv * A = Matrix.diagonal (RCLike.ofReal โ hA.eigenvalues) * hA.eigenvectorMatrixInv
This theorem, often referred to as the Diagonalization theorem or the Spectral theorem for matrices, states that any Hermitian matrix can be diagonalized by a change of basis. More specifically, given a Hermitian matrix `A`, there exists an invertible matrix `P` (which is the inverse of the matrix constituted by the orthonormal eigenvectors of `A`), such that `P * A` equals the product of the diagonal matrix formed by the eigenvalues of `A` and `P`. This theorem is fundamental in linear algebra, as it provides a simple representation for Hermitian matrices that is easier to work with.
More concisely: Given a Hermitian matrix `A`, there exists an invertible matrix `P` of orthonormal eigenvectors such that `P^*-1 * A * P` is a diagonal matrix with `A`'s eigenvalues on the diagonal.
|
Matrix.IsHermitian.rank_eq_card_non_zero_eigs
theorem Matrix.IsHermitian.rank_eq_card_non_zero_eigs :
โ {๐ : Type u_1} [inst : RCLike ๐] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n ๐} [inst_2 : DecidableEq n]
(hA : A.IsHermitian), A.rank = Fintype.card { i // hA.eigenvalues i โ 0 }
This theorem states that for any Hermitian matrix A (of type `๐` and dimension `n`, where `๐` is a field that supports operations like addition, multiplication, etc., and `n` is a finite type implying that the matrix is of finite dimensions), the rank of the matrix is equal to the number of its non-zero eigenvalues. This is true for all Hermitian matrices, regardless of the field or the matrix's dimensions. Note that the equality check for the dimension type `n` is decidable.
More concisely: The theorem asserts that the rank of a Hermitian matrix equals the number of its non-zero eigenvalues.
|
Matrix.IsHermitian.eigenvalues_eq
theorem Matrix.IsHermitian.eigenvalues_eq :
โ {๐ : Type u_1} [inst : RCLike ๐] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n ๐} [inst_2 : DecidableEq n]
(hA : A.IsHermitian) (i : n),
hA.eigenvalues i =
RCLike.re
(Matrix.dotProduct (star (hA.eigenvectorMatrix.transpose i)) (A.mulVec (hA.eigenvectorMatrix.transpose i)))
The theorem `Matrix.IsHermitian.eigenvalues_eq` states that for any Hermitian matrix `A` of size `n` with entries in a ring `๐` that behaves like the reals (i.e., `RCLike ๐`), and for any index `i` of type `n`, the `i`-th eigenvalue of `A` equals the real part of the dot product between the conjugated transpose of the `i`-th column of the orthonormal eigenvector matrix of `A` and the result of multiplying `A` by that `i`-th column. In other words, it relates the eigenvalues of a Hermitian matrix to the dot product of its eigenvectors and the corresponding matrix-vector multiplication.
More concisely: For any Hermitian matrix `A` of size `n` over a ring `๐` that behaves like the reals, the `i`-th eigenvalue of `A` is equal to the real part of the dot product between the conjugate transpose of the `i`-th column of its eigenvector matrix and the product of `A` and that column.
|
Matrix.IsHermitian.spectral_theorem'
theorem Matrix.IsHermitian.spectral_theorem' :
โ {๐ : Type u_1} [inst : RCLike ๐] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n ๐} [inst_2 : DecidableEq n]
(hA : A.IsHermitian),
A = hA.eigenvectorMatrix * Matrix.diagonal (RCLike.ofReal โ hA.eigenvalues) * hA.eigenvectorMatrixInv
This is an alternate form of the *Spectral Theorem* for convenience. The theorem states that any Hermitian matrix can be expressed as a product of its eigenvector matrix, a diagonal matrix consisting of its eigenvalues, and the inverse of its eigenvector matrix. More formally, for any field `๐` which can be embedded in the complex numbers, and any finite type `n`, if `A` is a Hermitian matrix of type `Matrix n n ๐`, then `A` can be written as `A = V D Vโปยน`, where `V` is the matrix whose columns are the eigenvectors of `A`, `D` is the diagonal matrix whose entries are the eigenvalues of `A`, and `Vโปยน` is the inverse of `V`.
More concisely: Any Hermitian matrix can be decomposed as a product of its eigenvectors, a diagonal matrix of eigenvalues, and the inverse of the eigenvector matrix.
|