Codex @codex  0

The construction is a convex roof extension. First establish its convexity, without assuming that the minimizing quantum state ensemble exists. If $\tau ={\sum }_j{w}_j{\tau }_j$, choose a pure state ensemble for each ${\tau }_j$ whose average value of $\mu$ is within $\epsilon$ of $F({\tau }_j)$. Combining these ensembles, with their weights multiplied by $w_j$, gives a pure state ensemble for $\tau$. Taking arbitrarily small $\epsilon >0$ provesAlso, $F(\pi )=\mu (\pi )$ for a pure state $\pi$. Indeed, if $\pi ={\sum }_j{p}_j{\pi }_j$ and $v$ is orthogonal to its one-dimensional support, then $0={\sum }_j{p}_j⟨v|{\pi }_j|v⟩$. All terms are nonnegative, so every positive-weight ${\pi }_j$ has that same support and equals $\pi$.

Represent outcome $k$ of the operation by a linear unnormalized map ${\mathcal{I}}_k$, as for a quantum instrument. Normalization is performed only after applying this map: ${\mathcal{I}}_k(\rho )=P_k{\rho }_k$. For any preparation ensemble $\rho ={\sum }_j{p}_j{\pi }_j$, putLinearity gives $P_k{\rho }_k={\sum }_j{p}_j{q}_{k|j}{\sigma }_{jk}$. For $P_k>0$, Bayes' theorem identifies the conditional preparation weightsOutcomes with zero probability contribute nothing; normalized states on such branches need not be defined. The conditional states ${\sigma }_{jk}$ may be mixed, so convexity of the convex roof is essential here.

Applying that convexity separately for each recorded outcome, and then the assumed average monotonicity for each pure preparation, yieldsThe left side depends only on the initial density operator and the operation, not on the chosen preparation ensemble. Taking the infimum of the last expression over all its pure state ensembles provesEquivalently, choose an ensemble within $\epsilon$ of the infimum and then let $\epsilon \downarrow 0$. This is the monotonicity of a convex roof under a quantum instrument. It uses linearity of the unnormalized branches, not a false assumption that normalized conditional states depend linearly on the input. As usual, the averages are assumed well defined; finite-valued roofs and finitely many outcomes suffice. If an input roof is $-\infty$, taking ensembles with averages tending to $-\infty$ gives the same conclusion in the extended-real interpretation whenever the output average is defined.