# Annular variation and dyadic absolute bounds for the triangular Hilbert transform

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [The maximal triangular Hilbert transform at the symmetric point](../../preprints/The-maximal-triangular-Hilbert-transform-at-the-symmetric-point-September-24-2026/paper.pdf)

## Scope

The formalized result proves the symmetric maximal estimate for the triangular Hilbert transform: for arbitrary complex $F,G\in L^3(\mathbb R^2)$, the $L^{3/2}$ norm of the supremum over all finite hard-truncation intervals is at most $C\|F\|_3\|G\|_3$ for one absolute constant $C$. It also establishes a common full-measure set on which the truncated integrals are defined and almost-everywhere measurability of the maximal output.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Maximal triangular Hilbert transform bound | [TriangularHilbert.lean](../ComparatorChallenges/TriangularHilbert.lean) |