$\Pi$ on $T_\nu$ is determined by $\Gamma$ (Hairer, Proposition 3.31)

Proved

Hairer.pi_determined_by_gamma

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

analysisdistributionsregularity-structuresspde

Proposition 3.31 of Hairer (2014), determinacy statement.

Let $\nu>0$ be an element of the index set $A$ . The action of $\Pi$ on the homogeneous component $T_\nu$ is completely determined by $\Gamma$ together with the action of $\Pi$ on lower homogeneities: if $(\Pi,\Gamma)$ and $(\Pi',\Gamma)$ are two models for the same regularity structure, with the same $\Gamma$ , and if $\Pi_x a = \Pi'_x a$ for every $x$ and every $a \in T_b$ with $b<\nu$ , then $\Pi_x a = \Pi'_x a$ for every $x$ and every $a \in T_\nu$ .

The mechanism is that for positive homogeneity the distribution $\Pi_x a$ is forced to be the reconstruction of the modelled distribution $y \mapsto \Gamma_{yx}a$ minus its lower-order part, so no freedom is left once $\Gamma$ and the lower levels are fixed. Hairer states the result together with the quantitative bound (3.42) on the $T_\nu$ component of $\Pi$ in terms of the model norms; the content formalized here is the determinacy assertion.

Preamble

import Definitions.Def_Hairer_Model

set_option autoImplicit false

open scoped Classical DirectSum

noncomputable section

Formal statement

namespace Hairer

/-- **Proposition 3.31, Hairer 2014.**

For `ν > 0`, the action of `Π` on `T_ν` is completely determined by its action on
`T_{<ν}` together with `Γ`: two models for the same regularity structure that share
the same `Γ` and whose `Π`-maps agree on all homogeneities strictly below `ν` also
agree on `T_ν`. -/
theorem pi_determined_by_gamma
    {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 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) (hmod' : IsModel s r G Pi' Gam)
    {ν : ℝ} (hν : 0 < ν) (hνA : ν ∈ A)
    (hlow : ∀ (b : A), (b : ℝ) < ν → ∀ (a : E b), ∀ x : Pt d,
      Pi x (incl b a) = Pi' x (incl b a)) :
    ∀ (a : E (⟨ν, hνA⟩ : A)), ∀ x : Pt d,
      Pi x (incl (⟨ν, hνA⟩ : A) a) = Pi' x (incl (⟨ν, hνA⟩ : A) a) := by
  sorry

end Hairer

Source

M. Hairer, A theory of regularity structures, Inventiones Mathematicae 198 (2014) 269-504, arXiv:1303.5113 (v4), Proposition 3.31, p. 44 (with the bound (3.42))

Read-back

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

Fix a dimension $d$ and a tuple $s$ of natural numbers with $s_i\ge1$ for every index; a set $A\subseteq\mathbb{R}$ with real normed spaces $(T_a)_{a\in A}$ and the algebraic direct sum $T=\bigoplus_{a\in A}T_a$ , with inclusions $\iota_a:T_a\to T$ ; a subgroup $G$ of the linear automorphisms of $T$ and a unit $\mathbf1$ making $(A,T,G)$ a regularity structure (in particular $0\in A$ , $A$ is bounded below and finite below each level, $\dim T_0=1$ , and every $\Gamma\in G$ fixes $\mathbf1$ and satisfies the triangularity condition).

Let $r$ be a natural number, let $\Gamma$ be a single family of automorphisms $\Gamma_{xy}$ , and let $\Pi$ and $\Pi'$ be two assignments of linear maps $T\to\mathcal D'$ such that both $(\Pi,\Gamma)$ and $(\Pi',\Gamma)$ are models with the same test order $r$ and the same $\Gamma$ : each satisfies $\Gamma_{xy}\in G$ , $\Gamma_{xx}=\mathrm{id}$ , $\Gamma_{xy}\Gamma_{yz}=\Gamma_{xz}$ , the compatibility $\Pi_y=\Pi_x\Gamma_{xy}$ (respectively $\Pi'_y=\Pi'_x\Gamma_{xy}$ ), and the two uniform bounds

|\langle\Pi_x\iota_\ell a,S^\delta_{s,x}\eta\rangle|\le C\|a\|\delta^{\ell},\qquad \|Q_m\Gamma_{xy}\iota_\ell a\|\le C\|a\|\,\|x-y\|_s^{\ell-m}

valid on each compact set for all degrees $\ell<\gamma$ (any $\gamma>0$ ), $m<\ell$ , $\delta\in(0,1]$ and test functions $\eta\in\mathcal B^{r}_{s,0}$ .

Assume a real number $\nu$ with $\nu>0$ and $\nu\in A$ , and assume that $\Pi$ and $\Pi'$ agree in all strictly lower degrees:

\Pi_x(\iota_b a)=\Pi'_x(\iota_b a)\qquad\text{for every }b\in A\text{ with }b<\nu,\ \text{every }a\in T_b,\ \text{every }x\in\mathbb{R}^d.

The conclusion is that they also agree in degree $\nu$ : for every $a\in T_{\nu}$ and every point $x\in\mathbb{R}^d$ ,

\Pi_x(\iota_{\nu}a)=\Pi'_x(\iota_{\nu}a)

as linear functionals on smooth compactly supported functions.

The equalities asserted and assumed are equalities of distributions in the sense used here, namely of arbitrary linear functionals on the space of smooth compactly supported test functions (no continuity requirement enters). Only elements of the single homogeneous component $T_\nu$ , injected into $T$ , are compared; nothing is claimed about non-homogeneous elements beyond what linearity and the lower-degree hypothesis give. The hypothesis on lower degrees ranges over all $b\in A$ strictly below $\nu$ , including negative ones.

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

Π\PiΠ on TνT_\nuTν​ is determined by Γ\GammaΓ (Hairer, Proposition 3.31)

$\Pi$ on $T_\nu$ is determined by $\Gamma$ (Hairer, Proposition 3.31)