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.

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, integral-operator application.

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.

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, Definition 11.6.6.

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.

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.

Proposition 11.6.8. Every compact metric space satisfies

$$\exists D\subseteq X,\quad D\text{ countable}\ \land\ \overline D=X.$$

Source proposition.

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.

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.

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, countable dense subsets.

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.

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, sequence compactness.

Selected references

• Jiří Lebl, Basic Analysis: Introduction to Real Analysis, Volume II, author-published open textbook, version 6.3, 2026, §11.6. Section text; edition information.
• The Mathlib community, Mathlib, Lean mathematical library, revision 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e, 2026. General Ascoli theorems, uniform convergence, topological bases and separability.