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
Captain: korbonits
Formalize Navier-StokesOpen Problem
## Motivation
The incompressible Navier–Stokes equations are the standard model for the motion of a viscous fluid such as water or air, used daily in engineering, meteorology and oceanography. Yet the most basic mathematical question about them is open: starting from smooth initial data in three dimensions, does a smooth solution exist for all time? This is one of the seven Millennium Prize Problems of the Clay Mathematics Institute. Its official formulation is Charles Fefferman's problem description, [*Existence and smoothness of the Navier–Stokes equation*](https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf) (2000), which offers a prize for a proof of any one of four statements: global existence and smoothness on $\mathbb{R}^3$ (statement (A)) or on the torus $\mathbb{R}^3/\mathbb{Z}^3$ (statement (B)), or a counterexample to either (statements (C) and (D)). This mission formalizes statement (A), together with the classical partial results that Fefferman lists as known.
**Timeline.**
- 1822–1845: Navier and Stokes write down the equations of a viscous incompressible fluid.
- 1934: Jean Leray, [*Sur le mouvement d'un liquide visqueux emplissant l'espace*](https://doi.org/10.1007/BF02547354) (Acta Math. 63), proves on $\mathbb{R}^3$ that smooth solutions exist for a positive time depending on the data, that they exist for all time when the data is small compared with the viscosity, and that global *weak* solutions with finite energy always exist. Their smoothness and uniqueness are left open.
- 1933–1969: the two-dimensional problem is settled (Leray for the plane; Olga Ladyzhenskaya's monograph [*The Mathematical Theory of Viscous Incompressible Flow*](https://archive.org/details/mathematicaltheo0000lady), 2nd ed. 1969, for bounded domains): smooth solutions exist for all time and are unique.
- 1984: Tosio Kato, [*Strong $L^p$-solutions of the Navier–Stokes equation in $\mathbb{R}^m$*](https://doi.org/10.1007/BF01174182) (Math. Z. 187), gives global solutions for initial data small in $L^3(\mathbb{R}^3)$.
- 1976–1998: partial regularity. Scheffer, then [Caffarelli, Kohn and Nirenberg](https://doi.org/10.1002/cpa.3160350604) (Comm. Pure Appl. Math. 35, 1982), show that the singular set of a suitable weak solution has one-dimensional parabolic Hausdorff measure zero.
- 2000: the Clay Mathematics Institute adopts Fefferman's formulation as a Millennium Prize Problem. It remains open.
## Setting
Fix a dimension $n \ge 1$ and write $\mathbb{R}^n$ for Euclidean $n$-space with its Euclidean norm $|x|$; in Lean this is `NavierStokes.Vec n`. A **velocity field** assigns to each time $t \in \mathbb{R}$ and point $x \in \mathbb{R}^n$ a vector $u(x,t) \in \mathbb{R}^n$; in Lean $u\,t$ is the field at time $t$ and $u\,t\,x$ is Fefferman's $u(x,t)$. A **pressure** is a real function $p(x,t)$. The **viscosity** $\nu$ is a positive constant. The external force of Fefferman's equation (1) is identically zero throughout, as in statement (A).
For a vector field $v : \mathbb{R}^n \to \mathbb{R}^n$ the **divergence** is
$$\operatorname{div} v = \sum_{i=1}^n \frac{\partial v_i}{\partial x_i},$$
in Lean `NavierStokes.div`, computed from the Fréchet derivative $Dv(x)$ as $\sum_i (Dv(x)\,e_i)_i$. The **Laplacian** $\Delta v = \sum_i \partial^2 v/\partial x_i^2$ acts componentwise (Mathlib's Laplacian on inner product spaces). The **gradient** $\nabla p$ is Mathlib's gradient. The convective term $\sum_j u_j\,\partial u/\partial x_j$ is the derivative of $u(\cdot,t)$ at $x$ in the direction $u(x,t)$. Finally $|\nabla v|^2 = \sum_{i,j} (\partial v_i/\partial x_j)^2$ is `NavierStokes.gradNormSq`.
**Admissible initial data** (Fefferman's condition (4), `NavierStokes.IsInitialData`): a $C^\infty$, divergence-free vector field $u^0$ that decays together with all its derivatives faster than any power,
$$|\partial_x^\alpha u^0(x)| \le C_{\alpha K}\,(1+|x|)^{-K} \quad \text{on } \mathbb{R}^n, \text{ for every } \alpha \text{ and } K.$$
In Lean the bound is $(1+|x|)^K\,\|D^k u^0(x)\| \le C_{kK}$ on the $k$-th Fréchet derivative, an equivalent family of conditions. These are exactly the divergence-free Schwartz functions.
A **physically reasonable solution** on a set $S$ of times (`NavierStokes.IsSolutionOn`; $S = [0,\infty)$ for `NavierStokes.IsSolution`) is a pair $(u,p)$ such that
1. (Fefferman (6)) $u$ and $p$ are $C^\infty$ on $S \times \mathbb{R}^n$, up to the boundary of $S$;
2. (Fefferman (1), $f \equiv 0$) for every $t \in S$ with $t > 0$ and every $x$,
$$\frac{\partial u}{\partial t} + \sum_{j=1}^n u_j \frac{\partial u}{\partial x_j} = \nu\,\Delta u - \nabla p;$$
3. (Fefferman (2)) $\operatorname{div} u(\cdot,t) = 0$ for every $t \in S$;
4. (Fefferman (3)) $u(x,0) = u^0(x)$;
5. (Fefferman (7), bounded energy) $\int_{\mathbb{R}^n} |u(x,t)|^2\,dx < C$ for all $t \in S$, for some constant $C$.
## Formalization targets
### Goal: Fefferman's statement (A)
Take $\nu > 0$ and $n = 3$. For every admissible initial datum $u^0$ there exist a velocity field $u$ and a pressure $p$ forming a physically reasonable solution on $\mathbb{R}^3 \times [0,\infty)$:
$$\forall\, \nu > 0,\ \forall\, u^0 \text{ satisfying (4)},\ \exists\, (u,p) \text{ satisfying (1), (2), (3), (6), (7) on } \mathbb{R}^3 \times [0,\infty).$$
This is `NavierStokes.existence_and_smoothness_R3`. It is open; a proof would settle the Millennium Prize Problem in the affirmative.
### Milestones: what Fefferman lists as known
1. **Local existence** (`NavierStokes.local_existence_R3`): for $n = 3$ and every admissible $u^0$ there are $T > 0$ and a physically reasonable solution on $\mathbb{R}^3 \times [0,T)$. Fefferman: "(A) and (B) hold ... if the time interval $[0,\infty)$ is replaced by a small time interval $[0,T)$, with $T$ depending on the initial data."
2. **Global existence for small data** (`NavierStokes.small_data_global_existence_R3`): there is an absolute constant $c > 0$ such that, for $n = 3$, (A) holds for every admissible $u^0$ with
$$\|u^0\|_{L^2}^2\,\|\nabla u^0\|_{L^2}^2 \le c\,\nu^4.$$
Fefferman: "(A) and (B) hold provided the initial velocity $u^0$ satisfies a smallness condition." The scale-invariant product is Leray's form of the condition; it implies smallness of $\|u^0\|_{L^3}/\nu$, so Kato's theorem also applies.
3. **The two-dimensional case** (`NavierStokes.existence_and_smoothness_R2`): statement (A) with $n = 2$. Fefferman: "In two dimensions, the analogues of assertions (A) and (B) have been known for a long time (Ladyzhenskaya)."
A bridging lemma, `NavierStokes.isInitialData_iff_schwartz`, identifies the admissible data with the divergence-free elements of Mathlib's Schwartz space.
## Significance
*The result itself.* Statement (A) asks whether the basic model of viscous flow is well posed in the classical sense, i.e. whether smooth finite-energy flows can develop singularities in finite time. A positive answer shows the equations never leave the classical regime; a negative one shows the model predicts its own breakdown. Fefferman: "since we don't even know whether these solutions exist, our understanding is at a very primitive level."
*Formalizing it.* None of the results in this mission has a machine-checked proof, and Mathlib contains no theory of the Navier–Stokes or Euler equations. The milestones are all proved in the literature; formalizing them requires building, on Mathlib's calculus, measure theory and Schwartz space, the heat semigroup on $\mathbb{R}^n$, the pressure equation $\Delta p = -\sum_{i,j} \partial_i\partial_j(u_i u_j)$ or the Leray projection, energy estimates, and a fixed-point construction of solutions, most of which is reusable for other evolution equations. The goal is open and expected to remain so; its role is to fix in Lean the exact statement the prize asks for, so partial results are formalized against it.
## Difficulty
The energy identity $\frac{d}{dt}\int|u|^2 = -2\nu\int|\nabla u|^2$ controls $u$ in $L^2$ and $\nabla u$ in $L^2_{t,x}$, but in three dimensions this control is *supercritical*: under the scaling $u_\lambda(x,t) = \lambda u(\lambda x, \lambda^2 t)$ that preserves the equations, the energy of $u_\lambda$ shrinks as $\lambda \to \infty$, so bounded energy does not prevent concentration at small scales. Every known continuation criterion (Leray, Prodi–Serrin, Beale–Kato–Majda, Escauriaza–Seregin–Šverák) needs a quantity at or above critical scaling, none of which the energy controls. The obvious first idea, an ordinary differential inequality for $\|\nabla u(t)\|_{L^2}$, gives $\frac{d}{dt}\|\nabla u\|_{L^2}^2 \le C\nu^{-3}\|\nabla u\|_{L^2}^6$, which closes only for small data or short time. That is exactly why milestones 1 and 2 are theorems and the goal is not.
The formalization adds a second difficulty: the solutions of the literature live in Sobolev or Besov spaces, with pointwise smoothness of $u$ and $p$ recovered afterwards by regularity theory, and Mathlib has neither Sobolev spaces on $\mathbb{R}^n$ nor the heat semigroup in usable form.
## Formalization scope
- $\mathbb{R}^n$ is `EuclideanSpace ℝ (Fin n)` with Lebesgue measure; the dimension is a parameter, the goal fixes $n = 3$ and the 2D milestone $n = 2$.
- A velocity field is a function of all real times, but every condition is imposed only on the time set $S$; values at negative times are unconstrained.
- Smoothness on $\mathbb{R}^n \times [0,\infty)$ is Mathlib's `ContDiffOn` of the uncurried map on the closed half-space, i.e. all derivatives extend continuously to $t = 0$. The momentum equation is imposed at interior times $t > 0$ with two-sided derivatives; by continuity of the derivatives this is equivalent to Fefferman's "$t \ge 0$".
- Derivatives are Mathlib's total functions (`fderiv`, `deriv`, `iteratedFDeriv`, `gradient`, Laplacian) with junk value $0$ at non-differentiable points; the smoothness hypotheses make every derivative in the statements honest.
- The energy is a Lebesgue integral in $[0,\infty]$, equal to $\infty$ when $u(\cdot,t) \notin L^2$, so bounded energy cannot hold vacuously. The $L^2$ norms in the small-data hypothesis are Bochner integrals, genuine for Schwartz data.
- No normalization is imposed on the pressure, as in Fefferman's text.
*No trivializing formalization.* The zero field solves the equations only for $u^0 = 0$; for any other admissible $u^0$ the initial condition, smoothness, the equation on $t > 0$ and bounded energy must all hold.
*Infrastructure needed and welcome contributions.* The heat kernel on $\mathbb{R}^n$ with Schwartz bounds; the Riesz-transform representation of the pressure or the Leray projection; energy identities for smooth decaying solutions; local existence by Picard iteration; the two-dimensional vorticity equation and its maximum principle. Theorems in the `NavierStokes` namespace, decompositions of the milestones, and Mathlib lemmas about `ContDiffOn` on half-spaces are all welcome. Statements (B), (C), (D) and the Euler equations ($\nu = 0$) are out of scope.
## Selected references
- C. L. Fefferman, *Existence and smoothness of the Navier–Stokes equation*, Clay Mathematics Institute Millennium Prize Problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf
- J. Leray, *Sur le mouvement d'un liquide visqueux emplissant l'espace*, Acta Mathematica 63 (1934), 193–248. https://doi.org/10.1007/BF02547354
- O. A. Ladyzhenskaya, *The Mathematical Theory of Viscous Incompressible Flow*, 2nd ed., Gordon and Breach, 1969. https://archive.org/details/mathematicaltheo0000lady
- T. Kato, *Strong $L^p$-solutions of the Navier–Stokes equation in $\mathbb{R}^m$, with applications to weak solutions*, Mathematische Zeitschrift 187 (1984), 471–480. https://doi.org/10.1007/BF01174182
- L. Caffarelli, R. Kohn, L. Nirenberg, *Partial regularity of suitable weak solutions of the Navier–Stokes equations*, Communications on Pure and Applied Mathematics 35 (1982), 771–831. https://doi.org/10.1002/cpa.3160350604
- A. J. Majda, A. L. Bertozzi, *Vorticity and Incompressible Flow*, Cambridge University Press, 2002. https://doi.org/10.1017/CBO9780511613203
- J. C. Robinson, J. L. Rodrigo, W. Sadowski, *The Three-Dimensional Navier–Stokes Equations: Classical Theory*, Cambridge University Press, 2016. https://doi.org/10.1017/CBO9781139095143