Papers With

← All papers
First page of Weak uniqueness for the stochastic heat equation with nondegenerate diffusion: the full Hölder regime

Weak uniqueness for the stochastic heat equation with nondegenerate diffusion: the full Hölder regime

Yi Han

math.PR Nov 5, 2026 · v1
formalization mathlib probability analysis
Read PDF arXiv abstract
TL;DR
The author formalized Theorems 1.1 and 1.2 end-to-end in Lean 4 on top of Mathlib and Brownian motion libraries (scalar-she-lean repository).
Abstract
We prove weak well-posedness for the scalar stochastic heat equation on the one-dimensional torus with uniformly nondegenerate diffusion that is Holder continuous of any positive order. This resolves the weak uniqueness problem in the full positive Holder range, extending our earlier result for exponents above two thirds (arXiv:2608.01279). The proof couples a weak solution to a smooth companion and uses spatial cancellation to estimate the signed covariance difference in a negative Sobolev norm. A finite Gaussian expansion on each Littlewood-Paley block gives the decay needed to remove the coupling drift by a change of measure. A localized Girsanov argument extends the result to measurable drifts of linear growth.
Problem

Weak uniqueness in law for the scalar stochastic heat equation on the one-dimensional torus with uniformly nondegenerate diffusion was previously known only for Hölder exponents above 2/3. Whether it holds for every positive Hölder exponent was an open conjecture.

Approach

Each weak solution is coupled to a smooth controlled companion process. Spatial cancellation is used to estimate the signed covariance difference in a negative Sobolev norm. A finite Gaussian expansion on each Littlewood-Paley block supplies decay strong enough to remove the coupling drift by a change of measure, and a localized Girsanov argument extends the result to measurable drifts of linear growth. Theorems 1.1 and 1.2 were formalized end-to-end in Lean 4 using Mathlib together with the BrownianMotion, KolmogorovExtension4 and MathFin libraries.

Results

Weak existence and uniqueness in law hold for every positive Hölder exponent with bounded nondegenerate diffusion. The result extends to unbounded diffusion with bounded initial data and to measurable linear-growth drifts. The accompanying Lean code is in the scalar-she-lean repository.