Single-copy Werner filtering normalization bound (source code)

= Single-copy Werner filtering normalization bound
{title2=$p=\operatorname{Tr}[W_F(A^\dagger A\otimes B^\dagger B)]\geq|\det A\det B|$}

Write $W_F=(I\otimes I-w\sum_j\sigma_j\otimes\sigma_j)/4$, with $w=(4F-1)/3\in(1/3,1]$. For positive matrices $X=A^\dagger A=a_0I+a\cdot\sigma$ and $Y=B^\dagger B=b_0I+b\cdot\sigma$, the success probability is $p=a_0b_0-w a\cdot b$. It is at least $a_0b_0-|a||b|\geq\sqrt{(a_0^2-|a|^2)(b_0^2-|b|^2)}=|\det A\det B|$. Squaring the middle comparison leaves $(a_0|b|-b_0|a|)^2\geq0$.