5 papers
Formalising Linear Elliptic PDE Theory in Lean 4
Alejandro José Soto Franco, Kobe Marshall-Stevens
We formalise in Lean 4, on top of Mathlib, the solvability of the Dirichlet problem for second-order linear elliptic operators in divergence form. The machine-verified results, wit…
Isoperimetry by stretching
Kobe Marshall-Stevens, Gongping Niu
We construct isoperimetric regions from separating hypersurfaces in closed manifolds. This yields isoperimetric boundaries exhibiting a wide variety of topological types and singul…
Generic regularity of isoperimetric regions in dimension eight
Kobe Marshall-Stevens, Gongping Niu, Davide Parise
We establish generic regularity results for isoperimetric regions in closed Riemannian manifolds of dimension eight. In particular, we show that every isoperimetric region has a sm…
Gradient flow of phase transitions with fixed contact angle
Kobe Marshall-Stevens, Mayu Takada, Yoshihiro Tonegawa +1
We study the gradient flow of the Allen-Cahn equation with fixed boundary contact angle in Euclidean domains for initial data with bounded energy. Under general assumptions, we est…
On isolated singularities and generic regularity of min-max CMC hypersurfaces
Costante Bellettini, Kobe Marshall-Stevens
In compact Riemannian manifolds of dimension 3 or higher with positive Ricci curvature, we prove that every constant mean curvature hypersurface produced by the Allen-Cahn min-max…