Solution (source code)

= Solution

Use $\widehat f(t)=\int f(x)e^{-itx}\,dx$ and its extension to <square-integrable functions>. For $T_kf(x)=f(x+k)$, changing variables gives $\widehat{T_kf}(t)=e^{ikt}\widehat f(t)$. The <Plancherel theorem> therefore gives
$$
\int_{\mathbb R}f(x+k)\overline{f(x+l)}\,dx=\frac1{2\pi}\int_{\mathbb R}|\widehat f(t)|^2e^{i(k-l)t}\,dt.
$$
For an arbitrary square-integrable $f$, the translation identity follows by approximation by integrable square-integrable functions: translations are isometries in $L^2$ and the <Fourier transform> is continuous in the Plancherel <norm>. The <Cauchy-Schwarz inequality> makes the product on the left integrable, and $|\widehat f|^2$ is integrable on the right.

Put $m=l-k$. Every unequal integer pair gives a nonzero integer $m$, and every nonzero integer arises, for example with $k=0,l=m$. The identity thus proves \b[both directions of the requested equivalence]. It is the <orthogonality of integer translates> criterion. A different Fourier normalization changes only the nonzero constant factor, not the vanishing conditions.