Lemma: Page–Sen input

A Haar pure state on ${\mathbb{C}}^r\otimes {\mathbb{C}}^b$ has mean reduction entropy $\mathsf{P}(r,b)$.

Proof. The Gaussian–Wishart evaluation in Appendix app:page gives (eq:PageMean). This is the established Page–Sen formula PageAverage,Sen.