Let $\mathcal{H}\_A\otimes\mathcal{H}\_B$ be a finite-dimensional bipartite Hilbert space, $P\_A$ a positive semi-definite operator on $\mathcal{H}\_A$, $P\_B$ a positive semi-definite operator on $\mathcal{H}\_B$, and $U\_{AB}$ a unitary operator on $\mathcal{H}\_A\otimes\mathcal{H}\_B$. In some roundabout way involving integrals over the unitary group it seems I can prove the following inequality:
$$\mathrm{tr}\_A\left(\mathrm{tr}\_B((P\_A\otimes P\_B)U\_{AB})\mathrm{tr}\_B((P\_A\otimes P\_B)U\_{AB}^\dagger)\right)\leq\mathrm{tr}(P\_A^2)\mathrm{tr}(P\_B)^2.$$
I have been unable to find a more ``conventional'' proof of this inequality, e.g. using von Neumann's trace inequality or Holder's inequality, so I am curious if this is a known result or if someone can provide a proof which uses only linear algebra.



Proving a bipartite trace inequality?
You can rewrite the left-hand side $\mathrm{tr}\_A\left(P\_AX P\_AX^\*\right)$,
where $X=\mathrm{tr}\_B((1\otimes P\_B)U\_{AB})$. By Hölder's inequality this is less than $\|P\_A\|\_2^2 \|X\|\_\infty^2$, so your inequality is just that $\|X\|\_\infty \leq \mathrm{tr}(P\_B)$, which is certainly "conventional". For a justification use Hölder's inequality to obtain $\mathrm{tr}\_A(CX) = \mathrm{tr}((C\otimes P\_B) U\_{AB}) \leq \|C\otimes P\_B\|\_1 = \|C\|\_1 \mathrm{tr}(P\_B)$, so this conventional inequality follows by taking the supremum over all $C$ with $\|C\|\_1 =1$.


