Matrix.isHermitian_diagonal
theorem Matrix.isHermitian_diagonal :
∀ {α : Type u_1} {n : Type u_4} [inst : AddMonoid α] [inst_1 : StarAddMonoid α] [inst_2 : TrivialStar α]
[inst_3 : DecidableEq n] (v : n → α), (Matrix.diagonal v).IsHermitian
The theorem states that a diagonal matrix is Hermitian if the entries in the diagonal obey a trivial star operation. This is typically the case for real numbers. More specifically, for any type `α` which has an additive monoid structure and a trivial star operation, and for any type `n` with decidable equality, any function `v : n → α` that provides the entries of a diagonal matrix, ensures that the resulting matrix is Hermitian. Hermitian matrices have the property that they are equal to their own conjugate transpose. In this case, the conjugate is trivial due to the `TrivialStar α` instance.
More concisely: A diagonal matrix with entries of type `α` having a trivial star operation is Hermitian.
|
Matrix.IsHermitian.zpow
theorem Matrix.IsHermitian.zpow :
∀ {α : Type u_1} {m : Type u_3} [inst : CommRing α] [inst_1 : StarRing α] [inst_2 : Fintype m]
[inst_3 : DecidableEq m] {A : Matrix m m α}, A.IsHermitian → ∀ (k : ℤ), (A ^ k).IsHermitian
The theorem `Matrix.IsHermitian.zpow` states that for any type `α` with a commutative ring structure and a star ring structure, any finite type `m` with a decidable equality, and a Hermitian matrix `A` with entries in `α` and indices in `m`, the matrix `A` raised to any integer power `k` is also Hermitian. The note at the beginning indicates that the lemma `IsSelfAdjoint.zpow`, which applies to division rings, cannot be used for matrices, which are not division rings.
More concisely: For any commutative ring with star structure `α`, finite type `m` with decidable equality, and Hermitian matrix `A` over `α` with indices in `m`, the Hermitian property is preserved under matrix multiplication by any integer power `k`. That is, `A ^ k` is also a Hermitian matrix for all `k ∈ ℤ`.
|
Matrix.isHermitian_mul_mul_conjTranspose
theorem Matrix.isHermitian_mul_mul_conjTranspose :
∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : NonUnitalSemiring α] [inst_1 : StarRing α]
[inst_2 : Fintype m] {A : Matrix m m α} (B : Matrix n m α),
A.IsHermitian → (B * A * B.conjTranspose).IsHermitian
This theorem states that for any non-unital semiring `α` and for any types `m` and `n` that have finite instances, given a matrix `A` which is a square matrix of `α` indexed by `m` and is Hermitian, and a potentially rectangular matrix `B` indexed by `n` and `m` with entries in `α`, the result of multiplying `B`, `A`, and the conjugate transpose of `B` (in that order) is also a Hermitian matrix. This theorem generalizes the property of being Hermitian under conjugate transpose to the case where the matrix `B` can be rectangular, not necessarily square.
More concisely: For any non-unital semiring `α` and finite types `m` and `n`, if `A` is a square Hermitian matrix over `α` indexed by `m`, and `B` is a matrix over `α` indexed by `n` and `m`, then the product of `B`, `A`, and the conjugate transpose of `B` is a Hermitian matrix.
|
Matrix.IsHermitian.fromBlocks
theorem Matrix.IsHermitian.fromBlocks :
∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : InvolutiveStar α] {A : Matrix m m α} {B : Matrix m n α}
{C : Matrix n m α} {D : Matrix n n α},
A.IsHermitian → B.conjTranspose = C → D.IsHermitian → (A.fromBlocks B C D).IsHermitian
The theorem `Matrix.IsHermitian.fromBlocks` states that given a block matrix that is composed of matrices `A`, `B`, `C`, and `D` (denoted as `A.fromBlocks B C D`), this block matrix is Hermitian if the matrices `A` and `D` are Hermitian and the conjugate transpose of `B` equals `C`. Here, Hermitian refers to a complex square matrix that is equal to its own conjugate transpose. The types of the matrices `A`, `B`, `C`, and `D` are `Matrix m m α`, `Matrix m n α`, `Matrix n m α`, and `Matrix n n α` respectively, where `α` is a type with an involution (the operation of the `star` function), and `m` and `n` are the indices of the rows and columns.
More concisely: A complex block matrix `A.fromBlocks B C D` of size `m x m` is Hermitian if matrices `A` and `D` are Hermitian and `B` equals the conjugate transpose of `C`.
|
Matrix.isHermitian_diagonal_of_self_adjoint
theorem Matrix.isHermitian_diagonal_of_self_adjoint :
∀ {α : Type u_1} {n : Type u_4} [inst : AddMonoid α] [inst_1 : StarAddMonoid α] [inst_2 : DecidableEq n]
(v : n → α), IsSelfAdjoint v → (Matrix.diagonal v).IsHermitian
This theorem states that given a type of elements `α` that forms an additive monoid and a star additive monoid, and a type `n` with decidable equality, for any function `v` from `n` to `α`, if `v` is self-adjoint, then the matrix resulting from applying the `Matrix.diagonal` function to `v` is Hermitian. In terms of linear algebra, this means that a diagonal matrix is Hermitian if all its diagonal entries are self-adjoint, where a self-adjoint element is one that is equal to its conjugate transpose (star).
More concisely: Given a self-adjoint function from adecidable type `n` to an additive monoid `α` with a star operation, the diagonal matrix obtained from the function is Hermitian.
|
Matrix.isHermitian_diagonal_iff
theorem Matrix.isHermitian_diagonal_iff :
∀ {α : Type u_1} {n : Type u_4} [inst : AddMonoid α] [inst_1 : StarAddMonoid α] [inst_2 : DecidableEq n]
{d : n → α}, (Matrix.diagonal d).IsHermitian ↔ ∀ (i : n), IsSelfAdjoint (d i)
The theorem `Matrix.isHermitian_diagonal_iff` states that for any type `α` which is an additive monoid and a star additive monoid, and for any type `n`, if equality is decidable in `n`, then a diagonal matrix with entries from a function `d : n → α` is Hermitian if and only if each of the diagonal entries, given by the function `d`, is self-adjoint. In the context of matrices, "self-adjoint" refers to an element that is equal to its complex conjugate (also known as its "star"), and a "Hermitian" matrix is one that is equal to its conjugate transpose.
More concisely: A diagonal matrix with entries from a function is Hermitian in the additive monoid and star additive monoid if and only if each diagonal entry is self-adjoint (equivalent to its complex conjugate).
|
Matrix.IsHermitian.transpose
theorem Matrix.IsHermitian.transpose :
∀ {α : Type u_1} {n : Type u_4} [inst : Star α] {A : Matrix n n α}, A.IsHermitian → A.transpose.IsHermitian := by
sorry
This theorem states that for any hermitian matrix `A`, its transpose is also hermitian. A matrix is defined as hermitian if it is equal to its conjugate transpose. In the context of real numbers, hermitian matrices are equivalent to symmetric matrices. Thus, this theorem essentially asserts that the property of being hermitian is preserved under transposition.
More concisely: For any hermitian matrix `A`, its transpose `A^T` is also hermitian, i.e., `A^T = conjg(A)^T`, where `conjg(A)` is the conjugate transpose of `A`.
|
Matrix.isHermitian_transpose_mul_self
theorem Matrix.isHermitian_transpose_mul_self :
∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : NonUnitalSemiring α] [inst_1 : StarRing α]
[inst_2 : Fintype m] (A : Matrix m n α), (A.conjTranspose * A).IsHermitian
This theorem states that for any matrix `A` of type `Matrix m n α`, where `α` is a type equipped with a non-unital semiring and a star ring structure, and `m` and `n` are types with a finite number of elements (i.e., finiteness), the product of the conjugate transpose of `A` and `A` itself is always a Hermitian matrix. This is a more generalized version of `IsSelfAdjoint.star_mul_self`, as `A` can be a rectangular matrix, not just a square one. In mathematical terms, a Hermitian matrix is a complex square matrix that is equal to its own conjugate transpose.
More concisely: For any rectangular matrix $A$ of type $\text{Matrix}\ m\ n\ \alpha$, where $\alpha$ is a finite non-unital semiring with a star ring structure, the product of the conjugate transpose and the matrix $A$ is Hermitian.
|
Matrix.IsHermitian.eq
theorem Matrix.IsHermitian.eq :
∀ {α : Type u_1} {n : Type u_4} [inst : Star α] {A : Matrix n n α}, A.IsHermitian → A.conjTranspose = A
This theorem states that for any matrix `A` whose entries lie in a type `α` that is equipped with a `star` operation (conjugation), if `A` is Hermitian (that implies it is equal to its conjugate transpose), then the conjugate transpose of `A` is indeed `A` itself. In mathematical terms, this means that if a matrix is Hermitian (i.e., it is equal to its conjugate transpose), then the equality is true. The `star` operation in this context typically refers to complex conjugation for complex numbers, and this theorem captures a key property of Hermitian matrices over the complex numbers (or symmetric matrices over the reals).
More concisely: If `A` is a matrixwhose entries lie in a type `α` with a `star` operation, and `A` is Hermitian (i.e., `A = A.transpose.star`), then `A` is equal to its conjugate transpose (`A = A.star.transpose`).
|
Matrix.isHermitian_one
theorem Matrix.isHermitian_one :
∀ {α : Type u_1} {n : Type u_4} [inst : Semiring α] [inst_1 : StarRing α] [inst_2 : DecidableEq n],
Matrix.IsHermitian 1
This theorem states that a unit matrix of any size and type is Hermitian. More specifically, for any semiring `α` with a star operation, which forms a StarRing, and any type `n` equipped with a decidable equality, the unit matrix (`1`) is declared to be Hermitian. Note that this is a more general statement than the `isSelfAdjoint_one` theorem for matrices, as it doesn't require the finiteness of `n`, which is necessary for the `Monoid (Matrix n n R)` structure.
More concisely: For any semiring with a star operation forming a StarRing and any type with decidable equality, the unit matrix is Hermitian.
|
Matrix.isHermitian_iff_isSymmetric
theorem Matrix.isHermitian_iff_isSymmetric :
∀ {α : Type u_1} {n : Type u_4} [inst : RCLike α] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n α},
A.IsHermitian ↔ (Matrix.toEuclideanLin A).IsSymmetric
This theorem states that, for a given matrix `A` of type `α` with indexes `n` (where `α` is of type `RCLike` and `n` is of type `Fintype` and `DecidableEq`), the matrix is Hermitian if and only if the corresponding linear map, obtained by applying the function `Matrix.toEuclideanLin` to `A`, is symmetric.
In other words, it provides a characterisation of hermitian matrices in terms of the symmetry of the corresponding linear maps in Euclidean space, thus connecting the properties of matrices and linear maps.
More concisely: A matrix of type `RCLike` with indexes of type `Fintype` and `DecidableEq` is Hermitian if and only if its corresponding linear map in Euclidean space, obtained via `Matrix.toEuclideanLin`, is symmetric.
|
Matrix.isHermitian_conjTranspose_mul_mul
theorem Matrix.isHermitian_conjTranspose_mul_mul :
∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : NonUnitalSemiring α] [inst_1 : StarRing α]
[inst_2 : Fintype m] {A : Matrix m m α} (B : Matrix m n α),
A.IsHermitian → (B.conjTranspose * A * B).IsHermitian
This theorem states that in a non-unital semiring with a star-ring operation, for any Hermitian matrix `A` of type `Matrix m m α` and any matrix `B` of type `Matrix m n α`, the product of the conjugate transpose of `B`, `A` and `B` is also a Hermitian matrix. This theorem is more general than `IsSelfAdjoint.conjugate'` because the matrix `B` can be rectangular. Here, `IsHermitian` is a property of a matrix that indicates it equals its own conjugate transpose.
More concisely: In a non-unital semiring with a star-ring operation, the product of the conjugate transpose of a matrix `B` and a Hermitian matrix `A`, and the matrix `B` itself, is a Hermitian matrix.
|
Matrix.isHermitian_mul_conjTranspose_self
theorem Matrix.isHermitian_mul_conjTranspose_self :
∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : NonUnitalSemiring α] [inst_1 : StarRing α]
[inst_2 : Fintype n] (A : Matrix m n α), (A * A.conjTranspose).IsHermitian
The theorem `Matrix.isHermitian_mul_conjTranspose_self` states that for any type `α`, which has a structure of `NonUnitalSemiring` and `StarRing`, and any types `m` and `n`, with `n` being a `Fintype`, a matrix `A` with entries in `α` and dimensions indexed by `m` and `n`, the product of `A` and the conjugate transpose of `A` is a Hermitian matrix. This theorem is a generalization of `IsSelfAdjoint.mul_star_self` because `A` can be a rectangular matrix, i.e., `A` doesn't necessarily have to be square. In mathematical terms, this theorem says that $A A^*$ is Hermitian for any matrix $A$, where $A^*$ is the conjugate transpose of $A$, and the entries of $A$ belong to a ring with a star operation and without a multiplicative identity, which we call a `NonUnitalSemiring`.
More concisely: For any rectangular matrix $A$ with entries in a NonUnitalSemiring endowed with a star operation, the product of $A$ and its conjugate transpose is a Hermitian matrix.
|
Matrix.IsHermitian.coe_re_diag
theorem Matrix.IsHermitian.coe_re_diag :
∀ {α : Type u_1} {n : Type u_4} [inst : RCLike α] {A : Matrix n n α},
A.IsHermitian → (fun i => ↑(RCLike.re (A.diag i))) = A.diag
This theorem establishes that if a matrix `A` of type `Matrix n n α` is Hermitian, then the real parts of its diagonal elements are equal to the diagonal elements themselves. Specifically, for any given index `i`, the value of the real part of the diagonal element at `i` is the same as the diagonal element at `i`. Here, `α` is a type with a `RCLike` instance, which allows complex numbers to have real and imaginary parts, and `n` is the type of indices for the matrix's rows and columns. The notation `↑(RCLike.re (A.diag i))` is used to denote the real part of a diagonal element.
More concisely: If `A` is a Hermitian matrix of type `Matrix n n α` with `α` having an `RCLike` instance, then the real parts of its diagonal elements equal the diagonal elements themselves: `↑(RCLike.re (A.diag i)) = A.diag i` for all indices `i`.
|
Matrix.IsHermitian.coe_re_apply_self
theorem Matrix.IsHermitian.coe_re_apply_self :
∀ {α : Type u_1} {n : Type u_4} [inst : RCLike α] {A : Matrix n n α},
A.IsHermitian → ∀ (i : n), ↑(RCLike.re (A i i)) = A i i
This theorem states that for any type `α` that behaves like a set of complex numbers (expressed as "RCLike α"), and any Hermitian matrix `A` of dimensions `n x n` with entries in `α`, the diagonal elements of `A` are real. More specifically, for any index `i`, the real part of the `i, i` entry of `A` equals the `i, i` entry itself. This is a property of Hermitian matrices: their diagonal entries are always real.
More concisely: For any Hermitian matrix A of dimensions n x n over a type α behaving like the complex numbers, the real part of the diagonal entry A(i, i) equals i-th diagonal entry itself for all i.
|
Matrix.isHermitian_fromBlocks_iff
theorem Matrix.isHermitian_fromBlocks_iff :
∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : InvolutiveStar α] {A : Matrix m m α} {B : Matrix m n α}
{C : Matrix n m α} {D : Matrix n n α},
(A.fromBlocks B C D).IsHermitian ↔ A.IsHermitian ∧ B.conjTranspose = C ∧ C.conjTranspose = B ∧ D.IsHermitian
This theorem states that for any type `α` which has an involutive star operation, and any matrices `A` of type `Matrix m m α`, `B` of type `Matrix m n α`, `C` of type `Matrix n m α`, and `D` of type `Matrix n n α`, the block matrix formed by `A`, `B`, `C`, and `D` is Hermitian if and only if the following conditions are all true: `A` is Hermitian, `B` is the conjugate transpose of `C`, `C` is the conjugate transpose of `B`, and `D` is Hermitian. The "Hermitian" property of a matrix refers to the matrix being equal to its own conjugate transpose. The "involutive star operation" is a unary operation that is its own inverse.
More concisely: For any matrices A : Matrix m m α, B : Matrix m n α, C : Matrix n m α, D : Matrix n n α over an type α with an involutive star operation, the block matrix [ A | B ; C | D ] is Hermitian if and only if A is Hermitian, B is the conjugate transpose of C, C is the conjugate transpose of B, and D is Hermitian.
|