Lindemann–Weierstrass I: Exponential IndependenceResearch Paper
## Motivation
The exponential function turns addition into multiplication. When its inputs are algebraic numbers, that elementary identity meets a rigid arithmetic boundary: distinct algebraic exponents cannot produce an algebraic linear relation among their exponentials. This principle is the **Lindemann–Weierstrass theorem**, one of the central results of transcendence theory. Its familiar consequences include the transcendence of Euler's number $e$ and of $\pi$, and therefore the impossibility of squaring the circle with straightedge and compass.
The historical line runs from Hermite's 1873 proof that $e$ is transcendental, through Lindemann's 1882 proof that $\pi$ is transcendental, to Weierstrass's general formulation in 1885. Modern algebraic presentations organize the theorem around conjugates, Galois symmetry, algebraic integers, and an auxiliary-polynomial estimate. The Lean development formalized here follows Yuyang Zhao's mathlib contribution [PR #28013](https://github.com/leanprover-community/mathlib4/pull/28013), whose mathematical reference is Jacobson's *Basic Algebra I*, §4.12, Theorem 4.22.
## Setting
A complex number is **algebraic** if it is a root of a nonzero polynomial with rational, equivalently integer, coefficients. A complex number is **transcendental** if it is not algebraic. Write $\overline{\mathbb Q}\subset\mathbb C$ for the field of algebraic complex numbers and $\exp(z)=e^z$ for the complex exponential.
For a family $(u_i)_{i\in I}$ in $\overline{\mathbb Q}$, injectivity means that distinct indices carry distinct exponents. A family $(x_i)$ is linearly independent over $\overline{\mathbb Q}$ when every finite relation $\sum_i a_i x_i=0$ with algebraic coefficients has all $a_i=0$. It is algebraically independent over $\overline{\mathbb Q}$ when no nonzero multivariate polynomial with algebraic coefficients vanishes on the family.
The strongest target uses natural-number linear independence of $(u_i)$: distinct finitely supported tuples of natural coefficients give distinct sums $\sum_i n_i u_i$. This is exactly the condition needed to distinguish the exponent attached to every monomial.
## Formalization targets
### Exponential linear independence
For every injective algebraic family $(u_i)$,
$$
\{e^{u_i}:i\in I\}\text{ is linearly independent over }\overline{\mathbb Q}.
$$
This includes the finite Lindemann–Weierstrass relation as its load-bearing finite core.
### Hermite–Lindemann and classical constants
For every nonzero algebraic $a\in\mathbb C$,
$$
e^a\text{ is transcendental}.
$$
The same development records the transcendence of $e$, the transcendence of $\pi$, and the transcendence of every nonzero principal logarithm of an algebraic complex number.
### Integer winding consumer
Let $\alpha\ne0$ be algebraic and let $w:I\to\mathbb Z$ be injective. The proved Hermite–Lindemann theorem discharges the formerly conditional winding interface and gives
$$
\bigl(e^{i\alpha w(j)}\bigr)_{j\in I}\text{ linearly independent over }\overline{\mathbb Q}.
$$
The integer labels are inputs to this arithmetic theorem. A separate topological or dynamical development is responsible for producing them as winding numbers.
### Algebraic independence capstone
If $(u_i)$ is a natural-number-linearly-independent family in $\overline{\mathbb Q}$, then
$$
\{e^{u_i}:i\in I\}\text{ is algebraically independent over }\overline{\mathbb Q}.
$$
This is the mission's capstone because it turns the linear theorem into a reusable multivariate interface: polynomial monomials become exponentials of distinct natural combinations.
## Significance
The theorem separates two kinds of structure that otherwise coexist in the exponential map. The character law $e^{x+y}=e^xe^y$ supplies exact multiplicative relations, but the theorem rules out unintended linear relations over algebraic coefficients. For integer winding consumers, one algebraic nonzero generator $a$ produces the two-sided phase family $(e^{na})_{n\in\mathbb Z}$; after a Laurent-polynomial shift, the theorem makes distinct integer labels linearly independent over $\overline{\mathbb Q}$. Winding supplies the discrete labels, while transcendence supplies arithmetic distinguishability.
The formalization contributes more than the named corollaries. It exposes a finite exponential-relation theorem, the algebraic orbit-sum reduction used by it, and general infinite-family interfaces. These components can be reused in later work on exponential polynomials, logarithms of algebraic numbers, and arithmetic representations of topological charges.
This mission formalizes a known theorem; it is not presented as an open mathematical problem. The private theorem graph is already machine-checked against Lean 4.30 and Mathlib revision `c5ea00351c28e24afc9f0f84379aa41082b1188f`. The mission records that proof as an independently inspectable dependency graph before any later upstream integration.
## Difficulty
The analytic approximation alone is insufficient. It produces a small complex error, but smallness does not imply vanishing, and taking a field norm does not repair the gap because the other embeddings have no corresponding analytic bound. Likewise, a field automorphism of $\overline{\mathbb Q}$ cannot be moved through the complex exponential as an algebraic operation.
The formal statement therefore requires both an analytic and an arithmetic layer. The arithmetic layer must replace a hypothetical algebraic relation by a Galois-stable relation with integer data and a genuinely nonzero integer contribution. The analytic layer must then make the absolute value of that integer strictly less than one. Managing conjugacy classes, root multisets, denominator clearing, finite supports, and the asymptotic prime choice in one kernel-checked chain is the central formalization difficulty.
## Formalization scope
The development is pinned to Lean 4.30 and Mathlib revision `c5ea00351c28e24afc9f0f84379aa41082b1188f`. Algebraic complex numbers are represented by `integralClosure ℚ ℂ`; transcendence corollaries are stated with `Transcendental ℤ`, which is equivalent to the usual absence of a nonzero integer polynomial relation. The finite theorem uses `Fintype`; the general linear and algebraic independence theorems permit arbitrary universe-zero index types and reduce relations to finite support internally.
The auxiliary algebraic theorem is stated over an arbitrary algebraically closed field over $\mathbb Q$ and a multiplicative character on its additive group. The analytic consumer specializes this character to the complex exponential. Two small support modules provide quotient lifting for finitely supported functions and evaluation identities for symmetric multivariate polynomials.
The condition $a\ne0$ in Hermite–Lindemann is load-bearing: $e^0=1$ is algebraic. Injectivity of the exponent family is load-bearing for linear independence: duplicate exponents duplicate vectors. The capstone's natural-number linear independence is not algebraic independence of the exponents and must not be silently strengthened or weakened.
The source is an attributed, compatibility-preserving port of the May 2026 Lean 4.30 snapshot of mathlib PR #28013. Platform packaging uses the conservative ASCII rename `linearIndependent_exp_finite` for the upstream private helper and `phi` for one Greek binder. The elaborated theorem types were compared against the upstream source; these are naming changes only.
## Selected references
- Yuyang Zhao, *The Lindemann–Weierstrass theorem*, mathlib4 PR #28013, 2022–2026. https://github.com/leanprover-community/mathlib4/pull/28013
- Nathan Jacobson, *Basic Algebra I*, 2nd edition, W. H. Freeman, 1985, §4.12, Theorem 4.22.
- Mathlib contributors, *AnalyticalPart: the analytic estimate for Lindemann–Weierstrass*. https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/Transcendental/Lindemann/AnalyticalPart.html
12 thms1 active userReviewed
🏆Completed
Captain: abcdefg
Weighted Root Integral Identity for Ordered Positive RealsTextbook
## Motivation
Chapter 11 of Walter Rudin's *Principles of Mathematical Analysis* (3rd edition, McGraw-Hill,
1976) replaces the Riemann integral of Chapter 6 with the **Lebesgue integral**, and the reward
is a theory of integration whose limit theorems have no superfluous hypotheses and whose space
of square-integrable functions is complete. The chapter runs from set functions and outer
measures, through the Carathéodory construction of Lebesgue measure, measurable functions and
the integral, to the convergence theorems (monotone convergence, Fatou, dominated convergence)
and finally to the space $\mathscr{L}^2(\mu)$ and the **Riesz–Fischer theorem** (Theorem 11.42):
$$\text{every Cauchy sequence in } \mathscr{L}^2(\mu) \text{ converges in the mean to an element of } \mathscr{L}^2(\mu).$$
That completeness is what makes $\mathscr{L}^2$ a Hilbert space, and it is the reason the
Fourier series of Chapter 8 converge in the mean to the functions they represent.
This mission is the eleventh and last in a series formalizing Rudin Chapters 1–11. It uses the
Riemann–Stieltjes integral of Mission VI (for Theorem 11.33, comparing the two integrals) and
the trigonometric Fourier series of Mission VIII (for the $\mathscr{L}^2$ reading of Parseval's
theorem).
## Setting
A **set function** on a ring $\mathscr{R}$ of sets is *countably additive* if it takes the value
$\sum \phi(A_n)$ on a countable disjoint union. Rudin constructs an **outer measure** $\mu^*$
from such a $\phi$ by covering with elementary sets and taking an infimum, calls a set
**measurable** when it is approximable by elementary sets in the metric $d(A, B) = \mu^*(A
\triangle B)$, and proves that the measurable sets form a $\sigma$-algebra on which $\mu^*$ is
countably additive (Theorem 11.10). A real function $f$ is **measurable** when $\{x : f(x) > a\}$
is measurable for every $a$, and the integral $\int_E f\,d\mu$ is defined first for simple
functions, then for nonnegative measurable functions as a supremum, and then for general $f$ by
$f = f^+ - f^-$.
The space $\mathscr{L}^2(\mu)$ consists of the measurable $f$ with $\int |f|^2 d\mu < \infty$,
normed by $\|f\|_2 = (\int |f|^2 d\mu)^{1/2}$; a sequence $\{f_n\}$ **converges in the mean** to
$f$ if $\|f_n - f\|_2 \to 0$.
Mathlib's measure theory is used wherever it is mathematically the same object:
`MeasureTheory.OuterMeasure` and its Carathéodory $\sigma$-algebra, `MeasurableSet`,
`Measurable`, the lower Lebesgue integral `∫⁻` for nonnegative extended-real functions, the
Bochner integral `∫` and `Integrable` for the general case. What is set up freshly is Rudin's
$\mathscr{L}^2$ **of functions** — `Rudin.MemL2`, `Rudin.L2Norm`, `Rudin.CauchyL2`,
`Rudin.TendstoL2` — rather than Mathlib's quotient space `Lp`, because the Riesz–Fischer theorem
as Rudin states it produces an honest limit *function*, and the ε-N phrasing of Cauchyness and
of mean convergence is part of the statement.
## Formalization targets
### Goal — the Riesz–Fischer theorem (Theorem 11.42)
If $\{f_n\}$ is a Cauchy sequence in $\mathscr{L}^2(\mu)$, then there exists $f \in
\mathscr{L}^2(\mu)$ with $\|f_n - f\|_2 \to 0$: the space $\mathscr{L}^2(\mu)$ is complete.
Rudin's proof extracts a subsequence with $\|f_{n_{k+1}} - f_{n_k}\|_2 < 2^{-k}$, sums the
telescoping series, uses the monotone convergence theorem and the Schwarz inequality to show
that the sum converges almost everywhere, and identifies the pointwise limit as the mean limit
of the whole sequence. Every ingredient is a milestone of this mission.
### Milestones
$$\text{the measurable sets of an outer measure form a } \sigma\text{-algebra on which it is countably additive} \qquad (11.10)$$
$$\sup_n f_n \text{ and } \limsup_n f_n \text{ are measurable} \qquad (11.17)$$
$$|f|,\ f+g,\ fg \text{ are measurable} \qquad (11.16,\ 11.18)$$
$$E \mapsto \int_E f\,d\mu \text{ is countably additive} \qquad (11.24)$$
$$\left|\int f\,d\mu\right| \le \int |f|\,d\mu \qquad (11.26,\ 11.27)$$
$$\int \lim_n f_n \,d\mu = \lim_n \int f_n\,d\mu \ \text{ for } 0 \le f_1 \le f_2 \le \cdots \qquad (11.28)$$
$$\int \sum_n f_n \,d\mu = \sum_n \int f_n\,d\mu \ \text{ for } f_n \ge 0 \qquad (11.30)$$
$$\int \liminf_n f_n\,d\mu \le \liminf_n \int f_n\,d\mu \qquad (11.31)$$
$$\text{dominated convergence} \qquad (11.32)$$
$$\text{Riemann-integrable} \Rightarrow \text{Lebesgue-integrable, with the same integral} \qquad (11.33)$$
$$\left|\int fg\,d\mu\right| \le \|f\|_2\,\|g\|_2 \qquad (11.35)$$
$$\text{continuous functions are dense in } \mathscr{L}^2[a,b] \qquad (11.38)$$
$$\sum_n c_n^2 = \int f^2 d\mu \text{ for a complete orthonormal system} \qquad (11.45)$$
## Significance
The Lebesgue theory is the point at which analysis acquires limit theorems that do not require
uniform convergence. Monotone convergence, Fatou's lemma and dominated convergence are the three
statements that make the integral usable in probability, in Fourier analysis and in the theory
of partial differential equations, and the Riesz–Fischer theorem is what makes $\mathscr{L}^2$ a
Hilbert space and therefore the natural home of Fourier expansions: Parseval's identity
(11.45) is the assertion that the Fourier coefficient map is an isometry onto $\ell^2$.
Theorem 11.33 is the bridge back to the earlier chapters — every Riemann-integrable function is
Lebesgue-integrable with the same integral, and a bounded function on $[a, b]$ is
Riemann-integrable exactly when it is continuous almost everywhere — so the two halves of the
book agree wherever both apply.
Mathlib has an extensive measure theory and proves many of these results in considerable
generality. This mission's contribution is to state them in Rudin's formulation, for Rudin's
$\mathscr{L}^2$ of functions and with his explicit ε-N definitions, so that the chapter is
available as a coherent, self-contained unit that matches the textbook line by line and links
back to the Riemann–Stieltjes integral of Mission VI.
## Difficulty
Individually, most milestones will reduce to Mathlib results after the correct dictionary is in
place, and the interesting work is exactly in that translation: Rudin's measurability
(`{x : f(x) > a}` measurable) versus Mathlib's `Measurable`, Rudin's integral of a nonnegative
function versus `∫⁻` with values in `ℝ≥0∞`, Rudin's $\mathscr{L}^2$ of genuine functions versus
`Lp` as a quotient by almost-everywhere equality. The last of these is what makes the goal
theorem nontrivial to derive: Mathlib's completeness of `Lp` gives a limit *class*, and one must
choose a measurable representative and verify Rudin's mean convergence with the concrete norm
`Rudin.L2Norm`, which is `Real.sqrt (∫ f²)` and not an `ENNReal` quantity.
Theorem 11.33 (Riemann implies Lebesgue) and Theorem 11.38 (density of continuous functions)
are the two other places where real work is required: the first has to connect the Chapter 6
definition of the Riemann integral with `intervalIntegral`, and the second is an approximation
argument.
## Formalization scope
Conventions fixed by this mission:
* Measure-theoretic vocabulary is Mathlib's: `MeasureTheory.Measure`, `MeasurableSet`,
`Measurable`, `Integrable`, `∫⁻ x, f x ∂μ` for nonnegative `ℝ≥0∞`-valued integrands and
`∫ x, f x ∂μ` for the general real case. Rudin's Carathéodory construction is
`MeasureTheory.OuterMeasure.caratheodory`.
* Statements about suprema and upper limits of sequences of functions (11.17), and about
term-by-term integration of series (11.30) and Fatou's theorem (11.31), use `ℝ≥0∞`-valued
functions, matching Rudin's use of extended real values there.
* `Rudin.MemL2 μ f` is "`f` is measurable and `f²` is integrable"; `Rudin.L2Norm μ f` is
`Real.sqrt (∫ x, (f x)^2 ∂μ)`; `Rudin.CauchyL2` and `Rudin.TendstoL2` are Rudin's ε-N Cauchy
condition and mean convergence. No quotient is taken, so the goal theorem produces a function.
* Theorem 11.33 is stated with `Rudin.RiemannIntegrable` and `Rudin.RiemannIntegral` from
Mission VI, so the two integrals are literally compared.
* Parseval (11.45) is stated for an arbitrary complete orthonormal system in $\mathscr{L}^2(\mu)$,
completeness being phrased as "a function orthogonal to every $\varphi_n$ has norm zero";
the trigonometric case is Theorem 8.16 of Mission VIII.
Contributions of the convergence theorems (11.28, 11.31, 11.32) and of the Schwarz inequality
(11.35) are especially useful, since the goal theorem consumes them directly.
## Selected references
- Walter Rudin, *Principles of Mathematical Analysis*, 3rd edition, McGraw-Hill, 1976,
Chapter 11 (pp. 300–332).
- Walter Rudin, *Real and Complex Analysis*, 3rd edition, McGraw-Hill, 1987, Chapters 1–3.
15 thms4 active usersReviewed
🏆Completed
Captain: Lucas
Rudin PMA VIII: Some Special FunctionsTextbook
## 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
19 thms4 active usersReviewed
🏆Completed
Captain: Lucas
Rudin PMA X: Integration of Differential FormsTextbook
## 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.
18 thms4 active usersReviewed
🏆Completed
Captain: Lucas
Rudin PMA IX: Functions of Several VariablesTextbook
## Motivation
Chapter 9 of Walter Rudin's *Principles of Mathematical Analysis* (3rd edition, McGraw-Hill,
1976) develops the differential calculus of mappings $\mathbf{f} : \mathbb{R}^n \to
\mathbb{R}^m$. The definition of the derivative changes character: it is no longer a number but
a **linear transformation** $\mathbf{f}'(\mathbf{x})$, the one that approximates the increment
of $\mathbf{f}$ to first order. Once that is in place, the chapter proves the two theorems that
make nonlinear analysis possible: the **inverse function theorem** (Theorem 9.24), which says
that a continuously differentiable map with invertible derivative at a point is locally
invertible with a continuously differentiable inverse, and the **implicit function theorem**
(9.28), which solves $\mathbf{f}(\mathbf{x},\mathbf{y}) = 0$ locally for $\mathbf{x}$ in terms
of $\mathbf{y}$.
The message of both is that a nonlinear map behaves locally like its linearization, provided
that linearization is invertible and varies continuously.
This mission is the ninth in a series formalizing Rudin Chapters 1–11; it uses the
completeness and compactness results of Missions II and IV and the mean value estimates of
Mission V, and it prepares the change-of-variables machinery used in Mission X.
## Setting
$L(\mathbb{R}^n, \mathbb{R}^m)$ is the space of linear maps with the operator norm
$\|A\| = \sup_{|x| \le 1} |Ax|$. A map $\mathbf{f}$ defined on an open $E \subseteq \mathbb{R}^n$
is **differentiable at** $\mathbf{x}$ with derivative $A \in L(\mathbb{R}^n,\mathbb{R}^m)$ if
$$\lim_{\mathbf{h} \to 0} \frac{|\mathbf{f}(\mathbf{x}+\mathbf{h}) - \mathbf{f}(\mathbf{x}) - A\mathbf{h}|}{|\mathbf{h}|} = 0 ,$$
and $\mathbf{f} \in \mathcal{C}'(E)$ — a **$C'$-mapping** — if it is differentiable on $E$ and
$\mathbf{x} \mapsto \mathbf{f}'(\mathbf{x})$ is continuous. The **partial derivative**
$D_j f_i$ is the derivative of $t \mapsto f_i(\mathbf{x} + t\mathbf{e}_j)$ at $t = 0$. A map
$\varphi$ of a metric space into itself is a **contraction** if
$d(\varphi(x),\varphi(y)) \le c\,d(x,y)$ for some $c < 1$.
## Formalization targets
### Goal — inverse function theorem (Theorem 9.24)
Let $\mathbf{f}$ be a $C'$-mapping of an open $E \subseteq \mathbb{R}^n$ into $\mathbb{R}^n$ and
suppose $\mathbf{f}'(\mathbf{a})$ is invertible at some $\mathbf{a} \in E$. Then there are open
sets $U \ni \mathbf{a}$ and $V \ni \mathbf{f}(\mathbf{a})$ such that
$$\mathbf{f}|_U \text{ is injective}, \qquad \mathbf{f}(U) = V, \qquad
\mathbf{g} = (\mathbf{f}|_U)^{-1} \in \mathcal{C}'(V).$$
### Milestones
$$\text{invertible operators form an open set; inversion is continuous} \qquad (9.8)$$
$$(\mathbf{g}\circ\mathbf{f})'(\mathbf{x}) = \mathbf{g}'(\mathbf{f}(\mathbf{x}))\,\mathbf{f}'(\mathbf{x}) \qquad (9.15)$$
$$\text{differentiability gives all partial derivatives} \qquad (9.17)$$
$$\|\mathbf{f}'\| \le M \text{ on a convex } E \Rightarrow |\mathbf{f}(b)-\mathbf{f}(a)| \le M|b-a| \qquad (9.19)$$
$$\mathbf{f} \in \mathcal{C}'(E) \iff \text{the } D_j f_i \text{ exist and are continuous} \qquad (9.21)$$
$$\text{a contraction of a complete metric space has a unique fixed point} \qquad (9.23)$$
$$\text{implicit function theorem} \qquad (9.28)$$
$$D_{21}f \text{ continuous at } (a,b) \Rightarrow D_{12}f(a,b) = D_{21}f(a,b) \qquad (9.41)$$
$$\text{differentiation under the integral sign} \qquad (9.42)$$
## Significance
The inverse function theorem is the local classification statement of differential calculus: it
says that the only local obstruction to invertibility is degeneracy of the derivative, and it is
the mechanism behind coordinate changes, the rank theorem (9.32), and the change-of-variables
formula for integrals in Chapter 10. The implicit function theorem is its standard reformulation
and is what makes level sets of smooth maps into manifolds. Theorem 9.21 is the practical
criterion for the $C'$ hypothesis, since it reduces it to continuity of finitely many partial
derivatives; Theorem 9.41 shows that the symmetry of second derivatives, though intuitive,
requires a hypothesis; Theorem 9.19 is the several-variable substitute for the mean value
theorem, whose equality form already failed in Chapter 5.
Mathlib has the Fréchet derivative, the inverse and implicit function theorems for Banach
spaces, the Banach fixed-point theorem, and symmetry of second derivatives. This mission states
the Rudin versions concretely in $\mathbb{R}^n$ — with the explicit open sets $U$ and $V$ and
the inverse mapping produced as data, rather than through a bundled local homeomorphism — and
so provides a bridge between the book's formulations and the library's.
## Difficulty
The inverse function theorem is the first theorem in the book whose proof combines several
chapters at once: the contraction principle (9.23) gives local surjectivity by solving
$\mathbf{f}(\mathbf{x}) = \mathbf{y}$ as a fixed point of
$\mathbf{x} \mapsto \mathbf{x} + A^{-1}(\mathbf{y} - \mathbf{f}(\mathbf{x}))$; openness of the
set of invertible operators (9.8) keeps the derivative invertible near $\mathbf{a}$; the mean
value inequality (9.19) controls the error; and the continuity of inversion gives the $C'$
regularity of $\mathbf{g}$. The delicate point is that all estimates must hold *uniformly* on a
neighbourhood chosen in advance, so the order in which the neighbourhoods are shrunk matters.
For Theorem 9.41 the trap is the hypothesis: continuity of $D_{21}f$ at the single point
$(a,b)$ is assumed, not continuity of both mixed partials on a neighbourhood; the conclusion is
existence of $D_{12}f$ at that point, and it genuinely fails without some such hypothesis.
## Formalization scope
Conventions fixed by this mission:
* Euclidean spaces are `EuclideanSpace ℝ (Fin n)`; linear maps are `→L[ℝ]` (continuous linear
maps), which in finite dimension is the same as Rudin's $L(\mathbb{R}^n,\mathbb{R}^m)$, with
the operator norm.
* Derivatives are `HasFDerivAt`, and the $C'$ condition is `ContDiffOn ℝ 1`.
* Partial derivatives are stated as `HasDerivAt` of the line restriction
`t ↦ f (x + t • eⱼ)` at `t = 0`, avoiding any coordinate-projection bookkeeping;
`eⱼ = EuclideanSpace.single j 1`.
* Invertibility of a derivative is `Function.Bijective`, which for a continuous linear map
between finite-dimensional spaces is equivalent to the existence of a continuous linear
inverse.
* In 9.8 the inverse operator is supplied as a function `inv` constrained on the invertible
operators, so that continuity of inversion can be stated without bundling.
* Theorem 9.41 uses explicitly supplied partial derivative functions `D1f`, `D2f`, `D21f`, which
is how Rudin states the hypotheses, and the conclusion asserts existence of `D₁₂f` at the
point as a `HasDerivAt` statement.
* Theorem 9.42 is stated for the Riemann–Stieltjes integral of Mission VI, matching Rudin's
hypotheses `α` increasing and `φ(·,t) ∈ ℛ(α)`.
## Selected references
- Walter Rudin, *Principles of Mathematical Analysis*, 3rd edition, McGraw-Hill, 1976,
Chapter 9 (pp. 204–243).
11 thms6 active usersReviewed
🏆Completed
Captain: Lucas
Rudin PMA VII: Sequences and Series of FunctionsTextbook
## Motivation
Chapter 7 of Walter Rudin's *Principles of Mathematical Analysis* (3rd edition, McGraw-Hill,
1976) asks when a limit of functions inherits the properties of its members. Pointwise
convergence preserves almost nothing: Rudin's opening examples give continuous $f_n$ with
discontinuous limit, and sequences where $\lim_n \int f_n \ne \int \lim_n f_n$. **Uniform
convergence** is the hypothesis that repairs this, and the chapter's second half asks the
converse question — which functions arise as uniform limits from a given family — answered by
the **Stone–Weierstrass theorem** (Theorem 7.32): an algebra of continuous real functions on a
compact set that separates points and vanishes nowhere is uniformly dense in all continuous
functions there.
The classical Weierstrass approximation theorem (7.26) — polynomials are dense in $C[a,b]$ — is
the special case that made the general theorem worth proving, and is used in Chapter 8 for
Fourier series and in Chapter 11 for the density of continuous functions in $L^2$.
This mission is the seventh in a series formalizing Rudin Chapters 1–11; it uses the compactness
results of Mission II, the continuity results of Mission IV and the Riemann–Stieltjes integral
of Mission VI.
## Setting
A sequence $f_n$ **converges uniformly** to $f$ on $E$ if for every $\varepsilon > 0$ there is
$N$ with $|f_n(x) - f(x)| \le \varepsilon$ for all $n \ge N$ and all $x \in E$ — the same $N$ for
every point. A family $\mathcal{F}$ is **equicontinuous** on $E$ if a single $\delta$ serves all
its members in the definition of uniform continuity; it is **pointwise bounded** if each orbit
$\{f(x) : f \in \mathcal{F}\}$ is bounded, and **uniformly bounded** if one bound works for all
$f$ and all $x$.
A set $\mathcal{A}$ of real functions is an **algebra** if it is closed under addition,
multiplication and multiplication by real scalars; it **separates points** on $K$ if for
$x \ne y$ in $K$ some $f \in \mathcal{A}$ has $f(x) \ne f(y)$; it **vanishes at no point** of $K$
if for each $x \in K$ some $f \in \mathcal{A}$ has $f(x) \ne 0$. The **uniform closure** of
$\mathcal{A}$ on $K$ is the set of uniform limits on $K$ of sequences from $\mathcal{A}$.
## Formalization targets
### Goal — Stone–Weierstrass (Theorem 7.32)
Let $K$ be compact and let $\mathcal{A}$ be an algebra of real continuous functions on $K$ which
separates points on $K$ and vanishes at no point of $K$. Then
$$\overline{\mathcal{A}}^{\,\text{unif}} \supseteq C(K,\mathbb{R}) :$$
every continuous real function on $K$ is a uniform limit on $K$ of members of $\mathcal{A}$.
### Milestones
$$\text{uniform convergence} \iff \text{uniform Cauchy criterion} \qquad (7.8)$$
$$|f_n| \le M_n \text{ on } E,\ \textstyle\sum M_n < \infty \Rightarrow \sum f_n \text{ converges uniformly} \qquad (7.10)$$
$$\lim_{t\to x}\lim_n f_n(t) = \lim_n \lim_{t \to x} f_n(t) \text{ under uniform convergence} \qquad (7.11)$$
$$\text{a uniform limit of continuous functions is continuous} \qquad (7.12)$$
$$f_n \in \mathcal{R}(\alpha),\ f_n \to f \text{ uniformly} \Rightarrow f \in \mathcal{R}(\alpha),\ \int f_n \, d\alpha \to \int f \, d\alpha \qquad (7.16)$$
$$f_n' \to h \text{ uniformly},\ f_n(x_0) \text{ convergent} \Rightarrow f_n \to g \text{ uniformly},\ g' = h \qquad (7.17)$$
$$\text{there is a continuous nowhere differentiable } f : \mathbb{R} \to \mathbb{R} \qquad (7.18)$$
$$\text{pointwise bounded} + \text{equicontinuous on compact} \Rightarrow \text{uniformly bounded, convergent subsequence} \qquad (7.24,\ 7.25)$$
$$\text{polynomials are uniformly dense in } C[a,b] \qquad (7.26)$$
## Significance
Uniform convergence is the standard hypothesis under which limits commute with continuity,
integration and (with an extra condition) differentiation, and Theorems 7.11, 7.12, 7.16 and
7.17 are used throughout the rest of the book; Chapter 8 in particular builds the exponential,
trigonometric and Gamma functions as uniform limits and differentiates them term by term on the
strength of 7.17. Theorem 7.18 shows how weak pointwise differentiability is as a consequence of
continuity: a uniform limit of piecewise-linear functions can fail to be differentiable
anywhere. Arzelà–Ascoli is the compactness criterion for families of functions, and it is the
standard route to existence theorems for differential and integral equations.
Stone–Weierstrass is the structural theorem of the chapter: it replaces the combinatorial
Bernstein-polynomial proof of Weierstrass's theorem with a statement about algebras of
functions, applicable to trigonometric polynomials, polynomials in several variables, and
Lipschitz algebras alike.
Mathlib contains a Stone–Weierstrass theorem for subalgebras of `C(X, ℝ)` on compact Hausdorff
spaces, and a version of Arzelà–Ascoli. This mission states the results in Rudin's terms — plain
sets of functions on a compact subset $K$ of a metric space, uniform closure defined by
sequences — so that they can be used together with the Riemann–Stieltjes integral built in
Mission VI, which is not part of the library.
## Difficulty
Stone–Weierstrass is the one theorem in this mission whose proof is genuinely structural: from
the algebra one first produces $|f|$ as a uniform limit of polynomials in $f$ (which needs the
polynomial approximation of $\sqrt{t}$ on $[0,1]$ and so cannot be circular with Theorem 7.26),
then maxima and minima of pairs, then functions matching prescribed values at two points, and
only then the local-to-global patching over a finite subcover. Each step is short; keeping the
uniform closure a lattice and an algebra simultaneously is the bookkeeping burden.
Two hypotheses are easy to lose and both are necessary: an algebra that vanishes at a point
cannot approximate functions that do not, and one that fails to separate two points cannot
approximate functions that distinguish them.
## Formalization scope
Conventions fixed by this mission:
* Uniform convergence is Mathlib's `TendstoUniformlyOn … atTop`; complex-valued sequences are
used where Rudin allows complex values.
* Algebras, separation, non-vanishing and uniform closure are the predicates
`Rudin.IsFunctionAlgebra`, `Rudin.SeparatesPointsOn`, `Rudin.VanishesAtNoPointOn`,
`Rudin.UniformClosureOn`, defined for sets of functions `X → ℝ` and a compact subset `K`.
The goal's conclusion is membership in the uniform closure, i.e. the existence of an
approximating sequence from the algebra.
* Equicontinuity and the two boundedness notions are `Rudin.EquicontinuousOn`,
`Rudin.PointwiseBoundedOn`, `Rudin.UniformlyBoundedOn`, stated with explicit $\varepsilon$ and
$\delta$ as in Definitions 7.19 and 7.22.
* Theorem 7.16 is stated for the Riemann–Stieltjes integral of Mission VI, not for a Mathlib
integral, so the two missions compose.
* Theorem 7.26 is stated for complex-valued $f$ and polynomials with complex coefficients
evaluated at real points, as in Rudin.
## Selected references
- Walter Rudin, *Principles of Mathematical Analysis*, 3rd edition, McGraw-Hill, 1976,
Chapter 7 (pp. 143–171).
- M. H. Stone, *The generalized Weierstrass approximation theorem*, Mathematics Magazine 21
(1948), 167–184 and 237–254. https://doi.org/10.2307/3029750
14 thms5 active usersReviewed
🏆Completed
Captain: Lucas
Rudin PMA VI: The Riemann-Stieltjes IntegralTextbook
## Motivation
Chapter 6 of Walter Rudin's *Principles of Mathematical Analysis* (3rd edition, McGraw-Hill,
1976) constructs the **Riemann–Stieltjes integral** $\int_a^b f\,d\alpha$: the Riemann integral
with the increments $\Delta x_i$ of the variable replaced by the increments
$\Delta \alpha_i = \alpha(x_i) - \alpha(x_{i-1})$ of a monotonically increasing *integrator*
$\alpha$. Taking $\alpha(x) = x$ recovers the ordinary Riemann integral; taking $\alpha$ a step
function turns integrals into sums, so series and integrals become special cases of one
construction. This is the reason Rudin develops the theory in this generality: it unifies
Chapter 3's series with the integral, and it is the natural setting for the Fourier coefficients
of Chapter 8.
The chapter's capstone is the **fundamental theorem of calculus** (Theorem 6.21): an
integrable function which is the derivative of some $F$ integrates to $F(b) - F(a)$.
This mission is the sixth in a series formalizing Rudin Chapters 1–11; it uses the uniform
continuity of Mission IV and the mean value theorem of Mission V.
## Setting
A **partition** $P$ of $[a,b]$ is a finite set of points $a = x_0 \le x_1 \le \dots \le x_n = b$,
with increments $\Delta \alpha_i = \alpha(x_i) - \alpha(x_{i-1})$ for a monotonically increasing
$\alpha$. For a bounded real $f$ put
$M_i = \sup_{[x_{i-1},x_i]} f$, $m_i = \inf_{[x_{i-1},x_i]} f$, and
$$U(P,f,\alpha) = \sum_{i=1}^n M_i\,\Delta\alpha_i, \qquad
L(P,f,\alpha) = \sum_{i=1}^n m_i\,\Delta\alpha_i .$$
The **upper** and **lower integrals** are $\inf_P U(P,f,\alpha)$ and $\sup_P L(P,f,\alpha)$;
$f$ is **integrable with respect to $\alpha$**, written $f \in \mathcal{R}(\alpha)$, when they
agree, and the common value is $\int_a^b f\,d\alpha$. $P'$ **refines** $P$ when every division
point of $P$ is one of $P'$. Writing $\mathcal{R}$ for $\mathcal{R}(\alpha)$ with
$\alpha(x) = x$ gives the Riemann integral $\int_a^b f\,dx$.
## Formalization targets
### Goal — the fundamental theorem of calculus (Theorem 6.21)
$$
f \in \mathcal{R} \text{ on } [a,b], \quad F' = f \text{ on } [a,b]
\;\Longrightarrow\;
\int_a^b f(x)\,dx = F(b) - F(a).
$$
### Milestones
$$P' \text{ refines } P \Rightarrow L(P,f,\alpha) \le L(P',f,\alpha),\ U(P',f,\alpha) \le U(P,f,\alpha) \qquad (6.4)$$
$$\underline{\int} f\,d\alpha \le \overline{\int} f\,d\alpha \qquad (6.5)$$
$$f \in \mathcal{R}(\alpha) \iff \forall \varepsilon>0\ \exists P,\ U(P,f,\alpha) - L(P,f,\alpha) < \varepsilon \qquad (6.6)$$
$$f \text{ continuous} \Rightarrow f \in \mathcal{R}(\alpha) \qquad (6.8)$$
$$f \text{ monotone},\ \alpha \text{ continuous} \Rightarrow f \in \mathcal{R}(\alpha) \qquad (6.9)$$
$$\text{linearity of the integral} \qquad (6.12\mathrm{a})$$
$$\text{monotonicity, additivity in the interval, and } \big|\!\int f\,d\alpha\big| \le M(\alpha(b)-\alpha(a)) \qquad (6.12\mathrm{b,c,d})$$
$$\alpha' \in \mathcal{R} \Rightarrow \big(f \in \mathcal{R}(\alpha) \iff f\alpha' \in \mathcal{R}\big),\ \int f\,d\alpha = \int f\alpha'\,dx \qquad (6.17)$$
$$\text{change of variable through a strictly increasing } \varphi \qquad (6.19)$$
$$F(x) = \int_a^x f\,dt \text{ is continuous, and } F'(x_0) = f(x_0) \text{ where } f \text{ is continuous} \qquad (6.20)$$
$$\text{integration by parts} \qquad (6.22)$$
## Significance
The fundamental theorem is what makes the integral computable: it reduces integration to
antidifferentiation and so links Chapters 5 and 6. Theorem 6.20 is its companion — it says the
integral of a continuous function *is* an antiderivative — and together they show the two
operations are mutually inverse to the extent that the hypotheses allow. Theorem 6.17 explains
when a Stieltjes integral collapses to a Riemann integral with the density $\alpha'$, and it is
the computational tool for integrators that are differentiable; the step-function case at the
other extreme (Rudin's 6.15–6.16) is what turns sums into integrals.
Mathlib has no Riemann–Stieltjes integral: it has the Bochner integral, the interval integral,
and a Lebesgue–Stieltjes measure, but the upper-and-lower-sum construction of Chapter 6 is
absent. This mission therefore builds the object from Rudin's definitions and develops its basic
theory; that development is reusable beyond this mission — Chapter 7's interchange theorem
(7.16) and Chapter 8's Fourier coefficients are stated with respect to it.
## Difficulty
Two obstacles are specific to formalizing this chapter. First, the upper and lower integrals are
an infimum and a supremum over the *set of all partitions*, which is not a lattice-friendly
index; every comparison between partitions goes through the common refinement, and Theorem 6.4
is the workhorse that makes such comparisons possible. Second, the fundamental theorem is proved
by choosing a partition on which $U - L < \varepsilon$ and applying the mean value theorem on
each subinterval, so the proof requires selecting an intermediate point per subinterval — a
finite choice that is easy on paper and must be organized explicitly in Lean.
The integrator $\alpha$ is only assumed monotone, so it may be discontinuous, and the theory
must not assume otherwise: Theorem 6.9 needs continuity of $\alpha$ precisely because it is not
available in general.
## Formalization scope
Conventions fixed by this mission:
* A partition of `[a, b]` is `Rudin.Partition a b`: the number `n` of subintervals together with
a monotone placement function `x` with `x 0 = a` and `x n = b`. Rudin allows
$x_{i-1} = x_i$, and so does this structure.
* `Rudin.upperSum`, `Rudin.lowerSum`, `Rudin.upperIntegral`, `Rudin.lowerIntegral`,
`Rudin.RSIntegrable`, `Rudin.RSIntegral` follow Definitions 6.1–6.2 literally, with `sSup` and
`sInf` over the images $f([x_{i-1},x_i])$.
* Since `sSup`/`sInf` on `ℝ` return `0` on unbounded sets, every statement carries Rudin's
boundedness hypothesis for $f$ explicitly; likewise monotonicity of $\alpha$ is assumed as
`MonotoneOn α (Set.Icc a b)` rather than built into a type.
* `Rudin.RiemannIntegrable` and `Rudin.RiemannIntegral` are the case $\alpha = \mathrm{id}$, in
which the goal theorem and Theorems 6.20–6.22 are stated, matching Rudin.
* Derivatives are `HasDerivAt`, so `F' = f` is stated pointwise on `[a, b]` with the value `f x`
supplied, as in Rudin's hypothesis.
The goal is not vacuous, and not a restatement of a library lemma: the integral in it is the one
defined in this mission, so a solution must connect the upper/lower sum construction to
differentiation rather than quoting Mathlib's interval integral.
## Selected references
- Walter Rudin, *Principles of Mathematical Analysis*, 3rd edition, McGraw-Hill, 1976,
Chapter 6 (pp. 120–142).
21 thms3 active usersReviewed
🏆Completed
Captain: Lucas
Rudin PMA IV: ContinuityTextbook
## Motivation
Continuity is the hypothesis under which limits may be moved inside a function, and Chapter 4
of Walter Rudin's *Principles of Mathematical Analysis* (3rd edition, McGraw-Hill, 1976) is
about what continuity gives once the domain is compact or connected. Three of its theorems are
used in nearly every later argument of the book: a continuous function on a compact set has
compact image (Theorem 4.14), hence attains its bounds (4.16); a continuous function on a
connected set has connected image (4.22), hence takes intermediate values (4.23); and a
continuous function on a *compact* metric space is **uniformly continuous** (Theorem 4.19) —
the $\delta$ can be chosen independently of the point.
The last of these is the chapter's capstone. Uniform continuity is exactly what is needed to
prove that continuous functions are Riemann-integrable (Chapter 6), and it is the first place
where compactness upgrades a pointwise hypothesis into a global one with a quantitative
conclusion.
This mission is the fourth in a series formalizing Rudin Chapters 1–11; it uses the metric
topology of Mission II and is a prerequisite for Missions V–VII.
## Setting
Let $X, Y$ be metric spaces, $E \subseteq X$, $f : E \to Y$, and let $p$ be a limit point of
$E$. Rudin writes $\lim_{x \to p} f(x) = q$ when for every $\varepsilon > 0$ there is
$\delta > 0$ with $d_Y(f(x), q) < \varepsilon$ for all $x \in E$ satisfying
$0 < d_X(x,p) < \delta$; the exclusion of $x = p$ is deliberate, and it is what makes the
notion agree with continuity only when $f(p) = q$ (Theorem 4.6). $f$ is **continuous at** $p$
if the same holds with the condition $0 < d_X(x,p)$ dropped, and **continuous** if it is
continuous at every point.
$f$ is **uniformly continuous** on $X$ if for every $\varepsilon > 0$ there is a single
$\delta > 0$ such that $d_Y(f(p), f(q)) < \varepsilon$ for *all* $p, q \in X$ with
$d_X(p,q) < \delta$. A real function on $(a,b)$ is **monotonically increasing** if $x < y$
implies $f(x) \le f(y)$; its one-sided limits are written $f(x-)$ and $f(x+)$, and it has a
**discontinuity of the first kind** at $x$ when both exist but do not agree with $f(x)$.
## Formalization targets
### Goal — uniform continuity on compacta (Theorem 4.19)
$$
X \text{ compact metric space},\ f : X \to Y \text{ continuous}
\;\Longrightarrow\;
\forall \varepsilon > 0\ \exists \delta > 0\ \forall p, q \in X,\
d(p,q) < \delta \Rightarrow d(f(p), f(q)) < \varepsilon .
$$
### Milestones
$$f \text{ continuous at } p \iff \lim_{x \to p} f(x) = f(p) \qquad (4.6)$$
$$f \text{ continuous} \iff f^{-1}(V) \text{ open for every open } V \qquad (4.8)$$
$$K \text{ compact} \Rightarrow f(K) \text{ compact} \qquad (4.14)$$
$$\text{a continuous real } f \text{ on a compact } X \text{ attains } \sup f \text{ and } \inf f \qquad (4.16)$$
$$f : X \to Y \text{ continuous bijection, } X \text{ compact} \Rightarrow f^{-1} \text{ continuous} \qquad (4.17)$$
$$E \text{ connected} \Rightarrow f(E) \text{ connected} \qquad (4.22)$$
$$f(a) < c < f(b) \Rightarrow f(x) = c \text{ for some } x \in (a,b) \qquad (4.23)$$
$$f \text{ monotone} \Rightarrow f(x-),\, f(x+) \text{ exist and } f(x-) \le f(x) \le f(x+) \qquad (4.29)$$
$$\text{the discontinuity set of a monotone function is at most countable} \qquad (4.30)$$
## Significance
Uniform continuity is the hypothesis that converts local approximation into global
approximation with a uniform error bound. In Chapter 6 it is what makes the upper and lower
Riemann–Stieltjes sums of a continuous function come together; in Chapter 7 it underlies the
equicontinuity of Arzelà–Ascoli; in Chapter 9 it appears again in the estimate of a $C'$
mapping on a compact ball. The extreme value theorem and the intermediate value theorem are the
two existence theorems of elementary analysis, and both come from this chapter by combining
Chapter 2's compactness and connectedness with continuity.
Theorem 4.30 — a monotone function has at most countably many discontinuities — is the result
that makes monotone integrators well behaved in Chapter 6, and it is the first place in the book
where a countability argument (Chapter 2) pays off analytically.
Mathlib has continuity, compactness and connectedness in general topological spaces, and most
of the milestones can be matched to library results after the statements are put in Rudin's
metric form. The formalization value is again in the dictionary: Rudin's punctured-limit
definition versus `ContinuousWithinAt`, and his $\varepsilon$–$\delta$ uniform continuity versus
the library's uniformity-filter definition.
## Difficulty
There is no single hard step; the difficulty is in the hypotheses being weaker than they look.
In Theorem 4.6 the limit is taken through $E \setminus \{p\}$, so the equivalence with
continuity genuinely needs $p \in E$ *and* $p$ a limit point; dropping the second hypothesis
makes the statement false at isolated points. In Theorem 4.19 the naive proof — pick $\delta_p$
at each point by continuity and take the infimum — fails because the infimum over infinitely
many points can be $0$; compactness is used to reduce to finitely many, and the factor of two
in the radii of the covering balls is essential. Theorem 4.30 requires an injection from the
discontinuity set into $\mathbb{Q}$, built from the gap between $f(x-)$ and $f(x+)$.
## Formalization scope
Conventions fixed by this mission:
* Continuity is Mathlib's `Continuous`, `ContinuousOn`, `ContinuousWithinAt`; Rudin's
$\lim_{x\to p} f(x) = q$ along $E$ is `Filter.Tendsto f (𝓝[E \ {p}] p) (𝓝 q)`.
* Uniform continuity is `Rudin.UniformlyContinuous`, stated with explicit $\varepsilon$ and
$\delta$ as in Definition 4.18, rather than through the uniformity filter.
* Limit points are `Rudin.IsLimitPoint` from the Chapter 2 mission, so the two missions share
one notion.
* Compactness of the domain in 4.16, 4.17 and 4.19 is the typeclass `[CompactSpace X]`, matching
Rudin's phrase "compact metric space"; 4.14 is stated for a compact subset instead, which is
the form later missions use.
* Monotone functions are `MonotoneOn f (Set.Ioo a b)`; one-sided limits are `𝓝[<] x` and
`𝓝[>] x` filters, and 4.29 also identifies them with the supremum and infimum of the
corresponding one-sided images, as Rudin does.
The goal is not vacuous and does not follow by unfolding: uniform continuity fails for
continuous functions on non-compact domains (e.g. $x \mapsto x^2$ on $\mathbb{R}$, or
$x \mapsto 1/x$ on $(0,1)$), so compactness is doing the work.
## Selected references
- Walter Rudin, *Principles of Mathematical Analysis*, 3rd edition, McGraw-Hill, 1976,
Chapter 4 (pp. 83–101).
11 thms2 active usersReviewed
🏆Completed
Captain: Lucas
Rudin PMA III: Numerical Sequences and SeriesTextbook
## Motivation
Chapter 3 of Walter Rudin's *Principles of Mathematical Analysis* (3rd edition, McGraw-Hill,
1976) develops the theory of convergence for sequences and series of numbers: subsequential
limits and upper limits, the Cauchy criterion, the comparison, root and ratio tests, power
series, summation by parts, and products of series. Its final section answers a question that
distinguishes analysis from algebra: an infinite sum is not a sum. For a series that converges
only conditionally, the value of the sum depends on the order of the terms, and **Riemann's
rearrangement theorem** (Theorem 3.54) makes the dependence total — by reordering the terms one
can prescribe *any* pair of limit inferior and limit superior for the partial sums, including
divergence to $\pm\infty$.
This mission is the third in a series formalizing Rudin Chapters 1–11. It uses the real and
complex number systems of Mission I and the compactness results of Mission II, and it supplies
the convergence machinery used by Missions VII and VIII.
## Setting
A **series** $\sum a_n$ is the sequence of **partial sums**
$s_n = a_0 + a_1 + \dots + a_{n-1}$; the series **converges to** $s$ when $s_n \to s$, and
**converges absolutely** when $\sum \|a_n\|$ converges. The **upper limit** of a real sequence
is $s^{*} = \limsup_{n} s_n$, taken in the extended real number system
$[-\infty, +\infty]$, and a **subsequential limit** is a limit of a subsequence there. A
**rearrangement** of $\sum a_n$ is a series $\sum a_{\sigma(n)}$ with $\sigma$ a bijection of
the index set onto itself.
The distinction that drives the chapter: for real or complex terms, absolute convergence is
equivalent to convergence of $\sum a_{\sigma(n)}$ for *every* $\sigma$, to the same sum
(Theorem 3.55), whereas mere convergence is not.
## Formalization targets
### Goal — Riemann's rearrangement theorem (Theorem 3.54)
Let $\sum a_n$ be a series of real numbers which converges but not absolutely, and let
$-\infty \le \alpha \le \beta \le +\infty$. Then there is a rearrangement $\sum a_{\sigma(n)}$
with partial sums $s_n'$ such that
$$\liminf_{n \to \infty} s_n' = \alpha, \qquad \limsup_{n \to \infty} s_n' = \beta .$$
### Milestones
$$s^{*} \text{ is a subsequential limit, and } x > s^{*} \Rightarrow s_n < x \text{ eventually; } s^{*} \text{ is unique with these properties} \qquad (3.17)$$
$$\textstyle\sum a_n \text{ converges} \iff \forall \varepsilon>0\ \exists N\ \forall m \ge n \ge N,\ \big|\sum_{k=n}^{m} a_k\big| \le \varepsilon \qquad (3.22)$$
$$\textstyle\sum_{n\ge 0} x^n = \tfrac{1}{1-x}\ (0 \le x < 1), \text{ divergence for } x \ge 1 \qquad (3.26)$$
$$\textstyle\sum n^{-p} \text{ converges} \iff p > 1 \qquad (3.28)$$
$$e = \textstyle\sum 1/n! = \lim_n (1 + 1/n)^n \qquad (3.30,\ 3.31)$$
$$\alpha = \limsup \|a_n\|^{1/n} < 1 \Rightarrow \text{convergence}, \ \alpha > 1 \Rightarrow \text{divergence} \qquad (3.33)$$
$$\text{ratio test} \qquad (3.34)$$
$$\text{radius of convergence of } \textstyle\sum c_n z^n \qquad (3.39)$$
$$\text{bounded partial sums} + b_n \downarrow 0 \Rightarrow \textstyle\sum a_n b_n \text{ converges} \qquad (3.42)$$
$$\text{absolute convergence} \Rightarrow \text{convergence} \qquad (3.45)$$
$$\text{Cauchy product: } \textstyle\sum c_n = AB \text{ when } \sum a_n \text{ converges absolutely} \qquad (3.50)$$
## Significance
The rearrangement theorem is the precise statement of why conditional convergence must be
handled with care, and it is the reason later chapters insist on *uniform* or *absolute*
hypotheses before interchanging limit operations: Theorem 3.50 (Mertens) needs absolute
convergence of one factor, and the Fourier and Lebesgue theories of Chapters 8 and 11 are built
on $L^2$ and $L^1$ convergence rather than pointwise summation. The supporting milestones are
the standard convergence tests, which are used constantly in the rest of the book, and the
characterization of $\limsup$, which is the tool that makes the root test and the radius of
convergence formula precise.
Mathlib's `Summable`/`HasSum` express *unconditional* summability, which over $\mathbb{R}$ and
$\mathbb{C}$ is equivalent to absolute convergence. The conditionally convergent series that
this chapter is about are therefore invisible to that API, and the mission works with partial
sums directly. Some of the classical tests exist in Mathlib in `Summable` form and will need
restating; the rearrangement theorem itself has to be built.
## Difficulty
The goal theorem is a construction, not an estimate: one splits $a_n$ into its positive and
negative parts $p_n, q_n$, observes that $\sum p_n$ and $\sum q_n$ both diverge while
$p_n, q_n \to 0$, and then alternately draws blocks of positive and negative terms to overshoot
targets $\beta_m \to \beta$ and undershoot targets $\alpha_m \to \alpha$. Formalizing the
alternating greedy construction requires defining the permutation recursively together with the
invariant that every index is eventually used — the bookkeeping, not the analysis, is the hard
part. The endpoint cases $\alpha = -\infty$ or $\beta = +\infty$ must be carried through the
same construction rather than treated separately.
## Formalization scope
Conventions fixed by this mission:
* Series convergence is `Rudin.SeriesConvergesTo` / `Rudin.SeriesConverges`, defined through
`Rudin.partialSum a n = ∑_{i<n} a i`. Absolute convergence is `Rudin.SeriesConvergesAbsolutely`.
Mathlib's `Summable` is deliberately *not* used, since it would collapse the distinction the
chapter is about.
* Upper and lower limits are taken in `EReal` via `Filter.limsup`/`Filter.liminf`, so
$\pm\infty$ are allowed as values of $\alpha$ and $\beta$ in the goal.
* Rearrangements are `Equiv.Perm ℕ`, and the rearranged series is `fun k => a (σ k)`.
* Series with complex terms are used where Rudin allows complex terms (3.22, 3.33, 3.34, 3.39,
3.42, 3.45, 3.50); the goal is about real series, as in the book.
* The radius-of-convergence milestone is stated as `α‖z‖ < 1` and `α‖z‖ > 1` rather than
`‖z‖ < 1/α`, to avoid inversion in `EReal`.
The goal is not vacuous: conditionally convergent series exist (the alternating harmonic
series), so the hypotheses are satisfiable, and the conclusion fixes both limit points exactly
rather than merely bounding them.
## Selected references
- Walter Rudin, *Principles of Mathematical Analysis*, 3rd edition, McGraw-Hill, 1976,
Chapter 3 (pp. 47–78).
- Bernhard Riemann, *Über die Darstellbarkeit einer Function durch eine trigonometrische
Reihe*, Abhandlungen der Königlichen Gesellschaft der Wissenschaften zu Göttingen 13 (1867),
Section 3.
13 thms2 active usersReviewed
🏆Completed
Captain: Lucas
Rudin PMA V: DifferentiationTextbook
## Motivation
Chapter 5 of Walter Rudin's *Principles of Mathematical Analysis* (3rd edition, McGraw-Hill,
1976) is the differential calculus of one real variable, developed from the definition of the
derivative as a limit of difference quotients. Its organizing result is the **mean value
theorem** and the family of consequences that follow from it: monotonicity criteria,
L'Hospital's rule, and — the chapter's capstone — **Taylor's theorem** (Theorem 5.15), which
approximates a function by a polynomial of degree $n-1$ and expresses the error exactly as a
single $n$-th derivative evaluated at an unspecified intermediate point.
Taylor's theorem is what makes differentiability quantitatively useful. It is the tool that
turns local smoothness into explicit error bounds, and the estimates of Chapter 8 for the
exponential, trigonometric and Gamma functions all rest on it.
This mission is the fifth in a series formalizing Rudin Chapters 1–11; it uses the continuity
and compactness results of Mission IV.
## Setting
Let $f$ be real-valued on $[a,b]$. For $x \in [a,b]$ the **derivative** is
$$f'(x) = \lim_{t \to x} \frac{f(t) - f(x)}{t - x},$$
whenever the limit exists. Higher derivatives $f', f'', \dots, f^{(n)}$ are defined by
iteration; $f^{(n)}$ exists on a set only if $f^{(n-1)}$ exists in a neighbourhood of each of
its points. $f$ has a **local maximum** at $x$ if $f(t) \le f(x)$ for all $t$ near $x$.
Given a positive integer $n$ and a point $\alpha$, the **Taylor polynomial** of $f$ at $\alpha$
of degree $n-1$ is
$$P(t) = \sum_{k=0}^{n-1} \frac{f^{(k)}(\alpha)}{k!}\,(t-\alpha)^k .$$
## Formalization targets
### Goal — Taylor's theorem (Theorem 5.15)
Let $f^{(n-1)}$ be continuous on $[a,b]$, let $f^{(n)}(t)$ exist for $t \in (a,b)$, and let
$\alpha \ne \beta$ be points of $[a,b]$. Then there is a point $x$ strictly between $\alpha$ and
$\beta$ such that
$$f(\beta) \;=\; \sum_{k=0}^{n-1} \frac{f^{(k)}(\alpha)}{k!}\,(\beta-\alpha)^k \;+\; \frac{f^{(n)}(x)}{n!}\,(\beta-\alpha)^n .$$
For $n = 1$ this is exactly the mean value theorem.
### Milestones
$$f \text{ differentiable at } x \Rightarrow f \text{ continuous at } x \qquad (5.2)$$
$$\text{local maximum at an interior } x,\ f'(x) \text{ exists} \Rightarrow f'(x) = 0 \qquad (5.8)$$
$$(f(b)-f(a))\,g'(x) = (g(b)-g(a))\,f'(x) \text{ for some } x \in (a,b) \qquad (5.9)$$
$$f(b) - f(a) = (b-a) f'(x) \text{ for some } x \in (a,b) \qquad (5.10)$$
$$f' \ge 0 \Rightarrow f \text{ increasing}; \quad f' = 0 \Rightarrow f \text{ constant}; \quad f' \le 0 \Rightarrow f \text{ decreasing} \qquad (5.11)$$
$$f'(a) < A < f'(b) \Rightarrow f'(x) = A \text{ for some } x \in (a,b) \qquad (5.12)$$
$$f, g \to 0 \text{ and } f'/g' \to A \Rightarrow f/g \to A \qquad (5.13)$$
$$\|f(b) - f(a)\| \le (b-a)\,\|f'(x)\| \text{ for some } x \in (a,b),\ f \text{ vector-valued} \qquad (5.19)$$
## Significance
The mean value theorem converts a hypothesis about derivatives into a statement about
increments, and everything in the chapter is an application of that conversion. Monotonicity
criteria (5.11) are the basis of every "the function is increasing, hence injective" argument,
including the change of variable in Chapter 6. Darboux's theorem (5.12) shows that derivatives,
though not necessarily continuous, cannot have simple discontinuities — a fact that is easy to
state and impossible to guess from the definition. Theorem 5.19 is the form of the mean value
theorem that survives for vector-valued functions: the equality is lost (there need be no single
point where the vector increment is proportional to the derivative), and only the inequality
remains; the same phenomenon dictates the statements of Chapter 9.
Mathlib contains the mean value theorem, L'Hospital's rule, and a Taylor theorem with various
remainder forms. The value of this mission is a statement of Taylor's theorem in Rudin's exact
formulation — arbitrary distinct endpoints $\alpha, \beta$ in $[a,b]$, hypotheses only on
$f^{(n-1)}$ and $f^{(n)}$, an intermediate point $x$ strictly between them — and the derivation
of the chapter's other results in a form the later missions can quote.
## Difficulty
Taylor's theorem is proved by choosing the constant $M$ so that
$f(\beta) = P(\beta) + M(\beta-\alpha)^n$ and applying Rolle's theorem $n$ times to
$g(t) = f(t) - P(t) - M(t-\alpha)^n$; the bookkeeping is in tracking that $g^{(k)}(\alpha) = 0$
for $k < n$ and that each application produces a new intermediate point strictly inside the
previous interval. In a proof assistant the iteration is the awkward part: the induction is on
$n$ with the interval shrinking, and the statement must be general enough in $\alpha$ and
$\beta$ (either order) for the inductive step to apply. The hypothesis that $f^{(n)}$ exists
only on the *open* interval, while $f^{(n-1)}$ is merely continuous on the closed one, must be
preserved — strengthening it to $C^n$ on $[a,b]$ would make the statement weaker than Rudin's.
## Formalization scope
Conventions fixed by this mission:
* Derivatives are Mathlib's `deriv` and `iteratedDeriv`, which are total functions returning
`0` where the function is not differentiable; every statement therefore carries explicit
differentiability hypotheses exactly where Rudin states them.
* Intervals are `Set.Icc a b` and `Set.Ioo a b`, and "for some $x$ between $\alpha$ and
$\beta$" is stated as an explicit disjunction, since the goal does not assume
$\alpha < \beta$.
* Vector-valued functions in 5.19 take values in `EuclideanSpace ℝ (Fin k)`, and the conclusion
is the inequality, not an equality — the equality version is false, as Rudin notes.
* L'Hospital's rule is formalized in the $0/0$ case at a finite left endpoint, which is the
first case of Rudin's Theorem 5.13; the $\infty$ case and the limits at $\pm\infty$ are not
part of this mission.
* Local maxima in 5.8 are stated with an explicit radius, matching Rudin's Definition 5.7.
## Selected references
- Walter Rudin, *Principles of Mathematical Analysis*, 3rd edition, McGraw-Hill, 1976,
Chapter 5 (pp. 103–119).
14 thms4 active usersReviewed
🏆Completed
Captain: Lucas
Rudin PMA II: Basic TopologyTextbook
## Motivation
Convergence, continuity and integration are all statements about *nearness*, and Chapter 2 of
Walter Rudin's *Principles of Mathematical Analysis* (3rd edition, McGraw-Hill, 1976) isolates
the amount of structure needed to talk about nearness: a metric. The chapter's payoff is a
single theorem, **Heine–Borel** (Theorem 2.41), which says that in $\mathbb{R}^k$ — and, as the
chapter's examples show, only in spaces resembling it — three very different-looking finiteness
conditions coincide: being closed and bounded, admitting finite subcovers, and forcing every
infinite subset to accumulate. Nearly every existence theorem in the rest of the book (a
continuous function on $[a,b]$ attains its maximum, is uniformly continuous, is
Riemann-integrable) is an application of that equivalence.
This mission is the second in a series formalizing Rudin Chapters 1–11. It builds on the
number systems of Mission I and supplies the topological input for Missions III–VII.
## Setting
A **metric space** is a set $X$ with a distance $d : X \times X \to \mathbb{R}$ that is
positive for distinct points, symmetric, and satisfies the triangle inequality. The
**neighbourhood** $N_r(p)$ is the set of $q$ with $d(p,q) < r$. A point $p$ is a **limit
point** of $E \subseteq X$ if every neighbourhood of $p$ contains a point of $E$ different
from $p$; $E$ is **closed** if it contains all its limit points, **open** if each of its points
has a neighbourhood inside $E$, and its **closure** $\bar E$ is $E$ together with its limit
points. $E$ is **perfect** if it is closed and every point of $E$ is a limit point of $E$, and
**bounded** if it is contained in some neighbourhood.
An **open cover** of $E$ is a family of open sets whose union contains $E$; $K$ is **compact**
if every open cover of $K$ has a finite subcover. A **$k$-cell** is a product
$\{x \in \mathbb{R}^k : a_j \le x_j \le b_j \text{ for all } j\}$. Two sets $A, B$ are
**separated** if $\bar A \cap B = A \cap \bar B = \varnothing$, and $E$ is **connected** if it
is not the union of two nonempty separated sets.
## Formalization targets
### Goal — Heine–Borel (Theorem 2.41)
For $E \subseteq \mathbb{R}^k$, the following are equivalent:
$$
\text{(a) } E \text{ closed and bounded} \quad\Longleftrightarrow\quad
\text{(b) } E \text{ compact} \quad\Longleftrightarrow\quad
\text{(c) every infinite } S \subseteq E \text{ has a limit point in } E .
$$
### Milestones
$$\textstyle\bigcup_n E_n \text{ countable when each } E_n \text{ is} \qquad (2.12)$$
$$\{0,1\}^{\mathbb{N}} \text{ is uncountable} \qquad (2.14)$$
$$\text{arbitrary unions of open sets, finite intersections of open sets, and the closed duals} \qquad (2.24)$$
$$\bar E = E \cup E', \quad \bar E \text{ closed}, \quad \bar E = E \Leftrightarrow E \text{ closed}, \quad E \subseteq F \text{ closed} \Rightarrow \bar E \subseteq F \qquad (2.27)$$
$$\sup E \in \bar E \qquad (2.28)$$
$$\text{open-cover compactness} \Leftrightarrow \text{compactness} \qquad (2.32)$$
$$F \subseteq K,\ F \text{ closed},\ K \text{ compact} \Rightarrow F \text{ compact} \qquad (2.35)$$
$$\text{finite intersection property for compact sets} \qquad (2.36)$$
$$\text{infinite } E \subseteq K \text{ compact} \Rightarrow E \text{ has a limit point in } K \qquad (2.37)$$
$$\text{nested } k\text{-cells have a common point} \qquad (2.39)$$
$$\text{every } k\text{-cell is compact} \qquad (2.40)$$
$$\text{nonempty perfect } P \subseteq \mathbb{R}^k \text{ is uncountable} \qquad (2.43)$$
$$E \subseteq \mathbb{R} \text{ connected} \Leftrightarrow (x,y \in E,\ x<z<y \Rightarrow z \in E) \qquad (2.47)$$
## Significance
Heine–Borel is the bridge between the order completeness of $\mathbb{R}$ established in
Chapter 1 and the analytic theorems of Chapters 3–7: the bisection argument that proves
$k$-cells compact is the same argument that produces convergent subsequences (Bolzano–Weierstrass,
Theorem 2.42), and compactness is what converts local information into global statements.
Theorem 2.43 supplies the standard source of uncountable sets of measure zero — the Cantor set
is the running example — which matters again in Chapter 11. Theorem 2.47, characterizing the
connected subsets of the line as the order-convex ones, is the topological content of the
intermediate value theorem proved in Chapter 4.
Mathlib has an extensive metric-space and compactness library, so much of this chapter exists
there in some form. What this mission adds is the explicit correspondence with Rudin's
formulations: his open-cover definition of compactness against the library's filter-based
`IsCompact` (a milestone in its own right), his $\varepsilon$-style limit points against
`closure`, and his $k$-cells against the library's boxes. The resulting dictionary is what the
remaining missions in the series use when they need a compactness argument.
## Difficulty
The mathematics is standard, and the difficulty is almost entirely in the translation layer.
Two places bite. First, Rudin's compactness quantifies over arbitrary open covers, so the
statement is a $\Pi$-type over families of sets, while Mathlib's `IsCompact` is a statement
about filters; the equivalence is available in the library but only after the cover is
presented in the right indexed form. Second, "limit point" in Rudin's sense is *not*
`p ∈ closure E`: the point must be approached by points of $E$ *other than* $p$, so isolated
points of $E$ are excluded, and statements such as 2.27(a) and 2.41(c) are false if the two
notions are conflated.
## Formalization scope
Conventions fixed by this mission:
* Metric spaces are Mathlib's `[MetricSpace X]`; `IsOpen`, `IsClosed`, `closure`, `Perfect`,
`IsCompact`, `Bornology.IsBounded` and `IsPreconnected` are used for Rudin's corresponding
notions.
* Rudin's limit points are `Rudin.IsLimitPoint p E`, defined with the explicit $\varepsilon$
and the condition $q \ne p$, and his open-cover compactness is `Rudin.IsCoverCompact`.
* $k$-cells are `Rudin.kCell k a b` inside `EuclideanSpace ℝ (Fin k)`; the case where some
$a_j > b_j$ gives the empty set, which is why the nested-cell milestone assumes each cell is
nonempty, exactly as Rudin's construction does.
* Connectedness is `IsPreconnected`, which admits the empty set, matching Rudin's convention
that a set is connected unless it splits into two *nonempty* separated pieces.
* The Heine–Borel goal is stated as a `TFAE` list in Rudin's order (a), (b), (c).
The equivalence is not vacuous: all three conditions are satisfied by any $k$-cell and all
three fail for $\mathbb{R}^k$ itself when $k \ge 1$.
## Selected references
- Walter Rudin, *Principles of Mathematical Analysis*, 3rd edition, McGraw-Hill, 1976,
Chapter 2 (pp. 24–55).
- The mathlib Community, *The Lean Mathematical Library*, CPP 2020.
https://doi.org/10.1145/3372885.3373824
15 thms2 active usersReviewed
🏆Completed
Captain: Lucas
Rudin PMA I: The Real and Complex Number SystemsTextbook
## Motivation
Every course in analysis begins by fixing what a real number is, because the theorems that
follow — the intermediate value theorem, the convergence of monotone bounded sequences, the
compactness of closed bounded intervals — are false over the rationals and true over the reals
for exactly one reason: the **least-upper-bound property**. Walter Rudin opens *Principles of
Mathematical Analysis* (3rd edition, McGraw-Hill, 1976) with this point. His Example 1.1
exhibits the gap concretely: the set of rationals $p$ with $p^2 < 2$ has no least upper bound
in $\mathbb{Q}$. Chapter 1 then constructs an ordered field in which no such gap occurs, and
derives from that single axiom the archimedean property, the density of $\mathbb{Q}$, and the
existence of $n$-th roots.
This mission is the first in a series formalizing Rudin Chapters 1–11. It covers the chapter's
number-system foundations: the ordering axioms, the real field, the complex field, and
euclidean space $\mathbb{R}^k$.
## Setting
An **ordered set** is a set $S$ with a transitive relation $<$ such that for $x, y \in S$
exactly one of $x < y$, $x = y$, $y < x$ holds. If $E \subseteq S$ and there is $\beta \in S$
with $x \le \beta$ for all $x \in E$, then $E$ is **bounded above** and $\beta$ is an **upper
bound**. A **least upper bound** (supremum) of $E$ is an upper bound $\alpha$ such that no
$\gamma < \alpha$ is an upper bound. The ordered set $S$ has the **least-upper-bound property**
if every nonempty $E \subseteq S$ that is bounded above has a least upper bound in $S$.
An **ordered field** is a field $F$ carrying an order such that $x + y < x + z$ whenever
$y < z$, and $xy > 0$ whenever $x > 0$ and $y > 0$. Rudin's Theorem 1.19 asserts that an
ordered field $\mathbb{R}$ with the least-upper-bound property exists and contains $\mathbb{Q}$
as a subfield; the members of $\mathbb{R}$ are the **real numbers**. The **complex field**
$\mathbb{C}$ is the set of ordered pairs $(a,b)$ of reals with the usual operations, written
$a + bi$, with $|z| = (z\bar z)^{1/2}$; **euclidean $k$-space** $\mathbb{R}^k$ is the set of
$k$-tuples with the inner product $x \cdot y = \sum_{j} x_j y_j$ and norm
$|x| = (x\cdot x)^{1/2}$.
## Formalization targets
### Goal — the real field is the unique complete ordered field (Theorem 1.19)
$$
\text{$K$ an ordered field with the least-upper-bound property}
\;\Longrightarrow\;
\exists!\, e : K \xrightarrow{\ \sim\ } \mathbb{R} \text{ an order-preserving field isomorphism.}
$$
Existence of such a field is witnessed in Lean by $\mathbb{R}$ itself; what carries the content
of Rudin's theorem, and what the goal asks for, is that the least-upper-bound property pins the
field down up to a unique isomorphism of ordered fields. Uniqueness of $e$ also gives Rudin's
second assertion for free: any embedding of $\mathbb{Q}$ is the canonical one, so $K$ contains
$\mathbb{Q}$ as an ordered subfield.
### Milestones
$$\neg\,\exists p \in \mathbb{Q},\ p^2 = 2 \qquad (\text{Example } 1.1)$$
$$\text{LUB property} \Rightarrow \text{GLB property, with } \inf B = \sup(\text{lower bounds of } B) \qquad (1.11)$$
$$x>0 \Rightarrow \exists n \in \mathbb{N},\ nx > y; \qquad x<y \Rightarrow \exists p \in \mathbb{Q},\ x<p<y \qquad (1.20)$$
$$x>0,\ n>0 \Rightarrow \exists!\, y>0,\ y^n = x \qquad (1.21)$$
$$|\bar z| = |z|,\quad |zw| = |z||w|,\quad |\operatorname{Re} z| \le |z|,\quad |z+w| \le |z|+|w| \qquad (1.33)$$
$$\Big|\sum_{j} a_j \overline{b_j}\Big|^2 \le \sum_j |a_j|^2 \sum_j |b_j|^2 \qquad (1.35)$$
$$|x \cdot y| \le |x|\,|y|, \quad |x+y| \le |x|+|y|, \quad |x-z| \le |x-y|+|y-z| \qquad (1.37)$$
## Significance
The least-upper-bound property is the only non-algebraic input to the whole of single-variable
analysis, and the chapter shows how much follows from it alone: the archimedean property, which
rules out infinitesimals; the density of $\mathbb{Q}$, which makes approximation arguments
possible; and the existence of $n$-th roots, which repairs precisely the defect exhibited by
$\sqrt{2}$. The uniqueness statement is what licenses the common practice of treating "the"
real numbers as a single object regardless of the construction used (Dedekind cuts, as in
Rudin's appendix, or Cauchy sequences).
Mathlib already contains $\mathbb{R}$, $\mathbb{C}$, and a uniqueness theorem for conditionally
complete linearly ordered fields, and several of the milestones are available there in some
form. The work this mission asks for is therefore bridging work: stating Rudin's hypotheses in
his own terms — an order with the least-upper-bound property as a *hypothesis on a set*, not as
a typeclass whose data includes a chosen supremum operator — and deriving the standard library
form from them. That bridge is what later missions in the series reuse.
## Difficulty
The individual statements are elementary, and the mathematical difficulty is genuinely low;
what makes the chapter non-mechanical in a proof assistant is the mismatch between hypothesis
and structure. Mathlib's completeness is packaged as `ConditionallyCompleteLinearOrder`, a
structure carrying `sSup` and `sInf` as data; Rudin's is a proposition about an arbitrary
ordered field. Turning the proposition into the structure (in order to invoke the library's
uniqueness theorem) is the one step where the obvious "just apply the Mathlib lemma" move does
not typecheck.
## Formalization scope
Conventions fixed by this mission:
* Rudin's least-upper-bound property is the predicate `Rudin.HasLeastUpperBoundProperty`, using
Mathlib's `IsLUB`, `BddAbove`, `lowerBounds`; no completeness typeclass is assumed of `K`.
* Ordered fields are `[Field K] [LinearOrder K] [IsStrictOrderedRing K]`, which is exactly
Rudin's Definition 1.17.
* Order-field isomorphisms are Mathlib's `≃+*o` (`OrderRingIso`), so "unique isomorphism"
is stated as `∃ e, ∀ e', e' = e`.
* $\mathbb{C}$ is Mathlib's `ℂ` and $|z|$ is the norm `‖z‖`; euclidean $k$-space is
`EuclideanSpace ℝ (Fin k)` with the inner product `inner ℝ x y`, so Rudin's $\mathbb{R}^k$
facts are norm and inner-product inequalities.
* Statements bundling several of Rudin's conclusions (1.33, 1.37) are stated as a single
conjunction, in the order the book lists them.
Nothing here is vacuous: the goal quantifies over an arbitrary ordered field satisfying the
property, and `ℝ` itself is such a field, so the hypothesis is satisfiable and the conclusion
is not automatic.
## Selected references
- Walter Rudin, *Principles of Mathematical Analysis*, 3rd edition, McGraw-Hill, 1976,
Chapter 1 (pp. 1–21) and its Appendix.
- The mathlib Community, *The Lean Mathematical Library*, CPP 2020.
https://doi.org/10.1145/3372885.3373824
10 thms2 active usersReviewed
🏆Completed
Captain: wamlart
Basic Analysis II: Stone–WeierstrassTextbook
## Motivation: approximating entire continuous functions
An approximation result must specify both the allowed approximants and the error being controlled. Matching finitely many values is different from approximating a function everywhere with one error bound. **Polynomial approximation** on a closed interval provides a model: finitely described functions can approach an arbitrary continuous function uniformly, without assuming that the function has derivatives or a convergent power-series expansion. [Lebl, Theorem 11.7.1](https://www.jirka.org/ra/html/sec_stoneweier.html).
The broader question replaces polynomials with a collection of continuous functions closed under algebraic operations. The relevant issue is which properties of that collection guarantee approximation of every continuous function. This distinguishes a useful approximation family from one that cannot detect some points or cannot approximate nonzero values at a particular point. The six targets follow the real and complex approximation results in §11.7 of Jiří Lebl’s *Basic Analysis*, Volume II. [Source section](https://www.jirka.org/ra/html/sec_stoneweier.html).
## Setting: function algebras and uniform error
A **metric space** is a set $X$ with a nonnegative, symmetric distance $d(x,y)$ that vanishes exactly when $x=y$ and satisfies the triangle inequality. It is **compact** if every cover by open sets has a finite subcover. Let $K$ be either the real numbers $\mathbb R$ or the complex numbers $\mathbb C$, and write $C(X,K)$ for the continuous functions from $X$ to $K$. Products, sums, and scalar multiplication of functions are taken pointwise. The notation $K[t]$ denotes polynomials in one indeterminate $t$ with coefficients in $K$, and $[a,b]=\{x\in\mathbb R:a\le x\le b\}$ for real endpoints $a,b$.
A **non-unital function algebra** $A$ contains the zero function and is closed under these three operations. It need not contain the constant function $1$. It **separates points** if, whenever $x\ne y$, some $g\in A$ satisfies $g(x)\ne g(y)$. It **vanishes nowhere** if, for each $x$, some $g\in A$ satisfies $g(x)\ne0$. The witness may depend on $x$; one everywhere nonzero function is not specified. A complex algebra is **self-adjoint** if it contains the pointwise complex conjugate of every member. These conventions retain the source’s non-unital setting. [Lebl, Definitions 11.7.5, 11.7.7, and 11.7.15](https://www.jirka.org/ra/html/sec_stoneweier.html).
**Uniform convergence** of $f_n$ to $f$ means
$$
\forall\varepsilon>0\;\exists N\in\mathbb N\;\forall n\ge N\;\forall x\in X,
\qquad |f_n(x)-f(x)|<\varepsilon.
$$
Here $|\cdot|$ is real absolute value or complex modulus. On compact $X$, the **closure** $\overline A$ in $C(X,K)$ uses this uniform topology; saying that $A$ is **dense** means $\overline A=C(X,K)$. [Mathlib’s compact-domain convergence interface](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/UniformSpace/CompactConvergence.lean).
## Formalization targets
The first four statements supply approximation, normalization, closure, and interpolation results. The final two state density, with the complex result as the goal. No approximation rate or degree bound is prescribed.
**Theorem 11.7.1.** For $K=\mathbb R$ and for $K=\mathbb C$, respectively,
$$
f\in C([a,b],K)\Longrightarrow
\exists(p_n)_{n\in\mathbb N}\subseteq K[t],\qquad
p_n\longrightarrow f\ \text{uniformly on }[a,b].
$$
The real clause requires real coefficients. Complex polynomials are evaluated at the complex embedding of the real argument. [Source theorem](https://www.jirka.org/ra/html/sec_stoneweier.html).
**Corollary 11.7.4.** For $a\ge0$,
$$
\exists(p_n)\subseteq\mathbb R[t],\qquad
(\forall n,\ p_n(0)=0)\ \land\
p_n\longrightarrow |\cdot|\ \text{uniformly on }[-a,a].
$$
[Source corollary](https://www.jirka.org/ra/html/sec_stoneweier.html).
**Proposition 11.7.6.** For compact metric $X$ and either scalar field,
$$
A\text{ a non-unital algebra in }C(X,K)
\Longrightarrow\overline A\text{ is such an algebra}.
$$
[Source proposition](https://www.jirka.org/ra/html/sec_stoneweier.html).
**Proposition 11.7.11.** For an arbitrary set $X$, without topology, let $A\subseteq K^X$ be an algebra separating points and vanishing nowhere. Then
$$
\forall x\ne y\;\forall c,d\in K\;\exists f\in A,
\qquad f(x)=c\ \land\ f(y)=d.
$$
Both scalar fields belong to this single target. [Source proposition](https://www.jirka.org/ra/html/sec_stoneweier.html).
**Theorem 11.7.12.** For compact metric $X$,
$$
A\subseteq C(X,\mathbb R)\text{ an algebra separating points and vanishing nowhere}
\Longrightarrow\overline A=C(X,\mathbb R).
$$
[Source theorem](https://www.jirka.org/ra/html/sec_stoneweier.html).
**Theorem 11.7.16, complex Stone–Weierstrass.** For compact metric $X$,
$$
\begin{gathered}
A\subseteq C(X,\mathbb C)\text{ a self-adjoint algebra},\\
A\text{ separates points and vanishes nowhere}
\end{gathered}
\Longrightarrow\overline A=C(X,\mathbb C).
$$
[Source theorem](https://www.jirka.org/ra/html/sec_stoneweier.html).
## Significance: density without an assumed unit
The density conclusion turns structural conditions on an approximation family into a statement about every continuous target function. Exact interpolation only controls specified values at two points; density controls all points simultaneously to any positive tolerance. The normalized absolute-value result retains a constraint on every approximating polynomial, rather than obtaining normalization only in the limit.
These are established theorems, not open conjectures. Mathlib already has machine-checked polynomial approximation, unital Stone–Weierstrass results, and non-unital algebra infrastructure. The six source-level statements also have standalone proofs checked in the pinned Lean environment. The contribution is an explicit textbook-facing non-unital formulation, with both scalar fields and the source’s normalization and interpolation clauses retained. It is not a claim to the first formalization of Stone–Weierstrass. [Polynomial approximation](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/ContinuousMap/Weierstrass.lean), [Stone–Weierstrass library](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean).
## Difficulty: local distinctions do not give uniform control
Point separation alone does not say that an algebra can approximate a nonzero value everywhere it is requested. A family may distinguish pairs of points while all its members vanish at one fixed point. Nor does interpolation at a pair of points establish a uniform error bound over an entire compact domain. These are distinct quantifier requirements.
Requiring $1\in A$ would remove the source’s non-unital case instead of resolving it. Likewise, complex scalar multiplication does not itself impose closure under conjugation. The formal difficulty is to preserve all these distinctions while connecting bundled algebras, continuous maps, and uniform closure. A direct use of the library’s unital theorem has an additional hypothesis that is absent here. [Library theorem hypotheses](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean).
## Formalization scope
Namespace `LeblRA` uses `NonUnitalSubalgebra`, `ContinuousMap`, real and complex polynomials, `TendstoUniformly`, and topological `closure`. Domains are arbitrary universe-polymorphic types, with metric and compactness structures only where the source requires them. The interpolation target has neither. Conjugation is the pointwise `star` operation on complex continuous maps.
The conventional algebra structure includes zero, but not an assumed unit. Empty compact spaces are allowed. Polynomial sequence indices start at zero. The interval approximation theorem permits arbitrary endpoints, including a singleton or an empty interval; the absolute-value corollary assumes $a\ge0$ and includes $a=0$. Neither finite-dimensional approximation spaces nor degree bounds are imposed. Replacing density by a finite-domain special case, adding a constant-one hypothesis, or assuming density itself would change the targets.
Reusable infrastructure includes non-unital subalgebras and their closures, polynomial evaluation, compact-domain uniform convergence, and real/complex continuous function spaces. The environment is Lean 4.29.0-rc3 with Mathlib revision `777aaa61dcd2a1258d2b4962dbe983ede4d23b2e`. Source-faithful alternative proofs and reusable interfaces between these existing structures are welcome; extra alias definitions are unnecessary. [Non-unital algebra structures](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean), [topological closures](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/Algebra/NonUnitalAlgebra.lean).
## Selected references
- Jiří Lebl, *Basic Analysis: Introduction to Real Analysis*, Volume II, author-published open textbook, version 6.3, 2026, §11.7. [Section text](https://www.jirka.org/ra/html/sec_stoneweier.html); [edition information](https://www.jirka.org/ra/).
- The Mathlib community, *Mathlib*, Lean mathematical library, revision `777aaa61dcd2a1258d2b4962dbe983ede4d23b2e`, 2026. [Polynomial approximation](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/ContinuousMap/Weierstrass.lean), [Stone–Weierstrass and zero-preserving continuous maps](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean), [non-unital algebra closures](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/Algebra/NonUnitalAlgebra.lean).
6 thms1 active userReviewed
🏆Completed
Captain: wamlart
Basic Analysis I: Arzelà–AscoliTextbook
## Motivation: limits of families of functions
Analysis often produces a sequence of candidate functions rather than a finished function. A useful existence theorem must say when some candidates approach a single limit everywhere with a common error bound. Ordinary boundedness is insufficient: Lebl gives bounded continuous functions on a closed interval with no uniformly convergent subsequence. The missing condition concerns how consistently the functions respond to nearby inputs. [Examples 11.6.2–11.6.4](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-6).
The Arzelà–Ascoli theorem answers this question for continuous complex-valued functions on a compact metric domain. Its uses include existence questions for differential equations and compactness properties of integral operators, both discussed in the source section. These applications require control of entire functions, not merely convergence at isolated points. [Differential-equation application](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-29), [integral-operator application](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-30).
The four targets follow §11.6 of Jiří Lebl’s *Basic Analysis*, Volume II, a textbook treatment of equicontinuity and compactness for uniform convergence. [Author’s book page](https://www.jirka.org/ra/).
## Setting: pointwise control and uniform control
A **metric space** is a set $X$ with a distance $d(x,y)$ that is nonnegative, symmetric, vanishes exactly when $x=y$, and satisfies the triangle inequality. It is **compact** when every cover by open sets has a finite subcover. Here $\mathbb C$ denotes the complex numbers, $|z|$ their absolute value, and $F_n:X\to\mathbb C$ the function at index $n\in\mathbb N$. Write $C(X,\mathbb C)$ for the continuous functions.
The sequence is **pointwise bounded** if each input has its own bound, and **uniformly bounded** if one bound works for every input and index:
$$
\forall x\in X\;\exists M_x\in\mathbb R\;\forall n\in\mathbb N,
\quad |F_n(x)|\le M_x,
$$
$$
\exists M\in\mathbb R\;\forall n\in\mathbb N\;\forall x\in X,
\quad |F_n(x)|\le M.
$$
It is **uniformly equicontinuous** when
$$
\forall\varepsilon>0\;\exists\delta>0\;\forall x,y\in X\;\forall n\in\mathbb N,
\quad d(x,y)<\delta\Longrightarrow |F_n(x)-F_n(y)|<\varepsilon.
$$
Thus $\delta$ cannot depend on the function index or the points. These are the source’s distinct boundedness and common-continuity conditions. [Definition 11.6.1](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-4), [Definition 11.6.6](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-13).
A **subsequence** has the form $F_{\varphi(n)}$, where $\varphi:\mathbb N\to\mathbb N$ is strictly increasing. **Pointwise convergence** to $f$ means convergence to $f(x)$ separately for every $x$. **Uniform convergence** means that for each $\varepsilon>0$ there is one $N$ such that $|F_n(x)-f(x)|<\varepsilon$ for every $n\ge N$ and every $x$. A subset $D\subseteq X$ is **dense** if its closure $\overline D$ is all of $X$.
## Formalization targets
The supporting targets distinguish countable domains, a necessary continuity condition, and the density property of compact metric spaces. The final target combines the hypotheses into uniform-convergence compactness; no quantitative rate is prescribed.
**Proposition 11.6.5.** For an arbitrary countable set $X$, without any topology or continuity assumption,
$$
F_n\text{ pointwise bounded}
\Longrightarrow
\exists\varphi,f,\quad
\varphi\text{ strictly increasing}\quad\land\quad
\forall x\in X,\ F_{\varphi(n)}(x)\longrightarrow f(x).
$$
[Source proposition](https://www.jirka.org/ra/html/sec_arzelaascoli.html#prop_subsequenceoncountableX).
**Proposition 11.6.7.** For compact metric $X$,
$$
F_n\in C(X,\mathbb C),\quad F_n\longrightarrow f\text{ uniformly}
\Longrightarrow F_n\text{ uniformly equicontinuous}.
$$
[Source proposition](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-16).
**Proposition 11.6.8.** Every compact metric space satisfies
$$
\exists D\subseteq X,\quad D\text{ countable}\ \land\ \overline D=X.
$$
[Source proposition](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-18).
**Theorem 11.6.9, Arzelà–Ascoli.** Suppose $X$ is compact metric, $F_n\in C(X,\mathbb C)$, and the sequence is pointwise bounded and uniformly equicontinuous. The complete conclusion is
$$
\left(\exists M\in\mathbb R\;\forall n,x,\ |F_n(x)|\le M\right)
\quad\land\quad
\left(\exists\varphi:\mathbb N\to\mathbb N\;\exists f\in C(X,\mathbb C),\quad
\varphi\text{ strictly increasing},\quad
F_{\varphi(n)}\longrightarrow f\text{ uniformly}\right).
$$
Both the global bound and the subsequence conclusion are required. The limit belongs to $C(X,\mathbb C)$, so its continuity is explicit. [Source theorem](https://www.jirka.org/ra/html/sec_arzelaascoli.html#thm_arzelaascoli).
## Significance: a compactness criterion with explicit hypotheses
The result supplies a uniform limit under hypotheses that concern individual inputs and a shared continuity condition. It therefore identifies a usable replacement for boundedness alone in a space of functions. The distinction matters downstream: retaining only pointwise convergence would not provide a common error bound across the domain, and assuming uniform boundedness in advance would discard one of the theorem’s conclusions. [Lebl, Theorem 11.6.9](https://www.jirka.org/ra/html/sec_arzelaascoli.html#thm_arzelaascoli).
These are established theorems, not open conjectures. Mathlib already contains machine-checked general Arzelà–Ascoli results, compactness and convergent-subsequence infrastructure, and the countable-dense-set interface. The four source-level statements also have ordinary local Lean proofs checked against their exact types. The contribution is a faithful textbook-facing formulation that keeps the distinct hypotheses, quantifier order, arbitrary countable domain, and both capstone conclusions visible. It is not a claim to the first formalization of Arzelà–Ascoli. [Mathlib Ascoli development](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/UniformSpace/Ascoli.lean), [countable dense subsets](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/Bases.lean).
## Difficulty: preserving the quantifier order
Convergence at every point does not automatically mean uniform convergence. A permissible index threshold may depend on the point, and different pointwise limits may require different subsequences. Likewise, separate continuity of every $F_n$ does not give a single $\delta$ valid for all $n$. Replacing these statements with their uniform versions silently changes the problem. Lebl’s bounded sequence $x\mapsto x^n$ on $[0,1]$ already rules out the naive implication from bounded continuous functions to a uniformly convergent subsequence. [Example 11.6.3](https://www.jirka.org/ra/html/sec_arzelaascoli.html#sec_arzelaascoli-7).
The formal challenge is to retain these distinctions across the representations of functions, convergence, and compactness. In particular, the countable-domain proposition must not acquire a compactness assumption, while the capstone must not acquire global bounds as an extra premise.
## Formalization scope
The development uses namespace `LeblRA`, arbitrary universe-polymorphic domain types, Lean’s complex numbers, and zero-based natural-number indices. Zero-based indexing only reindexes the source’s sequence starting at one. A strictly increasing map is represented by `StrictMono`; pointwise limits use `Tendsto` at `atTop`, uniform limits use `TendstoUniformly`, and density uses `Dense`. Finite and empty domains remain allowed.
The boundedness and equicontinuity hypotheses are written as explicit quantifiers, not new custom definitions. No claim may be replaced by a finite-domain special case, a vacuous hypothesis, or a statement that assumes its uniform conclusion.
Reusable infrastructure consists of complex norms, metric and compact spaces, continuous maps, uniform convergence, equicontinuity, and sequence compactness. The pinned environment is Lean 4.29.0-rc3 with Mathlib revision `777aaa61dcd2a1258d2b4962dbe983ede4d23b2e`. Source-faithful alternative proofs and explicit equivalences between the raw conditions and library predicates are welcome; applications beyond the four numbered targets are outside this scope. [Uniform-convergence interface](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/UniformSpace/UniformConvergence.lean), [sequence compactness](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/Sequences.lean).
## Selected references
- Jiří Lebl, *Basic Analysis: Introduction to Real Analysis*, Volume II, author-published open textbook, version 6.3, 2026, §11.6. [Section text](https://www.jirka.org/ra/html/sec_arzelaascoli.html); [edition information](https://www.jirka.org/ra/).
- The Mathlib community, *Mathlib*, Lean mathematical library, revision `777aaa61dcd2a1258d2b4962dbe983ede4d23b2e`, 2026. [General Ascoli theorems](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/UniformSpace/Ascoli.lean), [uniform convergence](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/UniformSpace/UniformConvergence.lean), [topological bases and separability](https://github.com/leanprover-community/mathlib4/blob/777aaa61dcd2a1258d2b4962dbe983ede4d23b2e/Mathlib/Topology/Bases.lean).