QuantumInfo.ForMathlib.HermitianMat.Proj

Given a submodule $S$ of the Euclidean space $\mathbb{k}^n$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$), the projector $P_S$ is the Hermitian matrix representing the orthogonal projection onto $S$. It satisfies $P_S^2 = P_S$, acts as the identity on vectors $v \in S$, and maps any vector in the orthogonal complement $S^\perp$ to zero.

For any submodule $S$ of the Euclidean space $\mathbb{k}^n$, the sum of the orthogonal projector onto $S$ and the orthogonal projector onto its orthogonal complement $S^\perp$ is equal to the identity matrix $I$. In other words, $P_S + P_{S^\perp} = I$.

Let $S$ be a submodule of the Euclidean space $\mathbb{k}^n$, where $\mathbb{k}$ is an `RCLike` field (such as $\mathbb{R}$ or $\mathbb{C}$). Let $P_S$ be the Hermitian matrix representing the orthogonal projection onto $S$. Then the trace of $P_S$ is equal to the rank of the submodule $S$ over $\mathbb{k}$, viewed as a real number: $$\text{Tr}(P_S) = \text{rank}_{\mathbb{k}}(S)$$

Given a Hermitian matrix $A$ acting on the Euclidean space $\mathbb{k}^n$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$), `supportProj` $A$ is the Hermitian matrix representing the orthogonal projection onto the support of $A$. Here, the support of $A$ is defined as the submodule spanned by the eigenvectors corresponding to the non-zero eigenvalues of $A$, which is equivalent to the range of $A$. In other words, this is the orthogonal projector onto $(\ker A)^\perp$.

Let $A$ be a Hermitian matrix in $\text{HermitianMat}(n, \mathbb{k})$, where $\mathbb{k}$ is either $\mathbb{R}$ or $\mathbb{C}$. The kernel projector of $A$, denoted as $P_{\ker A}$, is the Hermitian matrix representing the orthogonal projection onto the kernel (null space) of $A$. Specifically, it is defined as the projector onto the submodule $S = \ker(A)$.

Let $A$ be a Hermitian matrix in $\text{Herm}_n(\mathbb{k})$. Let $P_{\ker A}$ (denoted by `kerProj`) be the orthogonal projector onto the kernel of $A$, and let $P_{\text{supp } A}$ (denoted by `supportProj`) be the orthogonal projector onto the support of $A$ (the subspace spanned by eigenvectors with non-zero eigenvalues). Their sum is equal to the identity matrix: $$P_{\ker A} + P_{\text{supp } A} = I$$

Let $A$ be a Hermitian matrix. If $A$ is non-singular, then its kernel projector $P_{\ker A}$ is the zero matrix. Here, the kernel projector $A.\text{kerProj}$ denotes the Hermitian matrix representing the orthogonal projection onto the kernel (null space) of $A$.

Let $A$ be a Hermitian matrix in $\text{Herm}_n(\mathbb{k})$. If $A$ is non-singular, then its support projector (the projector onto the subspace spanned by eigenvectors with non-zero eigenvalues) is equal to the identity matrix $I$.

Let $S$ be a submodule of the Euclidean space $\mathbb{k}^n$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$) and let $\{b_i\}_{i \in \iota}$ be an orthonormal basis for $S$. The matrix representation of the orthogonal projector $P_S$ onto the submodule $S$ is equal to the sum over $i \in \iota$ of the outer products of the basis vectors, i.e., $$(P_S)_{\text{mat}} = \sum_{i \in \iota} v_i v_i^\dagger$$ where $v_i = \text{subtype}(b_i)$ is the inclusion of the basis vector $b_i$ into $\mathbb{k}^n$, and $v_i^\dagger$ denotes its conjugate transpose.

Let $A$ be a Hermitian matrix of size $n$ over $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$). The matrix representing the orthogonal projector onto the support of $A$ (the subspace spanned by eigenvectors with non-zero eigenvalues) is given by the sum: $$\text{supportProj}(A) = \sum_{i} f(\lambda_i) \cdot v_i v_i^*$$ where $\lambda_i$ are the eigenvalues of $A$, $v_i$ are the corresponding orthonormal eigenvectors, $v_i^*$ denotes the conjugate transpose of $v_i$, and the coefficient $f(\lambda_i)$ is $1$ if $\lambda_i \neq 0$ and $0$ if $\lambda_i = 0$.

Let $A$ be a Hermitian matrix. The orthogonal projector onto the support of $A$, denoted $\text{supportProj}(A)$, is equal to the result of the continuous functional calculus applied to $A$ with the indicator function $f(x)$ that is $0$ if $x = 0$ and $1$ otherwise. That is, $$\text{supportProj}(A) = f(A)$$ where $f(x) = \mathbb{1}_{\mathbb{k} \setminus \{0\}}(x) = \begin{cases} 0 & \text{if } x = 0 \\ 1 & \text{if } x \neq 0 \end{cases}$.

Given two Hermitian matrices $A$ and $B$, the function $\text{projLE}(A, B)$ (denoted as $\{A \le_p B\}$) returns the Hermitian matrix representing the orthogonal projector onto the subspace spanned by the eigenvectors of $B - A$ corresponding to non-negative eigenvalues. Specifically, it is defined by applying the continuous functional calculus to the matrix $(B - A)$ with the indicator function $f(x) = \begin{cases} 1 & \text{if } x \ge 0 \\ 0 & \text{if } x < 0 \end{cases}$. This operator is the unique maximum projector $P$ (satisfying $P^2 = P$) such that $P A P \le P B P$ holds in the Loewner order.

Given two Hermitian matrices $A$ and $B$ in the space $\text{HermitianMat}_n(\mathbb{k})$, the projector onto the positive eigenspace of $B - A$ is defined as the result of applying the continuous functional calculus to $B - A$ with the indicator function $f(x) = \begin{cases} 1 & \text{if } x > 0 \\ 0 & \text{otherwise} \end{cases}$. This operator projects onto the subspace spanned by the eigenvectors of $B - A$ corresponding to strictly positive eigenvalues.

For two Hermitian matrices $A$ and $B$, the notation $\{A \ge_p B\}$ represents the Hermitian projector onto the subspace spanned by the eigenvectors of $A - B$ corresponding to non-negative eigenvalues.

For any two Hermitian matrices $A$ and $B$ (of type `HermitianMat`), the notation $\{A \le_p B\}$ represents the orthogonal projector onto the nonnegative eigenspace of the operator $B - A$.

For two Hermitian matrices $A$ and $B$, the notation $\{A >_p B\}$ (or $\{A >ₚ B\}$) represents the projector onto the positive eigenspace of the Hermitian matrix $A - B$. This is equivalent to `projLT B A`.

This is a scoped notation used to represent the projector onto the positive eigenspace of the difference of two Hermitian matrices $B$ and $A$. Specifically, the notation $\{A <_p B\}$ denotes the operator `projLT A B`, which is the Hermitian matrix projecting onto the subspace spanned by the eigenvectors of $B - A$ corresponding to strictly positive eigenvalues.

For any two Hermitian matrices $A$ and $B$, the projector onto the nonnegative eigenspace of $B - A$, denoted as $\{A \le_p B\}$, is defined as the result of applying the continuous functional calculus to the matrix $B - A$ with the indicator function $f(x) = \begin{cases} 1 & \text{if } 0 \le x \\ 0 & \text{if } x < 0 \end{cases}$.

For any two Hermitian matrices $A$ and $B$, the projector $\{A <_p B\}$ onto the positive eigenspace of $B - A$ is defined as the continuous functional calculus of $B - A$ with the indicator function $f(x) = \begin{cases} 1 & \text{if } x > 0 \\ 0 & \text{otherwise} \end{cases}$.

Let $A$ and $B$ be Hermitian matrices of size $n$ over a field $\mathbb{k}$. Let $\{A \leq_p B\}$ denote the projector onto the nonnegative eigenspace of the difference $B - A$, defined via the continuous functional calculus as $\chi_{[0, \infty)}(B - A)$. Then, this operator is idempotent, satisfying $\{A \leq_p B\}^2 = \{A \leq_p B\}$.

Let $A$ and $B$ be Hermitian matrices of size $n$ over a field $\mathbb{k}$. Let $\{A <_p B\}$ denote the projector onto the positive eigenspace of the Hermitian matrix $B - A$. Then, $\{A <_p B\}$ is idempotent, specifically $\{A <_p B\}^2 = \{A <_p B\}$.

Let $A$ be a Hermitian matrix in $\text{HermitianMat}_n(\mathbb{k})$. The projector onto the nonnegative eigenspace of $A$, denoted by $\{0 \leq_p A\}$, is equal to the result of applying the continuous functional calculus to $A$ with the indicator function $f(x) = \begin{cases} 1 & \text{if } 0 \le x \\ 0 & \text{otherwise} \end{cases}$.

Let $A$ be a Hermitian matrix. The projector onto the positive eigenspace of $A$, denoted by $\{0 <ₚ A\}$, is equal to the result of applying the continuous functional calculus to $A$ with the indicator function $f(x) = \begin{cases} 1 & \text{if } 0 < x \\ 0 & \text{otherwise} \end{cases}$.

For a Hermitian matrix $A$, the projector onto the non-positive eigenspace, denoted by $\{A \leq_p 0\}$, is equal to the continuous functional calculus of $A$ applied to the indicator function of the interval $(-\infty, 0]$. That is, $\{A \leq_p 0\} = \text{cfc}_A(f)$, where $f(x) = 1$ if $x \leq 0$ and $f(x) = 0$ otherwise.

Let $A$ be a Hermitian matrix. The projector onto the positive eigenspace of $0 - A$ (denoted by $\{A <_p 0\}$) is equal to the result of the continuous functional calculus applied to $A$ with the indicator function of the negative real numbers $f(x) = \begin{cases} 1 & \text{if } x < 0 \\ 0 & \text{if } x \geq 0 \end{cases}$.

Let $A$ and $B$ be Hermitian matrices of size $n$ over a field $\mathbf{k}$. Let $\{A \le_p B\}$ denote the projector onto the nonnegative eigenspace of the difference $B - A$, defined via the continuous functional calculus as the indicator function of the interval $[0, \infty)$. Then $\{A \le_p B\}$ is a positive semidefinite matrix, i.e., $0 \le \{A \le_p B\}$ in the Loewner partial order.

Let $A$ and $B$ be Hermitian matrices in $\text{HermitianMat}(n, \mathbb{k})$. Let $\{A <_p B\}$ denote the projector onto the positive eigenspace of the difference $B - A$. Then $\{A <_p B\}$ is a positive semidefinite matrix, i.e., $0 \le \{A <_p B\}$ in the Loewner partial order.

Let $A$ and $B$ be Hermitian matrices in $\text{HermitianMat}(n, \mathbf{k})$. Let $\{A \le_p B\}$ (denoted in Lean as `projLE A B`) be the Hermitian projector onto the nonnegative eigenspace of the difference $B - A$. Then $\{A \le_p B\} \le I$, where $I$ is the identity matrix and $\le$ denotes the Loewner partial order.

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})$, let $\{A \le_p B\}$ denote the projector onto the nonnegative eigenspace of $B - A$. Then the product of the matrix $\{A \le_p B\}$ and the matrix $(B - A)$ is a positive semidefinite matrix, i.e., $0 \le \{A \le_p B\} \cdot (B - A)$.

Let $A$ and $B$ be Hermitian matrices of size $n$ over a field $\mathbb{k}$. Let $P = \{A \leq_p B\}$ be the projector onto the nonnegative eigenspace of the matrix $B - A$. Then, the product of $P$ and $A$ is less than or equal to the product of $P$ and $B$ in terms of their underlying matrices, i.e., $P A \leq P B$.

Let $A$ and $B$ be Hermitian matrices in $\text{Herm}_n(\mathbb{k})$. Let $\{A <_p B\}$ denote the projector onto the positive eigenspace of $B - A$, and let $\{B \le_p A\}$ denote the projector onto the non-negative eigenspace of $A - B$. Then the sum of these two projectors is the identity matrix $I$, i.e., $\{A <_p B\} + {B \le_p A} = 1$.

Let $A$ be a Hermitian matrix in $\text{Herm}_n(\mathbb{k})$. Let $\{A <_p 0\}$ denote the projector onto the negative eigenspace of $A$, and let $\{0 \le_p A\}$ denote the projector onto the nonnegative eigenspace of $A$. Then the sum of the conjugations of these projectors by $A$ satisfies: $$A \{A <_p 0\} A^* + A \{0 \le_p A\} A^* = A$$ where $A.conj(P)$ represents the action of the matrix on a projector via conjugation, and the notation $\{A <_p 0\}$ and $\{0 \le_p A\}$ refers to the projectors onto the strictly negative and nonnegative parts of the spectrum of $A$, respectively.

For any Hermitian matrix $A \in \text{Herm}_n(\mathbb{k})$, the projector onto the support of $A$ (the subspace spanned by eigenvectors with non-zero eigenvalues), denoted by $A.\text{supportProj}$, is equal to the sum of the projector onto the negative eigenspace of $A$ (denoted by $\{A <_p 0\}$) and the projector onto the positive eigenspace of $A$ (denoted by $\{0 <_p A\}$).

For a Hermitian matrix $A \in \text{HermitianMat}_n(\mathbb{k})$, its positive part $A^+$ is defined as the application of the continuous functional calculus to $A$ with the function $f(x) = \max(x, 0)$. This corresponds to the projection of the matrix onto the subspace spanned by its positive eigenvalues.

For a Hermitian matrix $A$ in the space of $n \times n$ Hermitian matrices over a field $\mathbb{k}$, the negative part $A^-$ is defined using the continuous functional calculus (CFC) as $A.cfc(f)$, where $f(x) = \max(-x, 0)$. This corresponds to the projection of the matrix onto the subspace spanned by its negative eigenvalues.

Let $A$ be a Hermitian matrix (represented as `HermitianMat n 𝕜`). The positive part of $A$, denoted as $A^+$, is equal to the result of applying the continuous functional calculus to $A$ with the function $f(x) = \max(x, 0)$ (written as $x \sqcup 0$).

Let $A$ be a Hermitian matrix. The negative part of $A$, denoted $A^{-}$, is equal to the result of applying the continuous functional calculus to $A$ with the function $f(x) = \max(-x, 0)$.

Let $A$ be a Hermitian matrix. The positive part of $A$, denoted $A^+$, is equal to the result of applying the continuous functional calculus to $A$ with the function $f(x) = \begin{cases} x & \text{if } x \ge 0 \\ 0 & \text{if } x < 0 \end{cases}$.

Let $A$ be a Hermitian matrix. The negative part of $A$, denoted $A^{-}$, is equal to the result of applying the continuous functional calculus to $A$ with the function $f(x) = \begin{cases} -x & \text{if } x \le 0 \\ 0 & \text{if } x > 0 \end{cases}$.

Let $A$ be a Hermitian matrix. The positive part of $A$ as defined on the type of Hermitian matrices, denoted $A^+$, is equal to the positive part of its underlying matrix representation, denoted $A.\text{mat}^+$. This theorem establishes that the specific `PosPart` instance for `HermitianMat` is consistent with the standard `PosPart` instance on general matrices.

Let $A$ be a Hermitian matrix. The negative part of $A$ as defined on the type of Hermitian matrices, denoted $A^-$, is equal to the negative part of its underlying matrix representation, denoted $A.\text{mat}^-$. This theorem establishes that the specific `NegPart` instance for `HermitianMat` is consistent with the standard `NegPart` instance on general matrices.

Let $A$ be a Hermitian matrix. The positive part of $A$, denoted $A^+$, is equal to the result of applying the continuous functional calculus to $A$ with the function $f(x) = \begin{cases} x & \text{if } 0 < x \\ 0 & \text{otherwise} \end{cases}$. This implies that the positive part can be equivalently defined using either a strict inequality ($0 < x$) or a non-strict inequality ($0 \le x$) within the functional calculus.

Let $A$ be a Hermitian matrix. The negative part of $A$, denoted $A^{-}$, is equal to the result of applying the continuous functional calculus to $A$ with the function $f(x) = \begin{cases} -x & \text{if } x < 0 \\ 0 & \text{if } x \ge 0 \end{cases}$.

For any Hermitian matrix $A$, the difference between its positive part $A^+$ and its negative part $A^-$ is equal to the matrix itself, i.e., $A^+ - A^- = A$. Here, $A^+$ is the projection of $A$ onto its nonnegative eigenvalues, and $A^-$ is the projection of $-A$ onto its nonnegative eigenvalues (corresponding to the absolute value of the negative eigenvalues of $A$).

Let $A$ be a Hermitian matrix in the space $\text{HermitianMat}(n, \mathbf{k})$. If $A$ is positive semidefinite (denoted as $0 \le A$ in the Loewner partial order), then its positive part $A^+$ is equal to $A$.

Let $A$ be a Hermitian matrix in $\text{HermitianMat}(n, \mathbf{k})$. Let $A^+$ denote the positive part of $A$, which is the result of applying the functional calculus to $A$ with the function $f(x) = \max(0, x)$. Then $A^+$ is a positive semidefinite matrix, i.e., $0 \le A^+$.

Let $A$ be a Hermitian matrix in $\text{HermitianMat } n \: \mathbb{k}$. The negative part of $A$, denoted $A^{-}$, is a positive semidefinite matrix, i.e., $0 \le A^{-}$, where the inequality $\le$ refers to the Loewner partial order.

Let $A$ be a Hermitian matrix in $\text{Herm}_n(\mathbb{k})$. Let $A^+$ denote the positive part of $A$, which is the restriction of $A$ to its nonnegative eigenvalues (formally defined via the continuous functional calculus as the function $f(x) = \max(x, 0)$ applied to $A$). Then it holds that $A \le A^+$ with respect to the Loewner partial order, meaning that $A^+ - A$ is a positive semidefinite matrix.

Let $A$ be a Hermitian matrix. Let $A^+$ and $A^-$ denote the positive and negative parts of $A$, respectively, defined via the continuous functional calculus. Then the product of their underlying matrices is zero, i.e., $A^+ \cdot A^- = 0$.

Let $A$ and $B$ be $n \times n$ Hermitian matrices with entries in an `RCLike` field $\mathbb{k}$. Let $\{A \le_p B\}$ denote the projector onto the nonnegative eigenspace of the Hermitian matrix $(B - A)$. Then the inner product of this projector and the difference $(B - A)$ is non-negative, i.e., $0 \le \langle \{A \le_p B\}, B - A \rangle$, where the inner product $\langle \cdot, \cdot \rangle$ is defined as the trace of the product of the matrices.

Let $A$ and $B$ be Hermitian matrices of the same dimension. Let $\{A \le_p B\}$ denote the projector onto the nonnegative eigenspace of $B - A$. Then the inner product of the projector and $A$ is less than or equal to the inner product of the projector and $B$: $$\langle \{A \le_p B\}, A \rangle \le \langle \{A \le_p B\}, B \rangle$$ where the inner product is defined as $\langle X, Y \rangle = \text{Tr}(XY)$.

Let $A$ and $B$ be $n \times n$ Hermitian matrices over an $\mathbb{R}$-clike field. Let $\{A \le_p B\}$ denote the projector onto the nonnegative eigenspace of $B - A$. The inner product of $\{A \le_p B\}$ and $B - A$, defined as $\langle \{A \le_p B\}, B - A \rangle = \text{Tr}(\{A \le_p B\}(B - A))$, is non-negative.

Let $A$ and $B$ be $n \times n$ Hermitian matrices over a field $\mathbb{K}$ (such as $\mathbb{R}$ or $\mathbb{C}$). Let $\{A \leq_p B\}$ denote the projector onto the nonnegative eigenspace of the Hermitian matrix $B - A$. Then the trace of the product of the projector with $A$ is less than or equal to the trace of its product with $B$, i.e., $$\langle \{A \leq_p B\}, A \rangle \leq \langle \{A \leq_p B\}, B \rangle$$ where $\langle \cdot, \cdot \rangle$ denotes the Frobenius inner product defined by $\langle X, Y \rangle = \text{Tr}(X Y)$.

The positive part operator $(\cdot)^+$, which maps a Hermitian matrix $A \in \text{HermitianMat}(n, \mathbb{C})$ to its projection onto its positive eigenvalues (formally defined via the continuous functional calculus as $A^+ = f(A)$ where $f(x) = \max(x, 0)$), is a continuous function.

Let $\text{HermitianMat}(n, \mathbb{C})$ be the space of $n \times n$ Hermitian matrices over the complex numbers. The negative part operator, denoted by $A \mapsto A^-$, is continuous. Here, the negative part $A^-$ is defined via the continuous functional calculus as $A^- = f(A)$ where $f(x) = \max(-x, 0)$.

Let $A$ and $B$ be Hermitian matrices. Let $\{B \le_p A\}$ be the orthogonal projector onto the non-negative eigenspace of $A - B$, and let $\{A <_p B\}$ be the orthogonal projector onto the positive eigenspace of $B - A$. Then the identity matrix minus the projector onto the non-negative eigenspace of $A - B$ equals the projector onto the positive eigenspace of $B - A$, i.e., $1 - \{B \le_p A\} = \{A <_p B\}$.

Let $A$ and $B$ be Hermitian matrices of size $n$ over a field $\mathbb{k}$. Let $\{A <_p B\}$ denote the projector onto the positive eigenspace of $B - A$, defined via continuous functional calculus as $\mathbb{1}_{(0, \infty)}(B - A)$. Then the product of this projector and the difference matrix $B - A$ is a positive semi-definite matrix, i.e., $0 \le \{A <_p B\} \cdot (B - A)$.

Let $A$ and $B$ be Hermitian matrices of size $n \times n$ over a field $\mathbb{k}$. Let $\{A <_p B\}$ (denoted as `projLT A B`) be the Hermitian matrix that projects onto the positive eigenspace of $B - A$. Then, the product of the matrix of this projector and $A$ is less than or equal to the product of the matrix of this projector and $B$: $$\{A <_p B\}.mat \cdot A.mat \le \{A <_p B\}.mat \cdot B.mat$$ where the inequality denotes the Loewner order (the difference of the matrices is positive semi-definite).

For any Hermitian matrix $A$, the inner product between $A$ and its negative part $A^-$ is non-positive, i.e., $\langle A, A^-\rangle \le 0$. Here, the inner product is defined as $\text{Tr}(AB)$ and the negative part $A^-$ is the restriction of the matrix to its non-positive eigenvalues.

Let $A$ be a Hermitian matrix. Let $A^+$ denote the positive part of $A$ and $A^-$ denote the negative part of $A$. The inner product $\langle A^+, A^- \rangle$ is equal to $0$. Here, the inner product of two Hermitian matrices $A$ and $B$ is defined as $\langle A, B \rangle = \text{tr}(AB)$.

Let $A$ be a Hermitian matrix and $A^-$ denote its negative part, which corresponds to the restriction of the matrix to its non-positive eigenvalues. Let $\langle A, B \rangle = \text{Tr}(AB)$ be the Frobenius inner product on the space of Hermitian matrices. Then, the inner product of $A$ and its negative part is zero, $\langle A, A^-\rangle = 0$, if and only if $A$ is positive semi-definite ($0 \le A$).