QuantumInfo.Finite.Entanglement

Let $\mathcal{H}_d$ be a $d$-dimensional Hilbert space. For a function $g: \mathbb{P}(\mathcal{H}_d) \to \mathbb{R}_{\ge 0}$ defined on the space of pure states (kets up to a global phase), the convex roof extension into the extended non-negative reals $\mathbb{R}_{\ge 0} \cup \{\infty\}$ is a function that maps a mixed state $\rho$ to the infimum of the average value of $g$ over all possible pure-state ensemble decompositions of $\rho$. Specifically, for a mixed state $\rho \in \text{MState}_d$, it is defined as: $$\text{convex\_roof\_ENNReal}(g)(\rho) = \inf_{n \in \mathbb{N}^+, \mathcal{E}} \left\{ \sum_{i=1}^n p_i g(|\psi_i\rangle) \;\middle\vert\; \sum_{i=1}^n p_i |\psi_i\rangle\langle\psi_i| = \rho \right\}$$ where $\mathcal{E} = \{(p_i, |\psi_i\rangle)\}_{i=1}^n$ is a pure-state ensemble consisting of $n$ pairs of probabilities $p_i$ and pure states $|\psi_i\rangle$ whose mixture equals $\rho$. The use of extended non-negative reals $\mathbb{R}_{\ge 0} \cup \{\infty\}$ ensures the existence of the infimum via complete lattice properties.

For a given function $f: \mathcal{S}(\mathcal{H}_d) \to \mathbb{R}_{\geq 0}$ defined on the set of mixed states of a $d$-dimensional Hilbert space, the mixed convex roof extension $\hat{f}$ maps a mixed state $\rho$ to a value in the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$. It is defined as the infimum of the average value of $f$ over all possible mixed-state ensembles $\{p_i, \rho_i\}$ that decompose $\rho$: $$\hat{f}(\rho) = \inf \left\{ \sum_{i=1}^n p_i f(\rho_i) \;\middle\vert\; n \in \mathbb{N}^+, \sum_{i=1}^n p_i \rho_i = \rho \right\}$$ where each ensemble $e$ consists of a finite collection of mixed states $\rho_i$ with associated probabilities $p_i$, such that their mixture $\text{mix}(e)$ equals $\rho$. The result is expressed in $\mathbb{R}_{\geq 0, \infty}$ to leverage the complete lattice properties of the extended reals during the infimum operation.

Let $d$ be a finite-dimensional Hilbert space and $g: \text{KetUpToPhase}(d) \to \mathbb{R}_{\ge 0}$ be a function mapping pure states (up to a global phase) to non-negative real numbers. For any mixed state $\rho$, the convex roof extension of $g$ evaluated at $\rho$ in the extended non-negative real numbers, denoted as $\hat{g}(\rho)$, is never infinite, i.e., $\hat{g}(\rho) \neq \infty$.

Let $d$ be a finite-dimensional Hilbert space and let $f: \mathcal{S}(d) \to \mathbb{R}_{\ge 0}$ be a function mapping mixed states to non-negative real numbers. For any mixed state $\rho \in \mathcal{S}(d)$, the mixed convex roof extension $\hat{f}(\rho)$, defined with values in the extended non-negative real numbers $[0, \infty]$, is never infinite, i.e., $\hat{f}(\rho) \neq \infty$.

Let $\mathcal{D}$ be a finite-dimensional Hilbert space and $\text{MState}(\mathcal{D})$ be the set of mixed states (density operators) on $\mathcal{D}$. Given a function $g: \text{KetUpToPhase}(\mathcal{D}) \to \mathbb{R}_{\ge 0}$ defined on pure states (up to a global phase), the convex roof extension $\text{convex\_roof}(g)$ is a function $\text{MState}(\mathcal{D}) \to \mathbb{R}_{\ge 0}$. For a density matrix $\rho$, it is defined as the infimum of the average value of $g$ over all possible pure-state ensembles $\{p_i, |\psi_i\rangle\}$ that realize $\rho$, i.e., $$\text{convex\_roof}(g)(\rho) = \inf_{\{p_i, \psi_i\}} \sum_i p_i g(|\psi_i\rangle)$$ subject to $\sum_i p_i |\psi_i\rangle\langle\psi_i| = \rho$. This specific definition converts the result from the extended non-negative reals $\overline{\mathbb{R}}_{\ge 0}$ to $\mathbb{R}_{\ge 0}$ using the fact that the infimum is always finite.

Let $d$ be a finite type representing the Hilbert space dimension. Given a function $f: \text{MState } d \to \mathbb{R}_{\ge 0}$ defined on the set of mixed quantum states, the mixed convex roof extension of $f$ is a function that maps a mixed state $\rho$ to the infimum of the average value of $f$ over all possible mixed-state ensembles $\{p_i, \rho_i\}$ that realize $\rho$. Formally, for a mixed state $\rho \in \text{MState } d$, it is defined as: $$\text{mixed\_convex\_roof}(f)(\rho) = \inf \left\{ \sum_i p_i f(\rho_i) \mid \sum_i p_i \rho_i = \rho \right\}$$ where $p_i \ge 0$, $\sum_i p_i = 1$, and $\rho_i$ are mixed states. The definition utilizes `ENNReal.toNNReal` to map the value from the extended non-negative reals $\mathbb{R}_{\ge 0} \cup \{\infty\}$ to the non-negative reals $\mathbb{R}_{\ge 0}$, guaranteed by the fact that the infimum is not infinite.

Let $d$ be a finite type representing the dimension of a Hilbert space, and let $\text{MState } d$ be the set of mixed quantum states (density operators). Given a function $f : \text{MState } d \to \mathbb{R}_{\ge 0}$ defined on mixed states, the function `convex_roof_of_MState_fun` is the convex roof extension of $f$ restricted to pure states. Specifically, let $g = f \circ \text{pureQ}$, where $\text{pureQ} : \text{KetUpToPhase } d \to \text{MState } d$ maps a pure state vector (modulo phase) to its corresponding density operator $|\psi\rangle\langle\psi|$. Then for any mixed state $\rho \in \text{MState } d$, the value is defined as the infimum of the average of $f$ over all pure-state decompositions of $\rho$: $$\text{convex\_roof\_of\_MState\_fun}(f)(\rho) = \inf_{\{p_i, |\psi_i\rangle\}} \sum_i p_i f(|\psi_i\rangle\langle\psi_i|)$$ where the infimum is taken over all ensembles $\{p_i, |\psi_i\rangle\}$ such that $\sum_i p_i |\psi_i\rangle\langle\psi_i| = \rho$.

Let $d$ be a finite-dimensional Hilbert space and $f: \text{MState } d \to \mathbb{R}_{\ge 0}$ be a function on mixed states. For any mixed state $\rho \in \text{MState } d$ and any constant $c \in \mathbb{R}_{\ge 0}$, if for every finite mixed-state ensemble $e = \{p_i, \rho_i\}_{i=1}^n$ such that its mixture $\sum_{i=1}^n p_i \rho_i = \rho$, the average value $\langle f \rangle_e = \sum_{i=1}^n p_i f(\rho_i)$ satisfies $c \le \langle f \rangle_e$, then $c \le \text{mixed\_convex\_roof}(f)(\rho)$.

Let $d$ be a finite-dimensional Hilbert space, $\text{MState}(d)$ be the set of density operators on $d$, and $g: \text{KetUpToPhase}(d) \to \mathbb{R}_{\ge 0}$ be a function defined on pure states. For any mixed state $\rho \in \text{MState}(d)$ and any constant $c \in \mathbb{R}_{\ge 0}$, if for every finite pure-state ensemble $\mathcal{E} = \{(p_i, |\psi_i\rangle)\}_{i=1}^n$ (where $n > 0$) that realizes $\rho$ (i.e., $\sum_i p_i |\psi_i\rangle\langle\psi_i| = \rho$), the average value $\sum_i p_i g(|\psi_i\rangle)$ is greater than or equal to $c$, then the convex roof extension $\text{convex\_roof}(g)(\rho)$ is also greater than or equal to $c$.

Let $d$ be a finite-dimensional Hilbert space and $g: \text{KetUpToPhase}(d) \to \mathbb{R}_{\ge 0}$ be a function defined on pure states (up to a global phase). For a mixed state $\rho \in \text{MState}(d)$ and a constant $c \in \mathbb{R}_{\ge 0}$, if there exists a pure-state ensemble $\mathcal{E} = \{(p_i, |\psi_i\rangle)\}_{i=1}^n$ (with $n > 0$) such that the mixture of the ensemble $\sum_{i=1}^n p_i |\psi_i\rangle\langle\psi_i|$ equals $\rho$, and the average value of $g$ over the ensemble $\sum_{i=1}^n p_i g(|\psi_i\rangle)$ is less than or equal to $c$, then the convex roof extension of $g$ evaluated at $\rho$ satisfies $\text{convex\_roof}(g)(\rho) \le c$.

Let $d$ be a finite-dimensional Hilbert space and $f: \text{MState}(d) \to \mathbb{R}_{\geq 0}$ be a function defined on the set of mixed quantum states. For any mixed state $\rho \in \text{MState}(d)$ and any constant $c \in \mathbb{R}_{\geq 0}$, if there exists a quantum ensemble $\mathcal{E} = \{(p_i, \rho_i)\}_{i=1}^n$ (where $n > 0$) such that the average state $\sum_i p_i \rho_i$ is equal to $\rho$ and the average value of $f$ over the ensemble $\sum_i p_i f(\rho_i)$ is less than or equal to $c$, then the mixed convex roof extension $\hat{f}(\rho)$ is also less than or equal to $c$.

Let $d$ be a finite-dimensional Hilbert space and let $f: \text{MState } d \to \mathbb{R}_{\ge 0}$ be a function defined on the set of mixed quantum states. The mixed convex roof extension of $f$, denoted as $\text{mixed\_convex\_roof}(f)$, is point-wise less than or equal to the convex roof extension of $f$ restricted to pure states, denoted as $\text{convex\_roof\_of\_MState\_fun}(f)$. That is, for any mixed state $\rho \in \text{MState } d$, $$\text{mixed\_convex\_roof}(f)(\rho) \le \text{convex\_roof\_of\_MState\_fun}(f)(\rho)$$ This inequality holds because the mixed convex roof minimizes over all possible mixed-state ensembles $\{p_i, \rho_i\}$ that average to $\rho$, which is a larger set of ensembles than the pure-state ensembles $\{p_i, |\psi_i\rangle\langle\psi_i|\}$ considered by the standard convex roof.

For any pure quantum state $|\psi\rangle$ (represented as a `Ket d`), the convex roof extension of a function $g$ mapping kets up to a phase (elements of `KetUpToPhase d`) to the non-negative real numbers $\mathbb{R}_{\ge 0}$, evaluated at the density matrix $\rho = |\psi\rangle\langle\psi|$ (represented by `MState.pure ψ`), is equal to the value of $g$ applied to the phase-equivalence class of $|\psi\rangle$. Mathematically, this is expressed as: $$\text{convex\_roof}(g)(|\psi\rangle\langle\psi|) = g([\psi])$$ where $[\psi]$ denotes the ket $|\psi\rangle$ modulo a global phase.

Let $d$ be a finite-dimensional Hilbert space and $f: \text{MState } d \to \mathbb{R}_{\ge 0}$ be a function defined on the set of mixed quantum states. For any pure state $|\psi\rangle$ (represented as a `Ket d`), the mixed convex roof extension of $f$ evaluated at the density matrix $\rho = |\psi\rangle\langle\psi|$ (denoted as `pure ψ`) is equal to the value of $f$ evaluated at that pure state. Mathematically, this is expressed as: $$\text{mixed\_convex\_roof}(f)(|\psi\rangle\langle\psi|) = f(|\psi\rangle\langle\psi|)$$

The Entanglement of Formation (EoF) is a function $E_F: \text{MState}(d_1 \times d_2) \to \mathbb{R}_{\ge 0}$ defined as the convex roof extension of the von Neumann entropy of the reduced density matrix of a pure state. Specifically, for a pure state $|\psi\rangle \in \mathcal{H}_{d_1} \otimes \mathcal{H}_{d_2}$, let $\rho_1 = \text{Tr}_2(|\psi\rangle\langle\psi|)$ be the reduced density matrix obtained by tracing out the right subsystem. The function $g$ is defined on the space of pure states up to a phase as $g([\psi]) = S_{vn}(\rho_1)$, where $S_{vn}(\rho) = -\text{Tr}(\rho \log \rho)$ is the von Neumann entropy. The Entanglement of Formation for a general mixed state $\rho$ is then given by: $$E_F(\rho) = \inf_{\{p_i, \psi_i\}} \sum_i p_i S_{vn}\left(\text{Tr}_2(|\psi_i\rangle\langle\psi_i|)\right)$$ where the infimum is taken over all pure-state decompositions such that $\sum_i p_i |\psi_i\rangle\langle\psi_i| = \rho$.

Let $d$ be a finite, non-empty set of basis states. Let $|\text{MES}_d\rangle$ be the maximally entangled state in the bipartite Hilbert space indexed by $d \times d$. The partial trace over the second subsystem of the pure state density matrix $\rho = |\text{MES}_d\rangle\langle\text{MES}_d|$ is equal to the maximally mixed state $\rho_{\text{unif}}$ on the first subsystem.

For a quantum mixed state $\rho$ in a finite-dimensional Hilbert space of dimension $d$, the von Neumann entropy $S_{vN}(\rho)$ is equal to the trace of the matrix obtained by applying the function $f(x) = -x \log x$ to the density matrix $\rho.M$ via the continuous functional calculus (CFC).

Let $d$ be a finite set and $dist$ be a probability distribution over $d$. Let $\rho = \text{MState.ofClassical}(dist)$ be the diagonal density matrix representing this classical distribution in the quantum state space. The von Neumann entropy $S_{vn}(\rho)$ of this state is equal to the Shannon entropy $H_s(dist)$ of the original distribution.

Let $d$ be a finite-dimensional Hilbert space index set. For the maximally entangled state $|\Phi^+\rangle$ (represented by `Ket.MES d`), the Entanglement of Formation $E_f$ of the corresponding pure state density matrix $\rho = |\Phi^+\rangle\langle\Phi^+|$ is equal to the natural logarithm of the dimension of $d$. Mathematically, $$E_f(|\Phi^+\rangle\langle\Phi^+|) = \log|d|$$ where $|d|$ is the cardinality of the set $d$.