Mathematics pursued for its own internal structure: the study of abstract objects, spaces, and the maps between them, guided by rigor and generality rather than immediate application. Its landscape includes real and complex analysis, topology and geometry, measure theory, and the logical and set-theoretic foundations on which the rest of mathematics is built.
Missions
🏆Completed
Captain: ykanoria
Excursion Coupling for the Monge Problem on the Line (Juillet 2019)Research Paper
The Monge optimal transport problem on the real line with the classical distance cost $|x-y|$ famously fails to have a unique solution. Juillet (2019) restored uniqueness by considering the strictly concave power costs $|x-y|^p$ with $p<1$ and letting $p\to 1^-$: the limit selects a distinguished optimal plan, the *excursion coupling*, built from the level sets of the difference $F_\sigma=F_\mu-F_\nu$ of the cumulative distribution functions. This mission formalizes the completed-graph construction, the generalized Banach indicatrix identities of Bertoin-Yor, the alternating crossing structure of almost every level, and the marginal identities for the crossing counting measures. It culminates in Propositions 3.5-3.6: every monotone transport plan is concentrated on the paired routes, and the marginals uniquely determine the coupling carried by those routes, including in the presence of atoms.
This mission formalizes the key implication 3=>4 in Juillet's Main Theorem.
37 thms4 active usersReviewed
🏆Completed
Captain: tabbott
The Hardy-Littlewood Method I: Weyl's InequalityTextbook
## Motivation
The Hardy--Littlewood circle method is the principal analytic tool for counting solutions to additive equations in integers. Introduced by Hardy and Ramanujan for the partition function and developed by Hardy and Littlewood in their *Partitio Numerorum* series (1920--1928), it produces asymptotic formulae for the number of representations of a large integer $n$ as a sum of $s$ terms drawn from a prescribed set — $k$-th powers, primes, values of a polynomial.
Its engine is an estimate for **exponential sums**. If a sum $\sum_{x<N} e(\alpha x^k)$, where $e(\theta)=\exp(2\pi i\theta)$, exhibits cancellation for every $\alpha$ not well approximable by a rational with small denominator, the method delivers an asymptotic formula; if it does not, the method stalls. Weyl's inequality (Weyl 1916) was the first such estimate and remains the standard one for moderate $k$.
A short timeline of the estimate this mission targets. Weyl (1916) proved the inequality below with the exponent $2^{1-k}$, in the course of his work on uniform distribution. Hardy and Littlewood (1920--1928) built the circle method on it, obtaining $G(k)\le (k-2)2^{k-1}+5$ for Waring's problem. Vinogradov (1935) replaced Weyl differencing by his mean value theorem, superior for large $k$, reducing the bound to $O(k\log k)$; Wooley's efficient congruencing (2012) and the Bourgain--Demeter--Guth decoupling theorem (2016) settled the main conjecture of Vinogradov's mean value theorem. For small $k$ — and as the entry point to the subject — Weyl's inequality is still the right tool, and it is the natural first capstone for a formalization of the method.
## Setting
For a real number $\theta$ write
$$e(\theta) \;=\; \exp(2\pi i \theta),$$
the standard additive character of $\mathbb{R}/\mathbb{Z}$: it satisfies $e(x+y)=e(x)e(y)$, $|e(x)|=1$, and $e(x)=1$ exactly when $x\in\mathbb{Z}$.
For a real number $\theta$ write $\|\theta\|$ for the distance from $\theta$ to the nearest integer. It is periodic with period $1$, vanishes exactly on $\mathbb{Z}$, satisfies the triangle inequality, and is at most $\tfrac12$.
Given a finite set $A\subseteq\mathbb{Z}$, its generating function is $f_A(\theta)=\sum_{a\in A}e(a\theta)$. The basic identity of the subject is
$$\int_0^1 f_A(\theta)^s\,e(-n\theta)\,d\theta \;=\; \#\{(a_1,\dots,a_s)\in A^s : a_1+\cdots+a_s=n\},$$
a consequence of the orthogonality relation $\int_0^1 e(m\theta)\,d\theta=[\,m=0\,]$.
A **Weyl sum** of degree $k$ is $\sum_{0\le x<N} e(\alpha x^k)$. The whole difficulty is to bound it for $\alpha$ in the *minor arcs* — those $\alpha$ admitting no rational approximation $a/q$ with $q$ small.
## Target
Fix $k\ge 2$. For every $\varepsilon>0$ there is a constant $C=C(k,\varepsilon)$ such that whenever $(a,q)=1$, $q\ge 1$, and $\left|\alpha-\frac{a}{q}\right|\le \frac{1}{q^2}$,
$$\left|\sum_{0\le x<N} e(\alpha x^{k})\right| \;\le\; C\,N^{1+\varepsilon}\left(\frac{1}{q}+\frac{1}{N}+\frac{q}{N^{k}}\right)^{2^{1-k}}.$$
The intermediate targets, weakest first, are the milestone list: the counting identity, the Weyl differencing (squaring) step, the Farey covering with coprime numerator, the divisor bound $d(n)\ll_\varepsilon n^\varepsilon$, Hua's fourth-moment inequality for $k=2$, and the degree-two case of the inequality itself.
## Significance
*The result itself.* Weyl's inequality is what makes the minor arcs negligible. Applied with $q$ in the range $N^{\delta}\le q\le N^{k-\delta}$ it gives a power saving over the trivial bound $N$, and integrating that saving over the minor arcs shows their contribution is smaller than the main term produced by the major arcs. Every classical application of the circle method — the asymptotic formula in Waring's problem, Vinogradov's three primes theorem, the Birch--Davenport theory of forms in many variables — passes through an estimate of this shape. Without it the method produces an identity, not a theorem.
*Formalizing it.* Mathlib currently contains the analytic prerequisites — Fourier characters on `AddCircle`, Dirichlet's approximation theorem, Abel summation, Gauss sums — but no circle-method apparatus whatsoever: no Weyl sums, no arc dissection, no singular series, no mean value estimates. This mission supplies the first layer. The foundational tier is already machine-checked: **53 theorems** covering the character $e$, the norm $\|\cdot\|$, the geometric sum bound $\left|\sum_{x<N}e(x\theta)\right|\le\min\!\left(N,\frac{1}{2\|\theta\|}\right)$, both orthogonality relations, both forms of Dirichlet's theorem, and the basic theory of $f_A$, are published on the platform with verified proofs and may be imported freely. What remains open is the combinatorial and analytic core listed in the milestones. None of the milestone statements is currently formalized anywhere, to the best of our knowledge.
## Difficulty
The obvious approach fails immediately. One would like to sum $\left|\sum_{x<N}e(\alpha x^k)\right|$ by comparing it to the linear case, where the geometric series gives $\min(N,\frac{1}{2\|\alpha\|})$ outright. But for $k\ge2$ the summand is not a geometric progression and there is no closed form.
Weyl's device is to square and difference: $\left|\sum_x e(\phi(x))\right|^2=\sum_{x,y}e(\phi(x)-\phi(y))$, and the substitution $y=x+h$ turns the inner polynomial into one of degree $k-1$ in $x$. Iterating $k-1$ times reduces to a linear sum, at the cost of raising the estimate to the power $2^{1-k}$ — which is why the saving is so weak for large $k$, and why Vinogradov's method eventually supersedes it.
The genuine obstacles in a formalization are: (i) bookkeeping the shifted ranges produced by each differencing step, which are not $[0,N)$ and must be handled uniformly; (ii) the divisor bound $d(n)\ll_\varepsilon n^\varepsilon$, needed to count the $h$ for which the resulting linear coefficient is close to an integer, and which is not currently in Mathlib in this form; (iii) tracking the $\varepsilon$-dependent constants through $k-1$ iterations without the informal $\ll$ notation.
## Formalization scope
Statements are given over the Prove2Me default environment (Lean `v4.30.0`, Mathlib `c5ea003`), in the shared namespace `CircleMethod`, and build on two published definitions: `CircleMethod_char` (the character `e` and the norm `nrm`) and `CircleMethod_genfun` (the generating function `f`).
Conventions this mission commits to:
- $\|\theta\|$ is `nrm θ = |θ - round θ|`. Mathlib's `round` breaks ties upwards, so `round` is *not* an odd function; the characterisation to use is minimality, `nrm θ ≤ |θ - n|` for every integer `n`, which is published as `CircleMethod.nrm_le`.
- Sums run over `Finset.range N`, that is $0\le x<N$, and $N$ is a natural number. Hypotheses `0 < N` and `0 < q` are stated explicitly rather than left implicit.
- Asymptotic notation is eliminated in favour of explicit existential constants: $X\ll_\varepsilon Y$ is rendered as `∀ ε > 0, ∃ C > 0, ∀ …, X ≤ C * Y`, with the constant quantified *outside* the parameters it may depend on and *inside* nothing else. Solvers should not weaken this by allowing $C$ to depend on $N$, $q$ or $\alpha$.
- Exponents such as $N^{1+\varepsilon}$ and $2^{1-k}$ are real powers (`Real.rpow`), not natural powers.
- Coprimality is `Nat.Coprime a.natAbs q`, which is the correct notion for a possibly negative numerator.
One trivialising formalization to rule out: the goal must not be read with $C$ permitted to depend on $N$, since then $C=N$ makes it vacuous. The quantifier order in the Lean statement already forbids this, and solvers should preserve it exactly.
Contributions welcome on any milestone independently; the divisor bound and the Farey covering are self-contained and need no other milestone. Both are reusable well beyond this mission.
## Selected references
- H. Weyl, *Über die Gleichverteilung von Zahlen mod. Eins*, Mathematische Annalen 77 (1916), 313--352. [DOI:10.1007/BF01475864](https://doi.org/10.1007/BF01475864)
- G. H. Hardy and J. E. Littlewood, *Some problems of 'Partitio Numerorum' I--VI*, 1920--1928.
- R. C. Vaughan, *The Hardy--Littlewood Method*, 2nd ed., Cambridge Tracts in Mathematics 125, Cambridge University Press, 1997. (Weyl's inequality is Lemma 2.4; the geometric sum bound is Lemma 2.1.)
- I. M. Vinogradov, *New estimates for Weyl sums*, Doklady Akademii Nauk SSSR 8 (1935), 195--198.
- T. D. Wooley, *Vinogradov's mean value theorem via efficient congruencing*, Annals of Mathematics 175 (2012), 1575--1627. [DOI:10.4007/annals.2012.175.3.12](https://doi.org/10.4007/annals.2012.175.3.12)
- J. Bourgain, C. Demeter and L. Guth, *Proof of the main conjecture in Vinogradov's mean value theorem for degrees higher than three*, Annals of Mathematics 184 (2016), 633--682. [DOI:10.4007/annals.2016.184.2.7](https://doi.org/10.4007/annals.2016.184.2.7)