I am reading K.Gröchenig's Introduction to Time-Frequency Analysis , Theorem 3.2.1. and the proof seems to be incorrect as it is presented.
The whole context is actually not important, but I will report it anyway. The map $$V_gf(x,\xi):=\int_{\mathbb{R}^d}f(t)\overline{g(t-x)}e^{-2\pi it\cdot \xi}dt,\qquad f,g\in L^2(\mathbb{R}^d) $$ is called the Short Time Fourier Transform (STFT) of window $g$. The theorem considered reads
Let $f_1,f_2,g_1,g_2\in L^2(\mathbb{R}^d)$. Then $V_{g_j}f_j\in L^2(\mathbb{R}^{2d})$ for $j=1,2$ and $$\left\langle V_{g_1}f_1,V_{g_2}f_2\right\rangle=\left\langle f_1,f_2\right\rangle \overline{\left\langle g_1,g_2\right\rangle}$$
The proof Gröchenig proposes is as follows. The equality above is first proved for $g_1,g_2\in (L^1\cap L^{\infty})(\mathbb{R}^d)$, which is dense in $L^2(\mathbb{R}^d)$ (this allows one to use Parseval's equality and Fubini's theorem). However, to extend the equality to $g_1,g_2\in L^2(\mathbb{R}^d)$, he proceeds as follows
With $g_1\in L^1\cap L^{\infty}$ fixed, the mapping $g_2\mapsto \left\langle V_{g_1}f_1,V_{g_2}f_2\right\rangle$ is a linear functional that coincides with $\left\langle f_1,f_2\right\rangle \overline{\left\langle g_1,g_2\right\rangle}$ on the dense subspace $L^1\cap L^{\infty}$. It is therefore bounded and extends to all $g_2\in L^2(\mathbb{R}^d)$.
Up to this point everything seems fine. But now:
In the same way, for arbitrary $f_1,f_2$ and $g_2\in L^2(\mathbb{R}^d)$, the conjugate linear functional $g_1\mapsto \left\langle V_{g_1}f_1,V_{g_2}f_2\right\rangle $ equals $\left\langle f_1,f_2\right\rangle \overline{\left\langle g_1,g_2\right\rangle}$ on $L^1\cap L^{\infty}$ and extends to all of $L^2$. The orthogonality relations are therefore established for all $f_j,g_j\in L^2(\mathbb{R}^d)$.
I believe that this proof is not correct. Reason: a priori the linear operator $g_2\mapsto \left\langle V_{g_1}f_1,V_{g_2}f_2\right\rangle$ is not bounded on $L^2(\mathbb{R}^d)$, as we do not even know if $V_{g_i}(f_i)\in L^2(\mathbb{R}^{2d})$ yet (it is part of the thesis), so the inner product might not even make sense. Therefore, even if we have extended the linear operator $g_2\mapsto \left\langle V_{g_1}f_1,V_{g_2}f_2\right\rangle$ , which is bounded on $(L^1\cap L^{\infty})(\mathbb{R}^d)$, on the whole $L^2(\mathbb{R}^d)$, the resulting operator will not necessarily be still given by the expression $g_2\mapsto \left\langle V_{g_1}f_1,V_{g_2}f_2\right\rangle$. A priori, the operator $g_2\mapsto \left\langle V_{g_1}f_1,V_{g_2}f_2\right\rangle$ is unbounded on $L^2(\mathbb{R}^d)$ (despite being bounded on $(L^1\cap L^{\infty})(\mathbb{R}^d)$) and the extension we have just found is different - they only agree on $(L^1\cap L^{\infty})(\mathbb{R}^d)$. Hence we cannot deduce that the equality we are looking to prove is preserved by the extension.
What do you think, MSE?
You are completely right that the given proof is not completely correct.
However, it can be salvaged by the following additional argument: In the following, I will use the notations $L_x f (y) = f(y-x)$ and $M_\xi f (x) = e^{2\pi i \langle x, \xi \rangle} f(x)$ for the translation and modulation of the function $f$, respectively. With this notation, you have $$ V_g f (x,\xi) = \langle f, M_\xi L_x g \rangle \, , $$ which is (for fixed $x,\xi$) jointly continuous as a function of $f,g \in L^2 (\mathbb{R})$. This uses that $M_\xi : L^2 \to L^2$ and $L_x : L^2 \to L^2$ are continuous (in fact isometric) linear maps.
Thus, even though we do not know yet that $V_g f \in L^2$, and in particular not that $(f,g) \mapsto V_g f$ is continuous as a map of $L^2 \times L^2$ into $L^2$, we know that the pointwise evaluations of the short time Fourier transform are continuous as functions of $f,g \in L^2$.
This is useful as follows: On a dense subset of $L^2$, you know that $\langle V_{g_1} f_1 , V_{g_2} f_2 \rangle = \langle f_1, f_2 \rangle \langle g_2, g_1 \rangle$. But this implies in particular that $\|V_g f \|_{L^2} = \|f\|_{L^2} \|g\|_{L^2}$ for $f,g$ in this dense subspace.
Now, let $f,g \in L^2$ be arbitrary, and choose sequences $f_n, g_n$ from the dense subspace that converge to $f,g$, respectively. As we saw above, this implies $V_{g_n} f_n \to V_g f$ pointwise. Using Fatou's Lemma, this easily implies $$ \|V_g f \|_{L^2} \leq \liminf_{n \to \infty} \|V_{g_n} f_n\|_{L^2} = \liminf_n \|f_n\|_{L^2} \|g_n\|_{L^2} = \|f\|_{L^2} \|g\|_{L^2} \, . \tag{$\ast$} $$ In particular, $V_g f \in L^2 (\Bbb{R}^{2n})$. Note that this holds for arbitrary $f,g \in L^2$.
Finally, it is not hard to see that the estimate $(\ast)$ implies that $L^2 \times L^2 \to L^2, (f,g) \mapsto V_g f$ is a continuous sesquilinear map. Indeed, if $f_n \to f$ and $g_n \to g$, then \begin{align*} \| V_{g_n} f_n - V_g f\|_{L^2} & \leq \|V_{g_n} f_n - V_{g_n} f\|_{L^2} + \|V_{g_n} f - V_{g} f\|_{L^2} \\ & \leq \|g_n\|_{L^2} \cdot \|f_n - f\|_{L^2} + \|f\|_{L^2} \cdot \|g_n - g\|_{L^2} \to 0 \, . \end{align*}
Finally, since you now know that the map $(f,g) \mapsto V_g f$ is continuous as a map of $L^2 \times L^2$ into $L^2$, and since you know that the identity to be proved holds on a dense subset (where the right-hand side is also continuous), the desired identity holds for all $f_1,f_2, g_1, g_2 \in L^2$.