QuantumInfo.ForMathlib.HermitianMat.LogExp

Let $A$ be a Hermitian matrix of size $d \times d$ over a field $\mathbb{K}$, and let $x$ be a non-zero scalar. The matrix logarithm (defined via the Continuous Functional Calculus) of the scaled matrix $x \cdot A$ satisfies: $$\ln(x \cdot A) = (\ln x) \cdot \mathbb{1}_{A \neq 0} + \ln A$$ where $\ln$ denotes the matrix logarithm `cfc Real.log`, and $\mathbb{1}_{A \neq 0}$ is the matrix obtained by applying the indicator function (which is $0$ at $0$ and $1$ elsewhere) to the eigenvalues of $A$ via functional calculus.

Let $A$ be a Hermitian matrix of dimension $d$ over a field $\mathbb{k}$. The function maps $A$ to its matrix exponential $\exp(A)$, defined via the continuous functional calculus (cfc) applied to the real exponential function $\exp: \mathbb{R} \to \mathbb{R}$. The resulting matrix is also a Hermitian matrix.

Let $A$ and $B$ be Hermitian matrices. If the underlying matrix of $A$ commutes with the underlying matrix of $B$ (i.e., $A_{mat}B_{mat} = B_{mat}A_{mat}$), then the matrix exponential of $A$ also commutes with the matrix of $B$: $\exp(A)_{mat}B_{mat} = B_{mat}\exp(A)_{mat}$.

Let $A$ and $B$ be Hermitian matrices. If the underlying matrix of $A$ commutes with the underlying matrix of $B$ (i.e., $A_{\text{mat}}B_{\text{mat}} = B_{\text{mat}}A_{\text{mat}}$), then the matrix of $A$ also commutes with the matrix exponential of $B$, such that $A_{\text{mat}}\exp(B)_{\text{mat}} = \exp(B)_{\text{mat}}A_{\text{mat}}$.

Let $A$ be a Hermitian matrix indexed by $d$, and let $e: d \simeq d_2$ be a bijection (equivalence) between the index types $d$ and $d_2$. Then the matrix exponential of the reindexed matrix $A$ is equal to the reindexing of the matrix exponential of $A$. That is, $\exp(A.\text{reindex}(e)) = (\exp A).\text{reindex}(e)$.

For any Hermitian matrix $A$, its matrix exponential $\exp(A)$ is non-singular (invertible).

For any Hermitian matrix $A \in \text{HermitianMat}_d(\mathbb{k})$, its matrix exponential $\exp(A)$ is positive semidefinite, i.e., $0 \le \exp(A)$ under the Loewner partial order.

Let $d$ be a non-empty finite index set and $\mathbf{k}$ be a field with an involution (such as $\mathbb{R}$ or $\mathbb{C}$). For any Hermitian matrix $A \in \text{HermitianMat}_d(\mathbf{k})$, its matrix exponential $\exp(A)$ is strictly positive with respect to the Loewner order, i.e., $0 < \exp(A)$. This operator inequality means that $\exp(A)$ is a positive definite matrix.

This is a `positivity` extension for the matrix exponential function. For a Hermitian matrix $A$ of dimension $d \times d$ over a field $\mathbb{k}$, if $d$ is non-empty, the extension automatically proves that the matrix exponential $\exp(A)$ is strictly positive definite (written $\exp(A) > 0$) by utilizing the property `HermitianMat.exp_pos`.

For a Hermitian matrix $A \in \mathbb{C}^{d \times d}$ (or $\mathbb{R}^{d \times d}$), the matrix logarithm $\log A$ is defined via the Continuous Functional Calculus (CFC). Specifically, if $A = U \Lambda U^\dagger$ is a spectral decomposition where $\Lambda = \text{diag}(\lambda_1, \dots, \lambda_d)$ is the diagonal matrix of real eigenvalues, then $\log A = U \log(\Lambda) U^\dagger$, where $\log(\Lambda) = \text{diag}(\ln \lambda_1, \dots, \ln \lambda_d)$. The real logarithm function $\ln(x)$ is applied elementwise to the eigenvalues. Note that for $\lambda \le 0$, the behavior follows the convention of the underlying real logarithm `Real.log` (typically $\ln |x|$ or $0$ for $x \le 0$ in formal libraries), and the result coincides with the standard matrix logarithm when $A$ is positive definite.

Let $A$ and $B$ be Hermitian matrices of dimension $d$ over a field $\mathbb{k}$. If the matrices $A$ and $B$ commute (i.e., $AB = BA$), then the matrix logarithm of $A$, denoted $\log(A)$, also commutes with $B$ (i.e., $\log(A)B = B\log(A)$).

Let $A$ and $B$ be Hermitian matrices of dimension $d$ over the field $\mathbb{K}$. If the matrices $A$ and $B$ commute (i.e., $AB = BA$), then $A$ also commutes with the matrix logarithm of $B$, denoted as $\log(B)$. In other words, $A \log(B) = \log(B) A$.

Let $A$ be a Hermitian matrix indexed by $d$, and let $e: d \simeq d_2$ be a bijection. Then the matrix logarithm of the reindexed matrix $A$ is equal to the reindexing of the matrix logarithm of $A$. That is, $\log(A.\text{reindex}(e)) = (\log A).\text{reindex}(e)$.

For a zero Hermitian matrix $0$ of dimension $d$ over the field $\mathbb{K}$, its matrix logarithm is also zero, i.e., $\log(0) = 0$.

For the identity Hermitian matrix $I$ (denoted as $1$) of dimension $d$ over the field $\mathbb{K}$, its matrix logarithm is zero, i.e., $\log(I) = 0$.

Let $A$ be a Hermitian matrix of dimension $d$ over the field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$), and let $x$ be a non-zero real number. The matrix logarithm of the scalar multiple $x \cdot A$ is given by $$\log(x \cdot A) = (\log |x|) \cdot \text{supportProj}(A) + \log A,$$ where $\text{supportProj}(A)$ is the Hermitian matrix representing the orthogonal projection onto the support (range) of $A$.

Let $A$ be a non-singular Hermitian matrix of dimension $d$ over $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$), and let $x$ be a non-zero real number. Then the matrix logarithm of the scalar product $x \cdot A$ is given by $$\log(x \cdot A) = (\log x) \cdot I + \log A,$$ where $I$ denotes the identity matrix.

Let $A$ and $B$ be Hermitian matrices. If $A$ is positive definite ($A > 0$) and $A \le B$ with respect to the Loewner partial order, then $B^{-1} \le A^{-1}$. Here, $\le$ denotes the Loewner order where $X \le Y$ if and only if $Y - X$ is a positive semidefinite matrix.

For any real numbers $x$ and $T$ such that $x > 0$ and $T > 0$, the definite integral of the difference of reciprocals is given by $$\int_{0}^{T} \left( \frac{1}{1 + t} - \frac{1}{x + t} \right) dt = \log x + \log \left( \frac{1 + T}{x + T} \right).$$

For any real number $x$, the limit of the function $f(T) = \log\left(\frac{1 + T}{x + T}\right)$ as $T$ approaches infinity is $0$. That is, $$\lim_{T \to \infty} \log\left(\frac{1 + T}{x + T}\right) = 0.$$

Let $x$ and $y$ be Hermitian matrices in $\text{HermitianMat}_d(\mathbb{k})$ such that both $x$ and $y$ are positive definite. If $x \le y$ with respect to the Loewner partial order, then for any real number $T > 0$, the following inequality holds between the finite integral approximations: $$\int_{0}^{T} \left( \frac{1}{1 + t} I - (x + tI)^{-1} \right) dt \le \int_{0}^{T} \left( \frac{1}{1 + t} I - (y + tI)^{-1} \right) dt,$$ where $I$ denotes the identity matrix.

For a finite-dimensional space $n$ and a field $\mathbb{k} \in \{\mathbb{R}, \mathbb{C}\}$, the function `logApprox` maps a Hermitian matrix $x \in \text{Herm}_n(\mathbb{k})$ and a real parameter $T$ to another Hermitian matrix defined by the Bochner integral: $$\int_{0}^{T} \left( \frac{1}{1+t} I - (x + tI)^{-1} \right) dt$$ where $I$ is the identity matrix. This expression serves as a parameterized approximation of the matrix logarithm $\log(x)$, specifically satisfying the property that as $T \to \infty$, the integral converges to $\log(x)$.

For a given upper limit $T \in \mathbb{R}$ and a value $u \in \mathbb{R}$, the function is defined as the integral: $$\text{scalarLogApprox}(T, u) = \int_0^T \left( \frac{1}{1 + t} - \frac{1}{u + t} \right) dt$$ This function serves as a scalar approximation of the natural logarithm, appearing in the context of proving operator monotonicity for the matrix logarithm.

For any real numbers $x$ and $T$ such that $x > 0$ and $T > 0$, the scalar logarithmic approximation function satisfies the identity $$\text{scalarLogApprox}(T, x) = \log x + \log \left( \frac{1 + T}{x + T} \right).$$

Let $x$ be a positive definite Hermitian matrix in $\text{Herm}_d(\mathbb{k})$ and let $T > 0$ be a real number. The matrix logarithm approximation $\text{logApprox}(x, T)$ is equal to the continuous functional calculus (CFC) of the scalar logarithm approximation function $\text{scalarLogApprox}(T, \cdot)$ applied to $x$, denoted as: $$\text{logApprox}(x, T) = \text{cfc}_x(\text{scalarLogApprox}(T, \cdot))$$

Let $x$ be a positive definite Hermitian matrix in $\text{Herm}_d(\mathbb{k})$ and let $T > 0$ be a real number. The matrix logarithm approximation $\text{logApprox}(x, T)$ is equal to the matrix logarithm $\log(x)$ plus an error term defined via the continuous functional calculus (CFC) as $$\text{logApprox}(x, T) = \log(x) + f(x)$$ where $f$ is the scalar function $f(u) = \log\left(\frac{1 + T}{u + T}\right)$.

Let $x$ be a Hermitian matrix in $\text{Herm}_d(\mathbb{k})$. As $T \to \infty$, the error term in the logarithm approximation, defined via continuous functional calculus as $$x.\text{cfc} \left( u \mapsto \log \left( \frac{1 + T}{u + T} \right) \right),$$ converges to the zero matrix $0$ in the norm topology of $\text{Herm}_d(\mathbb{k})$.

Let $x$ be a Hermitian matrix in $\text{Herm}_d(\mathbb{k})$ such that $x$ is positive definite. As $T \to \infty$, the log approximation of $x$, denoted by $\text{logApprox}(x, T)$, converges to the matrix logarithm $\log(x)$ in the norm topology.

Let $A$ and $B$ be Hermitian matrices. If $A$ is positive definite and $A \le B$ (with respect to the Loewner order), then $B$ is also positive definite. Here, $A \le B$ is defined as $B - A$ being a positive semidefinite matrix.

Let $A$ and $B$ be $d \times d$ Hermitian matrices over a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$). If $A$ is positive definite and $A \le B$ in the Loewner order (meaning $B - A$ is positive semidefinite), then $\log(A) \le \log(B)$.

Let $A$ and $B$ be Hermitian matrices. Under the assumption that $A$ and $B$ commute, if $e^A \le e^B$ with respect to the Loewner partial order, then $A \le B$.

Let $x$ and $y$ be $d \times d$ Hermitian matrices over a field $\mathbb{k}$. Suppose that $x$ and $y$ are positive definite matrices. For any real numbers $a, b \ge 0$ such that $a + b = 1$, the following inequality holds with respect to the Loewner partial order: $$(a x + b y)^{-1} \le a x^{-1} + b y^{-1}$$ In this context, the relation $A \le B$ for Hermitian matrices signifies that $B - A$ is a positive semidefinite matrix.

Let $x$ and $y$ be $d \times d$ Hermitian matrices over a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$), and assume that both $x$ and $y$ are positive definite. For any real numbers $a, b \ge 0$ such that $a + b = 1$, and for any real number $t \ge 0$, it holds that: $$(a x + b y + t I)^{-1} \le a (x + t I)^{-1} + b (y + t I)^{-1}$$ where $I$ is the identity matrix and $\le$ denotes the Loewner partial order (i.e., $A \le B$ if $B - A$ is positive semidefinite).

Let $A$ be a Hermitian matrix in $\text{Herm}_d(\mathbb{k})$ that is positive definite. For any non-negative real number $b \ge 0$, the function $f(t) = (A + tI)^{-1}$, where $I$ is the identity matrix, is interval integrable with respect to the Lebesgue measure over the interval $[0, b]$.

Let $x$ and $y$ be $n \times n$ Hermitian matrices over $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$) that are positive definite. For any non-negative real numbers $a, b$ such that $a + b = 1$, and for any non-negative real number $T$, the finite integral approximation of the matrix logarithm, $\text{logApprox}$, satisfies the operator concavity inequality: $$a \cdot \text{logApprox}(x, T) + b \cdot \text{logApprox}(y, T) \le \text{logApprox}(a x + b y, T)$$ where $\le$ denotes the Loewner partial order.

Let $x$ and $y$ be $d \times d$ Hermitian matrices over a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$) such that $x$ and $y$ are positive definite. For any real numbers $a, b \ge 0$ such that $a + b = 1$, the following inequality holds with respect to the Loewner partial order: $$a \log(x) + b \log(y) \le \log(a x + b y)$$ where $\log$ denotes the matrix logarithm.

Let $m$ and $n$ be finite types with decidable equality, and let $\mathbb{k}$ be either $\mathbb{R}$ or $\mathbb{C}$. Given two vectors $d_1: m \to \mathbb{R}$ and $d_2: n \to \mathbb{R}$ with strictly positive entries ($d_1(i) > 0$ and $d_2(j) > 0$ for all $i, j$), the logarithm of the Kronecker product of the diagonal matrices formed by $d_1$ and $d_2$ satisfies: $$\log(\text{diag}(d_1) \otimes_k \text{diag}(d_2)) = \log(\text{diag}(d_1)) \otimes_k I_n + I_m \otimes_k \log(\text{diag}(d_2))$$ where $\otimes_k$ denotes the Kronecker product, $\log$ is the matrix logarithm for Hermitian matrices, and $I_m, I_n$ are the identity matrices of the respective dimensions.

Let $A$ be a Hermitian matrix and $U$ be a unitary matrix. The logarithm of the Hermitian matrix formed by the unitary conjugation of $A$—defined as $U A U^\dagger$—is equal to the unitary conjugation of the logarithm of $A$. That is, $\log(U A U^\dagger) = U (\log A) U^\dagger$.

Let $A$ be a non-singular Hermitian matrix and $B$ be a Hermitian matrix. For any non-zero real number $x$, the inner product of the matrix logarithm of the scaled matrix $x \cdot A$ with $B$ satisfies: $$\langle \log(x \cdot A), B \rangle = (\log x) \cdot \text{Tr}(B) + \langle \log A, B \rangle$$ where $\text{Tr}(B)$ denotes the trace of $B$, and the inner product is the Frobenius inner product on the space of Hermitian matrices.

Let $f: d \to \mathbb{R}$ and $g: d_2 \to \mathbb{R}$ be functions defining the diagonal Hermitian matrices $\text{diag}(f)$ and $\text{diag}(g)$. Then the matrix logarithm of their Kronecker product is given by: $$\log(\text{diag}(f) \otimes \text{diag}(g)) = \log(\text{diag}(f)) \otimes \text{supportProj}(\text{diag}(g)) + \text{supportProj}(\text{diag}(f)) \otimes \log(\text{diag}(g))$$ where $\otimes$ denotes the Kronecker product, and $\text{supportProj}(M)$ is the orthogonal projector onto the support of a matrix $M$.

Let $A$ and $B$ be Hermitian matrices. The matrix logarithm of their Kronecker product $A \otimes B$ is given by $$\log(A \otimes B) = (\log A) \otimes P_B + P_A \otimes (\log B)$$ where $\otimes$ denotes the Kronecker product and $P_A$, $P_B$ denote the orthogonal projectors onto the support (the subspace spanned by eigenvectors with non-zero eigenvalues) of $A$ and $B$, respectively. This generalizes the rule for non-singular matrices by replacing the identity matrix with the projector onto the range.

Let $A$ and $B$ be non-singular Hermitian matrices. Then the matrix logarithm of their Kronecker product is given by the sum of the Kronecker products of their individual logarithms with the identity matrix: $$\log(A \otimes B) = (\log A) \otimes I + I \otimes (\log B)$$ where $\otimes$ denotes the Kronecker product and $I$ denotes the identity matrix of the appropriate dimension.