Papers With

← All papers
First page of Carleson operators on doubling metric measure spaces

Carleson operators on doubling metric measure spaces

Lars Becker, Floris van Doorn, Asgar Jamneshan, Rajula Srivastava, Christoph Thiele

math.CA Aug 7, 2025 · v1
formalization verification mathlib analysis
Read PDF arXiv abstract
TL;DR
Main Lp-bound theorems for Carleson operators on doubling metric measure spaces were computer-verified in Lean using Mathlib.
Abstract
Doubling metric measure spaces provide a natural framework for singular integral operators. In contrast, the study of maximally modulated singular integral operators, the so-called Carleson operators, has largely been limited to Euclidean space with modulation functions such as polynomials defined by algebraic means. We present a general axiomatic approach to modulation functions on doubling metric measure spaces and prove $L^p$ bounds for the corresponding Carleson operators in Theorem 1.1 and Theorem 1.2. This generalizes classical and modern results on Carleson operators. In addition to the proofs presented here, our main results have been computer verified using the language Lean and the library mathlib, as documented in the sibling communication arXiv:2405.06423.
Problem

The study of maximally modulated singular integral operators (Carleson operators) has been largely limited to Euclidean space with algebraically defined modulation functions. Extending these results to doubling metric measure spaces requires a new axiomatic framework.

Approach

The authors present a general axiomatic approach to modulation functions on doubling metric measure spaces and prove L^p bounds for the corresponding Carleson operators. The proof proceeds through tile structure existence, organization of tile sets into forests and antichains, and separate estimation of antichain and forest operators. In addition to the paper proofs, the main results have been computer-verified using Lean and the mathlib library, as documented in the sibling paper arXiv:2405.06423.

Results

The main theorems (Theorem 1.1 and Theorem 1.2) establish L^p bounds for Carleson operators on general doubling metric measure spaces, generalizing classical and modern results previously limited to Euclidean settings. The proofs are fully formalized in Lean/mathlib.