Prove2Me

Existence of the reconstruction of a modelled distribution for γ>0\gamma>0

Open
Hairer.reconstruction_existence_pointwise_pos

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

analysisdistributionsregularity-structuresspde

Existence half of Hairer's Theorem 3.10 for a positive exponent, stated for one modelled distribution.

Let T=(A,T,G)\mathscr T=(A,T,G) be a regularity structure, let (Π,Γ)(\Pi,\Gamma) be a model for it on Rd\mathbb R^d with scaling ss and test order rr, let α=min⁡A<0\alpha=\min A<0, and let γ>0\gamma>0. Then for every modelled distribution f∈Dγf\in\mathcal D^\gamma there exists a distribution ξ\xi such that

ξ∈Csα,∣(ξ−Πxf(x))(Ss,xδη)∣  ≤  C δγ,\xi\in\mathcal C^{\alpha}_s,\qquad \bigl|(\xi-\Pi_xf(x))(S^{\delta}_{s,x}\eta)\bigr|\;\le\;C\,\delta^{\gamma},

the second bound holding, for every compact set KK with a constant C=C(K,f)C=C(K,f), uniformly over x∈Kx\in K, δ∈(0,1]\delta\in(0,1] and all test functions η∈Bs,0r\eta\in\mathcal B^r_{s,0}.

Only the existence of ξ\xi for a single ff is asserted. For γ>0\gamma>0 the displayed bound determines ξ\xi uniquely, so the linearity of the assignment f↦ξf\mapsto\xi — which is part of the statement of Theorem 3.10 — is a formal consequence of uniqueness and is deliberately not included here. This is the analytic core of the theorem in the positive range: Hairer obtains ξ\xi as the limit of a convergent multiscale approximation built from a wavelet multiresolution analysis adapted to the scaling ss (§3.1).

Preamble
import Definitions.Def_Hairer_Model

set_option autoImplicit false

open scoped Classical DirectSum

noncomputable section
Formal statement
namespace Hairer

/-- **Theorem 3.10 (existence of the reconstruction), Hairer 2014**, in the case `γ > 0`,
stated for a single modelled distribution.

For `f ∈ D^γ` with `γ > 0` there is a distribution `ξ ∈ C^α_s` such that, on every
compact set `K`, `|(ξ - Π_x f(x))(S^δ_{s,x} η)| ≲ δ^γ` uniformly over `x ∈ K`,
`δ ∈ (0,1]` and `η ∈ B^r_{s,0}`. For `γ > 0` such a `ξ` is unique, so the linearity of
`f ↦ ξ` is automatic and is not part of this statement. -/
theorem reconstruction_existence_pointwise_pos
    {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α : IsLeast A α) (hαneg : α < 0)
    {γ : ℝ} (hγ : 0 < γ)
    {f : Pt d → ModelSpace A E} (hf : IsModelled s γ Gam f) :
    ∃ ξ : Distrib d,
      MemCalpha s α ξ ∧
      ∀ 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, Invent. Math. 198 (2014) 269-504, arXiv:1303.5113 (v4), Theorem 3.10, p. 31 (existence half, case gamma > 0; construction in Section 3.1)

View graph