QuantumInfo.ForMathlib.Majorization

For a square complex matrix $A \in M_{d \times d}(\mathbb{C})$, the singular values $\sigma_i(A)$ are defined for each index $i \in d$ as the square roots of the eigenvalues of the Hermitian matrix $A^\dagger A$, where $A^\dagger$ denotes the conjugate transpose of $A$.

Let $A$ be a $d \times d$ complex matrix. For any index $i \in d$, the $i$-th singular value of $A$, denoted $\sigma_i(A)$, is non-negative, i.e., $0 \le \sigma_i(A)$.

Given a square complex matrix $A \in \text{Mat}_{d \times d}(\mathbb{C})$, the function $\sigma^{\downarrow}(A)$ returns the singular values of $A$ sorted in non-increasing order. Specifically, it maps an index $i \in \{0, \dots, n-1\}$ (where $n$ is the dimension of the matrix) to the $(i+1)$-th largest singular value $\sigma^{\downarrow}_i(A)$, obtained by sorting the multiset of singular values $\{\sigma_j(A) : j \in d\}$ such that $\sigma^{\downarrow}_0 \geq \sigma^{\downarrow}_1 \geq \dots \geq \sigma^{\downarrow}_{n-1}$.

Let $A$ be a $d \times d$ complex matrix. For any index $i \in \{0, \dots, n-1\}$ (where $n$ is the dimension of the matrix), the $i$-th sorted singular value $\sigma^{\downarrow}_i(A)$ satisfies $0 \le \sigma^{\downarrow}_i(A)$.

Let $A$ be a $d \times d$ complex matrix and $p$ be a real number. Let $\sigma_i(A)$ denote the $i$-th singular value of $A$, and let $\sigma^\downarrow_i(A)$ denote the $i$-th singular value of $A$ sorted in non-increasing order. Then the sum of the $p$-th powers of the singular values equals the sum of the $p$-th powers of the sorted singular values: $$\sum_{i \in d} \sigma_i(A)^p = \sum_{i=1}^n \sigma^\downarrow_i(A)^p$$ where $n$ is the cardinality of the index set $d$.

For any square complex matrix $A \in \text{Mat}_{d \times d}(\mathbb{C})$, the sequence of its sorted singular values $\sigma^\downarrow_i(A)$ is antitone. That is, for indices $i, j \in \{0, 1, \dots, n-1\}$ (where $n$ is the dimension of the matrix), if $i \le j$, then $\sigma^\downarrow_i(A) \ge \sigma^\downarrow_j(A)$.

Let $f, g: \{0, \dots, n-1\} \to \mathbb{R}$ be two sequences. If $f$ and $g$ are both antitone (non-increasing) and take only non-negative values (i.e., $f(i) \ge 0$ and $g(i) \ge 0$ for all $i$), then their pointwise product sequence $i \mapsto f(i)g(i)$ is also antitone.

Given a finite type $\alpha$ with decidable equality, there exists a linear order $( \alpha, \le )$ on it. This order is constructed classically by utilizing the well-ordering principle on the elements of the type.

Let $d$ be a finite index set and $M$ be a $d \times d$ matrix over the complex numbers $\mathbb{C}$. For any natural number $k$, the $k$-th compound matrix $C_k(M)$ is a matrix whose rows and columns are indexed by subsets of $d$ with cardinality $k$. Specifically, for two such subsets $S, T \subseteq d$ with $|S| = |T| = k$, the $(S, T)$-th entry of $C_k(M)$ is the minor defined by the determinant of the submatrix of $M$ formed by the rows in $S$ and the columns in $T$. To compute this, the subsets $S$ and $T$ are ordered using their natural order embeddings from $\{0, \dots, k-1\}$.

Let $R$ be a commutative ring and $n$ be a finite type equipped with a linear order. For any $m \in \mathbb{N}$, an $m \times n$ matrix $A$ over $R$, and an $n \times m$ matrix $B$ over $R$, the determinant of their product is given by the Cauchy–Binet formula: $$\det(A B) = \sum_{S \subseteq n, |S| = m} \det(A_{S}) \det(B_{S})$$ where the sum is taken over all subsets $S$ of $n$ with cardinality $m$. Here, $A_S$ denotes the $m \times m$ submatrix of $A$ formed by the columns indexed by $S$, and $B_S$ denotes the $m \times m$ submatrix of $B$ formed by the rows indexed by $S$, both ordered according to the linear order on $n$.

For any two $d \times d$ complex matrices $M$ and $N$, and any natural number $k$, the $k$-th compound matrix of their product $M N$ is equal to the product of their respective $k$-th compound matrices: $$C_k(MN) = C_k(M) C_k(N)$$ where $C_k(M)$ denotes the `compoundMatrix` of $M$ of order $k$, whose entries are the $k \times k$ minors of $M$.

Let $M$ be a $d \times d$ complex matrix and $k$ be a natural number. The $k$-th compound matrix of the conjugate transpose of $M$ is equal to the conjugate transpose of the $k$-th compound matrix of $M$. High-level notationally: $C_k(M^*) = (C_k(M))^*$.

Let $M = \text{diag}(f)$ be a diagonal matrix indexed by a finite set $d$. For any $k \in \mathbb{N}$, the $k$-th compound matrix $C_k(M)$ is also a diagonal matrix. Its entries are indexed by subsets $S \subseteq d$ with $|S|=k$, and the diagonal entry corresponding to such a subset $S$ is given by the product of the diagonal elements of $M$ indexed by $S$, i.e., $\prod_{i \in S} f_i$.

Let $d$ be a finite index set and $M$ be a $d \times d$ complex matrix. For any natural number $k$, let $C_k(M)$ denote the $k$-th compound matrix of $M$, whose rows and columns are indexed by subsets $S \subseteq d$ of size $k$. Then for every such subset $S$, there exists a corresponding index $j$ in the index set of the compound matrix such that the $j$-th singular value of $C_k(M)$ is equal to the product of the singular values of $M$ indexed by the elements of $S$. That is, $$\sigma_j(C_k(M)) = \prod_{i \in S} \sigma_i(M)$$ where $\sigma$ denotes the singular values of the respective matrices.

Let $f: \{0, \dots, n-1\} \to \mathbb{R}$ be a non-increasing sequence of non-negative real numbers. Let $k$ be a natural number such that $k \le n$, and let $g: \{0, \dots, k-1\} \to \{0, \dots, n-1\}$ be an injective function. Then the product of any $k$ values of $f$ is bounded by the product of its $k$ largest values: $$\prod_{i=0}^{k-1} f(g(i)) \le \prod_{i=0}^{k-1} f(i)$$

Let $A$ be a $d \times d$ complex matrix where $d$ is a finite index set with strictly positive cardinality $|d| > 0$. Let $\sigma \downarrow_i(A)$ denote the $i$-th singular value of $A$ when sorted in non-increasing order. Then the $0$-th sorted singular value is equal to the maximum of all singular values of $A$: $$\sigma \downarrow_0(A) = \max_{i \in d} \sigma_i(A)$$

Let $A$ be a $d \times d$ complex matrix, where $d$ is a finite index set. Let $\sigma(A)$ denote the collection of singular values of $A$ indexed by $d$, and let $\sigma^\downarrow(A)$ be the sequence of these singular values sorted in non-increasing order, indexed by $\{0, \dots, |d|-1\}$. For any index $i \in d$, there exists an index $j \in \{0, \dots, |d|-1\}$ such that the $i$-th singular value of $A$ is equal to the $j$-th element of the sorted singular value sequence: $$\sigma_i(A) = \sigma^\downarrow_j(A)$$

Let $A$ be a $d \times d$ complex matrix where $d$ is a finite index set. Let $\sigma_i(A)$ denote the collection of singular values of $A$, and let $\sigma^\downarrow_j(A)$ denote the $j$-th element of the sorted sequence of these singular values (arranged in non-increasing order). Then for any index $j \in \{0, \dots, |d|-1\}$, there exists an index $i \in d$ such that $\sigma^\downarrow_j(A) = \sigma_i(A)$.

Let $M$ be a $d \times d$ complex matrix and let $k$ be a natural number. Let $C_k(M)$ denote the $k$-th compound matrix of $M$, whose rows and columns are indexed by the set $\mathcal{S}_k = \{ S \subseteq d : |S| = k \}$. Then there exists a permutation $\sigma$ of the index set $\mathcal{S}_k$ such that for every $S \in \mathcal{S}_k$, the singular values of the compound matrix $C_k(M)$ are related to the singular values of $M$ by: $$\sigma_{C_k(M)}(\sigma(S)) = \prod_{i \in S} \sigma_M(i)$$ where $\prod_{i \in S} \sigma_M(i)$ represents the product of the singular values of $M$ indexed by the elements of the subset $S$.

Let $M$ be a $d \times d$ complex matrix and let $k$ be a natural number. Let $C_k(M)$ be the $k$-th compound matrix of $M$, whose indices are subsets of $d$ with cardinality $k$. For any index $j$ of the compound matrix, there exists a subset $S \subseteq d$ with $|S| = k$ such that the singular value of the compound matrix $\sigma_j(C_k(M))$ is equal to the product of the singular values of $M$ indexed by the elements of $S$, i.e., $$\sigma_j(C_k(M)) = \prod_{i \in S} \sigma_i(M).$$ More formally, for any $j \in \{ S \subseteq d : |S| = k \}$, there exists $S \in \{ S \subseteq d : |S| = k \}$ such that $\sigma_j(C_k(M)) = \prod_{i=0}^{k-1} \sigma_{s_i}(M)$, where $s_i$ are the elements of $S$ in increasing order.

Let $M$ be a $d \times d$ complex matrix, and let $n$ be the cardinality of the index set $d$. Let $\sigma_j(M)$ for $j \in d$ denote the singular values of $M$, and let $\sigma^\downarrow_i(M)$ for $i \in \{0, \dots, n-1\}$ denote the singular values of $M$ sorted in non-increasing order. There exists a bijection $\sigma : \{0, \dots, n-1\} \simeq d$ such that for all $i$, $\sigma_{\sigma(i)}(M) = \sigma^\downarrow_i(M)$.

Let $M$ be a $d \times d$ complex matrix, and let $\sigma_1(M) \ge \sigma_2(M) \ge \dots \ge \sigma_n(M) \ge 0$ denote its singular values sorted in non-increasing order, where $n$ is the dimension of the index set $d$. For any natural number $k \le n$ and any subset $S \subseteq d$ of cardinality $k$, the product of the singular values associated with the indices in $S$ is less than or equal to the product of the top $k$ sorted singular values. That is, $$\prod_{s \in S} \sigma_s(M) \le \prod_{i=1}^k \sigma_i(M).$$

Let $M$ be a $d \times d$ complex matrix and $k$ be a natural number such that $k \le |d|$, where $|d|$ denotes the cardinality of the index set $d$. Then there exists a subset $S$ of the indices of $d$ with size $k$ such that the product of the singular values of $M$ indexed by $S$ is equal to the product of the $k$ largest singular values of $M$. Mathematically, \[ \exists S \subseteq d, |S| = k \implies \prod_{i=0}^{k-1} \sigma_{\text{idx}(S, i)}(M) = \prod_{i=0}^{k-1} \sigma^\downarrow_i(M) \] where $\sigma_{\text{idx}(S, i)}(M)$ represents the singular values associated with the elements of $S$ (ordered by the index set's natural order) and $\sigma^\downarrow_i(M)$ represents the $i$-th singular value in non-increasing order.

Let $M$ be a $d \times d$ complex matrix and let $k$ be a natural number such that $k \le \text{card}(d)$. Let $\sigma\downarrow_i(M)$ denote the $i$-th singular value of $M$ arranged in non-increasing order. Then the product of the $k$ largest singular values of $M$ is equal to the largest singular value of the $k$-th compound matrix $C_k(M)$: $$\prod_{i=0}^{k-1} \sigma\downarrow_i(M) = \sigma\downarrow_0(C_k(M))$$ where the index $0$ on the right-hand side denotes the largest singular value of $C_k(M)$.

Let $H$ be a Hermitian matrix of size $n \times n$ (where $n > 0$) with entries in $\mathbb{C}$. Let $\lambda$ denote the eigenvalues of $H$. Then for any vector $v \in \mathbb{C}^n$, the Rayleigh quotient bound holds: $$\text{Re}(v^\dagger H v) \le (\max_i \lambda_i) \cdot \text{Re}(v^\dagger v)$$ where $v^\dagger$ denotes the conjugate transpose of $v$.

Let $A$ be a $d \times d$ complex matrix where the dimension $d = |e|$ is positive. For any index $i \in e$, the $i$-th eigenvalue of the Hermitian matrix $A^* A$ (constructed via `isHermitian_mul_conjTranspose_self`) is less than or equal to the square of the largest singular value of $A$, denoted by $\sigma_1(A)$ (represented by `singularValuesSorted A ⟨0, h⟩`).

Let $A$ be a square matrix of size $d \times d$ over the complex numbers $\mathbb{C}$, where $d > 0$. For any vector $v \in \mathbb{C}^d$, the real part of the quadratic form associated with $A^\dagger A$ satisfies the inequality $$\text{Re}(\langle v, A^\dagger A v \rangle) \le \sigma_1(A)^2 \cdot \text{Re}(\langle v, v \rangle)$$ where $A^\dagger$ is the conjugate transpose of $A$, $\langle \cdot, \cdot \rangle$ denotes the standard Hermitian inner product (specifically $v^\dagger v$), and $\sigma_1(A)$ is the largest singular value of $A$ (denoted in the formal text as the $0$-th element of the sorted singular values).

Let $e$ be a finite index set with cardinality $|e| > 0$. For any two $e \times e$ complex matrices $M$ and $N$, let $\sigma_1(A)$ denote the largest singular value of a matrix $A$ (represented as the first element of the sorted singular values). Then the largest singular value of the product $M N$ satisfies the inequality $$\sigma_1(MN) \leq \sigma_1(M) \sigma_1(N).$$ This property is known as the submultiplicativity of the operator norm (spectral norm).

Let $A$ and $B$ be $d \times d$ complex matrices, and let $\sigma\downarrow_i(M)$ denote the $i$-th largest singular value of a matrix $M$. For any $k \leq \text{card}(d)$, the product of the $k$ largest singular values of $AB$ is less than or equal to the product of the $k$ largest singular values of $A$ and $B$. That is, $$\prod_{i=0}^{k-1} \sigma\downarrow_i(AB) \leq \prod_{i=0}^{k-1} (\sigma\downarrow_i(A) \cdot \sigma\downarrow_i(B)).$$

Let $f: \{0, \dots, n-1\} \to \mathbb{R}$ be a sequence of real numbers. If $f$ is non-negative ($f(i) \ge 0$ for all $i$) and antitone (monotonically non-increasing), then for any positive real number $r > 0$, the sequence $f^r$ defined by $i \mapsto f(i)^r$ is also antitone.

Let $x, y: \{0, \dots, n-1\} \to \mathbb{R}$ be sequences of non-negative real numbers such that $x$ is weakly log-majorized by $y$; that is, for every $k \in \{0, \dots, n\}$, $$\prod_{i=0}^{k-1} x_i \leq \prod_{i=0}^{k-1} y_i.$$ Then for any $r > 0$, the sequences $x^r$ and $y^r$ defined by $(x^r)_i = x_i^r$ and $(y^r)_i = y_i^r$ also satisfy the weak log-majorization property: $$\prod_{i=0}^{k-1} x_i^r \leq \prod_{i=0}^{k-1} y_i^r$$ for all $k \in \{0, \dots, n\}$.

Let $x, y: \{0, \dots, n-1\} \to \mathbb{R}$ be finite sequences of positive real numbers. Suppose that $x$ is antitone (non-increasing) and that $x$ is weakly log-majorized by $y$, such that for every $k \in \{0, \dots, n\}$, the product of the first $k$ terms satisfies $\prod_{i=0}^{k-1} x_i \le \prod_{i=0}^{k-1} y_i$. Then the following inequality holds: $$0 \leq \sum_{i=0}^{n-1} x_i \log\left(\frac{y_i}{x_i}\right)$$

For any real numbers $a$ and $b$ such that $a > 0$ and $b > 0$, the following inequality holds: $$b - a \ge a \log(b/a)$$ where $\log$ denotes the natural logarithm.

Let $x, y \in \mathbb{R}^n$ be finite sequences of non-negative real numbers ($x_i, y_i \ge 0$ for all $i \in \{0, \dots, n-1\}$) that are both non-increasing (antitone). If $x$ is weakly log-majorized by $y$, such that for every $k \in \{0, \dots, n\}$ the product of the first $k$ terms satisfies $$\prod_{i=0}^{k-1} x_i \le \prod_{i=0}^{k-1} y_i,$$ then the sum of the elements of $x$ is less than or equal to the sum of the elements of $y$: $$\sum_{i=0}^{n-1} x_i \le \sum_{i=0}^{n-1} y_i.$$

Let $x = (x_0, \dots, x_{n-1})$ and $y = (y_0, \dots, y_{n-1})$ be sequences of $n$ real numbers. Suppose that for all $i$, $x_i \ge 0$ and $y_i \ge 0$, and that both sequences are antitone (i.e., $x_0 \ge x_1 \ge \dots \ge x_{n-1}$ and $y_0 \ge y_1 \ge \dots \ge y_{n-1}$). If $x$ is weakly log-majorized by $y$, such that for every $k \in \{1, \dots, n\}$ the product of the $k$ largest elements satisfies $$\prod_{i=0}^{k-1} x_i \le \prod_{i=0}^{k-1} y_i,$$ then for any real number $r > 0$, the sum of the $r$-th powers satisfies $$\sum_{i=0}^{n-1} x_i^r \le \sum_{i=0}^{n-1} y_i^r.$$

Let $A$ and $B$ be $d \times d$ complex matrices, and let $\sigma_i(M)$ denote the $i$-th singular value of a matrix $M$ sorted in non-increasing order ($\sigma_1 \ge \sigma_2 \ge \dots$). For any real number $r > 0$, the sum of the $r$-th powers of the singular values of the product $AB$ is bounded by the sum of the products of the $r$-th powers of the individual singular values: $$\sum_{i=1}^d \sigma_i(AB)^r \le \sum_{i=1}^d (\sigma_i(A) \sigma_i(B))^r$$

Let $A$ and $B$ be complex $d \times d$ matrices, and let $\sigma_i(A)$ and $\sigma_i(B)$ denote their respective singular values sorted in non-increasing order. For any positive real numbers $r, p, q$ such that $\frac{1}{r} = \frac{1}{p} + \frac{1}{q}$, the following inequality holds: $$\sum_{i=1}^n (\sigma_i(A)^r \cdot \sigma_i(B)^r) \le \left( \sum_{i=1}^n \sigma_i(A)^p \right)^{r/p} \left( \sum_{i=1}^n \sigma_i(B)^q \right)^{r/q}$$ where $n$ is the dimension of the matrices. This corresponds to a finite-sum Hölder inequality applied to sequences of the $r$-th powers of sorted singular values with conjugate exponents $p' = p/r$ and $q' = q/r$.