Plancherel theorem

View Schwartz functions as a normed subspace of $L^2$: a continuous function vanishing a.e. vanishes everywhere, since any nonzero value persists on a positive-volume box. Thus the association with its class is injective. By [F1], Fourier is a bounded linear isometry on this dense subspace, and [F5] makes the target Banach. [F4] and [F2] give a unique bounded linear extension ${\mathcal{F}}_2$. For each fixed $f$, countable choice selects a sequence $u_k\in \mathcal{S}$ with $\mathrm{\parallel }{u}_k-f{\mathrm{\parallel }}_2<1\mathrm{/}(k+1)$ for $k\in \mathbb{N}$; its Fourier images converge to ${\mathcal{F}}_{2}f$. The isometry on the subspace gives $\mathrm{\parallel }{\mathcal{F}}_{2}f{\mathrm{\parallel }}_2={\lim }_k\mathrm{\parallel }{\widehat{u}}_k{\mathrm{\parallel }}_2={\lim }_k\mathrm{\parallel }{u}_k{\mathrm{\parallel }}_2=\mathrm{\parallel }f{\mathrm{\parallel }}_2$. Independence of the sequence follows also from $\mathrm{\parallel }{\widehat{u}}_k-{\widehat{v}}_k{\mathrm{\parallel }}_2=\mathrm{\parallel }{u}_k-v_k{\mathrm{\parallel }}_2\to 0$.

For any $g\in L^2$, [F2] and countable choice give $v_k\in \mathcal{S}$ tending to $g$. By [F3], define the uniquely determined $u_k={\mathcal{F}}^{-1}{v}_k\in \mathcal{S}$. By [F1], $\mathrm{\parallel }{u}_k-u_l{\mathrm{\parallel }}_2=\mathrm{\parallel }{v}_k-v_l{\mathrm{\parallel }}_2$, so [F5] gives a limit $u\in L^2$. Continuity of the extension in step 1.1 gives ${\mathcal{F}}_{2}u={\lim }_k{v}_k=g$. Thus the extension is surjective.

For approximants $u_k\to f$, $v_k\to g$, Cauchy–Schwarz in [F5] bounds $\mathrm{\mid }⟨u_k,v_k⟩-⟨f,g⟩\mathrm{\mid }$ by $\mathrm{\parallel }{u}_k-f{\mathrm{\parallel }}_2\mathrm{\parallel }{v}_k{\mathrm{\parallel }}_2+\mathrm{\parallel }f{\mathrm{\parallel }}_2\mathrm{\parallel }{v}_k-g{\mathrm{\parallel }}_2\to 0$, since a convergent sequence is norm bounded. Apply the same estimate to their transform images and pass to the limit in [F1]. This proves pairing preservation. Steps 1.1 and 2.1 give the remaining unitary properties. Countable choice was used only in the cited interfaces and to select countable approximation sequences for each fixed input; no simultaneous arbitrary-index selection or Hilbert basis is needed.