Motivation

Chapter 8 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) puts the general theory of the preceding chapters to work on concrete functions. Power series are differentiated term by term; the exponential function is defined by its series and the trigonometric functions and the number $\pi$ are extracted from it; the fundamental theorem of algebra is proved; Fourier series are introduced through general orthonormal systems; and the Gamma function is characterized by log-convexity.

The chapter's capstone is Parseval's theorem (Theorem 8.16): for Riemann-integrable $2\pi$-periodic functions, the Fourier series converges in the mean square sense and the $L^2$ inner product is computed by the (absolutely convergent) sum of products of Fourier coefficients. It is the statement that the trigonometric system is not merely orthonormal but complete, and it is the finite-dimensional Pythagorean theorem carried to infinite dimensions.

This mission is the eighth in a series formalizing Rudin Chapters 1–11; it uses the convergence tests of Mission III and the uniform-convergence and approximation theorems of Mission VII, and it is the analytic counterpart of the abstract $L^2$ theory of Mission XI.

Setting

A power series is $\sum c_n x^n$; by Chapter 3 it converges on an interval $(-R,R)$. A sequence $\{\varphi_n\}$ of complex functions on $[a,b]$ is an orthonormal system if $\int_a^b \varphi_n \overline{\varphi_m} = 0$ for $n \ne m$ and $\int_a^b |\varphi_n|^2 = 1$; the Fourier coefficients of $f$ relative to it are $c_n = \int_a^b f \overline{\varphi_n}$, and the Fourier series is $\sum c_n \varphi_n$. For the trigonometric system on $[-\pi,\pi]$ one writes

$$c_n = \frac{1}{2\pi}\int_{-\pi}^{\pi} f(x)e^{-inx}\,dx, \qquad s_N(f;x) = \sum_{n=-N}^{N} c_n e^{inx}, \qquad \|h\|_2 = \Big(\frac{1}{2\pi}\int_{-\pi}^{\pi}|h|^2\Big)^{1/2}.$$

A trigonometric polynomial is a finite sum $\sum_{n=-N}^{N} c_n e^{inx}$. The Gamma function is $\Gamma(x) = \int_0^\infty t^{x-1}e^{-t}\,dt$ for $x > 0$.

Formalization targets

Goal — Parseval's theorem (Theorem 8.16)

For Riemann-integrable $2\pi$-periodic $f$ and $g$ with Fourier coefficients $c_n$ and $\gamma_n$:

$$\lim_{N\to\infty}\|f - s_N(f)\|_2 = 0, \qquad \frac{1}{2\pi}\int_{-\pi}^{\pi} f\bar g = \sum_{n=-\infty}^{\infty} c_n \overline{\gamma_n}, \qquad \frac{1}{2\pi}\int_{-\pi}^{\pi} |f|^2 = \sum_{n=-\infty}^{\infty} |c_n|^2 .$$

Milestones

$$\text{term-by-term differentiation of a power series} \qquad (8.1)$$ $$\textstyle\sum c_n = C \Rightarrow \sum c_n x^n \to C \text{ as } x \to 1^- \qquad (8.2)$$ $$\text{interchange of the order of summation in a double series} \qquad (8.3)$$ $$\text{two power series agreeing on a set with a limit point have equal coefficients} \qquad (8.5)$$ $$E(z+w) = E(z)E(w),\ E' = E,\ \text{growth of } E \qquad (8.6)$$ $$\cos(\pi/2) = 0,\ \cos > 0 \text{ on } [0,\pi/2),\ e^{z+2\pi i} = e^z,\ |z| = 1 \Rightarrow z = e^{it} \qquad (8.7)$$ $$\text{every nonconstant complex polynomial has a root} \qquad (8.8)$$ $$\text{Fourier partial sums minimize the mean square error; Bessel's inequality} \qquad (8.11,\ 8.12)$$ $$\text{a local Lipschitz condition at } x \text{ forces } s_N(f;x) \to f(x) \qquad (8.14)$$ $$\text{trigonometric polynomials approximate continuous periodic functions uniformly} \qquad (8.15)$$ $$\Gamma(x+1) = x\Gamma(x),\ \Gamma(n+1) = n!,\ \log\Gamma \text{ convex} \qquad (8.18)$$ $$\text{Bohr–Mollerup: these three properties characterize } \Gamma \qquad (8.19)$$

Significance

Parseval's theorem is the completeness statement for the trigonometric system: Bessel's inequality (8.12) holds for every orthonormal system, and equality for all $f$ is exactly what distinguishes a complete system. The proof shows how the pieces of the book fit together: it uses the approximation theorem 8.15 (itself a corollary of Stone–Weierstrass from Chapter 7), the minimizing property 8.11, and the Schwarz inequality of Chapter 1. Chapter 11 generalizes the conclusion to arbitrary complete orthonormal systems in $L^2$, where the Riemann-integrable hypothesis can be dropped.

The other milestones are where the elementary functions acquire their properties: the $2\pi$-periodicity of the complex exponential, the definition of $\pi$ as twice the first positive zero of the cosine, and the log-convexity characterization of the Gamma function are all established here rather than assumed.

Mathlib has the exponential and trigonometric functions, $\pi$, the fundamental theorem of algebra, the Gamma function with the Bohr–Mollerup theorem, and a Fourier theory on the additive circle. The work in this mission is to state Rudin's versions — $2\pi$-periodic functions on $\mathbb{R}$, generic orthonormal systems on an interval, Riemann-integrable rather than square-integrable hypotheses — and connect them to that library.

Difficulty

Parseval's theorem is where an approximation argument in the uniform norm has to be converted into one in the mean square norm. The chain is: approximate $f$ in $\|\cdot\|_2$ by a continuous periodic $h$ (a nontrivial step for a merely Riemann-integrable $f$, and the place where the hypothesis is really used), approximate $h$ uniformly by a trigonometric polynomial $P$, and then use the minimizing property of the partial sums to conclude $\|f - s_N(f)\|_2$ is small. The first step has no analogue in the uniform theory and is the main obstacle; the third depends on $s_N$ being an orthogonal projection, which is Theorem 8.11.

Formalization scope

Conventions fixed by this mission:

• Integrals of complex-valued functions use Mathlib's interval integral ∫ x in a..b, f x, not the real-valued Riemann–Stieltjes integral built in Mission VI; for the Riemann-integrable integrands of this chapter the two agree. Integrability hypotheses are stated as IntervalIntegrable.
• Fourier notions are Rudin.fourierCoeff, Rudin.fourierPartialSum, Rudin.L2Norm, Rudin.IsTrigPolynomial, Rudin.HasPeriodTwoPi, and, for general systems, Rudin.IsOrthonormalSystem and Rudin.genFourierCoeff, all following Rudin's normalizations (in particular the $1/2\pi$ in $c_n$ and in $\|\cdot\|_2$).
• Series of real numbers use Rudin.SeriesConvergesTo from Mission III, so that conditional convergence is expressible; the two-sided sums $\sum_{n=-\infty}^{\infty}$ of Parseval are stated as limits of the symmetric partial sums $\sum_{|n| \le N}$, as in Rudin.
• $\exp$, $\cos$, $\pi$ and $\Gamma$ are Mathlib's; Theorem 8.7 is therefore stated as the list of properties Rudin derives, not as a redefinition of $\pi$.

Selected references

• Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 8 (pp. 172–201).
• P. J. Davis, Leonhard Euler's integral: A historical profile of the Gamma function, American Mathematical Monthly 66 (1959), 849–869. https://doi.org/10.2307/2309786