Mixed-point norm identity for alternating updates (source code)

= Mixed-point norm identity for alternating updates
{title2=$\|(p-\tau a,q)\|^2-\|(p,q+\tau b)\|^2$}

For two mixed points with difference $(p,q)$ and gradient difference $(a,b)$, the input difference is $(p,q+\tau b)$ and the output difference is $(p-\tau a,q)$. Their squared-norm difference is $-2\tau(\langle p,a\rangle+\langle q,b\rangle)+\tau^2(\|a\|^2-\|b\|^2)$. This exact identity is a reusable way to prove averagedness without assuming the two block maps are individually nonexpansive.