Physlib.Mathematics.SchurTriangulation

Given a finite index $i \in \{0, 1, \dots, m + n - 1\}$ and a proof $h$ that $i \geq m$, this function returns the value $i - m$ as an element of the set $\{0, 1, \dots, n - 1\}$.

The equivalence defines a bijection between the disjoint union of two finite sets $\text{Fin } m \oplus \text{Fin } n$ and the dependent sum $\sum_{b \in \{\text{true, false}\}} S_b$, where $S_{\text{true}} = \text{Fin } m$ and $S_{\text{false}} = \text{Fin } n$. Here, $\text{Fin } k$ denotes the set of natural numbers $\{0, 1, \dots, k-1\}$, and the mapping uses the conditional operator $\text{cond}(b, \text{Fin } m, \text{Fin } n)$ to select the appropriate set based on the boolean index $b$.

The equivalence defines a bijection between the set of indices $\text{Fin}(m + n) = \{0, 1, \dots, m + n - 1\}$ and the dependent sum $\sum_{b \in \{\text{true, false}\}} S_b$, where $S_{\text{true}} = \text{Fin } m$ and $S_{\text{false}} = \text{Fin } n$. For an index $i \in \text{Fin}(m + n)$, the mapping is defined such that if $i < m$, it corresponds to $(\text{true}, i) \in S_{\text{true}}$, and if $i \ge m$, it corresponds to $(\text{false}, i - m) \in S_{\text{false}}$. This construction is used to partition basis indices during the recursive step of Schur triangulation.

Let $m$ and $n$ be natural numbers. For any index $i \in \text{Fin}(m + n)$, if $i < m$, then the equivalence $\text{finAddEquivSigmaCond}$ maps $i$ to the element $\langle \text{true}, i, h \rangle$ in the dependent sum $\sum_{b \in \text{Bool}} \text{cond}(b, \text{Fin } m, \text{Fin } n)$, where $h$ is the proof that $i < m$. In other words, indices less than $m$ are mapped to the first component (the "true" branch) of the partition.

Let $m$ and $n$ be natural numbers. For any index $i \in \text{Fin}(m + n)$, if $i \ge m$, then the equivalence $\text{finAddEquivSigmaCond}$ maps $i$ to the element $\langle \text{false}, i - m \rangle$ in the dependent sum $\sum_{b \in \text{Bool}} \text{cond}(b, \text{Fin } m, \text{Fin } n)$. In this context, $i - m$ is treated as an element of $\text{Fin } n$, and the "false" branch corresponds to the second component of the partition.

Given two finite types $m$ and $n$, for any boolean value $b$, the type defined by the conditional $\text{cond}(b, m, n)$ (which is $m$ if $b$ is $\text{true}$ and $n$ if $b$ is $\text{false}$) is also a finite type.

Given two types $m$ and $n$ that both possess decidable equality, the dependent sum type $\sum_{b \in \{\text{true}, \text{false}\}} \text{cond}(b, m, n)$ also possesses decidable equality. Here, $\text{cond}(b, m, n)$ evaluates to $m$ if $b$ is true and $n$ if $b$ is false, effectively representing the disjoint union $m \sqcup n$. Two elements $\langle b_1, x_1 \rangle$ and $\langle b_2, x_2 \rangle$ in this type are equal if and only if $b_1 = b_2$ and $x_1 = x_2$.

Let $n$ be a type equipped with a less-than relation $<$ and $R$ be a commutative ring. A square matrix $A$ with entries in $R$ and indexed by $n$ is upper triangular if for all $i, j \in n$, the entry $A_{i,j} = 0$ whenever $i > j$.

For a type $n$ equipped with a less-than relation $<$ and a commutative ring $R$, `Matrix.UpperTriangular n R` is the subtype consisting of all square matrices $A$ of size $n \times n$ with entries in $R$ that are upper triangular. A matrix $A$ is upper triangular if its entries $A_{i,j}$ satisfy $A_{i,j} = 0$ for all $i, j \in n$ such that $i > j$.

Given a linear endomorphism $f: E \to E$ on a finite-dimensional inner product space $E$ over an algebraically closed field $\mathbb{k}$, this definition implements the recursive algorithm for Schur triangulation (also known as Schur decomposition). It constructs an orthonormal basis $\mathcal{B}$ for $E$ such that the matrix representation $[f]_{\mathcal{B}}$ of the operator is upper triangular. The algorithm proceeds as follows: 1. If $E$ is trivial, it returns an empty basis. 2. If $E$ is non-trivial, it selects an eigenvalue $\mu$ and its corresponding eigenspace $V \subseteq E$. 3. It considers the orthogonal complement $W = V^\perp$ and recursively applies the algorithm to the map $g: W \to W$ defined by $g = P_W \circ f|_W$, where $P_W$ is the orthogonal projection onto $W$. 4. The final orthonormal basis $\mathcal{B}$ is formed by joining an orthonormal basis for $V$ with the orthonormal basis of $W$ obtained from the recursion.

Given a square matrix $A$ of size $n \times n$ over an algebraically closed field $\mathbb{k}$, this definition provides a pair $(\mathcal{B}, T)$ consisting of an orthonormal basis $\mathcal{B}$ for the Euclidean space $\mathbb{k}^n$ and an upper triangular matrix $T$. The matrix $T$ is the matrix representation of the linear endomorphism $x \mapsto Ax$ with respect to the basis $\mathcal{B}$. The construction is obtained by adapting the recursive Schur triangulation algorithm for linear maps to the specific case of matrices acting on Euclidean space.

Given a square matrix $A$ of size $n \times n$ over an algebraically closed field $\mathbb{k}$, this definition provides the orthonormal basis $\mathcal{B}$ of the Euclidean space $\mathbb{k}^n$ such that the matrix representation of the linear operator $x \mapsto Ax$ with respect to $\mathcal{B}$ is upper triangular. It is defined as the first component of the pair $(\mathcal{B}, T)$ generated by the Schur triangulation algorithm `Matrix.schurTriangulationAux`.

Given a square matrix $A$ of size $n \times n$ over an algebraically closed field $\mathbb{k}$ (such as the complex numbers $\mathbb{C}$), this definition provides the unitary matrix $U \in \mathrm{U}(n, \mathbb{k})$ such that $A = U T U^*$, where $T$ is an upper triangular matrix and $U^*$ is the conjugate transpose of $U$. Specifically, $U$ is the change-of-basis matrix from the standard basis of the Euclidean space $\mathbb{k}^n$ to the orthonormal basis $\mathcal{B}$ (the Schur basis) derived during the triangulation procedure, meaning the columns of $U$ are the vectors of $\mathcal{B}$.

Given a square matrix $A$ of size $n \times n$ over an algebraically closed field $\mathbb{k}$ (such as the complex numbers $\mathbb{C}$), this definition returns the upper triangular matrix $T$ that is unitarily similar to $A$. Specifically, $T$ is the matrix such that $A = U T U^*$ for some unitary matrix $U$, where $T_{i,j} = 0$ for all indices $i, j$ such that $i > j$. This matrix is the second component of the auxiliary Schur triangulation result, representing the linear map $x \mapsto Ax$ with respect to the orthonormal basis derived during the triangulation procedure.

For any square matrix $A$ over an algebraically closed field $\mathbb{k}$, the matrix $A$ can be decomposed as $A = U T U^*$, where $U$ is the unitary matrix provided by `schurTriangulationUnitary`, $T$ is the upper triangular matrix provided by `schurTriangulation`, and $U^*$ denotes the conjugate transpose of $U$.