Prove2Me

Existence of a linear reconstruction operator for α<γ≤0\alpha<\gamma\le 0

Open
Hairer.reconstruction_operator_nonpos

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

analysisdistributionsregularity-structuresspde

Retired. Superseded by Hairer.reconstruction_existence_pointwise_nonpos, which asks only for the pointwise reconstruction in the same range α<γ≤0\alpha<\gamma\le 0 and is therefore strictly weaker: the linearity of f↦Rff\mapsto\mathcal Rf required by Theorem 3.10 can be recovered from the pointwise statement, because the pairs (f,ξ)(f,\xi) satisfying the reconstruction conditions form a linear subspace surjecting onto Dγ\mathcal D^\gamma, and that surjection admits a linear section. Prove the replacement instead.

Existence half of Hairer's Theorem 3.10 in the non-positive range α<γ≤0\alpha<\gamma\le 0.

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\alpha<\gamma\le 0. Then there is a map R\mathcal R, linear on Dγ\mathcal D^\gamma, with Rf∈Csα\mathcal Rf\in\mathcal C^{\alpha}_s and

∣(Rf−Πxf(x))(Ss,xδη)∣≤C δγ\bigl|(\mathcal Rf-\Pi_xf(x))(S^{\delta}_{s,x}\eta)\bigr|\le C\,\delta^{\gamma}

uniformly over xx in a compact set, δ∈(0,1]\delta\in(0,1] and η∈Bs,0r\eta\in\mathcal B^r_{s,0}.

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 operator), Hairer 2014**, in the
case `α < γ ≤ 0`.

For `γ ≤ 0` the bound (3.3) no longer determines the reconstruction, so a *linear*
choice `f ↦ Rf` has to be constructed; Hairer does this with a wavelet multiresolution
analysis adapted to the scaling `s` (§3.1). The conclusion is that of Theorem 3.10:
`R` is linear on `D^γ`, takes values in `C^α_s`, and satisfies
`|(Rf - Π_x f(x))(S^δ_{s,x} η)| ≲ δ^γ` uniformly over `x` in a compact set,
`δ ∈ (0,1]` and `η ∈ B^r_{s,0}`.

The range `γ ≤ α` is excluded because it is degenerate: there the only modelled
distribution is `f = 0`. -/
theorem reconstruction_operator_nonpos
    {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γα : α < γ) (hγ : γ ≤ 0) :
    ∃ R : (Pt d → ModelSpace A E) → Distrib d,
      (∀ f g : Pt d → ModelSpace A E, IsModelled s γ Gam f → IsModelled s γ Gam g →
        R (f + g) = R f + R g) ∧
      (∀ (c : ℝ) (f : Pt d → ModelSpace A E), IsModelled s γ Gam f →
        R (c • f) = c • R f) ∧
      (∀ f : Pt d → ModelSpace A E, IsModelled s γ Gam f →
        MemCalpha s α (R f) ∧
        ∀ K : Set (Pt d), IsCompact K → ∃ C : ℝ, ∀ x ∈ K, ∀ δ : ℝ, 0 < δ → δ ≤ 1 →
          ∀ η : Pt d → ℝ, IsTestBall s r η →
            |(R f - 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 in the non-positive range; construction in Section 3.1)

View graph