Motivation

Chapter 10 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) builds the calculus of differential forms in $\mathbb{R}^n$ and proves the theorem that unifies the integral theorems of vector analysis. The fundamental theorem of calculus, the Green, divergence and classical Stokes theorems all say the same thing — that integrating a derivative over a region is the same as integrating the original object over the boundary of that region — and Stokes' theorem (Theorem 10.33),

$$\int_\Psi d\omega = \int_{\partial \Psi} \omega ,$$

is that statement, once "region" is made precise as a chain of parametrized surfaces and "derivative" as the exterior derivative.

This mission is the tenth in a series formalizing Rudin Chapters 1–11; it uses the inverse function theorem and the several-variable calculus of Mission IX.

Setting

For an open $E \subseteq \mathbb{R}^n$, a $k$-surface in $E$ is a $C'$-mapping $\Phi$ from a parameter domain $D \subseteq \mathbb{R}^k$ — a $k$-cell or the standard simplex $Q^k = \{u : u_i \ge 0, \sum u_i \le 1\}$ — into $E$; surfaces are maps, not point sets. A $k$-form in $E$ is a formal sum

$$\omega = \sum a_{i_1\cdots i_k}(\mathbf{x})\,dx_{i_1}\wedge\cdots\wedge dx_{i_k}$$

with continuous coefficients, whose meaning is the rule assigning to each $k$-surface $\Phi$ the number

$$\int_\Phi \omega = \int_D \sum a_{i_1\cdots i_k}(\Phi(\mathbf{u}))\, \frac{\partial(\varphi_{i_1},\dots,\varphi_{i_k})}{\partial(u_1,\dots,u_k)}\,d\mathbf{u}.$$

The exterior derivative of $\omega$ is the $(k+1)$-form with coefficients $D_j a_I$; the pullback $\omega_T$ along a differentiable $T$ substitutes $T$ into the coefficients and the differentials. A $k$-chain is a formal integer combination of $k$-surfaces with parameter domain $Q^k$, its integral is the corresponding combination of integrals, and its boundary $\partial\Psi$ is obtained from the alternating sum $\sum_j (-1)^j$ of the faces of $Q^k$.

Formalization targets

Goal — Stokes' theorem (Theorem 10.33)

If $\Psi$ is a $k$-chain of class $C''$ in an open $V \subseteq \mathbb{R}^n$ and $\omega$ is a $(k-1)$-form of class $C'$ in $V$, then

$$\int_\Psi d\omega = \int_{\partial\Psi} \omega .$$

For $k = n = 1$ this is the fundamental theorem of calculus, for $k = n = 2$ Green's theorem, for $k = n = 3$ the divergence theorem, and for $k = 2$, $n = 3$ the theorem of Stokes.

Milestones

$$\text{the iterated integrals of a continuous function on a cell agree} \qquad (10.2)$$ $$\text{partitions of unity subordinate to an open cover of a compact set} \qquad (10.8)$$ $$\int f(\mathbf{y})\,d\mathbf{y} = \int f(T(\mathbf{x}))\,|J_T(\mathbf{x})|\,d\mathbf{x} \qquad (10.9)$$ $$d(d\omega) = 0 \qquad (10.20)$$ $$(d\omega)_T = d(\omega_T) \qquad (10.22\mathrm{c})$$ $$\int_{T\circ\Phi}\omega = \int_\Phi \omega_T \qquad (10.25)$$ $$\text{reordering the vertices of a simplex multiplies the integral by the sign} \qquad (10.27)$$ $$\text{Poincaré's lemma: on a convex open set, closed forms are exact} \qquad (10.39)$$

Significance

Stokes' theorem is the organizing theorem of multivariable analysis; its formal content is that $d$ and $\partial$ are adjoint, which is also the starting point of de Rham cohomology. Poincaré's lemma is its local converse: on a convex set the only obstruction to a closed form being exact disappears, so the failure of exactness measures the shape of the domain. The change of variables theorem (10.9) is what makes integrals independent of the parametrization and is used in the proof of Stokes itself, and partitions of unity (10.8) are the standard device for passing from local to global statements.

Mathlib has a general change-of-variables theorem for the Lebesgue integral, smooth partitions of unity, and the theory of alternating forms and de Rham differentials on manifolds; it does not have Rudin's concrete apparatus of parametrized surfaces, affine chains, and their boundaries, nor a version of Stokes' theorem for such chains. This mission builds that apparatus and states the chapter's theorems for it; the definitions are reusable for any development that wants a hands-on, coordinate-based treatment of forms.

Difficulty

This is the most demanding mission of the series, for two reasons. First, the objects have to be set up before anything can be said: forms as coefficient families, their integrals as Jacobian integrals, chains, and the boundary operator with its signs. Second, Stokes' theorem is proved by reducing to a single oriented simplex, transporting along the parametrization by Theorem 10.25, and then computing the integral over $Q^k$ by an iterated integral in which all but two terms of the boundary cancel; the cancellation is entirely a matter of getting the signs of the face maps right, and it is where a formalization will spend its time.

A further subtlety: with forms presented by coefficients indexed by all index tuples, the identity $d(d\omega) = 0$ is false coefficient-wise and true as an identity of forms. Since Rudin defines a form to be its integration functional, statements of the shape "this form vanishes" are formalized as "its integral over every surface vanishes", and that is how 10.20, 10.22(c) and 10.39 are stated here.

Formalization scope

Conventions fixed by this mission:

• Points of $\mathbb{R}^n$ are Fin n → ℝ. A $k$-form is Rudin.KForm k n, a coefficient function indexed by all tuples Fin k → Fin n, following Rudin's equation (34).
• Rudin.integralOverCell and Rudin.integralOverSimplex are Rudin's equation (35) for the two admissible parameter domains, with Rudin.jacobian the determinant of the matrix of partial derivatives. The integral over the parameter domain is the Lebesgue integral for the volume measure, which agrees with Rudin's Riemann integral for continuous integrands.
• Rudin.extDeriv and Rudin.pullback are the exterior derivative and the pullback; Rudin.Chain, Rudin.Chain.integral and Rudin.Chain.boundary are chains with integer multiplicities, their integrals, and the boundary built from the faces of the standard simplex with Rudin's signs $(-1)^j$.
• Regularity is ContDiff ℝ 1 and ContDiff ℝ 2 for Rudin's $C'$ and $C''$.
• Equalities between forms are stated as equalities of their integrals over surfaces, as explained above; the goal theorem is an equality of two real numbers, so it is not vacuous.

Contributions of the supporting differential-form identities (10.20, 10.22, 10.25) are especially welcome, since they are exactly the lemmas the goal theorem consumes.

Selected references

• Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 10 (pp. 245–299).
• Michael Spivak, Calculus on Manifolds, W. A. Benjamin, 1965.