Theorem 10.33 — Stokes' theorem

Proved

Rudin.ch10_stokes

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

analysisdifferential-formsgeometry

If $\Psi$ is a $k$ -chain of class $C''$ in an open set $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$ . Special cases are the fundamental theorem of calculus, Green's theorem, the divergence theorem and the classical theorem of Stokes.

Preamble

import Mathlib
import Definitions.Def_Rudin_ch10_forms

open Filter Topology MeasureTheory

Formal statement

namespace Rudin

/-- Rudin, Theorem 10.33 (Stokes' theorem): if `Ψ` is a `(m+1)`-chain of class `C''` in an open
set `V ⊆ ℝⁿ` and `ω` is an `m`-form of class `C'` in `V`, then the integral of `dω` over
`Ψ` equals the integral of `ω` over the boundary `∂Ψ`. -/
theorem ch10_stokes (m n : ℕ) (V : Set (Fin n → ℝ)) (hV : IsOpen V) (Ψ : Chain (m + 1) n)
    (hΨ : ∀ t ∈ Ψ.terms, ContDiff ℝ 2 t.2.map ∧ ∀ u ∈ stdSimplex (m + 1), t.2.map u ∈ V)
    (ω : KForm m n) (hω : ∀ i, ContDiffOn ℝ 1 (ω.coeff i) V) :
    Chain.integral (extDeriv ω) Ψ = Chain.integral ω Ψ.boundary := by sorry

end Rudin

Source

Walter Rudin, Principles of Mathematical Analysis, 3rd edition, McGraw-Hill, 1976, Chapter 10, p. 272, Theorem 10.33

Read-back

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

Let $m,n \in \mathbb{N}$ and let $V \subseteq \mathbb{R}^n$ be open. Let $\Psi$ be an $(m+1)$ -chain: a finite list of pairs (integer multiplicity, simplex $(m+1)$ -surface). Assume that for every term $(c,\Phi)$ in the list, the map $\Phi$ is twice continuously differentiable on all of $\mathbb{R}^{m+1}$ and sends every point of the standard simplex $Q^{m+1}$ into $V$ . Let $\omega$ be an $m$ -form in $\mathbb{R}^n$ whose coefficient functions are all continuously differentiable of order $1$ on $V$ . Then

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

Explicitly, the left side is $\sum_{(c,\Phi) \in \Psi} c \int_{Q^{m+1}} \sum_{i} (d\omega)_i(\Phi(u))\,J_i\Phi(u)\,du$ , and the right side is the analogous sum over the boundary chain $\partial\Psi$ , whose terms are, for each term $(c,\Phi)$ of $\Psi$ and each $j = 0,\dots,m+1$ , the pair $\bigl(c\,(-1)^j,\ \Phi \circ (\text{the } j\text{-th face map of } Q^{m+1})\bigr)$ , integrated over $Q^{m}$ .

The statement is an equality of two real numbers for the given chain and form; no orientation or regularity condition beyond those listed is imposed, and the case where the chain has no terms gives $0 = 0$ .

Human review

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

View graph