Uniqueness in the reconstruction theorem

Proved

Hairer.reconstruction_uniqueness

by Lucas · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisdistributionsregularity-structuresspde

Uniqueness clause of Hairer's Theorem 3.10.

In the setting of the reconstruction theorem with $\gamma>0$ , let $f \in \mathcal{D}^\gamma$ and suppose that two distributions $\xi$ and $\zeta$ both satisfy the reconstruction bound: for every compact $K$ there is a constant $C$ with

\big|(\xi - \Pi_x f(x))(S^{\delta}_{s,x}\eta)\big| \le C\,\delta^{\gamma}, \qquad \big|(\zeta - \Pi_x f(x))(S^{\delta}_{s,x}\eta)\big| \le C\,\delta^{\gamma},

uniformly over $x \in K$ , $\delta \in (0,1]$ and $\eta \in \mathcal{B}^r_{s,0}$ . Then $\xi = \zeta$ .

This is the part of Theorem 3.10 that does not require the wavelet construction: the difference $\xi-\zeta$ is tested against localised test functions at scale $\delta$ and the resulting $O(\delta^{\gamma})$ bound, with $\gamma>0$ , forces it to vanish.

Preamble

import Definitions.Def_Hairer_Model

set_option autoImplicit false

open scoped Classical DirectSum

noncomputable section

Formal statement

namespace Hairer

/-- **Theorem 3.10 (uniqueness clause), Hairer 2014.**

If `γ > 0`, the bound (3.3) determines the reconstruction of a modelled distribution
uniquely: two distributions that are both approximated by the jets `Π_x f(x)` to order
`δ^γ` on every compact set coincide. -/
theorem reconstruction_uniqueness
    {d : ℕ} {s : Fin d → ℕ} (hs : IsScaling s)
    {A : Set ℝ} {E : A → Type} [∀ a : A, NormedAddCommGroup (E a)]
    [∀ a : A, NormedSpace ℝ (E a)]
    {G : Subgroup (ModelSpace A E ≃ₗ[ℝ] ModelSpace A E)} {one : ModelSpace A E}
    (hT : IsRegularityStructure A E G one)
    {r : ℕ} {Pi : Pt d → ModelSpace A E →ₗ[ℝ] Distrib d}
    {Gam : Pt d → Pt d → ModelSpace A E ≃ₗ[ℝ] ModelSpace A E}
    (hmod : IsModel s r G Pi Gam)
    {γ : ℝ} (hγ : 0 < γ)
    {f : Pt d → ModelSpace A E} (hf : IsModelled s γ Gam f)
    (ξ ζ : Distrib d)
    (hξ : ∀ K : Set (Pt d), IsCompact K → ∃ C : ℝ, ∀ x ∈ K, ∀ δ : ℝ, 0 < δ → δ ≤ 1 →
      ∀ η : Pt d → ℝ, IsTestBall s r η →
        |(ξ - Pi x (f x)).eval (scaledTest s δ x η)| ≤ C * δ ^ γ)
    (hζ : ∀ K : Set (Pt d), IsCompact K → ∃ C : ℝ, ∀ x ∈ K, ∀ δ : ℝ, 0 < δ → δ ≤ 1 →
      ∀ η : Pt d → ℝ, IsTestBall s r η →
        |(ζ - Pi x (f x)).eval (scaledTest s δ x η)| ≤ C * δ ^ γ) :
    ξ = ζ := by
  sorry

end Hairer

Source

M. Hairer, A theory of regularity structures, Inventiones Mathematicae 198 (2014) 269-504, arXiv:1303.5113 (v4), Theorem 3.10 (uniqueness clause) and its proof on p. 32-33

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

The ambient data are as follows: a dimension $d$ and a tuple $s$ of natural numbers with $s_i\ge1$ for all $i$ ; a set $A\subseteq\mathbb{R}$ and a family $(T_a)_{a\in A}$ of real normed spaces, with $T=\bigoplus_{a\in A}T_a$ the algebraic direct sum, $Q_a$ its projections and $\iota_a$ its inclusions; a subgroup $G$ of linear automorphisms of $T$ and an element $\mathbf 1$ satisfying the regularity-structure axioms ( $0\in A$ , $A$ bounded below and finite below every level, $\dim T_0=1$ , $\mathbf1\ne0$ purely of degree $0$ , the triangularity $Q_b(\Gamma\iota_a\tau-\iota_a\tau)=0$ for $a\le b$ , and $\Gamma\mathbf1=\mathbf1$ ); a natural number $r$ and maps $\Pi,\Gamma$ forming a model in the sense recalled by the model axioms ( $r$ least with $A\subseteq(-r,\infty)$ ; $\Gamma_{xy}\in G$ ; $\Gamma_{xx}=\mathrm{id}$ ; $\Gamma_{xy}\Gamma_{yz}=\Gamma_{xz}$ ; $\Pi_y=\Pi_x\Gamma_{xy}$ ; and the two uniform analytic bounds on $\Pi$ and $\Gamma$ over compact sets). Assume also $\gamma>0$ and that $f:\mathbb{R}^d\to T$ is modelled of order $\gamma$ : all components of $f(x)$ in degrees $\ge\gamma$ vanish, and on each compact set one constant controls both $\|Q_bf(x)\|$ and $\|Q_b(f(x)-\Gamma_{xy}f(y))\|/\|x-y\|_s^{\gamma-b}$ for $b<\gamma$ and $\|x-y\|_s\le1$ .

Let $\xi$ and $\zeta$ be two distributions — linear functionals on the space of smooth compactly supported functions, with no continuity requirement — and assume each of them approximates the local jets of $f$ to order $\gamma$ : for every compact $K\subseteq\mathbb{R}^d$ there is a real constant $C$ (depending only on $K$ and on the distribution in question) such that

\bigl|\langle\xi-\Pi_xf(x),\,S^{\delta}_{s,x}\eta\rangle\bigr|\le C\,\delta^{\gamma},\qquad \bigl|\langle\zeta-\Pi_xf(x),\,S^{\delta}_{s,x}\eta\rangle\bigr|\le C\,\delta^{\gamma},

for all $x\in K$ , all $\delta\in(0,1]$ and all $\eta$ in the class $\mathcal B^{r}_{s,0}$ of smooth functions whose closed support lies in $\{y:\|y\|_s\le1\}$ and whose iterated Fréchet derivatives of every order $k\le r$ have norm at most $1$ at every point.

The conclusion is the equality $\xi=\zeta$ of the two linear functionals.

Here $S^{\delta}_{s,x}\eta$ is the function $y\mapsto\delta^{-\sum_is_i}\,\eta\bigl((y_i-x_i)/\delta^{s_i}\bigr)_i$ , the pairing of a distribution with a function returns $0$ whenever the function is not smooth with compact support, and $\delta^{\gamma}$ is a real power. The constants are not required to be nonnegative, and the test class contains the zero function. The regularity exponent $\alpha=\min A$ plays no role in this statement; only $\gamma>0$ is assumed.

Human review

Endorsed by Shuze Chen · Sep 12, 2026
Endorsed by Lucas · Sep 12, 2026
Confirmed by the mission captain (proposal self-audit).

View graph