Papers With

← All papers
First page of A curved three-dimensional simplex Hilbert transform

A curved three-dimensional simplex Hilbert transform

Polona Durcik, Marco Fraccaroli, Joris Roos

math.CA Oct 17, 2026 · v1
formalization mathlib ai-agents analysis
Read PDF arXiv abstract Code
TL;DR
The main harmonic-analysis theorem was formally verified in Lean 4 with Mathlib by AI coding agents; the proof is published on GitHub.
Abstract
We prove Lebesgue space estimates for a curved three-dimensional simplex Hilbert transform associated with the moment curve $t \mapsto (t,t^2,t^3)$. The analysis relies on smoothing inequalities for curved multilinear averages and on estimates for a three-dimensional anisotropic variant of the twisted paraproduct. The result has been formally verified in Lean 4.
Problem

The goal is to prove Lebesgue space bounds for a curved three-dimensional simplex Hilbert transform along the moment curve t ↦ (t, t², t³). This is a curved analogue of the simplex Hilbert transform, whose boundedness is a major open problem.

Approach

The operator is decomposed with Littlewood–Paley methods into two parts. The first is handled by smoothing inequalities for curved multilinear averages, building on Kosz–Mirek–Peluse–Wan–Wright. The second is a three-dimensional anisotropic twisted paraproduct, bounded via cone decompositions, tree localization, Cauchy–Schwarz, telescoping identities, Brascamp–Lieb inequalities and stopping-time arguments. AI coding agents formally verified the result in Lean 4 using Mathlib.

Results

The operator is bounded from L^{p1}×L^{p2}×L^{p3} to L^p for p in (1, 4/3), p_i in (1, 4) with Hölder scaling. The proof is machine-checked in Lean 4 and available on GitHub.