QuantumInfo.ForMathlib.HermitianMat.Order

For a finite-dimensional Hilbert space (or more generally, a matrix space over a field $\mathbf{k}$ with an involution), the type `HermitianMat n 𝕜` of Hermitian matrices (self-adjoint matrices) is equipped with a partial order $\le$. This order is the Loewner order, where for two Hermitian matrices $A$ and $B$, we define $A \le B$ if and only if the difference $B - A$ is a positive semidefinite matrix.

The set of Hermitian matrices $\text{HermitianMat}_n(\mathbb{k})$ of size $n$ over a field $\mathbb{k}$ satisfies the axioms of an ordered additive monoid. Specifically, for any such Hermitian matrices $A, B$, and $C$, if $A \le B$, then $C + A \le C + B$, where the partial order $\le$ is defined such that $A \le B$ if and only if the difference $B - A$ is a positive semidefinite matrix.

Let $n$ be a natural number and $\mathbb{k}$ be a field. For any two Hermitian matrices $A, B \in \text{HermitianMat}(n, \mathbb{k})$, the relation $A \le B$ holds if and only if the matrix difference $B - A$ is positive semidefinite. Here, $\le$ denotes the partial order on Hermitian matrices, and $\text{PosSemidef}$ denotes the property of a matrix being positive semidefinite.

Let $A \in \text{HermitianMat}(n, \mathbb{k})$ be a Hermitian matrix of size $n$ over a field $\mathbb{k}$. Then $0 \le A$ with respect to the Loewner partial order if and only if the underlying matrix $A$ is positive semidefinite.

Let $A$ and $B$ be Hermitian matrices of size $n$ over a field $\mathbf{k}$. Then $A \le B$ with respect to the Loewner partial order if and only if for every vector $x$, the quadratic form inequality $x^* A x \le x^* B x$ holds, where $x^*$ (denoted by `star x`) is the conjugate transpose of $x$.

In the space of Hermitian matrices of size $n$ over a field $\mathbf{k}$, the zero matrix $0$ is less than or equal to the identity matrix $I$ ($0 \le I$) with respect to the Loewner partial order.

For any two Hermitian matrices $A$ and $B$, the relation $A < B$ holds if and only if the matrix difference $B - A$ is positive semidefinite and $A$ is not equal to $B$.

The space of Hermitian matrices $\text{HermitianMat}(n, \mathbb{k})$ over a field $\mathbb{k}$ (where $\mathbb{k}$ is typically $\mathbb{R}$ or $\mathbb{C}$) forms a strictly ordered module over the real numbers $\mathbb{R}$. This means that for any Hermitian matrices $A, B$ and any real scalar $c > 0$, if $A < B$ in the sense of the Loewner order (i.e., $B - A$ is positive definite), then $cA < cB$.

Let $A$ be a Hermitian matrix in $\text{HermitianMat}(n, \mathbb{k})$. $A$ is positive semidefinite ($0 \le A$ in the Loewner order) if and only if the spectrum of its underlying matrix, denoted $\sigma(A)$, is a subset of the interval $[0, \infty)$.

Let $A$ be a Hermitian matrix in $\text{HermitianMat}(n, \mathbb{k})$. $A$ is positive semidefinite ($0 \le A$) if and only if every element $x$ in the spectrum of its underlying matrix $A.\text{mat}$ is non-negative ($0 \le x$).

Let $A$ be a Hermitian matrix in $\text{HermitianMat}(n, \mathbf{k})$. If $A$ is positive semidefinite (denoted as $0 \le A$), then its trace $\text{tr}(A)$ is a non-negative real number, i.e., $0 \le \text{tr}(A)$.

Let $\mathbb{k}$ be an $\mathbb{R}$-clike field (such as $\mathbb{R}$ or $\mathbb{C}$) and $n$ be a finite type. Let $A$ be a Hermitian matrix of size $n \times n$ over $\mathbb{k}$. If $A$ is strictly greater than zero in the partial order of Hermitian matrices (meaning $A$ is positive semidefinite and $A \neq 0$), then its trace is strictly positive, i.e., $\text{tr}(A) > 0$.

The definition provides a tactic extension for the `positivity` tactic to handle the trace of a Hermitian matrix. Specifically, for a Hermitian matrix $A$, it identifies the positivity property of $\text{Tr}(A)$ based on the property of $A$: - If $A$ is positive definite ($A > 0$), it concludes that $\text{Tr}(A) > 0$ using the lemma `trace_pos`. - If $A$ is positive semi-definite ($A \geq 0$), it concludes that $\text{Tr}(A) \geq 0$ using the lemma `trace_nonneg`.

The space of Hermitian matrices $\text{HermitianMat}(n, \mathbf{k})$ constitutes a positively monotone scalar multiplication module over the real numbers $\mathbb{R}$. Specifically, for any positive real number $c > 0$ and any two Hermitian matrices $A, B \in \text{HermitianMat}(n, \mathbf{k})$, if $A \le B$ with respect to the Löwner partial order, then $c \cdot A \le c \cdot B$.

The space of Hermitian matrices $\text{HermitianMat}(n, \mathbb{k})$ satisfies the property that scalar multiplication by a positive Hermitian matrix is monotonic with respect to real numbers. Specifically, for any real numbers $r, s \in \mathbb{R}$ and any Hermitian matrix $A \in \text{HermitianMat}(n, \mathbb{k})$ such that $0 \le A$, if $r \le s$, then $r \cdot A \le s \cdot A$.

The space of Hermitian matrices $\text{Herm}_n(\mathbb{k})$ satisfies the property of reflecting scalar multiplication by positive real numbers with respect to the partial order $\le$ (the Loewner order). Specifically, for any $r \in \mathbb{R}$ such that $0 < r$ and any Hermitian matrices $A, B \in \text{Herm}_n(\mathbb{k})$, if $r \cdot A \le r \cdot B$, then $A \le B$.

Let $A$ be a Hermitian matrix of size $n \times n$ over an $\mathbb{R}$-clike field $\mathbb{k}$ (such as $\mathbb{R}$ or $\mathbb{C}$). If $A$ is positive semidefinite ($0 \le A$), then $A \le \text{tr}(A) \cdot I$, where $\text{tr}(A)$ is the trace of $A$, $I$ is the identity matrix, and $\le$ denotes the Loewner partial order.

Let $A$ and $B$ be Hermitian matrices of dimensions $m \times m$ and $n \times n$ respectively over a field $\mathbb{k}$. If $A$ and $B$ are non-negative ($0 \le A$ and $0 \le B$), then their Kronecker product $A \otimes_k B$ is also non-negative ($0 \le A \otimes_k B$). In the context of Hermitian matrices, the relation $0 \le A$ is equivalent to $A$ being a positive semidefinite matrix.

Let $A$ and $B$ be Hermitian matrices of dimensions $m \times m$ and $n \times n$ respectively over an $\mathbb{R}$-clike field $\mathbb{k}$. If $A$ and $B$ are strictly positive in the Loewner partial order (meaning they are positive semidefinite and non-zero, denoted $0 < A$ and $0 < B$), then their Kronecker product $A \otimes_k B$ is also strictly positive ($0 < A \otimes_k B$).

Let $A$ be a square matrix of size $n \times n$ over a field $\mathbb{k}$. If $A$ is positive semidefinite (denoted as $A.\text{PosSemidef}$), then $A$ is non-negative when viewed as a Hermitian matrix (denoted as $0 \leq A$).

Let $A$ be a square matrix of size $n \times n$ over a field $\mathbb{k}$. If $n$ is non-empty and $A$ is positive definite ($A \succ 0$ in the sense of `Matrix.PosDef`), then $A$ is strictly positive ($0 < A$) when viewed as an element of the space of Hermitian matrices.

The definition `HermitianMat.evalMatrixPSD` provides a computational procedure (a `Positivity` tactic extension) that searches the local hypothesis context for proofs of positive semidefiniteness ($A \succeq 0$) or positive definiteness ($A \succ 0$) for a square matrix $A$. If a proof of `A.PosDef` is found, the tactic concludes $A > 0$ in the relevant sense. If a proof of `A.PosSemidef` is found, it concludes $A \geq 0$.

Let $A$ be a Hermitian matrix. If the underlying matrix of $A$ (denoted by $A.\text{mat}$) is positive semidefinite, then $A$ is non-negative with respect to the partial order on Hermitian matrices ($0 \le A$).

Let $n$ be a non-empty finite set and $A$ be a Hermitian matrix of size $n \times n$ over a field $\mathbb{k}$. If the underlying matrix of $A$ is positive definite ($A_{\text{mat}} \succ 0$), then $A$ is strictly greater than zero ($A > 0$) with respect to the partial order on Hermitian matrices.

The `evalHermitianMatPSD` tactic extension for the `positivity` tactic facilitates proofs of the positivity or non-negativity of a Hermitian matrix $A$. It searches the local context for hypotheses identifying the underlying matrix $A.\text{mat}$ as either positive definite ($A.\text{mat.PosDef}$) or positive semidefinite ($A.\text{mat.PosSemidef}$). If a positive definite hypothesis is found, it proves $0 < A$. If only a positive semidefinite hypothesis is found, it proves $0 \le A$.

This is a computational tactic extension for the `positivity` framework. It provides a procedure to automatically prove that the Kronecker product $A \otimes B$ of two Hermitian matrices is positive semidefinite ($0 \le A \otimes B$) or positive definite ($0 < A \otimes B$). Specifically: - If both $A$ and $B$ are strictly positive definite ($0 < A$ and $0 < B$), the tactic proves that $A \otimes B$ is strictly positive definite. - If both $A$ and $B$ are positive semidefinite ($0 \le A$ and $0 \le B$), the tactic proves that $A \otimes B$ is positive semidefinite. The extension functions by inspecting the expression for `HermitianMat.kronecker`, recursively determining the positivity of the factors $A$ and $B$, and then applying the corresponding lemma (`HermitianMat.kronecker_pos` or `HermitianMat.kronecker_nonneg`).

Let $A$ be a Hermitian matrix of size $n \times n$ over a field $\mathbb{k}$, and let $M$ be an $m \times n$ matrix. If $A$ is positive semidefinite ($0 \le A$), then its conjugation by $M$, defined as $A.\text{conj}(M) = MAM^*$, is also positive semidefinite ($0 \le MAM^*$).

Let $A$ be a Hermitian $n \times n$ matrix over a field $\mathbb{k}$, and let $M$ be an $m \times n$ matrix. If $A$ is positive definite ($0 < A$) and the kernel of the linear map defined by $M$ is contained within the kernel of $A$ ($\ker M \subseteq \ker A$), then the conjugation of $A$ by $M$, defined as $MAM^*$, is also positive definite ($0 < MAM^*$).

This definition provides an extension for the `positivity` tactic to automatically prove that the conjugation of a Hermitian matrix $A$ by a matrix $M$, denoted as $MAM^*$, is positive semidefinite ($0 \le MAM^*$). Specifically, if the tactic can verify that the input Hermitian matrix satisfies $A \ge 0$, it constructs a proof that $MAM^* \ge 0$ using the theorem `HermitianMat.conj_nonneg`.

Let $A$ and $B$ be Hermitian matrices such that $A \ge 0$ and $B \ge 0$. For any non-negative real scalars $c_1 \ge 0$ and $c_2 \ge 0$, the linear combination $c_1 A + c_2 B$ is also non-negative, i.e., $c_1 A + c_2 B \ge 0$. Here, the inequality $\ge 0$ refers to the partial order on Hermitian matrices, where $M \ge 0$ if and only if $M$ is positive semidefinite.

For any Hermitian matrix $A$ over a field $\mathbb{k}$ with indices in a finite type $n$ (where equality is decidable), the square of the matrix $A^2$ is positive semidefinite, i.e., $0 \le A^2$.

Let $A$ and $B$ be Hermitian matrices. If $A$ is positive semidefinite (i.e., $0 \leq A$), then $A \leq B$ implies that the kernel of $B$ is a subspace of the kernel of $A$ (i.e., $\ker B \subseteq \ker A$). Here, the inequalities refer to the Löwner partial order on Hermitian matrices.

Let $A$ and $B$ be Hermitian matrices of the same dimensions such that $A \le B$ with respect to the Löwner partial order (meaning $B - A$ is positive semidefinite). For any matrix $M$, let $A.conj M$ denote the congruence transformation $M^* A M$. Then, the inequality $M^* A M \le M^* B M$ holds.

Let $A$ be a Hermitian matrix and $N$ be an invertible matrix. If $A$ is positive definite (denoted $A.mat.PosDef$), then the congruence transformation of $A$ by $N$, defined as $N A N^H$ (denoted $A.conj \ N$), is also positive definite.

Let $A$ be a Hermitian matrix and $M$ be an invertible matrix. Then the inverse of the congruence $M^* A M$ (denoted as $A\text{.conj } M$) is equal to the congruence of the inverse of $A$ by the adjoint of the inverse of $M$. That is, $(M^* A M)^{-1} = (M^{-1}) A^{-1} (M^{-1})^*$, or in terms of the `conj` notation: $(A\text{.conj } M)^{-1} = A^{-1}\text{.conj } (M^{-1})^\dagger$.

Let $A$ and $B$ be Hermitian matrices of size $n$ over a field $\mathbb{k}$. Then $A \le B$ if and only if for every vector $v \in \mathbb{k}^n$, the quadratic form inequality $v^* A v \le v^* B v$ holds, where $v^*$ denotes the conjugate transpose (star) of $v$ and $v^* A v$ is the inner product of $v$ with $Av$.

Let $A$ be a Hermitian matrix in $\text{HermitianMat}(n, \mathbb{k})$. If $A$ is positive semi-definite (denoted $0 \le A$), then for any vector $v \in \mathbb{k}^n$, the quadratic form is non-negative, specifically $0 \le v^\dagger A v$, where $v^\dagger$ denotes the conjugate transpose of $v$ and $A$ is the underlying matrix of the Hermitian operator.

Let $A$ be a positive semidefinite Hermitian matrix ($0 \le A$) of size $n$ over a field $\mathbb{k}$, and let $v$ be a vector in the Euclidean space $\mathbb{k}^n$. If the quadratic form associated with $A$ and $v$ is zero, i.e., $v^* A v = 0$ (where $v^*$ denotes the conjugate transpose), then $v$ lies in the kernel of $A$.

[DecidableEq n] (hA : 0 ≤ A) (hB : 0 ≤ B) : (A + B).ker = A.ker ⊓ B.ker

Let $f: \iota \to \text{HermitianMat}_n(\mathbb{k})$ be a finite family of Hermitian matrices such that each $f(i)$ is positive semidefinite ($0 \le f(i)$). Then the kernel of the sum of these matrices is equal to the intersection of the kernels of the individual matrices: $$\ker\left(\sum_{i \in \iota} f(i)\right) = \bigcap_{i \in \iota} \ker(f(i))$$ where the intersection is taken in the lattice of submodules.

Let $A$ be a positive semidefinite Hermitian matrix ($0 \le A$) and $B$ be a square matrix. The kernel of the congruence transformation $(A.\text{conj } B) = B^* A B$ is given by the preimage of the kernel of $A$ under the linear map defined by the conjugate transpose $B^*$. That is, $\ker(B^* A B) = (B^*)^{-1}(\ker A)$, where $B^*$ is viewed as a linear map on Euclidean space.

Let $n$ be a finite type with decidable equality and $\mathbf{k}$ be a field. Let $A$ and $B$ be Hermitian matrices of size $n \times n$ over $\mathbf{k}$. For any non-zero real number $\alpha \neq 0$, if $A$ is positive semidefinite ($0 \le A$) and $A$ is bounded above by a scalar multiple of $B$ in the Loewner order ($A \le \alpha \cdot B$), then the kernel of $B$ is a submodule of the kernel of $A$ ($\ker B \subseteq \ker A$).

Let $A$ be a Hermitian matrix in $\text{HermitianMat}(n, \mathbb{k})$. If $A$ is positive semi-definite (denoted by $0 \le A$), then all its eigenvalues $\lambda_i$ (for $i \in n$) are non-negative, i.e., $0 \le \lambda_i$.

Let $A$ be a Hermitian matrix. If $A$ is positive semi-definite (i.e., $0 \le A$ in the Loewner order), then its underlying matrix representation $A.\text{mat}$ is also non-negative ($0 \le A.\text{mat}$).

Let $A$ be a Hermitian matrix. If $A$ is strictly positive ($0 < A$) according to the partial order on Hermitian matrices, then its underlying matrix $A.\text{mat}$ is also strictly positive ($0 < A.\text{mat}$) in the Loewner order.

Let $M$ be an $m \times n$ matrix over a field $\mathbb{k}$, where $m$ is a finite type. Then the product of its conjugate transpose and itself, $M^H M$, is positive semidefinite (nonnegative in the Loewner order), denoted as $0 \le M^H M$.

For any matrix $M$ with entries in $\mathbb{K}$ whose row index set $m$ is finite, the product of $M$ and its conjugate transpose $M^H$ is positive semidefinite, denoted as $0 \le M M^H$, in the Loewner order.

Let $M$ be an $m \times m$ matrix over a field $\mathbf{k}$. If $M$ is positive semidefinite (denoted $0 \le M$), then the corresponding element in the subtype of Hermitian matrices $\text{HermitianMat}_m(\mathbf{k})$, formed by $M$ and the proof that it is Hermitian, is also non-negative (positive semidefinite) within that subtype.

Let $M \in \mathbb{M}_{m \times m}(\mathbb{k})$ be a square matrix over the field $\mathbb{k}$. If $M$ is positive definite (denoted $0 < M$), then the corresponding element in the type of Hermitian matrices $\text{HermitianMat}(m, \mathbb{k})$ (constructed from $M$ and the proof that its positive semidefiniteness implies it is Hermitian) is also strictly positive (denoted $0 < \langle M, h_{Hermitian} \rangle$).

This is a computational extension for the `positivity` tactic. Given a Hermitian matrix $A$ (of type `HermitianMat`), if the tactic can prove $A$ is positive definite ($0 < A$), it concludes that its underlying matrix representation $A.\text{mat}$ is also positive definite. If the tactic can only prove $A$ is positive semi-definite ($0 \le A$), it concludes that $A.\text{mat}$ is positive semi-definite.

The `positivity` extension for the underlying matrix of a Hermitian matrix $A$. If $A$ is proved to be positive ($0 < A$), the extension proves that its matrix representation $A.\text{mat}$ is positive. If $A$ is proved to be non-negative ($0 \le A$), the extension proves that $A.\text{mat}$ is non-negative.

For any matrix $M$, the product of the matrix and its conjugate transpose, $M M^H$, is a positive semi-definite (non-negative) matrix. This statement provides a tactic extension for the `positivity` tool to automatically prove that $M M^H \geq 0$.

This is a tactic extension for the `positivity` framework that proves the product of a conjugate transpose of a matrix and the matrix itself, $M^H M$ (or $M^* M$), is always a positive semidefinite matrix. Specifically, for any matrix $M$, it identifies the pattern $M^H M$ and applies the theorem that such a product is non-negative ($M^H M \ge 0$).

This is a `positivity` extension for the constructor of a Hermitian matrix $\langle M, \text{pf} \rangle$, where $M$ is a matrix and $\text{pf}$ is a proof that $M$ is Hermitian ($M = M^\dagger$). It allows the `positivity` tactic to conclude that a Hermitian matrix is positive ($0 < \langle M, \text{pf} \rangle$) or non-negative ($0 \le \langle M, \text{pf} \rangle$) in the partial order of Hermitian matrices if the underlying matrix $M$ satisfies the corresponding property in the matrix order ($0 < M$ or $0 \le M$).

Given a square matrix $M$ and an index $i$, if $M$ is a Hermitian matrix ($M = M^*$) and $M$ is positive semidefinite ($M \ge 0$), then the $i$-th eigenvalue of $M$, denoted as $\lambda_i(M)$, is non-negative, i.e., $\lambda_i(M) \ge 0$. This definition serves as a tactic extension for the `positivity` solver, allowing it to automatically infer the non-negativity of eigenvalues by verifying the positive semidefiniteness of the underlying Hermitian matrix.