# Derive Parseval's theorem in one dimension

Parseval's theorem (in one dimension) is a fundamental result in the theory of Fourier transforms. If $$f(t) \Leftrightarrow F(\omega )$$ are Fourier transform pairs and $$t$$ (time) and $$\omega$$ (angular frequency) are conjugate variables, Parseval's Theorem states (up to a constant of proportionality):

$$\int\limits_{t= - \infty}^\infty |f(t)|^2\ dt = \int\limits_{\omega = -\infty}^\infty |F(\omega )|^2\ d \omega$$

Here both $$f(t)$$ and $$F(\omega )$$ can be complex-valued, and $$| \cdot |$$ denotes the absolute value, and thus $$| \cdot |^2$$ is real-valued.

It is fairly straightforward to verify Parseval's theorem with the specific case of chosen functions, e.g., $$f(t) = e^{-t^2} \cos t$$, using FourierTransform and Conjugate.

My question is instead: How can one most elegantly and efficiently derive the theorem using the symbol-manipulation power of Mathematica?

The following is my trial for automating the manual deduction here. You can press Ctrl+Shift+t to transform the output to TraditionalForm to make it look good.

With[{int = Inactive[Integrate]},

ftformula[f_] := ℱ[f][ω_] :> int[f[t] Exp[I ω t], {t, -∞, ∞}]/Sqrt[2 π];

moveconj = Conjugate[int[expr_, tlst : {_, -∞, ∞}]] :> int[Conjugate[expr], tlst];

mergecoef = int[expr_, {t_, b__}] coef_ /; FreeQ[coef, t] :> int[expr coef, {t, b}];

exchange = int[int[expr_, tlst_], ωlst_] :> int[int[expr, ωlst], tlst];

extractcoef = int[coef_ expr_, {ω_, b__}] /; FreeQ[coef, ω] :> coef int[expr, {ω, b}];

ift = int[ℱ[f_][ω] E^(-I t_ ω), {ω, -∞, ∞}] :> Sqrt[2 π] f[t];

step[1] = int[ℱ[f][ω] Conjugate[ℱ[g][ω]], {ω, -∞, ∞}]]


step@2 = step@1 /. ftformula[g]
(* There's a bug in TraditionalForm of Conjugate@Inactive[Integrate][…]. *)
(* To make the conjugate of integral display properly, use Activate. *)


step@3 = Simplify[step@2 /. moveconj, {t, ω} ∈ Reals]


step@4 = step@3 /. mergecoef


step@5 = step@4 /. exchange


step@6 = step@5 //. extractcoef


step@7 = step@6 /. ift /. extractcoef


So we manage to deduce

$$\int _{-\infty }^{\infty }(\mathcal{F}(g)(\omega ))^* \mathcal{F}(f)(\omega )d\omega =\int _{-\infty }^{\infty }g(t)^* f(t)dt$$

where $$\mathcal{F}(f)$$ denotes Fourier transform of $$f$$. Identity in the question is a special case of this identity, because

$$|f(t)|^2=f(t) f(t)^*$$

I admit the procedure still heavily depends on manual analysis so it's not quite satisfactory, but at least it illustrates the deduction without ambiguity.

• Thanks ($+1$)... Let's wait to see if a more elegant solution arrives. Commented Apr 12, 2023 at 16:21