Analysis

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 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
• T. Radó, On non-computable functions, Bell System Tech. J. 41 (1962), 877–884. DOI
• R. O. Davies, Some remarks on the Kakeya problem, Math. Proc. Cambridge Philos. Soc. 69 (1971), 417–421. DOI
• C. J. Read, A solution to the invariant subspace problem on the space $\ell_1$, Bull. London Math. Soc. 17 (1985), 305–317. DOI
• K. Falconer, On the Hausdorff dimensions of distance sets, Mathematika 32 (1985), 206–212. DOI
• W. Zudilin, One of the numbers $\zeta(5),\zeta(7),\zeta(9),\zeta(11)$ is irrational, Russian Math. Surveys 56 (2001), 774–776. DOI
• P. Mihăilescu, Primary cyclotomic units and a proof of Catalan's conjecture, J. reine angew. Math. 572 (2004), 167–195. DOI
• Z. Dvir, On the size of Kakeya sets in finite fields, J. Amer. Math. Soc. 22 (2009), 1093–1097. DOI
• B. Bukh and T.-W. Chao, Sharp density bounds on the finite field Kakeya problem, Discrete Analysis 26 (2021). DOI
• G. Gardam, A counterexample to the unit conjecture for group rings, Ann. of Math. 194 (2021), 967–979. DOI
• K. Saito, Mills' constant is irrational, Mathematika 71 (2025), e70027. arXiv: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
• Google DeepMind, Formal Conjectures, Apache-2.0, 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.

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.

Motivation

The iteration of a rational map $f:\hat{\mathbb C}\to\hat{\mathbb C}$ of the Riemann sphere is the model problem of holomorphic dynamics. The subject was founded by Fatou and Julia around 1918–1920, who split the sphere into a region of stable behaviour and a region of chaotic behaviour, and it was revived in the 1980s by Douady, Hubbard, Sullivan and Thurston. John Milnor's textbook Dynamics in One Complex Variable (3rd ed., Princeton, 2006) is the standard graduate introduction. This mission, the first of a series on the book, formalizes the chain of results that leads from Montel's theorem on normal families to Sullivan's theorem that rational maps have no wandering domains.

Timeline of the results formalized here:

• 1912–1927, Montel. Families of holomorphic maps omitting three values are normal (Milnor, Theorem 3.7).
• 1918–1920, Fatou and Julia. Definition of the Fatou and Julia sets; the Julia set of a map of degree $d\ge2$ is nonempty and equals the closure of the repelling periodic points (Milnor, Lemma 4.8 and Theorem 14.1).
• 1920s–1942. Fatou classified the possible dynamics on an invariant Fatou component; Siegel (1942) showed that Siegel disks exist, and Herman (1979) constructed Herman rings. Together these give the four cases of Milnor's Theorem 16.1.
• 1985, Sullivan. Every Fatou component is eventually periodic (Sullivan, Quasiconformal homeomorphisms and dynamics I, Ann. of Math. 122 (1985); Milnor, Theorem 16.4).

Setting

The Riemann sphere is $\hat{\mathbb C}=\mathbb C\cup\{\infty\}$, the one-point compactification of $\mathbb C$, with the two coordinates $z$ (near finite points) and $1/z$ (near $\infty$). A rational map is $f=p/q$ with $p,q$ coprime complex polynomials, $q\neq0$; it acts on $\hat{\mathbb C}$ in the usual way, and its degree is $d=\max(\deg p,\deg q)$. Write $f^{\circ n}$ for the $n$-th iterate.

A family of maps from an open set to $\hat{\mathbb C}$ is normal if every sequence in it has a subsequence converging locally uniformly in the spherical (chordal) metric. The Fatou set $F(f)$ is the set of points having a neighbourhood on which the iterates $\{f^{\circ n}\}$ form a normal family; the Julia set is its complement $J(f)=\hat{\mathbb C}\setminus F(f)$. A Fatou component is a connected component of $F(f)$. A periodic point $z_0=f^{\circ m}(z_0)$ of minimal period $m$ has multiplier $\lambda=(f^{\circ m})'(z_0)$, computed in a local coordinate; it is repelling if $|\lambda|>1$ and attracting if $|\lambda|<1$.

A Fatou component $U$ with $f(U)=U$ is a Siegel disk (resp. Herman ring) if $f|_U$ is conformally conjugate to an irrational rotation of the unit disk (resp. of a round annulus $\{1<|w|<r\}$).

Formalization targets

Goal: no wandering domains (Theorem 16.4)

For a rational map $f$ of degree $d\ge2$ and every Fatou component $U$ there are $n\ge0$, $p\ge1$ with

$$f^{\circ p}\bigl(f^{\circ n}(U)\bigr)=f^{\circ n}(U).$$

Milestones

1. Lemma 2.5: $\hat{\mathbb C}\setminus\{0,1,\infty\}$ is covered holomorphically by the unit disk.
2. Corollary 3.3 (case $\mathbb D\to\mathbb C\setminus\{0,1\}$): holomorphic maps between hyperbolic surfaces form a normal family.
3. Lemma 3.5 (case $\mathbb C\setminus\{0,1\}\subset\hat{\mathbb C}$).
4. Theorem 3.7 (Montel): holomorphic maps from a domain to $\hat{\mathbb C}$ omitting three values form a normal family.
5. Lemma 4.3: $z\in J(f)\iff f(z)\in J(f)$.
6. Lemma 4.4: $J(f^{\circ k})=J(f)$ for $k>0$.
7. Lemma 4.8: $J(f)\neq\emptyset$ when $d\ge2$.
8. Theorem 14.1: $J(f)=\overline{\{\text{repelling periodic points}\}}$ when $d\ge2$.
9. Theorem 16.1: an invariant Fatou component is an attracting basin, a parabolic basin, a Siegel disk or a Herman ring.

Significance

The results. Montel's theorem is the engine of the Fatou–Julia theory: nonemptiness of $J$, density of iterated preimages and density of repelling cycles all rest on it. Theorem 14.1 identifies the non-normality locus with the closure of the repelling cycles, the form in which the Julia set is usually computed and pictured. Sullivan's theorem, combined with Theorem 16.1, gives a complete qualitative picture of the dynamics on the Fatou set; it is used throughout the later theory, e.g. to show that the Julia set of a postcritically finite map without superattracting cycles is the whole sphere (Milnor, Corollary 16.5).

Formalizing them. All results here are classical theorems with published proofs; none is open. A text search of Mathlib at the platform's pinned revision (0df444a) finds no Montel theorem for families of holomorphic maps, no Fatou or Julia sets and no wandering-domain results; it does contain the Schwarz lemma and the hyperbolic metric on the upper half-plane. The remaining work is to formalize the known proofs.

Difficulty

The early milestones need the uniformization-type input that $\mathbb C\setminus\{0,1\}$ is covered by the disk (via the modular function or an equivalent construction) and Schwarz–Pick-type estimates on hyperbolic surfaces; Mathlib has the Schwarz lemma and the hyperbolic metric of the upper half-plane, but not the Poincaré metric of general hyperbolic domains or covering-space uniformization. Theorem 14.1 requires a quantitative use of Montel's theorem around points of $J$ that are not critical values. Theorem 16.1 needs the Denjoy–Wolff-type classification of self-maps of hyperbolic surfaces and the Snail Lemma for parabolic points. The goal is substantially harder: Sullivan's proof uses the measurable Riemann mapping theorem (Morrey–Ahlfors–Bers) to build an infinite-dimensional family of quasiconformal deformations of $f$, contradicting the finite dimensionality of the space of rational maps of degree $d$. The theory of quasiconformal maps and Beltrami equations is absent from Mathlib, and no elementary argument avoiding it is known.

Formalization scope

All declarations live in the book-wide namespace MilnorDynamics and build on the published definition files MilnorDynamics_NormalFamilies, MilnorDynamics_RationalMaps and MilnorDynamics_PeriodicPoints; one new definition file, MilnorDynamics_FatouComponents, adds Fatou components, immediate basins, Siegel disks and Herman rings.

• $\hat{\mathbb C}$ is OnePoint ℂ; a rational map is a structure of coprime polynomials $p,q$ with $q\ne0$, acting on OnePoint ℂ via RationalMap.toFun; the degree is $\max(\deg p,\deg q)$.
• Holomorphy of a map into $\hat{\mathbb C}$ on an open $U\subseteq\mathbb C$ is continuity plus complex differentiability in the charts $z$ and $1/z$ (IsHolomorphicOn). Normality is locally uniform subconvergence in the chordal metric (IsNormalFamily); the Fatou set is defined through the standard charts of $\hat{\mathbb C}$.
• Multipliers are derivatives of $f^{\circ m}$ in the standard chart at the periodic point, $m$ the minimal period.
• Montel's theorem is stated for a domain $U\subseteq\mathbb C$ rather than an arbitrary Riemann surface (normality is local, Milnor Problem 3-e); Lemma 2.5, Corollary 3.3 and Lemma 3.5 are linked in the special cases used for Montel's theorem.
• The degree hypotheses are Milnor's: $d\ge1$ (nonconstant) in §4 Lemmas 4.3–4.4, $d\ge2$ elsewhere. Without $d\ge2$ several statements are false (e.g. $J(z\mapsto 2z)=\emptyset$), so the hypothesis must not be dropped.

Welcome contributions: the Poincaré metric and Schwarz–Pick on hyperbolic domains, the modular covering of $\mathbb C\setminus\{0,1\}$, the degree theory of rational maps, quasiconformal maps and the measurable Riemann mapping theorem. These are reusable far beyond this mission.

Selected references

• J. Milnor, Dynamics in One Complex Variable, 3rd ed., Annals of Mathematics Studies 160, Princeton University Press, 2006. https://doi.org/10.1515/9781400835539
• D. Sullivan, Quasiconformal homeomorphisms and dynamics I. Solution of the Fatou–Julia problem on wandering domains, Ann. of Math. 122 (1985), 401–418. https://doi.org/10.2307/1971308
• L. Carleson and T. W. Gamelin, Complex Dynamics, Universitext, Springer, 1993. https://doi.org/10.1007/978-1-4612-4364-9
• P. Montel, Leçons sur les familles normales de fonctions analytiques et leurs applications, Gauthier-Villars, Paris, 1927.

The set

For a complex parameter $c$, iterate the quadratic map

$$f_c(z) = z^2 + c$$

starting at the critical point $z = 0$. The Mandelbrot set is the set of parameters for which this orbit stays bounded:

$$M = \{\, c \in \mathbb{C} \ : \ \sup_{k \in \mathbb{N}} \left| f_c^{\,k}(0) \right| < \infty \,\}.$$

Equivalently -- and this is the first milestone of the mission -- $c \in M$ if and only if $|f_c^{\,k}(0)| \le 2$ for every $k$, which exhibits $M$ as a compact subset of the plane.

$M$ is the parameter-space picture of the simplest non-trivial family in complex dynamics, and it acts as a dictionary: the shape of $M$ near a parameter $c$ encodes the dynamics of $f_c$ on its Julia set, so structural questions about $M$ are questions about the whole quadratic family at once. Douady and Hubbard proved in 1982 that $M$ is connected, by exhibiting a conformal isomorphism

$$\Phi : \mathbb{C} \setminus M \longrightarrow \mathbb{C} \setminus \overline{\mathbb{D}}$$

between the complement of $M$ and the exterior of the closed unit disk.

The question

MLC conjecture. $M$ is locally connected: every point of $M$ has a neighbourhood basis, in the subspace topology, consisting of connected sets.

By Caratheodory's theorem, MLC is equivalent to the statement that $\Phi^{-1}$ extends continuously to the unit circle. That extension would deliver a complete combinatorial description of $M$ -- the pinched disk model of Douady and Thurston -- in which every boundary point is labelled by the external rays landing on it. Two headline consequences follow: the density of hyperbolicity in the quadratic family (Fatou's conjecture: every quadratic polynomial can be perturbed to one with an attracting cycle), and zero area for $\partial M$.

MLC has been open since the early 1980s and is regarded as the central problem of one-dimensional complex dynamics.

Timeline

• 1982 -- Douady and Hubbard prove that $M$ is connected, via the Boettcher uniformisation of its complement, and formulate MLC.
• 1984/85 -- The Orsay notes develop the combinatorics of external rays and the pinched-disk model, and show that MLC implies the density of hyperbolicity in the quadratic family.
• 1990 -- Yoccoz proves MLC at every finitely renormalizable parameter without an indifferent periodic point, introducing the Yoccoz puzzle and the rigidity techniques that dominate later work.
• 1997 -- Lyubich extends local connectivity to infinitely renormalizable parameters of bounded type, using complex bounds for quadratic-like renormalization.
• 1997 -- Graczyk-Swiatek and Lyubich prove density of hyperbolicity in the real quadratic family.
• 1998 -- Shishikura proves that $\partial M$ has Hausdorff dimension $2$, by parabolic implosion. Whether $\partial M$ has positive area remains open.
• 2005 -- Buff and Cheritat construct quadratic Julia sets of positive area, showing that the analogous area question in the dynamical plane has a negative answer.
• Today -- MLC is known at large classes of parameters, but the general case, and with it the density of hyperbolicity, remain open.

What this mission asks for

The goal theorem is MLC itself, in the form "the Mandelbrot set, as a topological subspace of $\mathbb{C}$, is a locally connected space".

The milestones are of three kinds, and are ordered accordingly:

1. Foundations provable today -- the escape criterion (in the quadratic and the general unicritical degree) and compactness. These make the filter-theoretic definition usable and are the natural entry point for a solver new to the mission.
2. Known theorems from the literature -- connectedness of $M$ (Douady-Hubbard), the implication MLC $\Rightarrow$ density of hyperbolicity (Douady-Hubbard), and $\dim_H(\partial M) = 2$ (Shishikura). These are hard but settled, and formalizing them builds the infrastructure -- Boettcher coordinates, external rays, parabolic implosion -- that any attack on the goal will need.
3. The open companions -- density of hyperbolicity in the quadratic and unicritical families, zero area of $\partial M$, and MLC for all Multibrot sets $M_n$, the parameter sets of $z \mapsto z^n + c$.

All statements are phrased against a single shared definition file, so a solver can move between milestones without re-fixing conventions.

Motivation

The Yukawa potential (or screened Coulomb potential)

$$V_{\mathrm{Yukawa}}(r) = -g^2\,\frac{e^{-\alpha m r}}{r}$$

was introduced by Hideki Yukawa in 1935 to model the short-range nuclear force as the exchange of a massive particle, later identified with the pion. The same profile reappears as the Debye–Hückel screened interaction in plasmas and electrolytes, as the static Green's function of the massive Klein–Gordon (screened Poisson) operator, and as the Newtonian correction in massive-graviton models. The mathematical facts behind these uses are classical, short, and stated in every textbook treatment — which makes them a natural, self-contained target for formalization: each one is an explicit identity of real analysis in three dimensions.

Timeline. Heisenberg (1932–33) proposed a short-range exchange interaction between nucleons; Fermi (1934) introduced exchange of light particles in beta decay; Yukawa (1935, Proc. Phys.-Math. Soc. Japan 17, 48) combined the two ideas, derived the potential above, and predicted a mediating particle of mass about 200 electron masses; the pion was observed in 1947.

Setting

Throughout, $g\in\mathbb R$ is the coupling (amplitude) constant, $\alpha>0$ a scaling constant, $m\ge 0$ the mass of the exchanged particle and $r>0$ the radial distance; $1/(\alpha m)$ is the range. The potential is the function

$$V(r) = -g^2\,\frac{e^{-\alpha m r}}{r}.$$

Points of space are $x\in\mathbb R^3$ with Euclidean norm $|x|$, and the potential of a point source at the origin is $x\mapsto V(|x|)$. The Laplacian $\Delta$ is the usual sum of unmixed second partial derivatives on $\mathbb R^3$. For a uniform, infinitesimally thin spherical shell of radius $R$ with total scaling constant $G$, the potential felt by a point of scaling constant $g$ located at $x$ is

$$V_{\mathrm{shell}}(x) = G\,g\;\frac{1}{4\pi}\int_{S^2}\frac{e^{-\alpha m |x-Ru|}}{|x-Ru|}\,d\sigma(u),$$

the average over the unit sphere $S^2$ (uniform surface measure $\sigma$) of the pair interaction.

Formalization targets

Goal — Fourier transform of the Yukawa potential

For $\alpha m>0$ and every $k\in\mathbb R^3$,

$$\int_{\mathbb R^3} e^{-i k\cdot x}\,V(|x|)\,d^3x \;=\; -g^2\,\frac{4\pi}{|k|^2+(\alpha m)^2}.$$

This is the identity the article's sections Fourier transform and Feynman amplitude rest on: the momentum-space Yukawa potential is the massive propagator $4\pi/(k^2+(\alpha m)^2)$ times $-g^2$.

Milestones (in the order of the article)

1. Negativity and monotonicity — for $g\neq0$, $V<0$ on $(0,\infty)$ and $V$ is strictly increasing there.
2. Massless limit — for $m=0$, $V(r) = -g^2\cdot\frac1r$ (the Coulomb potential).
3. Screened Poisson equation — $\Delta\,V(|x|) = (\alpha m)^2\,V(|x|)$ for $x\neq0$.
4. Inverse Fourier representation — for $x\ne0$, $V(|x|) = \lim_{\Lambda\to\infty} \frac{-g^2}{(2\pi)^3}\int_{|k|<\Lambda} e^{ik\cdot x}\frac{4\pi}{|k|^2+(\alpha m)^2}\,d^3k$.
5. Born amplitude — $\frac{-2\mu}{\hbar^2 q}\int_0^\infty r\,V(r)\sin(qr)\,dr = \frac{2\mu g^2}{\hbar^2[(\alpha m)^2+q^2]}$ for $q>0$.
6. Momentum transfer — $|\vec p-\vec p'| = 2p\sin(\theta/2)$ when $|\vec p|=|\vec p'|=p$ and $\theta$ is the angle between them.
7. Total cross section — $\frac{4\mu^2g^4}{\hbar^4}\int_0^\pi\frac{2\pi\sin\theta\,d\theta}{[(\alpha m)^2+4p^2\sin^2(\theta/2)]^2} = \frac{4\mu^2g^4}{\hbar^4}\,\frac{4\pi}{(\alpha m)^2[(\alpha m)^2+4p^2]}$.
8. Shell, exterior — for $|x|>R$, $V_{\mathrm{shell}}(x) = G g\,\frac{e^{-\alpha m|x|}}{|x|}\,\frac{\sinh(\alpha m R)}{\alpha m R}$.
9. Shell, interior — for $0<|x|<R$, $V_{\mathrm{shell}}(x) = G g\,\frac{e^{-\alpha m R}}{R}\,\frac{\sinh(\alpha m |x|)}{\alpha m |x|}$.

Significance

The results. The Fourier identity is what makes the Yukawa potential the non-relativistic limit of single-meson exchange; milestone 3 identifies it as the Green's function of the screened Poisson operator $-\Delta + (\alpha m)^2$; milestones 5–7 give the Born-approximation scattering amplitude and the closed-form total cross section quoted in quantum mechanics textbooks (e.g. Griffiths); milestones 8–9 are the Yukawa analogue of Newton's shell theorem, whose failure to reduce to a point source of the same strength is the reason massive-graviton models violate the weak equivalence principle.

Formalizing them. All statements are classical and proved on paper. The mission produces machine-checked versions together with reusable infrastructure: three-dimensional Fourier integrals of radial functions, Laplacians of radial functions, spherical averages with respect to the surface measure, and conditionally convergent oscillatory integrals.

Difficulty

The individual computations are short on paper but each crosses a gap in the library. The goal requires reducing a three-dimensional Lebesgue integral of a radial function to a one-dimensional integral (polar coordinates in $\mathbb R^3$), then evaluating $\int_0^\infty e^{-ar}\sin(kr)\,dr$. The inverse transform is not absolutely convergent — $1/(|k|^2+a^2)$ is not integrable on $\mathbb R^3$ — so the naive Lebesgue statement is false (it would assign the value $0$); only the ball-truncated limit is meaningful, and its evaluation needs the improper integral $\int_0^\infty \frac{k\sin(kr)}{k^2+a^2}dk = \frac{\pi}{2}e^{-ar}$. The shell theorem needs the surface measure on $S^2$ and the Archimedes-type change of variables $u\mapsto |x-Ru|$.

Formalization scope

All quantities are real numbers; space is EuclideanSpace ℝ (Fin 3) with Lebesgue measure. The potential is a single definition YukawaPotential.yukawaPotential g α m r; at $r=0$ Lean's division convention gives the junk value $0$, so every statement either restricts to $r>0$ / $x\neq0$ or integrates (where a single point is null). The physical conventions $\alpha>0$, $m\ge0$ (and $m>0$ where the article divides by $\alpha m$) are explicit hypotheses. The Fourier transform uses the convention $\hat V(k)=\int e^{-ik\cdot x}V$, $V=(2\pi)^{-3}\int e^{ik\cdot x}\hat V$; the inverse is stated as a limit over balls. The shell potential averages over the unit sphere with Mathlib's Measure.toSphere (uniform surface measure); since it is an average, its normalisation is irrelevant. The Laplacian is Mathlib's Laplacian.laplacian on inner-product spaces. Physical constants $\mu,\hbar$ in milestones 5 and 7 are arbitrary reals: the identities hold without sign assumptions on them.

Out of scope: the historical mass estimate of the pion, the heuristic wave-equation derivation of the photon/pion dispersion relations, the perturbative asymptotic expansions of Schrödinger eigenvalues and Regge trajectories (stated in the source only up to unspecified $\mathcal O(K^{-7})$ and "$\cdots$" terms), and the $m\to0$ limits of the shell formulas.

Contributions welcome: polar-coordinate integration for radial functions on $\mathbb R^3$, spherical-average lemmas, and the improper integrals above as standalone lemmas.

Selected references

• H. Yukawa, On the interaction of elementary particles, Proc. Phys.-Math. Soc. Japan 17, 48 (1935). https://doi.org/10.11429/ppmsj1919.17.0_48
• D. J. Griffiths, Introduction to Quantum Mechanics, Cambridge University Press (2017), p. 415.
• R. P. Feynman, R. B. Leighton, M. Sands, The Feynman Lectures on Physics, Vol. II, Ch. 28 (1964). https://www.feynmanlectures.caltech.edu/II_28.html
• K. McDonald, A Naïve Estimate of the Coupling Constant in Yukawa Theory (1984/2021). http://kirkmcd.princeton.edu/examples/yukawa.pdf
• Wikipedia, Yukawa potential, revision 1371658231. https://en.wikipedia.org/w/index.php?title=Yukawa_potential&oldid=1371658231

Motivation

The newsvendor problem is the basic single-period inventory model: a decision maker orders $q$ units before a random demand $D$ is observed, pays $b>0$ per unit of unmet demand and $h>0$ per unit left over, and minimizes the expected cost $C(q)=E[b(D-q)^+ + h(q-D)^+]$. When the distribution of $D$ is known, the optimal order is the $b/(b+h)$ quantile of $D$. In practice the distribution is unknown and only a sample of past demands is available; the standard data-driven order is the sample average approximation (SAA), the $b/(b+h)$ quantile of the empirical distribution.

R. Levi, G. Perakis and J. Uichanco, The Data-Driven Newsvendor Problem: New Bounds and Insights (Operations Research 63(6), 2015), ask how many samples guarantee that the SAA order is $\epsilon$-optimal with high probability. Levi, Roundy and Shmoys (2007) gave a distribution-free bound. Levi, Perakis and Uichanco show that, asymptotically in $\epsilon$, the right measure of difficulty is a single scalar of the demand law, the weighted mean spread at the critical quantile, and that for the class of log-concave demand distributions (normal, uniform, exponential, logistic, Laplace and many others used in inventory theory) this scalar is bounded below by $\min(b,h)/(b+h)$. That uniform bound turns a distribution-dependent sample-size guarantee into one that holds for every log-concave demand, and is markedly tighter than the distribution-free one.

This mission formalizes the bound (Proposition 2) and the chain of lemmas the paper uses to prove it. The source is the authors' accepted manuscript of the paper (MIT DSpace), cited by its own page numbers.

Setting

Fix costs $b>0$, $h>0$ and the critical ratio $\beta=b/(b+h)\in(0,1)$. A demand law is given by a probability density $f:\mathbb R\to\mathbb R$: measurable, nonnegative, with $\int f=1$. Its cdf is $F(t)=\int_{(-\infty,t]}f$, and its $\beta$ quantile is

$$q^*=\inf\{q : F(q)\ge \beta\}.$$

The absolute mean spread (AMS, Definition 1) at $t$ is the gap between the conditional means above and below $t$,

$$\Delta(t)=E(D\mid D\ge t)-E(D\mid D\le t)=\frac{\int_{[t,\infty)}x f(x)\,dx}{1-F(t)}-\frac{\int_{(-\infty,t]}x f(x)\,dx}{F(t)},$$

and the weighted mean spread (WMS, Definition 2) is $\Delta(q^*)f(q^*)$.

A density is log-concave (Definition 3) if $\log f$ is concave on its support. Equivalently, $f(x)^a f(y)^{1-a}\le f(ax+(1-a)y)$ for all $x,y$ and $a\in[0,1]$; this form allows $f$ to vanish outside an interval.

For a log-concave $f$ and a point $t$ with $f(t)>0$, the number $\gamma_1$ is a supergradient of $\log f$ at $t$, written $\gamma_1\in\partial\log f(t)$, if $\log f(x)\le\log f(t)+\gamma_1(x-t)$ for all $x$ with $f(x)>0$. The paper splits the class $\mathbb L$ of log-concave densities into the subclasses $\mathbb L_{q^*,\gamma_0,\gamma_1}$ of densities with quantile $q^*$, $f(q^*)=\gamma_0$ and $\gamma_1\in\partial\log f(q^*)$, and minimizes the AMS over each subclass (problem (11)). The minimizer is the truncated exponential density

$$\tilde f(x)=\gamma_0e^{\gamma_1(x-q^*)}\ \text{ on }[\underline x,\overline x],\qquad \underline x=q^*+\tfrac1{\gamma_1}\log\!\big(1-\tfrac{\gamma_1}{\gamma_0}\beta\big),\quad \overline x=q^*+\tfrac1{\gamma_1}\log\!\big(1+\tfrac{\gamma_1}{\gamma_0}(1-\beta)\big),$$

and zero elsewhere (display (12)), with AMS $z^*_{q^*,\gamma_0,\gamma_1}$ in closed form.

The Lean development uses the names IsPdf, cdfOf, quantileOf, ams, IsLogSupergradient, tildeF and zStar for these objects, in the namespace DataDrivenNV.WMS.

Formalization targets

Goal: Proposition 2

For every log-concave density $f$,

$$\Delta(q^*)\,f(q^*)\ \ge\ \frac{\min(b,h)}{b+h}.$$

The statement has no further hypothesis: no moment condition, no continuity, no restriction on $\gamma_0,\gamma_1$.

Milestones, in the order of the paper's proof

1. Lemma 1: at the quantile, $-\frac{b+h}{h}\le\frac{\gamma_1}{\gamma_0}\le\frac{b+h}{b}$.
2. Lemma 2: $f(x)\le\gamma_0e^{\gamma_1(x-t)}$ for every $x$.
3. Lemma 3 (Domination Lemma): a density dominated on the support of another, with the same mass left of $t$, has the larger AMS at $t$.
4. Proposition 1: $\tilde f$ belongs to $\mathbb L_{q,\gamma_0,\gamma_1}$ and minimizes the AMS there.
5. The closed form: $\Delta_{\tilde f}(q)=z^*_{q,\gamma_0,\gamma_1}=\frac{\gamma_0}{\gamma_1^2}\big[(\frac{b+h}{h}+\frac{\gamma_1}{\gamma_0})\log(1+\frac{\gamma_1}{\gamma_0}\frac{h}{b+h})+(\frac{b+h}{b}-\frac{\gamma_1}{\gamma_0})\log(1-\frac{\gamma_1}{\gamma_0}\frac{b}{b+h})\big]$.
6. Lemma 4: three elementary inequalities in $\beta\in(0,1)$ and $\eta\in(-\frac1{1-\beta},\frac1\beta)$.

Significance

The proposition is what makes the paper's log-concave sample-size bound (Theorem 4) parameter-free: the probability that the biased SAA order is $\epsilon$-optimal is, asymptotically, at least $1-2\exp(-\frac14N\epsilon\,\Delta(q^*)f(q^*))$ (Theorem 3), and Proposition 2 replaces the unknown $\Delta(q^*)f(q^*)$ by $\min(b,h)/(b+h)$. A manager who only knows that demand is log-concave can then size a sample without estimating any parameter of the law.

The result is proved in the paper; nothing about it is open. As far as is known it has no machine-checked proof. Formalizing it produces a checked lower bound for an inventory-theory quantity together with reusable facts about log-concave densities on the line: exponential envelopes from a supergradient, the quantile-and-slope constraints of Lemma 1, and the comparison of conditional means behind the Domination Lemma.

Difficulty

The definitions are elementary, but the proof passes through an infinite-dimensional optimization problem over a class of densities. The obvious first step, "the AMS is minimized by the most concentrated density", has no direct meaning without fixing the density value and the slope of $\log f$ at the quantile; after fixing them, one needs the envelope of Lemma 2, a stochastic comparison (Lemma 3) and an explicit integral of a truncated exponential. The Domination Lemma as printed is false (a density whose support has a gap to the right of $t$ is a counterexample), so it is formalized under the hypothesis that the dominating density is positive exactly on an interval around $t$, which is how Proposition 1 uses it. The case $\gamma_1=0$ (uniform minimizer) and the two boundary values of $\gamma_1/\gamma_0$ (one-sided exponential minimizers) are not covered by the closed form (12) and must be handled separately in a proof of the goal. Finally, Lemma 1 rests on the monotonicity of the failure rate $f/(1-F)$ and the reversed hazard rate $f/F$ of log-concave laws, which must be proved from log-concavity.

Formalization scope

Densities are functions ℝ → ℝ with IsPdf f (measurable, nonnegative everywhere, integrable, total integral 1); the law of $D$ is never introduced separately. Log-concavity is the published definition ConvexOptimization.LogConcaveOn Set.univ f (power form, zeros allowed). Concavity of Real.log ∘ f is not used, because Real.log 0 = 0 would treat $\log f$ as $0$ off the support. The quantile is an sInf; for $\beta\in(0,1)$ its defining set is nonempty and bounded below. The AMS is the difference of two ratios of integrals. At the quantile both denominators are positive, and the goal and Proposition 1 assume no integrability of $xf(x)$, since log-concave densities have exponential tails. The value $f(q^*)$ is taken pointwise; $q^*$ lies in the interior of the support, where a log-concave density is continuous.

Conventions and disclosed departures from the page:

• "$\gamma_1\in\partial\log f$, the set of all subgradients" is read as the superdifferential of the concave $\log f$ on $\{f>0\}$.
• Lemma 3 carries three added hypotheses: $f_2$ vanishes outside some $[l,u]\ni t$ and is positive on $(l,u)$; $0<F_1(t)<1$; and $xf_1(x)$, $xf_2(x)$ are integrable. The first repairs the printed statement; the other two are the conditions under which Definition 1 makes sense for general densities.
• Proposition 1 and the closed form of $z^*$ are stated for $\gamma_1\neq0$ and $\gamma_1/\gamma_0$ strictly inside the interval of Lemma 1, where (12) is a finite interval.
• The goal has no such restriction.

Assumption 1 of the paper (monotonicity of $f$ beyond $q^*$) and the continuity assumption of §3 are hypotheses of Theorems 3–4 only and are not used here. A formalization in which $f(q^*)$ or $\Delta(q^*)$ takes a junk value (a non-integrable $xf(x)$, a zero denominator) would make the goal trivially true or false; the hypotheses above exclude this, and no statement assumes the conclusion of another.

Contributions welcome: proofs of the milestones in any order; general lemmas on log-concave densities on $\mathbb R$ (exponential tails, integrability of moments, monotone hazard rates, continuity in the interior of the support); and the boundary cases of problem (11).

Selected references

• R. Levi, G. Perakis, J. Uichanco, The Data-Driven Newsvendor Problem: New Bounds and Insights, Operations Research 63(6):1294–1306, 2015. Authors' accepted manuscript, MIT DSpace. https://doi.org/10.1287/opre.2015.1422
• R. Levi, R. O. Roundy, D. B. Shmoys, Provably Near-Optimal Sampling-Based Policies for Stochastic Inventory Control Models, Mathematics of Operations Research 32(4):821–839, 2007. https://doi.org/10.1287/moor.1070.0272

Motivation

Existence theory for elliptic, parabolic and nonlinear PDEs mostly runs through one argument: build approximate solutions, bound them in a Sobolev norm, extract a convergent subsequence, and pass to the limit. The extraction step needs a compact embedding: a bound on derivatives must buy convergence of the functions themselves in a weaker norm. On a bounded domain this is the Rellich–Kondrachov theorem. It is what makes the resolvent of the Dirichlet Laplacian compact, and so gives the Fredholm alternative and the discrete spectrum of elliptic operators on bounded domains. The companion topics of the same section, extension and trace, are how Sobolev functions are moved between a domain and all of space, and how they are given boundary values.

This mission follows Chapter 3 (§3.9–3.10) and Theorem 1.15 of J. K. Hunter's Notes on Partial Differential Equations (UC Davis lecture notes, revised 6/18/2014).

Timeline. Rellich proved the compactness of $H^1_0 \hookrightarrow L^2$ on bounded domains in 1930. Kondrachov extended it to $W^{1,p}$ and exponents below the Sobolev exponent in 1945. The $L^p$ compactness criterion used in the notes goes back to Kolmogorov (1931) and M. Riesz (1933); a modern account with a history is Hanche-Olsen and Holden 2010. Gagliardo characterized the traces of $W^{1,p}$ in 1957.

Setting

Throughout, $\mathbb{R}^n$ carries Lebesgue measure, and functions are real-valued. For an open set $\Omega \subseteq \mathbb{R}^n$, a test function $\phi \in C_c^\infty(\Omega)$ is smooth with compact support inside $\Omega$. A locally integrable $g$ is the weak derivative $\partial^\alpha f$ of a locally integrable $f$ if $\int_\Omega g\phi = (-1)^{|\alpha|}\int_\Omega f\,\partial^\alpha\phi$ for every test function $\phi$. Here $\alpha \in \mathbb{N}_0^n$ is a multi-index of order $|\alpha| = \sum_i \alpha_i$.

For $k \in \mathbb{N}$ and $1 \le p \le \infty$, the Sobolev space $W^{k,p}(\Omega)$ consists of the $f$ whose weak derivatives $\partial^\alpha f$, $|\alpha| \le k$, exist and lie in $L^p(\Omega)$. For $p < \infty$ its norm is

$$\|f\|_{W^{k,p}(\Omega)} = \Big(\sum_{|\alpha|\le k} \int_\Omega |\partial^\alpha f|^p\,dx\Big)^{1/p},$$

and for $p = \infty$ it is the maximum of the essential suprema. The space $W^{k,p}_0(\Omega)$ is the closure of $C_c^\infty(\Omega)$ in this norm. For $1 \le p < n$ the Sobolev conjugate is $p^* = np/(n-p)$.

The upper half-space is $\mathbb{R}^n_+ = \{x = (x', x_n) : x_n > 0\}$, with closure $\overline{\mathbb{R}}^n_+$ and boundary $\partial\mathbb{R}^n_+ = \{(x', 0)\} \cong \mathbb{R}^{n-1}$. The space $C_c^\infty(\overline{\mathbb{R}}^n_+)$ consists of the functions that are smooth up to the boundary and vanish outside a compact set. Unlike $C_c^\infty(\mathbb{R}^n_+)$, they need not vanish on $\partial\mathbb{R}^n_+$.

A subset of a metric space is precompact if its closure is compact. $C_0(\mathbb{R}^n)$ is the space of continuous functions vanishing at infinity, with the sup norm.

In Lean the weak derivative is HasWeakDeriv (with weakDeriv and weakGradNorm) in the series' shared namespace HunterPDE.Shared; the other objects are MemW k p Ω f, sobolevNorm k p Ω f, MemW0 k p Ω f, sobolevConjugate, upperHalfSpace m, IsSmoothCompactClosedHalfSpace and boundaryPoint, in the namespace HunterPDE.Compactness.

Formalization targets

Goal: Rellich–Kondrachov (Theorem 3.45)

Let $\Omega$ be a bounded open set in $\mathbb{R}^n$, $1 \le p < n$ and $1 \le q < p^*$. If $\mathcal{F} \subseteq W^{1,p}_0(\Omega)$ satisfies $\|f\|_{W^{1,p}(\Omega)} \le M$ for all $f \in \mathcal{F}$, then

$$\{\, f\mathbf{1}_\Omega : f \in \mathcal{F} \,\} \ \text{is precompact in } L^q(\mathbb{R}^n).$$

Milestones

• Theorem 1.15 (Kolmogorov–Riesz). For $1 \le p < \infty$, a set $\mathcal{F} \subseteq L^p(\mathbb{R}^n)$ is precompact if and only if it is bounded, tight ($\sup_{f}\|f\|_{L^p(|x|>R)} \to 0$ as $R \to \infty$), and $L^p$-equicontinuous:

$$\forall \varepsilon > 0\ \exists \delta > 0:\ |h| < \delta \implies \|f(\cdot + h) - f\|_{L^p(\mathbb{R}^n)} < \varepsilon \quad \forall f \in \mathcal{F}.$$

• Theorem 3.41 (extension). There is a bounded linear $E : W^{1,p}(\mathbb{R}^n_+) \to W^{1,p}(\mathbb{R}^n)$ with $Ef = f$ a.e. on $\mathbb{R}^n_+$ and $\|Ef\|_{W^{1,p}(\mathbb{R}^n)} \le C(n,p)\,\|f\|_{W^{1,p}(\mathbb{R}^n_+)}$.
• Theorem 3.42 (density). $C_c^\infty(\overline{\mathbb{R}}^n_+)$ is dense in $W^{k,p}(\mathbb{R}^n_+)$ for $1 \le p < \infty$.
• Theorem 3.44 (trace). For $1 \le p < \infty$ there is a bounded linear $T : W^{1,p}(\mathbb{R}^n_+) \to L^p(\mathbb{R}^{n-1})$ with $(Tf)(x') = f(x', 0)$ on $C_c^\infty(\overline{\mathbb{R}}^n_+)$ and $\|Tf\|_{L^p} \le C(p)\,\|f\|_{W^{1,p}(\mathbb{R}^n_+)}$, whose kernel is exactly $W^{1,p}_0(\mathbb{R}^n_+)$.
• Theorem 3.48 ($p > n$). For $\Omega$ bounded and $n < p < \infty$, a family with $\operatorname{supp} f \Subset \Omega$ and $\|Df\|_{L^p} \le C$ is precompact in $C_0(\mathbb{R}^n)$.

The goal is stated qualitatively (precompactness), with no constants, so it does not depend on any particular form of the Sobolev inequality.

Significance

The result itself. Rellich–Kondrachov is the source of compactness in the $L^2$ theory of elliptic equations. With it, the solution operator of a coercive elliptic problem on a bounded domain is compact. That yields the Fredholm alternative, the discreteness of the Dirichlet spectrum, and existence results for semilinear problems via compactness and fixed-point arguments. The trace theorem makes the boundary condition "$u = 0$ on $\partial\Omega$" meaningful for Sobolev functions, and identifies $W^{1,p}_0$ as the space in which Dirichlet problems are posed. The extension theorem transfers whole-space results to domains. Theorem 3.48 gives the uniform-norm counterpart above the critical exponent.

Formalizing it. All results here are classical and proved. The notes prove 3.45, 3.48 and the forward direction of 3.44. They describe 3.41 and 3.42 in a sentence each, and cite 1.15 without proof. Mathlib has the Lebesgue spaces Lp, Arzelà–Ascoli for bounded continuous functions, and mollification. It has no weak derivatives, no Sobolev spaces on domains, no trace, no extension operators and no Kolmogorov–Riesz criterion. A complete development would supply the first machine-checked versions of these in the notes' form, and a formal $W^{1,p}_0$ compactness theorem usable by the elliptic chapters of the same series.

Difficulty

The obvious route to the goal is: approximate by test functions, extend by zero, and verify the three Kolmogorov–Riesz conditions. The first two follow from the Sobolev inequality and the boundedness of $\Omega$. The hard parts are elsewhere. First, the Kolmogorov–Riesz criterion is not in Mathlib, and its "if" direction needs a mollification and total-boundedness argument in $L^p(\mathbb{R}^n)$. Second, the $L^q$-equicontinuity for $q$ above $p$ needs an interpolation between an $L^1$ translation estimate and the critical Sobolev embedding into $L^{p^*}$, so the Gagliardo–Nirenberg–Sobolev inequality must be available for $W^{1,p}_0(\Omega)$, not only for smooth compactly supported functions. Third, weak derivatives are defined by integration against test functions, and every density step has to be carried through that definition. The exponent restriction $q < p^*$ is sharp (Example 3.47 in the notes), so no argument that ignores it can succeed.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n) with volume. Open sets are Ω : Set _ with IsOpen Ω, and bounded means Bornology.IsBounded Ω. Coordinates are 0-based (i : Fin n), and multi-indices are α : Fin n → ℕ.
• Functions are ℝⁿ → ℝ, and only their values on the relevant set matter. weakDeriv is a chosen representative, used only where a weak derivative is assumed to exist. sobolevNorm takes values in ℝ≥0∞.
• $W^{1,p}_0(\Omega)$ is the norm closure of $C_c^\infty(\Omega)$, not "zero trace". "Bounded in $W^{1,p}_0(\Omega)$" is a uniform bound on sobolevNorm 1 p Ω.
• In the goal, $\mathcal{F}$ is placed in $L^q(\mathbb{R}^n)$ by extension by zero (Ω.indicator f). The conclusion asserts both that each extension lies in $L^q$ and that the set of their classes in Mathlib's Lp ℝ q volume has compact closure. The hypothesis $q < p^*$ rules out $q = \infty$.
• Half-space results use dimension $n = m+1$ and the last coordinate Fin.last m. The boundary is $\mathbb{R}^m$ via $x' \mapsto (x',0)$. Extension and trace operators are maps on functions that are linear up to a.e. equality on $W^{1,p}(\mathbb{R}^n_+)$.
• Conventions read off the page: in Theorem 3.44 the trace constant is quantified before the dimension ("depending only on $p$"), and its final clause is taken with $k = 1$ (the printed "$W^{k,p}_0$" cannot mean $k \ge 2$, as the notes remark after the proof). Theorem 3.42 is stated for $1 \le p < \infty$, and Theorem 3.41 for $1 \le p \le \infty$. Theorem 3.48 assumes $n \ge 1$.
• A trivializing reading is ruled out: the goal's conclusion is compactness of the closure in $L^q(\mathbb{R}^n)$ of the zero extensions themselves, not of some other representative. The norm bound is on the genuine weak derivatives, which the hypotheses guarantee exist, not on a junk value.
• Reusable infrastructure: weak derivatives and Sobolev spaces on open sets, the Kolmogorov–Riesz criterion, and the half-space extension and trace operators. Contributions of any of these as standalone lemmas are welcome.

Selected references

• J. K. Hunter, Notes on Partial Differential Equations, UC Davis lecture notes, revised 6/18/2014, §1.5 and §3.9–3.10. https://www.math.ucdavis.edu/~hunter/pdes/pde_notes.pdf
• H. Hanche-Olsen and H. Holden, The Kolmogorov–Riesz compactness theorem, Expositiones Mathematicae 28 (2010) 385–394. https://arxiv.org/abs/0906.4883
• L. C. Evans, Partial Differential Equations, 2nd ed., AMS Graduate Studies in Mathematics 19, 2010, §5.5–5.7. https://doi.org/10.1090/gsm/019

Why holomorphic functions of several variables

Several complex variables studies functions of $z = (z_1, \dots, z_n) \in \mathbb{C}^n$ that are holomorphic in every coordinate. It underlies complex geometry, the theory of analytic spaces, and parts of mathematical physics and harmonic analysis. Every later topic of the subject (domains of holomorphy, pseudoconvexity, the $\bar\partial$-problem, the Bergman kernel, analytic varieties) starts from the same foundation: a function that is holomorphic in each variable separately and locally bounded is jointly smooth and is locally the sum of a convergent power series. This mission formalizes that foundation as it appears in the first chapter of Jiří Lebl's textbook Tasty Bits of Several Complex Variables (jirka.org/scv).

Historically, the step from separate to joint regularity is due to Osgood (1899), who showed that a continuous (later: locally bounded) function that is holomorphic in each variable separately is holomorphic; Hartogs (1906) later removed the boundedness assumption altogether, a much harder theorem not covered here.

Setting

Points of $\mathbb{C}^n$ are $z = (z_1, \dots, z_n)$. For a center $a \in \mathbb{C}^n$ and a polyradius $\rho = (\rho_1, \dots, \rho_n)$ with every $\rho_k > 0$, the polydisc is

$$\Delta_\rho(a) = \{ z \in \mathbb{C}^n : |z_k - a_k| < \rho_k,\ k = 1, \dots, n \},$$

a product of open discs $\Delta_1 \times \cdots \times \Delta_n$. Its distinguished boundary is the torus $\Gamma = \partial\Delta_1 \times \cdots \times \partial\Delta_n = \{ |\zeta_k - a_k| = \rho_k \text{ for all } k \}$, and $\overline{\Delta}$ denotes the closed polydisc.

A function $f$ on an open set $U \subset \mathbb{C}^n$ is holomorphic (the book's Definition 1.1.2) if it is locally bounded (every point of $U$ has a neighborhood on which $f$ is bounded) and complex-differentiable in each variable separately: for every $z \in U$ and every $k$, the one-variable limit

$$\lim_{\xi \to 0} \frac{f(z_1, \dots, z_k + \xi, \dots, z_n) - f(z)}{\xi}$$

exists. A map $f = (f_1, \dots, f_m) : U \to \mathbb{C}^m$ is holomorphic if every component is.

A multi-index is $\alpha = (\alpha_1, \dots, \alpha_n) \in \mathbb{N}_0^n$, with $\alpha! = \alpha_1! \cdots \alpha_n!$, $(z-a)^\alpha = \prod_k (z_k - a_k)^{\alpha_k}$ and $\rho^\alpha = \prod_k \rho_k^{\alpha_k}$. A power series $\sum_\alpha c_\alpha (z-a)^\alpha$ is summed over all multi-indices; since $\mathbb{N}_0^n$ has no natural order, convergence means absolute convergence, and the series converges uniformly absolutely on a set $X$ when $\sum_\alpha |c_\alpha (z-a)^\alpha|$ converges uniformly for $z \in X$. The Wirtinger derivative is $\partial/\partial z_k = \tfrac12(\partial/\partial x_k - i\,\partial/\partial y_k)$ for $z_k = x_k + i y_k$, and $\partial^{|\alpha|}/\partial z^\alpha$ applies $\partial/\partial z_k$ exactly $\alpha_k$ times for each $k$.

Formalization targets

Goal: Theorem 1.2.1 (power series on a polydisc)

Let $\Delta = \Delta_\rho(a)$ be a polydisc. If $f : \overline{\Delta} \to \mathbb{C}$ is continuous and holomorphic in $\Delta$, then there are coefficients $c_\alpha$ with

$$f(z) = \sum_\alpha c_\alpha (z-a)^\alpha \qquad (z \in \Delta),$$

the series converging uniformly absolutely on every compact subset of $\Delta$. Conversely, a function defined on $\Delta$ by such a series is holomorphic on $\Delta$. Both directions are part of the goal.

Milestones

In attack order:

1. Proposition 1.1.3. A holomorphic function on an open $U$ is $C^\infty$, and every $\partial f/\partial z_k$ is again holomorphic.
2. Theorem 1.1.4 (Cauchy integral formula). For $f$ continuous on $\overline{\Delta}$ and holomorphic in $\Delta$, and $z \in \Delta$,

$$f(z) = \frac{1}{(2\pi i)^n} \int_\Gamma \frac{f(\zeta)}{(\zeta_1 - z_1)\cdots(\zeta_n - z_n)}\, d\zeta_1 \wedge \cdots \wedge d\zeta_n.$$

3. Proposition 1.2.2. The derivative formula $\frac{\partial^{|\alpha|} f}{\partial z^\alpha}(z) = \frac{1}{(2\pi i)^n}\int_\Gamma \frac{\alpha!\, f(\zeta)}{(\zeta - z)^{\alpha+1}}\,d\zeta$, the coefficient formula $c_\alpha = \frac{1}{\alpha!}\frac{\partial^{|\alpha|} f}{\partial z^\alpha}(a)$, and the Cauchy estimates $|c_\alpha| \le \|f\|_\Gamma / \rho^\alpha$.
4. Proposition 1.2.3. A limit, uniform on compact subsets, of holomorphic functions is holomorphic, and all derivatives $\partial^{|\alpha|}/\partial z^\alpha$ converge uniformly on compact subsets.
5. Theorem 1.2.7 (identity theorem). On a domain, a holomorphic function vanishing on a nonempty open subset vanishes identically.
6. Theorem 1.2.8 (maximum principle). On a domain, if $|f|$ has a local maximum at $a$, then $f \equiv f(a)$.
7. Theorem 1.3.5. Compositions of holomorphic mappings are holomorphic.
8. Proposition 1.3.7. For holomorphic $f : U \to \mathbb{C}^n$, $|\det Df(p)|^2 = \det D_{\mathbb{R}} f(p)$.

Significance

Theorem 1.2.1 is the statement that makes the theory of several complex variables possible: it identifies the book's elementary, one-variable-at-a-time definition of holomorphy with local representability by power series. Uniqueness of the coefficients, the Cauchy estimates, the identity theorem, the maximum principle, and holomorphy of compositions and of implicit functions all follow from it, and every later chapter of the book (Hartogs figures, pseudoconvexity, the Bergman kernel, Weierstrass preparation) uses it without comment.

Mathlib already develops complex analysis in several variables for Fréchet-differentiable maps: analyticity of DifferentiableOn ℂ functions, torusIntegral, Cauchy integrals over circles, and Osgood-type regularity for maps on $\mathbb{C}^n$ are available or published on the platform. What this mission adds is the bridge from the weaker separate notion of holomorphy, with local boundedness, to these results, stated with multi-index power series and uniform absolute convergence on compact sets exactly as in the textbook. The results are classical and fully proved in the book; none has a machine-checked proof in this form.

Difficulty

The hypothesis controls $f$ only along complex lines parallel to the coordinate axes, plus a bound. Nothing in the definition says that $f$ is continuous, let alone jointly differentiable, so no joint limit, Fréchet derivative, or change of the order of integration is available at the start. Every tool that the one-variable theory and Mathlib's multivariable library supply presupposes joint regularity; the obstacle is to obtain it from separate information.

A second difficulty is bookkeeping: power series over $\mathbb{N}_0^n$ have no natural order, so convergence must be handled as unconditional summation with a uniformity statement over compact sets, and iterated Wirtinger derivatives must be related to derivatives of the series term by term.

Formalization scope

• $\mathbb{C}^n$ is Fin n → ℂ; multi-indices are Fin n → ℕ. A polyradius is ρ : Fin n → ℝ with the hypothesis ∀ k, 0 < ρ k; the polydisc is defined coordinatewise (not Metric.ball, which only gives equal radii).
• Holomorphy is the book's Definition 1.1.2, IsHolomorphicOn f U: local boundedness plus complex differentiability at $\xi = 0$ of $\xi \mapsto f(z_1, \dots, z_k + \xi, \dots, z_n)$ (via Function.update). Openness of $U$ is a hypothesis wherever the book says "open". Maps into $\mathbb{C}^m$ are holomorphic componentwise.
• Ruled out: defining holomorphy as Mathlib's DifferentiableOn ℂ. That makes Proposition 1.1.3 and the first half of the goal off-target (they would follow from existing library results) and is not the book's definition.
• The closed polydisc is closure (polydisc a ρ); "continuous on $\overline{\Delta}$, holomorphic in $\Delta$" keeps both hypotheses.
• Power series: HasSum (unconditional summation) of the terms $c_\alpha (z-a)^\alpha$ to $f(z)$, and uniform absolute convergence on a set $X$ means the finite partial sums of $|c_\alpha (z-a)^\alpha|$, directed by inclusion, converge uniformly on $X$. Mathlib's HasFPowerSeriesOnBall is not used: its balls for the sup norm are equiradial polydiscs only.
• The integral over $\Gamma$ is torusIntegral, whose parametrization $\zeta_k = a_k + \rho_k e^{i\theta_k}$ includes the Jacobian $\prod_k i\rho_k e^{i\theta_k}$ and orients each circle positively. The integrands are continuous on the compact torus, so no integrability hypothesis is needed.
• $\partial/\partial z_k$ is defined from real partial derivatives (deriv along $t \mapsto z_k + t$ and $t \mapsto z_k + it$); $\partial^{|\alpha|}/\partial z^\alpha$ iterates it. $\det D_{\mathbb{R}} f(p)$ is LinearMap.det of the real Fréchet derivative, which is basis independent.
• The Cauchy estimate is stated for every bound $M$ of $|f|$ on $\Gamma$, which is equivalent to the book's $\|f\|_\Gamma$ form.

A complete development needs the one-variable Cauchy integral formula (in Mathlib), iterated circle integrals and torusIntegral, and summation over Fin n → ℕ. The regularity bridge from separate to joint holomorphy and the multi-index power-series API are reusable across the whole series of missions on this book; contributions of either as standalone lemmas are welcome.

Selected references

• J. Lebl, Tasty Bits of Several Complex Variables, version 4.4, 2026, Chapter 1, §§1.1–1.3. https://www.jirka.org/scv/scv.pdf
• W. F. Osgood, "Note über analytische Functionen mehrerer Veränderlichen", Mathematische Annalen 52 (1899), 462–464.
• L. Hörmander, An Introduction to Complex Analysis in Several Variables, 3rd ed., North-Holland, 1990, Chapter II.