Matrix.PosSemidef.sq_sqrt
theorem Matrix.PosSemidef.sq_sqrt :
β {n : Type u_2} {π : Type u_4} [inst : Fintype n] [inst_1 : RCLike π] [inst_2 : DecidableEq n] {A : Matrix n n π}
(hA : A.PosSemidef), hA.sqrt ^ 2 = A
The theorem `Matrix.PosSemidef.sq_sqrt` states that for any given square matrix 'A' of type 'π' with 'n' as the index type, where 'n' is of finite type and 'π' is a type that behaves like a ring with conjugation (i.e., 'π' is `RCLike`), and also 'n' has a decidable equality, if 'A' is found to be positive semi-definite (meaning that it's Hermitian and the product of the conjugate transpose of any vector 'x' and the resultant of matrix 'A' multiplied with 'x' is non-negative), then the square of the square root of 'A' is equal to 'A' itself. In mathematical terms, if 'A' is positive semi-definite, then $(\sqrt{A})^2 = A$.
More concisely: If 'A' is a square matrix of finite index type 'n' over a conjugate ring 'π' with decidable equality, and 'A' is positive semi-definite, then 'A' equals the square of its square root.
|
Matrix.PosSemidef.toLinearMapβ'_zero_iff
theorem Matrix.PosSemidef.toLinearMapβ'_zero_iff :
β {n : Type u_2} {π : Type u_4} [inst : Fintype n] [inst_1 : RCLike π] [inst_2 : DecidableEq n] {A : Matrix n n π},
A.PosSemidef β β (x : n β π), ((Matrix.toLinearMapβ' A) (star x)) x = 0 β (Matrix.toLin' A) x = 0
This theorem states that for a given matrix `A` that is positive semidefinite, the statement `xβ A x = 0` is equivalent to `A x = 0`, when expressed in terms of linear maps. Here, `n` is the type for indexing the rows and columns of the matrix, `π` denotes the type of the elements in the matrix, and `x` is a function mapping indices of the matrix to elements. The equivalence holds for all `x` of the appropriate type and the positive semidefinite matrix `A`. The `star` function in `xβ A x` represents the adjoint or conjugate transpose of `x`. The statement `xβ A x = 0` can be read as "the result of multiplying the adjoint of `x` with `A` and then with `x` equals zero", while `A x = 0` can be read as "the result of applying the linear map `A` to `x` equals zero".
More concisely: For a positive semidefinite matrix A, the vector x is in the null space of A if and only if the dot product xβAβx is zero.
|
Matrix.PosSemidef.eigenvalues_nonneg
theorem Matrix.PosSemidef.eigenvalues_nonneg :
β {n : Type u_2} {π : Type u_4} [inst : Fintype n] [inst_1 : RCLike π] [inst_2 : DecidableEq n] {A : Matrix n n π}
(hA : A.PosSemidef) (i : n), 0 β€ β―.eigenvalues i
This theorem states that the eigenvalues of a positive semi-definite matrix are non-negative. In more detail, it applies to any finite type `n`, any type `π` that behaves like real or complex numbers (denoted by `RCLike π`), and any matrix `A` of type `Matrix n n π` (i.e., a matrix with both row and column indices taken from `n` and entries in `π`). If `A` is a positive semi-definite matrix (as indicated by `A.PosSemidef`), then for any index `i` in `n`, the eigenvalue of `A` at index `i` is greater than or equal to zero.
More concisely: If `A` is a positive semi-definite matrix of type `Matrix n n π`, then all its eigenvalues are non-negative.
|
Matrix.PosSemidef.dotProduct_mulVec_zero_iff
theorem Matrix.PosSemidef.dotProduct_mulVec_zero_iff :
β {n : Type u_2} {π : Type u_4} [inst : Fintype n] [inst_1 : RCLike π] {A : Matrix n n π},
A.PosSemidef β β (x : n β π), Matrix.dotProduct (star x) (A.mulVec x) = 0 β A.mulVec x = 0
The theorem states that for a positive semidefinite matrix `A` over a field `π` indexed by the type `n`, for any vector `x` of elements from `π`, the dot product of the conjugate of `x` and the result of multiplying `A` and `x` equals zero if and only if the result of multiplying `A` and `x` equals zero. This theorem is essential in the field of matrix algebra and can be used to derive many interesting properties of positive semidefinite matrices.
More concisely: For a positive semidefinite matrix A over a field π and any vector x from π of length n, the dot product of the conjugate of x and Ax equals zero if and only if Ax equals the zero vector.
|
Matrix.PosDef.eigenvalues_pos
theorem Matrix.PosDef.eigenvalues_pos :
β {n : Type u_2} {π : Type u_4} [inst : Fintype n] [inst_1 : RCLike π] [inst_2 : DecidableEq n] {A : Matrix n n π}
(hA : A.PosDef) (i : n), 0 < β―.eigenvalues i
This theorem states that the eigenvalues of a positive definite matrix are positive. More precisely, for any type `n` which has finite instances and decidable equality, any type `π` which behaves like an ordered ring, and any positive definite matrix `A` of type `Matrix n n π`, the eigenvalues of `A` are all greater than zero. That is, for every index `i` in `n`, the `i`-th eigenvalue of `A` is positive.
More concisely: The eigenvalues of a positive definite matrix are all positive.
|
Matrix.PosDef.re_dotProduct_pos
theorem Matrix.PosDef.re_dotProduct_pos :
β {n : Type u_2} {π : Type u_4} [inst : Fintype n] [inst_1 : RCLike π] {M : Matrix n n π},
M.PosDef β β {x : n β π}, x β 0 β 0 < RCLike.re (Matrix.dotProduct (star x) (M.mulVec x))
The theorem `Matrix.PosDef.re_dotProduct_pos` states that for any type `n` with a finite number of instances, any `π` which is a RC-like structure (an algebraic structure that behaves like the complex numbers), and any given matrix `M` with dimensions `n x n` and entries in `π`, if `M` is positive definite, then for any non-zero vector `x` with entries in `π`, the real part of the dot product of the conjugate of `x` and the vector obtained by multiplying `M` with `x` is greater than zero. The dot product is computed as the sum of the entrywise products, and the real part is extracted using the `RCLike.re` function. This essentially states that the real part of the conjugate transpose of a vector times a positive definite matrix times the vector itself is always positive for non-zero vectors, a key property of positive definite matrices.
More concisely: For any non-zero vector x and positive definite matrix M of compatible dimensions over an RC-like structure π, the real part of the dot product of the conjugate of x and the product of M and x is positive.
|
Matrix.posSemidef_diagonal_iff
theorem Matrix.posSemidef_diagonal_iff :
β {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : CommRing R] [inst_2 : PartialOrder R]
[inst_3 : StarRing R] [inst_4 : StarOrderedRing R] [inst_5 : DecidableEq n] {d : n β R},
(Matrix.diagonal d).PosSemidef β β (i : n), 0 β€ d i
The theorem `Matrix.posSemidef_diagonal_iff` states that for any finite type `n`, commutative ring `R` which is also a star ring, star ordered ring, and has decidable equality, and a function `d : n β R`, a diagonal matrix is positive semidefinite if and only if its diagonal entries are nonnegative. That is, a matrix `Matrix.diagonal d` is positive semidefinite if and only if for all `i` in `n`, `d i` is greater than or equal to zero. In mathematical terms, a diagonal matrix $D$ is positive semidefinite, denoted as $D \succeq 0$, if and only if all its diagonal entries $d_i$ are nonnegative, denoted as $d_i \geq 0$, for all $i$ in $n$.
More concisely: A diagonal matrix over a commutative ring that is also a star ring, star ordered, and has decidable equality is positive semidefinite if and only if all its diagonal entries are nonnegative.
|
Matrix.posSemidef_iff_eq_transpose_mul_self
theorem Matrix.posSemidef_iff_eq_transpose_mul_self :
β {n : Type u_2} {π : Type u_4} [inst : Fintype n] [inst_1 : RCLike π] {A : Matrix n n π},
A.PosSemidef β β B, A = B.conjTranspose * B
This theorem states that a matrix is positive semidefinite if and only if it can be expressed in the form `Bα΄΄ * B` for some matrix `B`. Here, `n` is the type indexing the rows and columns of the matrices, `π` is the type of the entries in the matrices, and `A` is any matrix of type `Matrix n n π`. The `PosSemidef` property of a matrix signifies that it is positive semidefinite. In other words, the theorem provides a characterization of positive semidefinite matrices in terms of the existence of a matrix `B` such that `A` equals the conjugate transpose of `B` multiplied by `B`.
More concisely: A matrix A of type Matrix n n π is positive semidefinite if and only if it can be expressed as Bα΄΄ * B for some matrix B of the same type.
|
Matrix.posSemidef_conjTranspose_mul_self
theorem Matrix.posSemidef_conjTranspose_mul_self :
β {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : CommRing R]
[inst_3 : PartialOrder R] [inst_4 : StarRing R] [inst_5 : StarOrderedRing R] (A : Matrix m n R),
(A.conjTranspose * A).PosSemidef
The theorem states that for any matrix `A` with entries in a commutative ring `R` that is also a star-ordered ring and has a partial order, the product of the conjugate transpose of `A` and `A` itself is always positive semidefinite. This means that the resulting matrix is Hermitian (its conjugate transpose equals itself) and for any vector `x`, the dot product of the conjugate of `x` with the matrix-vector product of `A` and `x` is nonnegative.
More concisely: For any matrix $A$ with entries in a commutative ring $R$ that is also a star-ordered ring with a partial order, the product of the conjugate transpose and $A$ is Hermitian and positive semidefinite.
|
Matrix.posSemidef_self_mul_conjTranspose
theorem Matrix.posSemidef_self_mul_conjTranspose :
β {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : CommRing R]
[inst_3 : PartialOrder R] [inst_4 : StarRing R] [inst_5 : StarOrderedRing R] (A : Matrix m n R),
(A * A.conjTranspose).PosSemidef
The theorem `Matrix.posSemidef_self_mul_conjTranspose` states that for any matrix `A` of type `Matrix m n R` where `R` is a commutative ring that additionally has a partial order relation, a star-ring operation and is a star-ordered ring, the result of the matrix `A` multiplied by its conjugate transpose is positive semidefinite. Here, `m` and `n` are the types that index the rows and columns of the matrix respectively.
More concisely: For any `m x n` matrix `A` over a commutative ring `R` with a partial order relation, star-ring operation, and star-order property, `A` multiplied by its conjugate transpose is positive semidefinite.
|
Matrix.PosSemidef.conjTranspose_mul_mul_same
theorem Matrix.PosSemidef.conjTranspose_mul_mul_same :
β {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : CommRing R] [inst_2 : PartialOrder R]
[inst_3 : StarRing R] [inst_4 : StarOrderedRing R] {A : Matrix n n R},
A.PosSemidef β β {m : Type u_5} [inst_5 : Fintype m] (B : Matrix n m R), (B.conjTranspose * A * B).PosSemidef
The theorem `Matrix.PosSemidef.conjTranspose_mul_mul_same` states that for any given commutative ring `R`, with a partial order and a star operation (i.e., it is a star-ordered ring), and finite types `n` and `m`; if matrix `A` with entries in `R` of size `n Γ n` is positive semidefinite, then for any matrix `B` of size `n Γ m` with entries in `R`, the product of the conjugate transpose of `B`, `A`, and `B` is also positive semidefinite. In mathematical terms, if `A` is positive semidefinite, then so is ${B^*}AB$ for any `B`.
More concisely: If `A` is a positive semidefinite `n Γ n` matrix over a commutative ring `R` with a partial order and a star operation, then for any `n Γ m` matrix `B` over `R`, the product `{B^*}AB` is also positive semidefinite.
|