Lemma: Finite decoder optima are attained

Both extrema in (eq:optimalError) and (eq:optimalBell) are attained.

Proof. The Choi matrices of CPTP maps of the fixed type are positive, have a fixed partial trace, and form a nonempty compact set. Bell fidelity and the channel norm are continuous on this finite-dimensional set.