Analysis

20 missions · 15 completed

Missions

Completed

Captain: lisamegawatts

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

Captain: Lucas

Formal Conjectures Portfolio: Bateman-Horn and CompanionsOpen Problem

## 1. Motivation Wikipedia's pages on open problems are, for many mathematicians, the first contact with a conjecture: a one-paragraph statement, a short history, a list of partial results. The [Formal Conjectures](https://github.com/google-deepmind/formal-conjectures) library (Google DeepMind, Apache-2.0) turned a large part of that material into Lean 4 statements, so that the conjectures can be attacked — and, just as importantly, *stated unambiguously* — by machine. This mission ports a coherent slice of that material to Prove2Me. It is deliberately a **portfolio mission**: the goal theorem is the Bateman–Horn conjecture, the strongest single statement in the collection, and the milestone list gathers the other conjectures and the landmark theorems that surround them. Some milestones are genuine steps toward the goal (the Bunyakovsky conjecture is literally the one-polynomial case); most are independent open problems from other fields, grouped here because they share a source, a level of difficulty, and a need for faithful formal statements. **A reader should not assume that proving a milestone advances the goal theorem.** The mission's value is that every statement in it has been written against the same Mathlib revision, checked to compile, and documented well enough to be attacked. A rough timeline of the collection's landmarks: - 1947 — Mills: a real $A>1$ with $\lfloor A^{3^n}\rfloor$ always prime. - 1962 — Radó: the busy beaver function outgrows every computable function. - 1971 — Davies: planar Kakeya sets have Hausdorff dimension $2$. - 1978 — Apéry: $\zeta(3)$ is irrational. - 1985 — Read (after Enflo, 1981): an operator on $\ell^1$ with no nontrivial closed invariant subspace. - 2001 — Zudilin: one of $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational. - 2002 — Mihăilescu: $8$ and $9$ are the only consecutive perfect powers (Catalan's conjecture). - 2009 / 2021 — Dvir; Bukh–Chao: the finite-field Kakeya bound and its sharp density constant. - 2021 — Gardam: Kaplansky's *unit* conjecture is false (its zero-divisor and idempotent companions remain open). - 2024 — Saito: Mills' constant is irrational; bbchallenge: $\mathrm{BB}(5)=47\,176\,870$. - 2025 — Wang–Zahl: the Kakeya set conjecture in $\mathbb{R}^3$. ## 2. Setting The goal theorem concerns prime values of polynomials. Fix a finite set $S=\{f_1,\dots,f_k\}\subseteq\mathbb{Z}[X]$ of distinct polynomials. Say that $f$ satisfies the **Bunyakovsky condition** if its leading coefficient is positive, $\deg f\ge 1$, and $f$ is irreducible over $\mathbb{Z}$; say that $S$ satisfies the **Schinzel condition** if for every prime $p$ there is an integer $n$ with $p\nmid f_1(n)\cdots f_k(n)$ — i.e. no fixed prime divides the product at every argument. For a prime $p$ let $\omega_p(S)$ be the number of residue classes $n \bmod p$ at which some $f_i$ vanishes, let $D=\prod_i \deg f_i$, and let $$\pi_S(x)=\#\{\,n\le x : |f_i(n)| \text{ is prime for every } i\,\}.$$ The **Bateman–Horn constant** is the (conditionally convergent) Euler product $$C=\lim_{N\to\infty}\ \prod_{p<N}\Big(1-\tfrac1p\Big)^{-k}\Big(1-\tfrac{\omega_p(S)}{p}\Big).$$ The other groups use their own vocabulary, each fixed in a definition item of this mission: Kakeya sets in $\mathbb{R}^n$ and over $\mathbb{F}_q$; Mills' property $\lfloor A^{3^n}\rfloor \in \mathbb{P}$; Wagstaff primes and Catalan–Mersenne numbers; polynomial self-maps and their Jacobian matrix; nontrivial closed invariant subspaces; linear extensions of a finite poset; Catalan's constant; and an explicit two-symbol Turing machine model with its maximum-shifts function $\mathrm{BB}$. ## 3. Target The goal theorem is the Bateman–Horn asymptotic: under the Bunyakovsky and Schinzel hypotheses, $C$ exists and is positive and $$\pi_S(x)\ \sim\ \frac{C}{D}\,\frac{x}{(\log x)^{k}}\qquad (x\to\infty).$$ Weaker statements in the same direction appear as milestones, first of all Bunyakovsky's conjecture: under the same hypotheses with $k=1$, $f$ takes prime values infinitely often. The remaining milestones are listed in the milestone panel and are grouped by subject: Diophantine equations (Brocard, Pillai, Lebesgue–Nagell, Catalan/Mihăilescu), Mersenne-type primality (New Mersenne, infinitude of Mersenne primes, Catalan–Mersenne), prime-representing constants (Mills), geometric measure theory (Kakeya in $\mathbb{R}^n$, Kakeya over $\mathbb{F}_q$, Falconer), operator theory (invariant subspace problem and Read's $\ell^1$ counterexample), group algebras (Kaplansky's zero-divisor and idempotent conjectures), affine algebraic geometry (the two-variable Jacobian conjecture), irrationality and transcendence ($\zeta(5)$, all odd zeta values, Zudilin's theorem, $e+\pi$, $e\pi$, $\gamma$, Catalan's constant), order theory (the $1/3$–$2/3$ conjecture), and computability (Radó's theorem). ## 4. Significance *The results themselves.* Bateman–Horn is the quantitative form of Schinzel's hypothesis H: it contains the twin prime conjecture, the infinitude of primes of the form $n^2+1$, and Bunyakovsky as special cases, and it is the standard heuristic behind prime-counting predictions. The other targets are each the headline question of their area: whether every bounded Hilbert-space operator has an invariant subspace; whether group algebras of torsion-free groups are domains; whether Kakeya sets must have full dimension. The solved milestones (Mihăilescu, Davies, Dvir, Zudilin, Read, Saito, Radó) are landmarks whose formal proofs would be significant library contributions in their own right. *Formalizing them.* None of the open statements is expected to fall here; the concrete deliverable is a set of faithful, compiling, reusable statements plus formal proofs of the solved milestones, most of which are not in Mathlib today. Several are realistically in reach: the finite-field Kakeya bound (Dvir's polynomial method is short), the elementary fact that $\pi+e$ and $\pi e$ cannot both be algebraic, and Radó's diagonal argument. ## 5. Difficulty For Bateman–Horn, the obstruction is visible already for $k=1$, $\deg f = 2$: sieve methods bound $\pi_S(x)$ from above by a constant times the conjectured main term and produce almost-primes, but the parity problem blocks every known sieve from producing a single prime value of an irreducible quadratic. The conditional convergence of the Euler product is a second, smaller trap: the product over $p<N$ must be taken in order, so any reformulation as an unordered infinite product changes the statement. Each other group has its own obstruction, and they do not transfer: the parity problem says nothing about Kakeya, where the difficulty is that dimension is not stable under the natural compactness arguments, nor about the invariant subspace problem, where the known counterexamples on $\ell^1$ show that no soft argument can work. ## 6. Formalization scope Conventions this mission commits to, all fixed in the definition items: - Polynomials are elements of `ℤ[X]`; primality of a polynomial value is primality of its absolute value, and the counting function ranges over natural numbers $n \le \lfloor x\rfloor$. - The Bateman–Horn constant is the limit of the *ordered* partial products over $p<N$, not an unordered infinite product. - Kakeya sets carry no compactness or measurability hypothesis, matching the source; the conjecture is stated as an equality of Hausdorff dimensions in $[0,\infty]$. - Falconer's hypothesis is written $d < 2\dim_H E$ to avoid division in $[0,\infty]$. - Torsion-freeness of a group is spelled out as "every element of finite order is the identity", which is the hypothesis the source intends (it is weaker than Mathlib's `IsMulTorsionFree`). - Linear extensions are order-preserving bijections onto $\{0,\dots,|P|-1\}$, and probabilities are quotients of set cardinalities in $\mathbb{Q}$. - The busy beaver model is an explicit $n$-state, $2$-symbol machine with a bi-infinite Boolean tape; $\mathrm{BB}$ counts transitions performed (maximum shifts), the halting transition included, and $\mathrm{BB}(0)=0$. - Several source statements are phrased as "is $X$ true?" with an unknown answer. Prove2Me statements must be definite, so each such question is recorded in its **affirmative** form (e.g. "$e+\pi$ is irrational"); a solver who can refute one should submit a disproof. The one question with no statable answer, "what is $\mathrm{BB}(6)$?", is replaced by Radó's growth theorem rather than guessed at. - Nothing here is vacuous: each hypothesis set is satisfiable (e.g. closed unit balls are Kakeya sets, and $X^2+1$ satisfies the Bunyakovsky and Schinzel conditions). Contributions welcome: proofs of the solved milestones; sharper variants; and additional faithful statements from the same source library, which contains far more than fits in one mission. ## 7. Selected references - P. T. Bateman and R. A. Horn, *A heuristic asymptotic formula concerning the distribution of prime numbers*, Math. Comp. 16 (1962), 363–367. [DOI](https://doi.org/10.1090/S0025-5718-1962-0148632-7) - T. Radó, *On non-computable functions*, Bell System Tech. J. 41 (1962), 877–884. [DOI](https://doi.org/10.1002/j.1538-7305.1962.tb00480.x) - R. O. Davies, *Some remarks on the Kakeya problem*, Math. Proc. Cambridge Philos. Soc. 69 (1971), 417–421. [DOI](https://doi.org/10.1017/S0305004100046867) - C. J. Read, *A solution to the invariant subspace problem on the space $\ell_1$*, Bull. London Math. Soc. 17 (1985), 305–317. [DOI](https://doi.org/10.1112/blms/17.4.305) - K. Falconer, *On the Hausdorff dimensions of distance sets*, Mathematika 32 (1985), 206–212. [DOI](https://doi.org/10.1112/S0025579300010998) - W. Zudilin, *One of the numbers $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational*, Russian Math. Surveys 56 (2001), 774–776. [DOI](https://doi.org/10.1070/RM2001v056n04ABEH000427) - P. Mihăilescu, *Primary cyclotomic units and a proof of Catalan's conjecture*, J. reine angew. Math. 572 (2004), 167–195. [DOI](https://doi.org/10.1515/crll.2004.048) - Z. Dvir, *On the size of Kakeya sets in finite fields*, J. Amer. Math. Soc. 22 (2009), 1093–1097. [DOI](https://doi.org/10.1090/S0894-0347-08-00607-3) - B. Bukh and T.-W. Chao, *Sharp density bounds on the finite field Kakeya problem*, Discrete Analysis 26 (2021). [DOI](https://doi.org/10.19086/da.30071) - G. Gardam, *A counterexample to the unit conjecture for group rings*, Ann. of Math. 194 (2021), 967–979. [DOI](https://doi.org/10.4007/annals.2021.194.3.9) - K. Saito, *Mills' constant is irrational*, Mathematika 71 (2025), e70027. [arXiv:2404.19461](https://arxiv.org/abs/2404.19461) - H. Wang and J. Zahl, *Volume estimates for unions of convex sets, and the Kakeya set conjecture in three dimensions*, [arXiv:2502.17655](https://arxiv.org/abs/2502.17655) - Google DeepMind, *Formal Conjectures*, Apache-2.0, [github.com/google-deepmind/formal-conjectures](https://github.com/google-deepmind/formal-conjectures) --- *Provenance note.* The Lean statements in this mission are adaptations of the Formal Conjectures library (Apache-2.0), rewritten to depend only on Mathlib and on this mission's own definition items, and checked to compile against the platform's Mathlib revision. Each draft item carries a read-back; **those read-backs are non-blind** — they were written by the same agent that drafted the statements, and each says so in its first line. They are documentation, not independent testimony.

42 thms2 active usersReviewed

Completed

Captain: abcdefg

Weighted Root Integral Identity for Ordered Positive RealsTextbook

## Selected references https://math.stackexchange.com/questions/4244874/can-we-prove-am-gm-inequality-using-these-integrals

7 thms2 active usersReviewed

Captain: Lucas

## 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

Captain: Lucas

Hairer: A Theory of Regularity Structures I — The Reconstruction TheoremResearch Paper

## Motivation Several equations of mathematical physics are written down formally but have no classical meaning as stated. The dynamical $\Phi^4_3$ model $\partial_t u = \Delta u - u^3 + \xi$ on the three-dimensional torus, the KPZ equation $\partial_t h = \partial_x^2 h + (\partial_x h)^2 - \infty + \xi$, and the parabolic Anderson model $\partial_t u = \Delta u + u\,\xi$ all require multiplying a distribution of negative regularity by itself, an operation that Schwartz distribution theory does not provide. Martin Hairer's *A theory of regularity structures* (Invent. Math. 198 (2014) 269–504, [arXiv:1303.5113](https://arxiv.org/abs/1303.5113)) develops a calculus in which such products, and the resulting fixed-point problems, become well posed. The line of work leading to it is short and well documented: rough path theory (Lyons, 1998) solved the analogous problem for controlled ordinary differential equations driven by irregular signals; Gubinelli's controlled paths (2004) and branched rough paths (2010) reorganised it around local expansions; Hairer's theory extends that idea from paths to fields on $\mathbb{R}^d$ with anisotropic (e.g. parabolic) scaling. Paracontrolled distributions (Gubinelli–Imkeller–Perkowski, 2015) give an alternative route to some of the same equations. The algebraic and probabilistic infrastructure around regularity structures has since been systematised (Bruned–Hairer–Zambotti, 2019; Chandra–Hairer, 2016), but the analytic core is still the 2014 paper. ## Setting Fix a dimension $d$ and a **scaling** $s = (s_1,\dots,s_d)$ of positive integers, with $|s| = \sum_i s_i$, and put $\|x\|_s = \max_i |x_i|^{1/s_i}$. For $\delta > 0$, a point $x \in \mathbb{R}^d$ and a test function $\varphi$, the **rescaled test function** is $$ (S^{\delta}_{s,x}\varphi)(y) = \delta^{-|s|}\,\varphi\!\left(\frac{y_1-x_1}{\delta^{s_1}},\dots,\frac{y_d-x_d}{\delta^{s_d}}\right). $$ Write $\mathcal{B}^r_{s,0}$ for the set of test functions supported in $\{\|y\|_s \le 1\}$ whose derivatives up to order $r$ are bounded by $1$. For $\alpha<0$, a distribution $\xi$ belongs to the Hölder–Besov space $\mathcal{C}^\alpha_s$ if, on every compact set $K$, $|\langle \xi, S^{\delta}_{s,x}\eta\rangle| \le C\delta^{\alpha}$ uniformly over $x\in K$, $\delta \in (0,1]$ and $\eta \in \mathcal{B}^r_{s,0}$ with $r=-\lfloor\alpha\rfloor$. A **regularity structure** $(A,T,G)$ consists of an index set $A \subseteq \mathbb{R}$ containing $0$, bounded below and locally finite; a graded vector space $T = \bigoplus_{\alpha\in A} T_\alpha$ with $T_0 \cong \mathbb{R}$ spanned by a unit $\mathbf{1}$; and a group $G$ of linear operators on $T$ with $\Gamma a - a \in \bigoplus_{\beta<\alpha}T_\beta$ for $a \in T_\alpha$, and $\Gamma\mathbf{1} = \mathbf{1}$. Elements of $T_\alpha$ are "homogeneous of order $\alpha$": they are placeholders for objects whose size at scale $\varepsilon$ is $\varepsilon^{\alpha}$. A **model** $(\Pi,\Gamma)$ assigns to each point $x$ a linear map $\Pi_x : T \to \mathcal{D}'(\mathbb{R}^d)$ and to each pair $(x,y)$ an element $\Gamma_{xy}\in G$, subject to $\Gamma_{xx}=\mathrm{id}$, $\Gamma_{xy}\Gamma_{yz}=\Gamma_{xz}$, $\Pi_y = \Pi_x\circ\Gamma_{xy}$ and, locally uniformly, the analytic bounds $$ |(\Pi_x a)(S^{\delta}_{s,x}\varphi)| \lesssim \|a\|_\ell\,\delta^{\ell}, \qquad \|\Gamma_{xy}a\|_m \lesssim \|a\|_\ell\,\|x-y\|_s^{\ell-m}, \qquad a \in T_\ell,\; m<\ell. $$ A **modelled distribution** of order $\gamma$ is a function $f : \mathbb{R}^d \to T_{<\gamma}$ such that on every compact $K$ $$ |||f|||_{\gamma;K} = \sup_{x\in K,\ \beta<\gamma}\|f(x)\|_\beta + \sup_{\substack{x,y \in K,\ \|x-y\|_s\le 1 \\ \beta<\gamma}} \frac{\|f(x)-\Gamma_{xy}f(y)\|_\beta}{\|x-y\|_s^{\gamma-\beta}} < \infty; $$ the space of these is $\mathcal{D}^\gamma$, and $\mathcal{D}^\gamma(V)$ if $f$ takes values in a **sector** $V$, that is, a graded $G$-invariant subspace vanishing in degrees below its regularity. ## Formalization targets ### Goal — reconstruction theorem, Theorem 3.10 for $\gamma>0$ With $\alpha = \min A < 0$ and $r$ the order attached to $A$, for every $f \in \mathcal{D}^\gamma$ with $\gamma>0$ there is a **unique** distribution $\mathcal{R}f \in \mathcal{C}^\alpha_s$ with $$ \big|(\mathcal{R}f - \Pi_x f(x))(S^{\delta}_{s,x}\eta)\big| \lesssim \delta^{\gamma} \qquad (x \in K,\ \delta\in(0,1],\ \eta\in\mathcal{B}^r_{s,0}). $$ The statement asserts only the shape of the estimate — a constant per compact set — and so is insensitive to any later sharpening of constants. ### Milestone level — the calculus around the reconstruction operator The uniqueness clause of Theorem 3.10 in isolation; the existence of a *linear* reconstruction operator for arbitrary $\gamma \in \mathbb{R}$ (for $\gamma\le 0$ the bound no longer pins it down); Corollary 3.16, improving the regularity of $\mathcal{R}f$ to $\mathcal{C}^\beta_s$ when $f$ takes values in a sector of regularity $\beta$; Proposition 3.31, that for $\nu>0$ the action of $\Pi$ on $T_\nu$ is determined by $\Gamma$ and by $\Pi$ in lower homogeneities; and Theorem 4.7, that the truncated pointwise product of $f_1 \in \mathcal{D}^{\gamma_1}(V)$ and $f_2\in\mathcal{D}^{\gamma_2}(W)$ lies in $\mathcal{D}^{\gamma}$ with $\gamma = (\gamma_1+\alpha_2)\wedge(\gamma_2+\alpha_1)$. ## Significance The reconstruction theorem is what turns a book-keeping device into analysis: it says that a coherent family of local expansions, indexed by base point, glues to a single genuine distribution, with an error controlled by the order of the expansion. Every subsequent operation in the theory — multiplication (Theorem 4.7), composition with smooth functions (Theorem 4.16), the multi-level Schauder estimate (Theorem 5.12), and the fixed-point theorem for singular SPDEs (Theorem 7.8) — is stated and used through it. Without it, the abstract spaces $\mathcal{D}^\gamma$ carry no information about actual distributions. Regularity structures are not currently available in Mathlib, and neither are the anisotropic Hölder–Besov spaces $\mathcal{C}^\alpha_s$ that the theory is phrased in. The result itself is proved in the literature; the work this mission asks for is a machine-checked proof of the known argument, together with the reusable definitions it needs. The formal development is a prerequisite for anything downstream — Schauder estimates, the fixed-point theory, or the $\Phi^4_3$ and PAM convergence results of §10 — which are natural follow-on missions rather than part of this one. ## Difficulty The naive construction fails: setting $\mathcal{R}f := \Pi_x f(x)$ for a fixed $x$ is wrong away from $x$, and the pointwise limit $\lim_{\delta\to0}$ of localisations of $\Pi_x f(x)$ around each $x$ does not obviously exist, because the objects being glued are distributions of negative order, not functions, so there is no value to take and no partition-of-unity argument that respects the scaling. Hairer's proof goes through a wavelet multiresolution analysis adapted to the scaling $s$: one defines the candidate on each dyadic level by pairing with wavelets centred at grid points, and shows the resulting sequence is Cauchy using the $\mathcal{D}^\gamma$ bound level by level. A formalization therefore needs either a scaled wavelet basis with Daubechies-type regularity (Theorem 3.17 in the paper) or a substitute for it; this, and the uniform-in-scale bookkeeping, is where the effort lies. Uniqueness for $\gamma>0$ is by contrast short, and is listed as a separate milestone. ## Formalization scope The development commits to the following conventions, fixed in the mission's definition files. Points of $\mathbb{R}^d$ are `Fin d → ℝ`. Test functions are smooth and compactly supported, forming a submodule of all real-valued functions, and a distribution is a linear functional on that submodule; the pairing is extended by $0$ to non-test functions, and a lemma in the definition file certifies that rescaling maps test functions to test functions, so no statement is vacuous for that reason. Hairer's $\mathcal{B}^r_{s,0}$ consists of $C^r$ functions; here it consists of smooth ones, which defines the same spaces $\mathcal{C}^\alpha_s$. The model space is the algebraic direct sum $\bigoplus_{a\in A} T_a$ over the index set, each $T_a$ a real normed space, with $Q_a$ the corresponding projection; the structure group is a subgroup of the linear automorphisms of that direct sum. Sectors are families of subspaces $V_a \subseteq T_a$; Hairer's requirement that each $V_a$ admit a complement is automatic in this algebraic setting. The integer $r$ appearing in the model bounds is the smallest one with $\ell > -r$ for all $\ell \in A$, which is part of the definition of a model rather than a free parameter. All statements quantify over an arbitrary regularity structure, an arbitrary model, and an arbitrary compact set, so they are not satisfiable by a degenerate choice; the goal in particular claims existence, membership in $\mathcal{C}^\alpha_s$, and uniqueness simultaneously. Infrastructure that a complete proof will need, and which is reusable beyond this mission: scaled wavelet bases on $\mathbb{R}^d$, the elementary theory of $\mathcal{C}^\alpha_s$ (including the positive-regularity case), and basic operations on compactly supported test functions under anisotropic rescaling. Contributions of any of these as separate lemmas are welcome, as are reductions that decompose the goal into wavelet-level estimates. ## Selected references - M. Hairer, *A theory of regularity structures*, Inventiones Mathematicae 198 (2014) 269–504. [arXiv:1303.5113](https://arxiv.org/abs/1303.5113), [DOI:10.1007/s00222-014-0505-4](https://doi.org/10.1007/s00222-014-0505-4) - T. Lyons, *Differential equations driven by rough signals*, Revista Matemática Iberoamericana 14 (1998) 215–310. [DOI:10.4171/RMI/240](https://doi.org/10.4171/RMI/240) - M. Gubinelli, *Controlling rough paths*, Journal of Functional Analysis 216 (2004) 86–140. [arXiv:math/0306433](https://arxiv.org/abs/math/0306433) - M. Gubinelli, P. Imkeller, N. Perkowski, *Paracontrolled distributions and singular PDEs*, Forum of Mathematics Pi 3 (2015) e6. [arXiv:1210.2684](https://arxiv.org/abs/1210.2684) - Y. Bruned, M. Hairer, L. Zambotti, *Algebraic renormalisation of regularity structures*, Inventiones Mathematicae 215 (2019) 1039–1156. [arXiv:1610.08468](https://arxiv.org/abs/1610.08468)

13 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

Captain: shivm

Irrationality and transcendence of Euler's constantOpen Problem

## What the constant is Euler's constant $\gamma$ measures the gap between the harmonic numbers and the logarithm: $$\gamma \;=\; \lim_{n\to\infty}\left(\sum_{k=1}^{n}\frac{1}{k} \;-\; \log n\right) \;=\; 0.5772156649\ldots$$ It appears wherever the harmonic series is compared against an integral, and it is the value at $1$ of the digamma function, $\psi(1) = -\gamma$, equivalently $\gamma = -\Gamma'(1)$. Among the classical constants of analysis it is the conspicuous one whose arithmetic nature is unknown. ## What is being asked For $\pi$ and $e$ the arithmetic questions were settled long ago: both are irrational and transcendental. For $\gamma$, **neither is known**. It is not known whether $\gamma$ is irrational, and a fortiori not whether it is transcendental, though it is universally expected to be both. The goal theorem of this mission is transcendence, $$\gamma \notin \overline{\mathbb{Q}},$$ with irrationality carried as a separate, weaker target — a proof of transcendence yields irrationality immediately, but not conversely, and irrationality alone would already be a landmark. ## What is actually known Progress has come in three forms, and the milestones below formalize each. **Conditional bounds on a putative denominator.** If $\gamma$ were rational, its denominator would have to be enormous. Brent and McMillan (1980), computing $\gamma$ to $30{,}000$ places by an algorithm built on modified Bessel functions, showed any denominator exceeds $10^{15000}$; a continued-fraction analysis by Papanikolaou (1997) pushed this past $10^{244663}$. These are not steps toward a proof so much as a measurement of how far brute computation can go. **Disjunctive results.** The strongest unconditional statements pair $\gamma$ with the Euler–Gompertz constant $$\delta \;=\; \int_0^{\infty} \frac{e^{-u}}{1+u}\, du \;=\; 0.5963473623\ldots$$ Aptekarev, building on work of Mahler and Shidlovskii, observed that **at least one of $\gamma$ and $\delta$ is irrational**. Rivoal later strengthened this to **at least one of them is transcendental**. Neither argument isolates which, and that is precisely the obstruction: the Padé-approximation machinery that controls the pair does not separate them. **Irrationality criteria.** Sondow, adapting Beukers' treatment of Apéry's theorem for $\zeta(3)$, gave criteria equivalent to the irrationality of $\gamma$ in terms of the fractional parts of certain integer sequences. They reformulate the problem rather than resolve it. ## Timeline - **1734** — Euler introduces the constant and computes it to six decimals. - **1790s–1800s** — Mascheroni computes further digits; the constant acquires its second name. - **1873** — Hermite proves $e$ transcendental; **1882** — Lindemann does the same for $\pi$. The methods do not reach $\gamma$. - **1980** — Brent and McMillan: if $\gamma = p/q$ then $q > 10^{15000}$. - **1997** — Papanikolaou: the same denominator exceeds $10^{244663}$. - **2009** — Aptekarev: at least one of $\gamma$, $\delta$ is irrational. - **2012** — Rivoal: at least one of $\gamma$, $\delta$ is transcendental. - **2010s** — Murty, Saradha and others obtain transcendence results for generalized Euler–Lehmer constants, again leaving $\gamma$ itself untouched. ## Formalization notes Mathlib provides the constant as `Real.eulerMascheroniConstant`, defined as the limit of $\sum_{k\le n} 1/k - \log n$, together with the identifications $\psi(1) = -\gamma$ and $\gamma = -\Gamma'(1)$ and the numeric bounds $1/2 < \gamma < 2/3$. `Irrational` and `Transcendental ℚ` are Mathlib's standard predicates. The Euler–Gompertz constant is not in Mathlib and is supplied here as a mission definition.

60 thms3 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).

4 thms1 active userReviewed