 Convex roof extension

A convex roof extension extends a function $\mu$ on pure states to arbitrary density operators by minimizing its ensemble average over all pure state decompositions. It agrees with $\mu$ on pure states: every positive-weight state in a decomposition of a rank-one density operator has the same one-dimensional support. Concatenating nearly minimizing ensembles proves that $F$ is a convex function. Moreover, every convex function that is no larger than $\mu$ on pure states is no larger than $F$, by applying convexity to each decomposition. Infima need not be attained; an arbitrarily small additive error suffices when $F$ is finite.