Papers With

← All papers
First page of Modulus of continuity for solutions of non-local heat equations

Modulus of continuity for solutions of non-local heat equations

Ben Andrews, Sophie Chen

math.AP Jul 25, 2025 · v4
formalization analysis
Read PDF arXiv abstract
TL;DR
Theorem 2.3 and its proof were formalized in Lean 4 with AI assistance (including Aristotle); the repository is available on request.
Abstract
We extend the method of modulus of continuity for solutions of parabolic equations–as used, for instance, to prove the Fundamental Gap Conjecture–to solutions of non-local heat equations on R^n and in dimension one with a non-local Neumann boundary condition. Specifically, we show that if a solution of a non-local heat equation has an initial modulus of continuity satisfying simple criteria, then this modulus of continuity is preserved at all subsequent times. In the process of trying to generalise our result in one dimension, we found a counterexample suggesting that a non-local analogue of the Payne-Weinberger inequality would depend on more than the diameter of a bounded (convex) domain.
Problem

The modulus-of-continuity method for parabolic equations, used for example in the proof of the Fundamental Gap Conjecture, applies to classical heat equations. The question is whether it extends to non-local heat equations, both on R^n and on bounded domains with a non-local Neumann condition.

Approach

A proof by contradiction applies a maximum principle to an auxiliary two-point function, regularized by a growing function Psi with bounded image under the non-local operator. A coupling-by-reflection change of variables reduces the problem to a one-dimensional non-local heat equation for the odd extension of the modulus. The argument is carried out on R^n with integrable kernels, on a compact interval (the regional equation), and for a non-linear gradient perturbation. Theorem 2.3 was formalized in Lean 4.

Figure 1. Change of variables using a ‘coupling-by-reflection’ technique.
Results

An initial modulus of continuity satisfying the stated criteria is preserved for all later times on R^n, in the one-dimensional regional case, and in the non-linear case. A counterexample indicates that a non-local Payne-Weinberger inequality would depend on more than the domain's diameter.