QuantumInfo.Finite.ResourceTheory.FreeState

Given two mixed states $\rho_1$ and $\rho_2$ belonging to the Hilbert spaces $H_i$ and $H_j$ respectively, the operation $\rho_1 \otimes_r \rho_2$ produces a new mixed state in the Hilbert space $H_{i \cdot j}$. This is defined by first taking the natural tensor product $\rho_1 \otimes \rho_2$ (resulting in a state on the product space $H_i \times H_j$) and then relabeling the basis indices using the equivalence $H_i \times H_j \simeq H_{i \cdot j}$ provided by the structure of the resource pretheory.

This is a notation definition for a binary operator $\otimes_r$ which represents the product relabeling operation `prodRelabel`. Given two resource states $\rho_1$ and $\rho_2$ belonging to the state spaces of indices $i$ and $j$ respectively, $\rho_1 \otimes_r \rho_2$ denotes the resulting state in the state space of the product index $i \cdot j$.

Let $\rho_1 \in \text{MState}(H_i)$, $\rho_2 \in \text{MState}(H_j)$, and $\rho_3 \in \text{MState}(H_k)$ be quantum mixed states in a resource pretheory. Then the tensor product with relabeling $\otimes_r$ satisfies the associativity property up to equivalence, such that $(\rho_1 \otimes_r \rho_2) \otimes_r \rho_3 \asymp \rho_1 \otimes_r (\rho_2 \otimes_r \rho_3)$, where $\asymp$ denotes the equivalence relation between mixed states in the resource pretheory.

Let $\rho_1 \in \text{MState}(H(i))$ and $\rho_2 \in \text{MState}(H(j))$ be quantum mixed states. Given proofs $hik: k = i$ and $hlj: l = j$, which imply a correspondence between the Hilbert space indices, and a proof $h: H(k \cdot l) = H(i \cdot j)$, the relabeling of the product state $\rho_1 \otimes_r \rho_2$ via the cast map of $h$ is equal to the product of the individually relabeled states. That is, $$(\rho_1 \otimes_r \rho_2).\text{relabel}(\text{cast } h) = (\rho_1.\text{relabel}(\text{cast } H(hik))) \otimes_r (\rho_2.\text{relabel}(\text{cast } H(hlj)))$$ where $\otimes_r$ denotes the product of mixed states in the resource pretheory and $\text{relabel}$ denotes the reindexing of a state via a bijection.

Let $M_1$ be a completely positive trace-preserving (CPTP) map from the space of matrices on $\mathcal{H}_i$ to $\mathcal{H}_j$, and $M_2$ be a CPTP map from $\mathcal{H}_k$ to $\mathcal{H}_l$. The operation $M_1 \otimes^{cp}_r M_2$ is a CPTP map from the space of matrices on $\mathcal{H}_{i \cdot k}$ to $\mathcal{H}_{j \cdot l}$. It is defined by the composition $$\Lambda_{out} \circ (M_1 \otimes M_2) \circ \Lambda_{in}$$ where: - $M_1 \otimes M_2$ is the standard tensor product of CPTP maps acting from $\mathcal{H}_i \otimes \mathcal{H}_k$ to $\mathcal{H}_j \otimes \mathcal{H}_l$. - $\Lambda_{in}$ is the CPTP map induced by the equivalence $\mathcal{H}_{i \cdot k} \simeq \mathcal{H}_i \times \mathcal{H}_k$. - $\Lambda_{out}$ is the CPTP map induced by the equivalence $\mathcal{H}_j \times \mathcal{H}_l \simeq \mathcal{H}_{j \cdot l}$. This construction ensures the tensor product is compatible with the indexing structure of the resource pretheory.

Let $M_1: \text{CPTPMap}(\mathcal{H}_i, \mathcal{H}_j)$ and $M_2: \text{CPTPMap}(\mathcal{H}_k, \mathcal{H}_l)$ be two Completely Positive Trace-Preserving (CPTP) maps between Hilbert spaces. The notation $M_1 \otimes^{cp}_r M_2$ denotes the tensor product of these CPTP maps, resulting in a map from $\text{CPTPMap}(\mathcal{H}_{i \cdot k}, \mathcal{H}_{j \cdot l})$.

Let $\rho$ and $\sigma$ be quantum mixed states on Hilbert spaces with dimensions $H(i)$ and $H(j)$ respectively. If the underlying matrix $m(\rho)$ is positive definite and the underlying matrix $m(\sigma)$ is positive definite, then the underlying matrix of their product state $m(\rho \otimes_r \sigma)$ is also positive definite.

Let $\rho_1, \rho_2$ be quantum mixed states acting on a Hilbert space of dimension $H(i)$, and let $\sigma_1, \sigma_2$ be quantum mixed states acting on a Hilbert space of dimension $H(j)$. The quantum relative entropy $D$ of the tensor product states (after relabeling) satisfies the additivity property: $$D(\rho_1 \otimes_r \sigma_1 \| \rho_2 \otimes_r \sigma_2) = D(\rho_1 \| \rho_2) + D(\sigma_1 \| \sigma_2)$$ where $\otimes_r$ denotes the tensor product of mixed states combined with a relabeling map to the space of dimension $H(i \cdot j)$.

Let $\alpha \in \mathbb{R}$ be a real number. For any quantum mixed states $\rho_1, \rho_2$ acting on a Hilbert space of dimension $H(i)$ and mixed states $\sigma_1, \sigma_2$ acting on a Hilbert space of dimension $H(j)$, the sandwiched Rényi relative entropy $\tilde{D}_\alpha$ satisfies the additivity property: $$\tilde{D}_\alpha(\rho_1 \otimes_r \sigma_1 \| \rho_2 \otimes_r \sigma_2) = \tilde{D}_\alpha(\rho_1 \| \rho_2) + \tilde{D}_\alpha(\sigma_1 \| \sigma_2)$$ where $\otimes_r$ denotes the tensor product of mixed states followed by a basis relabeling to the Hilbert space of dimension $H(i \cdot j)$.

The indexing set $\iota$ of a `UnitalPretheory` is equipped with a `Monoid` structure. This structure defines a binary operation (multiplication) on $\iota$, representing the composition or aggregation of resource spaces, and a unit element $1 \in \iota$ representing the trivial or identity resource space.

Given a `UnitalPretheory` with an indexing set $\iota$, let $i \in \iota$ represent a type of resource space. For any natural number $n \in \mathbb{N}$, the operation $i^n$ denotes the $n$-th power of the space $i$ within the monoid structure of $\iota$. This represents the composition or aggregation of $n$ copies of the resource space $i$, where the identity $1 \in \iota$ corresponds to the unit space (the $0$-th power).

The notation $i \otimes^H[n]$ denotes the $n$-fold tensor power of a space (or index) $i$, defined by the function `spacePow`. Here, $i \in \iota$ is an element of the index type of the pretheory and $n \in \mathbb{N}$ is a natural number representing the power.

For any element $i$ in a monoid $\iota$, the power of $i$ to the exponent $0$ is equal to the identity element $1$, denoted $i^0 = 1$.

For any element $i$ in a monoid $\iota$, the power of $i$ to the exponent $1$ is equal to $i$, i.e., $i^1 = i$.

For any element $i$ in a monoid $\iota$ and any natural number $n \in \mathbb{N}$, the power of $i$ to the successor of $n$ is given by $i^{n + 1} = (i^n) \cdot i$.

Let $\iota$ be a type with a monoid structure. For any element $i \in \iota$ and any natural numbers $m, n \in \mathbb{N}$, the power operation satisfies the exponent addition rule: $i^{m + n} = (i^m) \cdot (i^n)$.

For any natural numbers $m, n \in \mathbb{N}$ and an element $i$ of a monoid $\iota$, it holds that $i^{m \cdot n} = (i^m)^n$.

Let $i$ be an element of a monoid $\iota$ representing a system dimension or index, and let $H: \iota \to \text{Type}$ be a mapping to the corresponding state spaces. Given a mixed state $\rho \in \text{MState}(H(i))$ and a natural number $n \in \mathbb{N}$, the state power $\rho^{\otimes_r n}$ (also denoted as $\rho \otimes_r^{[n]}$) is an element of $\text{MState}(H(i^n))$. It is defined by induction on $n$: - For $n = 0$, it is the default state (typically the identity or unit state of the resource theory). - For $n+1$, it is defined as $\rho^{\otimes_r n} \otimes_r \rho$, where $\otimes_r$ is the product operation defined in the resource theory.

This definition introduces the notation $\rho^{\otimes_r n}$ (or $\rho \otimes_r^{[n]}$) for the $n$-th tensor power of a mixed state $\rho$. Given a state $\rho$ in the state space $H(i)$ and a natural number $n$, the expression $\rho^{\otimes_r n}$ represents the repeated resource-theoretic product of the state $\rho$ with itself $n$ times, yielding a state in $H(i^n)$.

Let $i$ be an element of a monoid $\iota$ and $H(i)$ be the corresponding state space. For any mixed state $\rho \in \text{MState}(H(i))$, its $0$-th tensor power $\rho^{\otimes_r 0}$ (denoted as $\rho \otimes_r^{[0]}$) is equal to the default state in $\text{MState}(H(i^0))$. In a unital pretheory, this default state corresponds to the maximally mixed state or the unit state of the resource theory.

Let $\rho$ be a mixed state in the Hilbert space associated with an index $i$ in a unital resource pretheory. Let $\rho^{\otimes n}$ (denoted formally as `ρ ⊗ᵣ^[n]`) denote the $n$-fold tensor power of the state. Then the first tensor power of $\rho$ is equivalent (up to relabeling) to the state itself, i.e., $\rho^{\otimes 1} \cong \rho$.

Let $i$ be an element of a monoid $\iota$ representing a system index, and let $H: \iota \to \text{Type}$ be a mapping to the corresponding state spaces. For any mixed state $\rho \in \text{MState}(H(i))$ and any natural number $n$, the $(n+1)$-th tensor power of the state, denoted $\rho^{\otimes_r (n+1)}$, is equal to the product of the $n$-th tensor power and the state itself, i.e., $\rho^{\otimes_r (n+1)} = \rho^{\otimes_r n} \otimes_r \rho$.

Let $i$ be an object in a unital resource pretheory and $\rho \in \text{MState}(H(i))$ be a mixed state on the associated Hilbert space. For any natural numbers $m$ and $n$, the $(m+n)$-th tensor power of the state $\rho$, denoted by $\rho^{\otimes (m+n)}$, is equivalent under the pretheory's equivalence relation $\asymp$ to the tensor product of its $m$-th and $n$-th powers, $\rho^{\otimes m} \otimes_r \rho^{\otimes n}$.

Let $i$ be an element of a monoid $\iota$ and $\rho \in \text{MState}(H(i))$ be a mixed state. For any natural numbers $m$ and $n$, the $(m+n)$-th tensor power of the state, denoted $\rho^{\otimes_r (m+n)}$, is equal to the state obtained by relabeling the tensor product of its $m$-th and $n$-th powers, $\rho^{\otimes_r m} \otimes_r \rho^{\otimes_r n}$, using the equivalence induced by the identity $i^{m+n} = i^m \cdot i^n$.

Let $i$ be an element of a monoid $\iota$ representing a system index, and let $H: \iota \to \text{Type}$ be a mapping to the corresponding state spaces in a unital resource pretheory. For any mixed state $\rho \in \text{MState}(H(i))$ and any natural numbers $m$ and $n$, the $(m \cdot n)$-th tensor power of the state $\rho$, denoted by $\rho^{\otimes_r (m \cdot n)}$, is equivalent under the pretheory's equivalence relation $\asymp$ to the $n$-th tensor power of the $m$-th tensor power of $\rho$, denoted by $(\rho^{\otimes_r m})^{\otimes_r n}$.

Let $i$ be an element of a monoid $\iota$ and $H$ be a mapping from $\iota$ to state spaces. For any quantum mixed state $\rho \in \text{MState}(H(i))$ and any natural numbers $m$ and $n$, the state power $\rho^{\otimes_r (m \cdot n)}$ is equal to the $n$-th state power of the $m$-th state power, $(\rho^{\otimes_r m})^{\otimes_r n}$, relabeled by the equivalence induced by the identity $H(i^{m \cdot n}) = H((i^m)^n)$ resulting from the power law $(i^m)^n = i^{m \cdot n}$.

Let $\rho$ be a quantum mixed state in a Hilbert space $H(i)$. If the underlying density matrix of $\rho$ is positive definite, then for any natural number $n$, the density matrix of the $n$-th tensor power $\rho^{\otimes n}$ (denoted $\rho \otimes_r^{[n]}$) is also positive definite.

For any mixed state $\rho \in \text{MState}(H(i))$ and natural numbers $n$ and $m$, if $n = m$, then the $n$-th tensor power of the state $\rho^{\otimes_r n}$ is equal to the $m$-th tensor power $\rho^{\otimes_r m}$ relabeled by the type-level equality (cast) between their respective basis spaces $H(i^n)$ and $H(i^m)$.

Let $\rho$ and $\sigma$ be two quantum mixed states in a Hilbert space $H(i)$. For any natural number $n$, let $\rho^{\otimes_r n}$ and $\sigma^{\otimes_r n}$ denote the $n$-th tensor powers of the states within the unital pretheory. The quantum relative entropy $D$ satisfies the following scaling property under the tensor power: $$D(\rho^{\otimes_r n} \| \sigma^{\otimes_r n}) = n \cdot D(\rho \| \sigma)$$ where $D(\cdot \| \cdot)$ denotes the quantum relative entropy taking values in the extended non-negative real numbers ($[0, \infty]$).

Let $\rho \in \text{MState}(H(i))$ and $\sigma \in \text{MState}(H(j))$ be two quantum mixed states in finite-dimensional Hilbert spaces. Let $\rho \otimes_r \sigma$ denote their tensor product within the unital pretheory, and let $m(\cdot)$ denote the underlying density matrix of a state. The infimum of the spectrum of the matrix of the tensor product is equal to the product of the infima of the spectra of the individual matrices: $$\inf(\text{spec}((\rho \otimes_r \sigma).m)) = \inf(\text{spec}(\rho.m)) \cdot \inf(\text{spec}(\sigma.m))$$ where $\text{spec}(\cdot)$ denotes the set of eigenvalues (spectrum) of the matrix in $\mathbb{R}$.

Let $\sigma \in \text{MState}(H(i))$ be a quantum mixed state in a finite-dimensional Hilbert space indexed by $i$. For any natural number $n$, let $\sigma^{\otimes n}$ (denoted formally as $\sigma \otimes_r^{[n]}$) be the $n$-th tensor power of the state. It holds that the infimum of the spectrum of the underlying matrix of the tensor power state is equal to the $n$-th power of the infimum of the spectrum of the original state's matrix, i.e., $$\inf(\text{spec}(\sigma^{\otimes n})) = (\inf(\text{spec}(\sigma)))^n$$ where $\text{spec}(\cdot)$ denotes the set of eigenvalues (spectrum) of the matrix in $\mathbb{R}$.

For any real number $\alpha$, any mixed states $\rho$ and $\sigma$ in a state space $H(i)$, and any natural number $n$, the $\alpha$-sandwiched Rényi relative entropy between the $n$-th tensor powers of the states is equal to $n$ times the $\alpha$-sandwiched Rényi relative entropy between the original states, i.e., $$\tilde{D}_\alpha(\rho^{\otimes_r n} \| \sigma^{\otimes_r n}) = n \cdot \tilde{D}_\alpha(\rho \| \sigma)$$ where $\otimes_r^{[n]}$ denotes the $n$-th tensor power within the unital pretheory.

The set of free states $\mathcal{F}_i$ is inhabited; that is, there exists at least one quantum mixed state $\rho$ that satisfies the property of being a free state within the specified resource theory indexed by $i$.

In a quantum resource theory indexed by $i$, if the underlying Hilbert space $H_i$ has a basis type of cardinality one (implying the space is 1-dimensional), then any mixed state $\rho \in \text{MState}(H_i)$ is a free state ($\rho \in \mathcal{F}_i$).

For a given quantum resource theory or system indexed by $i$, the set of free states $\mathcal{F}_i$ is a compact subset of the space of mixed states $\text{MState}(H_i)$. This space $\text{MState}(H_i)$ is equipped with the subspace topology of $d \times d$ complex matrices and is itself a compact space.

Let $\iota$ be an index set and assume a free state theory is defined over $\iota$. For any index $i \in \iota$ and any mixed states $\sigma_1, \sigma_2 \in \text{MState}(H_i)$, if $\sigma_1$ and $\sigma_2$ are free states, then their convex combination $p\sigma_1 + (1-p)\sigma_2$ (denoted $p[\sigma_1 \leftrightarrow \sigma_2]$) is also a free state for any probability $p \in [0, 1]$.

Let $\iota$ be an index set for a system within a free state theory. For any index $i \in \iota$ and any mixed state $\rho \in \text{MState}(H(i))$, if $\rho$ is a free state, then its $n$-th tensor power $\rho^{\otimes_r n}$ (denoted $\rho \otimes_r^{[n]}$) is also a free state for any natural number $n \in \mathbb{N}$.

Let $\iota$ be an index set for a unital free state theory, where $H_i$ denotes the Hilbert space basis for each $i \in \iota$. For any two indices $i, j \in \iota$ such that $j = i$, and any mixed state $\rho \in \text{MState}(H_i)$, let $\text{relabel}(\text{cast})$ denote the reindexing of the state via the cast equivalence between $H_j$ and $H_i$. Then the relabeled state $\rho'$ is a free state if and only if the original state $\rho$ is a free state.

In a unital free state theory, for any quantum mixed state $\rho$, the minimum quantum relative entropy $D(\rho\|\sigma)$ over all free states $\sigma$ is finite (i.e., not equal to $\infty$). Here, $D(\cdot\|\cdot)$ denotes the quantum relative entropy and $\text{IsFree}$ denotes the set of free states in the theory.

In a unital free state theory, the function maps a quantum mixed state $\rho \in \text{MState}(\mathcal{H}_i)$ to a non-negative real number $\mathbb{R}_{\ge 0}$ representing its relative entropy of resource. This value is defined as the infimum of the quantum relative entropy $D(\rho \| \sigma)$ over the set of free states $\sigma \in \text{IsFree}$: $$R_r(\rho) = \inf_{\sigma \in \text{IsFree}} D(\rho \| \sigma)$$ The definition uses the `untop` operation to convert the infimum from an extended non-negative real ($[0, \infty]$) to a non-negative real ($\mathbb{R}_{\ge 0}$), which is justified by the property that this infimum is always finite ($\neq \infty$) for any state $\rho$.

$R_r$ is a mathematical notation representing the Relative Entropy of Resource, defined within the context of Unital Free State Theory. It is defined as a function $R_r: \text{MState}(\mathcal{H}_i) \to \mathbb{R}_{\ge 0}$ that maps a quantum state $\rho$ to the infimum of the quantum relative entropy $D(\rho \| \sigma)$ over the set of free states $\sigma \in \text{IsFree}$. Specifically: $$R_r(\rho) = \inf_{\sigma \in \text{IsFree}} D(\rho \| \sigma)$$ The notation $R_r$ is introduced as a scoped parser descriptor to allow this symbol to be used in formal expressions.

Given a mixed state $\rho$ in the Hilbert space $\mathcal{H}_i$, there exists a free state $\sigma \in \text{IsFree}$ such that the quantum relative entropy between $\rho$ and $\sigma$, denoted by $D(\rho\|\sigma)$, is equal to the relative entropy of resource of $\rho$, denoted by $R_r(\rho)$. This $R_r(\rho)$ is defined as the infimum of the relative entropy over all free states, $R_r(\rho) = \inf_{\sigma \in \text{IsFree}} D(\rho\|\sigma)$.

Let $\rho$ be a quantum mixed state in the Hilbert space $H(i)$ for some index $i$ in a unital pretheory. We define $R_r(\rho)$ as the relative entropy resource measure of $\rho$, given by $\inf_{\sigma \in \text{IsFree}} D(\rho \| \sigma)$. Let $\rho^{\otimes_r n}$ denote the $n$-th power of the state $\rho$ under the resource-theoretic tensor product. Then the sequence $a_n = R_r(\rho^{\otimes_r n})$ is subadditive, meaning that for all $m, n \in \mathbb{N}$, it satisfies: $$R_r(\rho^{\otimes_r (m+n)}) \leq R_r(\rho^{\otimes_r m}) + R_r(\rho^{\otimes_r n})$$

Let $\rho \in \text{MState}(H(i))$ be a quantum mixed state in a unital free state theory. The regularized relative entropy of resource, denoted as $R_r^\infty(\rho)$, is defined as the limit of the normalized relative entropy of resource of the $n$-th tensor power of the state: $$R_r^\infty(\rho) = \lim_{n \to \infty} \frac{R_r(\rho^{\otimes_r n})}{n}$$ Given that the sequence $a_n = R_r(\rho^{\otimes_r n})$ is subadditive, this limit exists and is equal to the infimum $\inf_{n \in \mathbb{N}^+} \frac{R_r(\rho^{\otimes_r n})}{n}$. The value is a non-negative real number $\mathbb{R}_{\ge 0}$.

Let $\rho$ be a quantum mixed state. We define the regularized relative entropy resource measure $R_r^\infty(\rho)$ as the asymptotic limit of the relative entropy resource measure per copy of the state, given by: $$R_r^\infty(\rho) = \lim_{n \to \infty} \frac{R_r(\rho^{\otimes_r n})}{n}$$ Where $R_r$ is the relative entropy of resource and $\otimes_r$ is the resource-theoretic tensor product. Due to the subadditivity of the sequence $R_r(\rho^{\otimes_r n})$, this limit exists and is equal to the infimum $\inf_n \frac{R_r(\rho^{\otimes_r n})}{n}$.

In a unital free state theory, let $\rho \in \text{MState}(H(i))$ be a quantum mixed state. Let $R_r(\rho^{\otimes_r n})$ denote the relative entropy of resource of the $n$-th tensor power of $\rho$, and let $R_r^\infty(\rho)$ denote the regularized relative entropy resource. As $n$ approaches infinity, the sequence of normalized relative entropy of resource values $\frac{1}{n} R_r(\rho^{\otimes_r n})$ converges to the regularized relative entropy resource $R_r^\infty(\rho)$. That is, $$\lim_{n \to \infty} \frac{R_r(\rho^{\otimes_r n})}{n} = R_r^\infty(\rho)$$

In a unital free state theory, let $\rho$ be a quantum mixed state in the state space $H(i)$. The sequence defined by the minimum quantum relative entropy of the $n$-th tensor power of $\rho$ with respect to the set of free states $\text{IsFree}$, normalized by $n$, converges to the regularized relative entropy resource of $\rho$. Specifically, $$\lim_{n \to \infty} \frac{1}{n} \inf_{\sigma \in \text{IsFree}} D(\rho^{\otimes_r n} \| \sigma) = R_r^\infty(\rho)$$ where $D(\cdot\|\cdot)$ denotes the quantum relative entropy in the extended non-negative real numbers $\overline{\mathbb{R}}_{\ge 0}$, $\rho^{\otimes_r n}$ is the $n$-th tensor power of the state, and $R_r^\infty(\rho)$ is the regularized relative entropy resource.

For a quantum state $\rho \in \text{MState}(\mathcal{H}_i)$, the global robustness is defined as the infimum of the values $s \in \mathbb{R}_{\geq 0}$ such that there exists a state $\sigma$ where the convex combination $\frac{1}{1+s}\rho + \frac{s}{1+s}\sigma$ is a free state (i.e., belongs to the set `IsFree`). Specifically, $$\text{RG}(\rho) = \inf \left\{ s \in \mathbb{R}_{\geq 0} \mid \exists \sigma, \frac{1}{1+s}\rho + \frac{s}{1+s}\sigma \in \text{IsFree} \right\}$$ where $H i$ denotes the Hilbert space of dimension $d$ associated with index $i$, and $[ \cdot \leftrightarrow \cdot ]$ represents the convex mixture of two states.

Let $\mathcal{H}_i$ denote the Hilbert space associated with index $i$, and let $\mathcal{H}_{d \otimes n}$ denote the $n$-fold tensor power of a space. For a sequence of completely positive trace-preserving (CPTP) maps $f_n: \text{MState}(\mathcal{H}_{d_{In} \otimes n}) \to \text{MState}(\mathcal{H}_{d_{Out} \otimes n})$, the sequence $f_n$ is asymptotically nongenerating if for every sequence of free states $\rho_n \in \text{MState}(\mathcal{H}_{d_{In} \otimes n})$, the global robustness of the transformed states tends to zero in the limit of large $n$: $$\lim_{n \to \infty} \text{RG}(f_n(\rho_n)) = 0$$ where $\text{RG}$ denotes the `GlobalRobustness` measure.