Papers With

← All papers
First page of A Fourier approach to Gromov's filling area conjecture

A Fourier approach to Gromov's filling area conjecture

Le Chen, Xiaolong Li, Yimin Zhong

math.DG Sep 8, 2026 · v1
formalization mathlib geometry
Read PDF arXiv abstract Code
TL;DR
The main theorems (universal and orientable filling area lower bounds) are formalized in Lean 4 with Mathlib, provided in a companion repository.
Abstract
We prove that every compact connected Riemannian isometric filling $M$ of a circle of length $2π$ satisfies $\operatorname{Area}(M) \geq \frac{14ζ(3)}π \approx 5.35677$, regardless of orientability or topological types. Our new approach uses the odd Fourier coefficients of the distance functions from boundary points. For orientable fillings, we use a cubic resonant perturbation to obtain $\operatorname{Area}(M)>5.40154$.
Problem

Gromov's filling area conjecture states that every orientable Riemannian isometric filling of a circle of length 2π has area at least 2π. It remains open for genus at least two. The goal is a lower bound on filling area that holds uniformly over all topological types.

Approach

The odd Fourier coefficients of distance functions from boundary points define planar maps whose Jacobians satisfy a common pointwise bound. Orthogonal combinations of these maps are built so that their boundary traces are Jordan curves. The area formula and the Z_2 relative fundamental class then bound the Jacobian integrals from below. For orientable fillings, a cubic resonant perturbation of the Fourier map, together with a comass estimate, gives a stronger bound. Theorems 1.1, 1.2 and 4.1 are formalized in Lean with Mathlib 4.29.0.

Results

Every compact connected isometric filling, orientable or not, satisfies Area(M) ≥ 14ζ(3)/π ≈ 5.35677. Orientable fillings satisfy Area(M) > 5.40154.