QuantumInfo.ForMathlib.HermitianMat.Inner

For $n \times n$ Hermitian matrices $A, B$ with entries in a field $\alpha$, the inner product $\langle A, B \rangle_{\mathbb{R}}$ is defined as the result of mapping the trace of the matrix product $AB$ to its self-adjoint part (as a real-valued scalar) via the map `selfadjMap`. That is, $\langle A, B \rangle_{\mathbb{R}} = \text{trace}(AB)$.

Let $A$ and $B$ be Hermitian matrices of size $n \times n$ over a ring $\alpha$. The inner product $\langle A, B \rangle_{\mathbb{R}}$ is defined as the self-adjoint part of the trace of the product of their underlying matrices, i.e., $\langle A, B \rangle_{\mathbb{R}} = \text{selfadjMap}(\text{tr}(A \cdot B))$.

Let $A, B$, and $C$ be Hermitian matrices of size $n \times n$. The inner product on the space of Hermitian matrices satisfies the right-linearity (additivity) property: $\langle A, B + C \rangle_{\mathbb{R}} = \langle A, B \rangle_{\mathbb{R}} + \langle A, C \rangle_{\mathbb{R}}$, where the inner product $\langle \cdot, \cdot \rangle_{\mathbb{R}}$ is the Hilbert–Schmidt inner product restricted to Hermitian matrices.

Let $A$, $B$, and $C$ be Hermitian matrices of the same dimension. The inner product on the space of Hermitian matrices satisfies left-distributivity over addition: $$\langle A + B, C \rangle_{\mathbb{R}} = \langle A, C \rangle_{\mathbb{R}} + \langle B, C \rangle_{\mathbb{R}}$$ Here, $\langle \cdot, \cdot \rangle_{\mathbb{R}}$ denotes the canonical inner product for Hermitian matrices, which is defined as the real-valued trace of the product of the matrices (equivalent to the Hilbert–Schmidt inner product in the Hermitian case).

Let $A$ be a Hermitian matrix. The inner product of $A$ with the zero matrix $0$ is equal to zero, denoted as $\langle A, 0 \rangle_{\mathbb{R}} = 0$. Here, the inner product on the space of Hermitian matrices is defined as the real part of the trace of the product of the matrices.

Let $A$ be a Hermitian matrix. The inner product of the zero matrix $0$ with $A$ is equal to zero, denoted as $\langle 0, A \rangle_{\mathbb{R}} = 0$. Here, the inner product on the space of Hermitian matrices is defined as $\langle A, B \rangle_{\mathbb{R}} = \text{re}(\text{tr}(AB))$, where $\text{re}$ denotes the self-adjoint part (real part) of the trace of the matrix product.

Let $A$ and $B$ be Hermitian matrices. The inner product of the negation of $A$ and the matrix $B$ is equal to the negation of the inner product of $A$ and $B$, denoted as $\langle -A, B \rangle_{\mathbb{R}} = -\langle A, B \rangle_{\mathbb{R}}$. Here, the inner product on the space of Hermitian matrices is defined as the real part of the trace of the product of the matrices.

Let $A$ and $B$ be Hermitian matrices. The inner product of $A$ and the negative of $B$ is equal to the negative of the inner product of $A$ and $B$. That is, $\langle A, -B \rangle = -\langle A, B \rangle$.

Let $A$, $B$, and $C$ be Hermitian matrices. The inner product on the space of Hermitian matrices satisfies linearity in the second argument with respect to subtraction: $$\langle A, B - C \rangle = \langle A, B \rangle - \langle A, C \rangle$$ where $\langle \cdot, \cdot \rangle$ denotes the canonical inner product for Hermitian matrices (derived from the trace of the product).

For any Hermitian matrices $A, B,$ and $C$ in the space $\text{HermitianMat}(n, \alpha)$, the inner product satisfies the right-substitutive property $\langle A - B, C \rangle_{\mathbb{R}} = \langle A, C \rangle_{\mathbb{R}} - \langle B, C \rangle_{\mathbb{R}}$.

Let $A$ and $B$ be Hermitian matrices in $\text{HermitianMat}(n, \alpha)$ and $r$ be a scalar in $R$. The inner product on Hermitian matrices satisfies left-linearity with respect to scalar multiplication, specifically $\langle r \cdot A, B \rangle_R = r \cdot \langle A, B \rangle_R$.

Let $A$ and $B$ be Hermitian matrices of size $n$ over a ring $R$ (typically $\mathbb{R}$ or $\mathbb{C}$), and let $r$ be a scalar in $R$. The inner product on the space of Hermitian matrices satisfies the property $\langle A, r \cdot B \rangle = r \langle A, B \rangle$.

Let $\text{HermitianMat}_n(\alpha)$ be the space of $n \times n$ Hermitian matrices over a ring $\alpha$. The definition `HermitianMat.innerₗ` defines the Hermitian inner product as a bilinear form $B: \text{HermitianMat}_n(\alpha) \times \text{HermitianMat}_n(\alpha) \to R$, where $R$ is the scalar ring. For any two Hermitian matrices $A$ and $B$, the bilinear form is given by the inner product $\langle A, B \rangle_R$.

Let $A$ be a Hermitian matrix and $1$ denote the identity matrix. The inner product of $A$ with the identity matrix, denoted by $\langle A, 1 \rangle_{\mathbb{R}}$, is equal to the trace of $A$.

Let $A$ be a Hermitian matrix and $I$ (denoted by $1$ in the formal statement) be the identity matrix. The inner product of the identity matrix and $A$, denoted $\langle I, A \rangle_{\mathbb{R}}$, is equal to the trace of the matrix $A$. Here, the inner product is the canonical inner product defined for Hermitian matrices (which coincides with the Frobenius inner product).

Let $A$ and $B$ be Hermitian matrices. The inner product $\langle A, B \rangle_R$ of these matrices, when embedded into the base field $\alpha$ via the algebra map, is equal to the trace of the product of their underlying matrices, denoted $(A \cdot B)$. In mathematical notation: $$\text{algebraMap}(R, \alpha, \langle A, B \rangle_R) = \text{tr}(A \cdot B)$$ where $\langle \cdot, \cdot \rangle_R$ is the $R$-valued inner product on the space of Hermitian matrices.

For any two Hermitian matrices $A$ and $B$ in the space of Hermitian matrices $\text{HermitianMat}_n(\mathbb{R})$, the inner product satisfies the symmetry property $\langle A, B \rangle_{\mathbb{R}} = \langle B, A \rangle_{\mathbb{R}}$. Here, the inner product is defined via the trace of the product of the underlying matrices.

Let $n$ be a finite type and $\alpha$ be a commutative semiring equipped with a star operation. Suppose $A$ and $B$ are $n \times n$ Hermitian matrices over $\alpha$ (of type `HermitianMat n α`). If the star operation on $\alpha$ is trivial (i.e., $x^* = x$ for all $x \in \alpha$), then the inner product of $A$ and $B$ is equal to the trace of their matrix product: $$\langle A, B \rangle_{\alpha} = \text{tr}(A \cdot B)$$ where $A.\text{mat}$ and $B.\text{mat}$ denote the underlying matrices of the Hermitian matrices $A$ and $B$.

Let $A$ and $B$ be Hermitian matrices of size $n \times n$ over an $\mathbb{R}$-clike field $\mathbb{K}$ (such as $\mathbb{R}$ or $\mathbb{C}$). The inner product of $A$ and $B$ is equal to the real part of the trace of their product, given by $\langle A, B \rangle = \text{Re}(\text{tr}(AB))$.

Let $A$ and $B$ be Hermitian matrices of size $n \times n$ over an `RCLike` field $\alpha$ (such as $\mathbb{R}$ or $\mathbb{C}$). The canonical inner product $\langle A, B \rangle$ on the space of Hermitian matrices is equal to the trace of the product of their underlying matrices, denoted $\text{tr}(A_{mat} B_{mat})$.

Let $A$ be a Hermitian matrix of dimensions $n \times n$ over an `RCLike` field $\alpha$ (such as $\mathbb{R}$ or $\mathbb{C}$). The inner product of $A$ with itself, defined as $\langle A, A \rangle = \text{Re}(\text{tr}(A^2))$, is non-negative, i.e., $0 \le \langle A, A \rangle$.

Let $A$ and $B$ be Hermitian matrices. If the product of their underlying matrices $A \cdot B$ is a positive semi-definite matrix (denoted $0 \le A \cdot B$), then their inner product is non-negative, i.e., $0 \le \langle A, B \rangle$. Here, the inner product $\langle A, B \rangle$ for Hermitian matrices is defined as the trace of the product of the matrices, $\text{tr}(AB)$.

Let $A$ and $B$ be Hermitian matrices of the same dimensions over a field such as $\mathbb{R}$ or $\mathbb{C}$. If both $A$ and $B$ are positive semi-definite (denoted by $0 \le A$ and $0 \le B$), then their Frobenius inner product is non-negative, i.e., $0 \le \langle A, B \rangle$. Here the inner product is defined as the real part of the trace of the product of the matrices, $\langle A, B \rangle = \text{Re}(\text{tr}(AB))$.

Let $A, B$, and $C$ be $n \times n$ Hermitian matrices over an `RCLike` field $\alpha$ (such as $\mathbb{R}$ or $\mathbb{C}$). If $A$ is positive semi-definite ($0 \le A$), then $B \le C$ implies that $\langle A, B \rangle \le \langle A, C \rangle$, where $\langle \cdot, \cdot \rangle$ denotes the real-valued Frobenius inner product (defined as $\text{Re}(\text{tr}(AB))$) and $\le$ denotes the Loewner order on Hermitian matrices.

Let $A$, $B$, and $C$ be Hermitian matrices of size $n \times n$ over an `RCLike` field $\alpha$ (such as $\mathbb{R}$ or $\mathbb{C}$). If $A$ is positive semi-definite ($0 \le A$), then the inequality $B \le C$ implies that the real-valued inner product $\langle B, A \rangle_{\mathbb{R}}$ is less than or equal to $\langle C, A \rangle_{\mathbb{R}}$, i.e., $\langle B, A \rangle_{\mathbb{R}} \le \langle C, A \rangle_{\mathbb{R}}$. Here, $\langle \cdot, \cdot \rangle_{\mathbb{R}}$ denotes the canonical inner product for Hermitian matrices (equivalent to the Frobenius inner product), and the matrix inequality refers to the Loewner order.

Let $A$ and $B$ be Hermitian matrices. If $A$ and $B$ are both positive semi-definite (denoted by $0 \le A$ and $0 \le B$), then their inner product $\langle A, B \rangle$ is less than or equal to the product of their traces: $$\langle A, B \rangle \le \text{tr}(A) \cdot \text{tr}(B)$$ Here, $\langle \cdot, \cdot \rangle$ refers to the canonical inner product on the space of Hermitian matrices (corresponding to the Frobenius or Hilbert–Schmidt inner product), and $\text{tr}(\cdot)$ denotes the trace operation.

Let $A$ and $B$ be positive semi-definite (PSD) Hermitian matrices of size $n \times n$ over an $\mathbb{R}$-clike field (such as $\mathbb{R}$ or $\mathbb{C}$). The inner product $\langle A, B \rangle$ is equal to zero if and only if the support of $A$ is contained within the kernel of $B$ (denoted $A.\text{support} \leq B.\text{ker}$), meaning they have disjoint supports.

Let $d$ and $d_2$ be index sets, and $e: d \simeq d_2$ be a bijection between them. For any Hermitian matrices $A \in \text{HermitianMat}_d(\mathbb{K})$ and $B \in \text{HermitianMat}_{d_2}(\mathbb{K})$ over an `RCLike` field $\mathbb{K}$, the inner product of the reindexed matrix $A$ (via $e$) with $B$ is equal to the inner product of $A$ with the reindexed matrix $B$ (via the inverse bijection $e^{-1}$). That is, $\langle \text{reindex}(e, A), B \rangle = \langle A, \text{reindex}(e^{-1}, B) \rangle$.

The inner product on the space of Hermitian matrices $\text{HermitianMat}_d(\mathbb{k})$ over an $\mathbb{R}$-clike field $\mathbb{k}$ (such as $\mathbb{R}$ or $\mathbb{C}$) is a continuous function from the product space into $\mathbb{R}$. That is, the map $(A, B) \mapsto \langle A, B \rangle$ is continuous with respect to the topology induced by the Frobenius inner product (which is chosen to be definitionally equal to the subtype topology inherited from the space of all matrices).

Let $d$ be an index set and $\mathbb{k}$ be an `RCLike` field (such as $\mathbb{R}$ or $\mathbb{C}$). For any fixed Hermitian matrix $A \in \text{HermitianMat}_d(\mathbb{k})$, the linear map defined by the inner product with $A$, mapping $B \mapsto \langle A, B \rangle$, is continuous.

The structure defines the core components of a real inner product space for the set of $d \times d$ Hermitian matrices $\text{HermitianMat}_d(\mathbb{k})$ over an $\mathbb{R}$-clike field $\mathbb{k}$ (typically $\mathbb{C}$ or $\mathbb{R}$). The inner product of two Hermitian matrices $A$ and $B$ is defined as the Frobenius inner product $\langle A, B \rangle = \text{Tr}(A^* B)$, which in the Hermitian case simplifies to $\text{Re}(\text{Tr}(A B))$. This structure provides the necessary proofs for the axioms of an inner product space over $\mathbb{R}$: 1. **Symmetry:** $\langle A, B \rangle = \langle B, A \rangle$ for all Hermitian matrices $A, B$. 2. **Linearity in the first argument:** $\langle aA + bB, C \rangle = a\langle A, C \rangle + b\langle B, C \rangle$ for $a, b \in \mathbb{R}$. 3. **Positive-definiteness:** $\langle A, A \rangle \ge 0$, and $\langle A, A \rangle = 0$ if and only if $A = 0$.

The space of Hermitian matrices $\text{Herm}_d(\mathbb{k})$ (where $\mathbb{k}$ is typically $\mathbb{C}$) is a normed additive abelian group. The norm $\|\cdot\|$ on this space is the Frobenius norm, defined for a matrix $A$ as $\|A\| = \left(\sum_{i,j} |A_{ij}|^2\right)^{1/2}$. This structure ensures that $\text{Herm}_d(\mathbb{k})$ is a complete metric space with respect to the addition and subtraction of matrices.

For any Hermitian matrix $A \in \text{HermitianMat}(d, \mathbb{k})$, its norm $\|A\|$ is equal to the Frobenius norm, defined as the square root of the sum of the squares of the norms of its entries: $$\|A\| = \left( \sum_{i \in d} \sum_{j \in d} \|A_{ij}\|^2 \right)^{1/2}$$ where $A_{ij}$ denotes the entry of the matrix $A$ at row $i$ and column $j$.

Let $A$ be a Hermitian matrix of dimension $d$ over an $\mathbb{R}$-clike field $\mathbb{k}$ (typically $\mathbb{C}$). The norm of $A$, defined as the Frobenius norm $\|A\| = \left(\sum_{i,j=1}^d |A_{ij}|^2\right)^{1/2}$, is equal to the square root of the inner product of $A$ with itself, denoted by $\sqrt{\langle A, A \rangle}$. Here, the inner product is the Hilbert–Schmidt inner product restricted to the space of Hermitian matrices.

For a finite-dimensional index set $d$ and a field $\mathbb{k}$ (typically $\mathbb{C}$ or $\mathbb{R}$), the space of Hermitian matrices $\text{Herm}_d(\mathbb{k})$ is a normed vector space over the real numbers $\mathbb{R}$. This structure utilizes the Frobenius norm, which is defined as $\|A\| = \left(\sum_{i,j \in d} \|A_{ij}\|^2\right)^{1/2}$, and satisfies the requirement that $\|\lambda A\| = |\lambda| \|A\|$ for any scalar $\lambda \in \mathbb{R}$ and Hermitian matrix $A$.

For a finite-dimensional space of indices $d$, the space of Hermitian matrices $\text{Herm}_d(\mathbb{K})$ (where $\mathbb{K}$ is either $\mathbb{R}$ or $\mathbb{C}$) is equipped with a canonical real inner product space structure. This structure is defined using the Frobenius (or Hilbert–Schmidt) inner product, $\langle A, B \rangle = \text{Tr}(A^* B)$, and is compatible with the existing normed space structure such that the norm $\|A\|$ and the inner product satisfy the identity $\|A\|^2 = \langle A, A \rangle$.

Let $\text{HermitianMat}_d(\mathbb{k})$ denote the space of $d \times d$ Hermitian matrices over a field $\mathbb{k}$ (typically $\mathbb{R}$ or $\mathbb{C}$). The space $\text{HermitianMat}_d(\mathbb{k})$ is a complete metric space, meaning that every Cauchy sequence of Hermitian matrices converges to a Hermitian matrix within the space.

The space of Hermitian matrices of size $d \times d$ over the real numbers $\mathbb{R}$, denoted as `HermitianMat d ℝ`, forms a normed additive abelian group. The norm on this space is the Frobenius norm, which is consistent with the metric topology inherited from the space of all $d \times d$ real matrices.

The space of Hermitian matrices of dimension $d$ over the complex numbers $\mathbb{C}$, denoted by $\text{Herm}_d(\mathbb{C})$, forms a normed additive abelian group. The norm associated with this structure is the Frobenius norm, which is induced by the canonical Hilbert–Schmidt inner product on the space of complex Hermitian matrices.

For an $\mathbb{R}$-clike field $\mathbf{k}$ (where $\mathbf{k}$ is typically $\mathbb{R}$ or $\mathbb{C}$), the topology on $\mathbf{k}$ is an order-closed topology. This means that the set of pairs $\{(x, y) \in \mathbf{k} \times \mathbf{k} \mid x \le y\}$ is a closed subset of the product space $\mathbf{k} \times \mathbf{k}$ with respect to the standard partial order defined on $\mathbb{R}$-clike fields. Specifically, for $x, y \in \mathbf{k}$, $x \le y$ is defined as $\text{Re}(x) \le \text{Re}(y)$ and $\text{Im}(x) = \text{Im}(y)$.

Let $A$, $B$, and $x$ be Hermitian matrices of dimension $d$ over a field $\mathbb{k}$ (where $\mathbb{k}$ is typically $\mathbb{R}$ or $\mathbb{C}$). If $A \le x \le B$ with respect to the Loewner order (i.e., $x - A$ and $B - x$ are positive semidefinite), then the Frobenius distance between $x$ and $A$ is less than or equal to the Frobenius distance between $B$ and $A$, denoted by $\|x - A\| \le \|B - A\|$.

Let $n$ be a natural number and $\mathbb{k}$ be an $\mathbb{R}$-clike field (such as $\mathbb{R}$ or $\mathbb{C}$). The set of all $n \times n$ Hermitian matrices over $\mathbb{k}$, $\{A \in M_{n \times n}(\mathbb{k}) \mid A = A^*\}$, is a closed subset of the space of $n \times n$ matrices equipped with its standard topology.

Let $n$ be a natural number and $\mathbb{k}$ be a field such that it is an instance of `RCLike` (typically $\mathbb{R}$ or $\mathbb{C}$). The set of all $n \times n$ positive semidefinite matrices over $\mathbb{k}$ is a closed set in the topology of the space of matrices $M_n(\mathbb{k})$.

Let $n$ be a natural number and $\mathbb{k}$ be a field providing an instance of `RCLike` (such as $\mathbb{R}$ or $\mathbb{C}$). In the space of Hermitian matrices $\text{Herm}_n(\mathbb{k})$, the set of all non-negative elements $\{A \in \text{Herm}_n(\mathbb{k}) \mid 0 \le A\}$ (the set of positive semidefinite Hermitian matrices) is a closed set with respect to the induced topology.

Let $d$ be a natural number and $\mathbb{k}$ be a field instance of `RCLike` (typically $\mathbb{R}$ or $\mathbb{C}$). The space of $d \times d$ Hermitian matrices over $\mathbb{k}$, denoted by `HermitianMat d 𝕜`, equipped with its natural partial order and topology, forms an order-closed topology. This means that the set of all pairs $(A, B)$ such that $A \le B$ is a closed subset of the product space $\text{HermitianMat}_d(\mathbb{k}) \times \text{HermitianMat}_d(\mathbb{k})$.

Let $d$ be a finite dimension and $\mathbb{k}$ denote a field (typically $\mathbb{R}$ or $\mathbb{C}$). The space of Hermitian matrices $\text{Herm}(d, \mathbb{k})$ is a compact interval space. That is, for any two Hermitian matrices $A$ and $B$, the order interval $[A, B] = \{X \in \text{Herm}(d, \mathbb{k}) \mid A \le X \text{ and } X \le B\}$ is a compact set with respect to the topology induced by the Frobenius norm, where $\le$ denotes the Loewner order (i.e., $X-A$ and $B-X$ are positive semidefinite).

Let $\text{HermitianMat}_d(\mathbb{k})$ denote the space of Hermitian matrices of dimension $d$ over a field $\mathbb{k}$ (typically $\mathbb{C}$ or $\mathbb{R}$). The set of positive semi-definite matrices that are less than or equal to the identity matrix, defined by the interval $\{m \in \text{HermitianMat}_d(\mathbb{k}) \mid 0 \le m \le 1\}$, is compact. Here $0$ and $1$ represent the zero matrix and the identity matrix respectively, and the inequalities refer to the Loewner order.

The Frobenius norm of the identity matrix $I$ in the space of Hermitian matrices of dimension $n$ (where $n$ is the cardinality of the index set $d$) over an $\mathbb{R}$-clike field $\mathbb{k}$ is equal to the square root of the dimension $n$, i.e., $\|I\| = \sqrt{n}$.

Let $A$ be a Hermitian matrix. The square of its norm $\|A\|^2$ is equal to the trace of the square of its underlying matrix $A^2$, where the norm is the Frobenius norm.

Let $A$ and $B$ be Hermitian matrices of size $n \times n$ over $\mathbb{C}$. Let $U_A$ and $U_B$ be the unitary matrices of eigenvectors that diagonalize $A$ and $B$ respectively, and let $\lambda_i(A)$ and $\lambda_j(B)$ be their respective eigenvalues. Let $C$ be the unitary matrix defined by $C = U_A^* U_B$. Then the real inner product of $A$ and $B$ is given by $$\langle A, B \rangle_{\mathbb{R}} = \sum_{i, j} \lambda_i(A) \lambda_j(B) |C_{ij}|^2$$ where $|C_{ij}|^2$ are the squared magnitudes of the entries of the transition matrix between the two eigenbases.