Theorem 8.16 — Parseval's theorem

Proved

Rudin.ch08_parseval

by Lucas · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisfourier-analysis

Let $f$ and $g$ be Riemann-integrable $2\pi$ -periodic functions with Fourier coefficients $c_n$ and $\gamma_n$ . Then $\|f - s_N(f)\|_2 \to 0$ ; $\frac{1}{2\pi}\int_{-\pi}^{\pi} f\bar g = \sum_n c_n\overline{\gamma_n}$ ; and, taking $g = f$ , $\frac{1}{2\pi}\int_{-\pi}^{\pi}|f|^2 = \sum_n |c_n|^2$ . The two-sided sums are the limits of the symmetric partial sums $\sum_{|n| \le N}$ .

Preamble

import Mathlib
import Definitions.Def_Rudin_ch08_fourier

open Filter Topology

Formal statement

namespace Rudin

/-- Rudin, Theorem 8.16 (Parseval's theorem): for Riemann-integrable `2π`-periodic functions
`f` and `g` with Fourier coefficients `cₙ` and `γₙ`, the Fourier series of `f` converges to
`f` in the mean square sense, the inner products agree with the sum of `cₙ conj γₙ`, and
`(1/2π) ∫ |f|² = ∑ |cₙ|²`. -/
theorem ch08_parseval (f g : ℝ → ℂ) (hfper : HasPeriodTwoPi f) (hgper : HasPeriodTwoPi g)
    (hf : IntervalIntegrable f MeasureTheory.volume (-Real.pi) Real.pi)
    (hg : IntervalIntegrable g MeasureTheory.volume (-Real.pi) Real.pi)
    (hf2 : IntervalIntegrable (fun x => ‖f x‖ ^ 2) MeasureTheory.volume (-Real.pi) Real.pi)
    (hg2 : IntervalIntegrable (fun x => ‖g x‖ ^ 2) MeasureTheory.volume (-Real.pi) Real.pi) :
    Tendsto (fun N => L2Norm (fun x => f x - fourierPartialSum f N x)) atTop (𝓝 0) ∧
    Tendsto (fun N => ∑ n ∈ Finset.Icc (-(N : ℤ)) (N : ℤ),
        fourierCoeff f n * (starRingEnd ℂ) (fourierCoeff g n)) atTop
      (𝓝 ((1 / (2 * Real.pi) : ℂ) *
        ∫ x in (-Real.pi)..Real.pi, f x * (starRingEnd ℂ) (g x))) ∧
    Tendsto (fun N => ∑ n ∈ Finset.Icc (-(N : ℤ)) (N : ℤ), ‖fourierCoeff f n‖ ^ 2) atTop
      (𝓝 ((1 / (2 * Real.pi)) * ∫ x in (-Real.pi)..Real.pi, ‖f x‖ ^ 2)) := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 8, p. 191, Theorem 8.16

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Let $f, g : \mathbb{R}\to\mathbb{C}$ satisfy $f(x+2\pi)=f(x)$ and $g(x+2\pi)=g(x)$ for all real $x$ , and assume that $f$ , $g$ , $\lVert f\rVert^2$ and $\lVert g\rVert^2$ are each interval-integrable on $[-\pi,\pi]$ with respect to Lebesgue measure. Write

\hat f(n) = \frac{1}{2\pi}\int_{-\pi}^{\pi} f(x)e^{-inx}dx, \qquad s_N(f;x)=\sum_{n=-N}^{N}\hat f(n)e^{inx}, \qquad \lVert h\rVert_2 = \sqrt{\frac{1}{2\pi}\int_{-\pi}^{\pi}\lVert h\rVert^2},

and similarly $\hat g(n)$ . Then three assertions hold simultaneously as $N \to \infty$ :

Mean-square convergence. $\lVert f - s_N(f;\cdot)\rVert_2 \to 0$ .
Polarized identity. $\displaystyle \sum_{n=-N}^{N} \hat f(n)\,\overline{\hat g(n)} \;\longrightarrow\; \frac{1}{2\pi}\int_{-\pi}^{\pi} f(x)\overline{g(x)}\,dx$ .
Parseval identity. $\displaystyle \sum_{n=-N}^{N} \lVert \hat f(n)\rVert^{2} \;\longrightarrow\; \frac{1}{2\pi}\int_{-\pi}^{\pi} \lVert f(x)\rVert^{2}dx$ .

All three concern the symmetric partial sums over $-N \le n \le N$ ; items 2 and 3 are stated as limits of those finite sums rather than as unconditional sums over $\mathbb{Z}$ . The square root in $\lVert\cdot\rVert_2$ returns $0$ on negative arguments, and integrability of the product $f\overline{g}$ is not assumed separately.

Human review

Endorsed by Shuze Chen · Sep 13, 2026
Endorsed by Lucas · Sep 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph