5 papers
A blueprint for the formalization of norm-variation of multiple ergodic averages for commuting transformations
Floris van Doorn, Polona Durcik, Joris Roos +2
This blueprint serves as a companion to a forthcoming, shorter traditional mathematical paper. The purpose of this blueprint is two-fold: first, it has served as the foundation for…
Quantitative Polynomial Wiener-Wintner Theorems
Lars Becker, Asgar Jamneshan, Christoph Thiele
We prove quantitative polynomial Wiener--Wintner theorems in a very general setup, including measure-preserving actions of nilpotent Lie groups. Our results apply both to ergodic a…
An SU(2n)-valued nonlinear Fourier transform
Michel Alexis, Lars Becker, Diogo Oliveira e Silva +1
We define a nonlinear Fourier transform which maps sequences of contractive matrices to -valued functions on the circle . We characterize the image…
Carleson operators on doubling metric measure spaces
Lars Becker, Floris van Doorn, Asgar Jamneshan +2
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…
A blueprint for the formalization of Carleson's theorem on convergence of Fourier series
Lars Becker, María Inés de Frutos-Fernández, Leo Diedering +14
This paper is the blueprint underlying the Lean formalization of the proof of Carleson's classical result asserting almost everywhere convergence of Fourier series of continuous fu…