Physlib.Mathematics.DataStructures.Matrix.LieTrace

Given a uniform space $\mathbb{K}$, the set of $m \times n$ matrices with entries in $\mathbb{K}$, denoted by $\text{Matrix}_{m \times n}(\mathbb{K})$, is equipped with a uniform space structure. This structure is the product uniform structure induced by the uniform structure on $\mathbb{K}$ for each entry $(i, j)$ of the matrix.

Let $\beta$ be a topological additive commutative monoid. For any sequence $f: \mathbb{N} \to \beta$, if $f(n) = 0$ for all $n \in \mathbb{N}$, then the infinite sum $\sum_{n=0}^{\infty} f(n)$ is equal to $0$.

Let $f: \mathbb{N} \to \text{Matrix}_{m \times m}(\mathbb{K})$ be a sequence of square matrices. If the series $\sum_{n=0}^\infty f_n$ is summable, then for any indices $i, j \in m$, the $(i, j)$-th entry of the infinite sum is equal to the infinite sum of the $(i, j)$-th entries of each matrix. That is, $$\left( \sum_{n=0}^\infty f_n \right)_{ij} = \sum_{n=0}^\infty (f_n)_{ij}$$

For any two upper-triangular matrices $A$ and $B$ (formalized as square matrices that are block-triangular with respect to the identity function), the diagonal of their product $AB$ is the element-wise product of their respective diagonals. That is, $(AB)_{ii} = A_{ii} \cdot B_{ii}$ for all indices $i$.

Let $A$ be a square matrix over a field $\mathbb{K}$. If $A$ is an upper-triangular matrix (defined as `BlockTriangular A id`), then for any natural number $k$, its $k$-th power $A^k$ is also an upper-triangular matrix.

Let $A$ be an $m \times m$ upper-triangular matrix over a field $\mathbb{K}$. For any natural number $k$, the diagonal of the matrix power $A^k$ is equal to the element-wise $k$-th power of the diagonal of $A$. That is, $\text{diag}(A^k) = \text{diag}(A)^k$, or equivalently, the $i$-th diagonal entry of the $k$-th power of $A$ is given by $(A^k)_{ii} = (A_{ii})^k$ for all indices $i$.

Let $A$ be an $m \times m$ matrix over a field $\mathbb{K}$. If $A$ is an upper-triangular matrix (formally defined as `BlockTriangular A id`), then its matrix exponential $\exp(A)$ is also an upper-triangular matrix.

Let $A$ be an $m \times m$ upper-triangular matrix (formally defined as `BlockTriangular A id`) over a field $\mathbb{K}$. For any natural number $n$ and any index $i$, the $(i, i)$-th diagonal entry of the $n$-th power of $A$ is equal to the $n$-th power of the $(i, i)$-th entry of $A$. That is, $(A^n)_{ii} = (A_{ii})^n$.

Let $A$ be an $m \times m$ upper-triangular matrix (formally defined as `BlockTriangular A id`) over a field $\mathbb{K}$. For any natural number $n$ and any index $i$, the $(i, i)$-th entry of the $n$-th term of the matrix exponential series, $\frac{1}{n!} A^n$, is equal to the $n$-th term of the scalar exponential series of the $(i, i)$-th entry of $A$. That is, $\left(\frac{1}{n!} A^n\right)_{ii} = \frac{1}{n!} (A_{ii})^n$.

Let $A$ be an $m \times m$ upper-triangular matrix (formally defined as `BlockTriangular A id`) over a field $\mathbb{K}$. For any index $i$, the sum of the $(i, i)$-th entries of the terms in the matrix exponential series equals the sum of the terms in the scalar exponential series for the diagonal entry $A_{ii}$. That is: $$\sum_{n=0}^\infty \left(\frac{1}{n!} A^n\right)_{ii} = \sum_{n=0}^\infty \frac{1}{n!} (A_{ii})^n$$

Let $A$ be an $m \times m$ upper-triangular matrix (formally defined as `BlockTriangular A id`) over a field $\mathbb{K}$. The $i$-th diagonal entry of the matrix exponential $\exp A$ is equal to the scalar exponential of the $i$-th diagonal entry of $A$. That is, for any index $i$: $$(\exp A)_{ii} = \exp(A_{ii})$$

Let $A$ be an $m \times m$ upper-triangular matrix (formally defined as `BlockTriangular A id`) over a field $\mathbb{K}$. The determinant of the matrix exponential of $A$ is equal to the exponential of the trace of $A$. That is: $$\det(\exp A) = \exp(\text{tr } A)$$

For any $m \times m$ matrix $A$ over a field $\mathbb{K}$ and any unitary matrix $U$ in the unitary group $\text{U}(m, \mathbb{K})$, the trace is invariant under unitary conjugation: $$\text{tr}(U A U^*) = \text{tr}(A)$$ where $U^*$ denotes the adjoint (conjugate transpose) of the matrix $U$.

Let $A$ be a square matrix of size $m \times m$ over a field $\mathbb{K}$, and let $U$ be an element of the unitary group of degree $m$ over $\mathbb{K}$. Then the determinant of the matrix product $U A U^*$ is equal to the determinant of $A$, where $U^*$ denotes the adjoint (star) of the unitary matrix $U$.

For any $m \times m$ matrix $A$ and any unitary matrix $U$ in the unitary group, the matrix exponential of the unitary conjugation of $A$ is equal to the unitary conjugation of the exponential of $A$: $$\exp(U A U^*) = U (\exp A) U^*$$ where $U^*$ denotes the adjoint (conjugate transpose) of the matrix $U$. This property shows that the matrix exponential commutes with unitary conjugation.

Let $A$ be an $m \times m$ matrix over a field $\mathbb{K}$, and let $U$ be a unitary matrix in the unitary group of degree $m$. The determinant of the matrix exponential of the unitary conjugation of $A$ is equal to the determinant of the matrix exponential of $A$: $$\det(\exp(U A U^*)) = \det(\exp A)$$ where $U^*$ denotes the adjoint (conjugate transpose) of the matrix $U$.

Let $\mathbb{K}$ be an algebraically closed field that satisfies the properties of the real or complex numbers (specifically an `RCLike` field), and let $m$ be a finite index set. For any square matrix $A \in \text{Mat}_{m \times m}(\mathbb{K})$, the determinant of the matrix exponential of $A$ is equal to the exponential of the trace of $A$. That is: $$\det(\exp A) = \exp(\text{tr } A)$$ This identity is known as **Lie's trace formula**.

Let $\alpha$ and $\beta$ be additive commutative monoids and topological spaces, where $\beta$ is a Hausdorff space. Let $f: \alpha \to \beta$ be a continuous additive homomorphism. For a sequence of $m \times n$ matrices $s_k$ with entries in $\alpha$, if the series $\sum_{k=0}^{\infty} s_k$ is summable, then the application of $f$ to each entry of the sum of the series is equal to the sum of the matrices obtained by applying $f$ to each entry of each $s_k$. That is, $$f\left( \sum_{k=0}^{\infty} s_k \right) = \sum_{k=0}^{\infty} f(s_k)$$ where $f$ is applied entry-wise to the matrices.

Let $n$ be a finite index set and $A$ be an $n \times n$ matrix with entries in the real numbers $\mathbb{R}$. Let $\iota: \mathbb{R} \to \mathbb{C}$ denote the standard inclusion (canonical map) from the real numbers to the complex numbers. The theorem states that applying this inclusion entry-wise to the matrix exponential $\exp(A)$ yields the same result as taking the matrix exponential of the matrix $A$ after its entries have been mapped to $\mathbb{C}$ via $\iota$. In formula terms: $$\text{map}(\iota, \exp A) = \exp(\text{map}(\iota, A))$$ where $\exp$ denotes the matrix exponential.

Let $n$ be a finite index set and let $A$ be an $n \times n$ matrix with entries in the real numbers $\mathbb{R}$. The determinant of the matrix exponential of $A$ is equal to the exponential of the trace of $A$. That is: $$\det(\exp A) = \exp(\text{tr } A)$$ where $\exp$ denotes the matrix exponential on the left-hand side and the standard exponential function on $\mathbb{R}$ on the right-hand side, and $\text{tr } A$ is the trace of the matrix. This identity is known as **Lie's trace formula** for real matrices.