∑math20

Real and complex analysis · Result 082

Annular variation and dyadic absolute bounds for the triangular Hilbert transform

3 papersLean

Proves maximal and annular r-variation bounds, for every r > 2, from complex \(L^3(\mathbb R^2)\times L^3(\mathbb R^2)\) to \(L^{3/2}(\mathbb R^2)\). The maximal estimate controls both hard truncation endpoints and gives almost-everywhere and norm convergence. Pairing with a third input settles the triangular Hilbert transform estimate at the symmetric \(L^3\times L^3\times L^3\) point.

Watch

1

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation
2

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation
▶The proposed solutionin preparation

Papers 3

First page of Annular variation of the triangular Hilbert transform at the symmetric point

Annular variation of the triangular Hilbert transform at the symmetric point

OpenAI · October 5, 2026

We prove the annular r-variation estimate for the triangular Hilbert transform from complex \(L^3\times L^3\) to L3/2 for every r > 2. The partitions may depend on the output point and range over all positive scales. The estimate yields the two-endpoint maximal bound and joint almost-everywhere and norm principal values, and resolves the symmetric scalar triangular Hilbert transform problem.

Read PDF Download Source

Cite
@misc{OAI:Annular-variation-of-the-triangular-Hilbert-transform-at-the-symmetric-point-October-5-2026,
  author = {{OpenAI}},
  title = {{Annular variation of the triangular Hilbert transform at the symmetric point}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Annular-variation-of-the-triangular-Hilbert-transform-at-the-symmetric-point-October-5-2026/annular-variation.pdf}{OAI:Annular-variation-of-the-triangular-Hilbert-transform-at-the-symmetric-point-October-5-2026}},
  year = {2026}
}
First page of An L³ bound for the dyadic triangular Hilbert form

An L³ bound for the dyadic triangular Hilbert form

OpenAI · October 5, 2026

We prove a uniform \(L^3\times L^3\times L^3\) estimate for the dyadic triangular Hilbert form with unrestricted real inputs. The sum of the absolute local contributions over any finite set of scales is bounded by forty times the product of the input norms. In particular, the bound allows coefficients of modulus at most one to vary independently among admissible interval triples.

Read PDF Download Source

Cite
@misc{OAI:An-L3-bound-for-the-dyadic-triangular-Hilbert-form-October-5-2026,
  author = {{OpenAI}},
  title = {{An $L^3$ bound for the dyadic triangular Hilbert form}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/An-L3-bound-for-the-dyadic-triangular-Hilbert-form-October-5-2026/dyadic-triangular-hilbert.pdf}{OAI:An-L3-bound-for-the-dyadic-triangular-Hilbert-form-October-5-2026}},
  year = {2026}
}
First page of The maximal triangular Hilbert transform at the symmetric point

The maximal triangular Hilbert transform at the symmetric point

OpenAI · September 24, 2026

For arbitrary complex inputs in \(L^3(\mathbb R^2)\), we prove the pointwise maximal \(L^3\times L^3\to L^{3/2}\) estimate for the triangular Hilbert transform, with the supremum over both hard truncation endpoints. The estimate yields joint almost-everywhere and L3/2 convergence as the lower endpoint tends to zero and the upper endpoint tends to infinity. This also proves the conjectured scalar estimate at the symmetric point.

Read PDF Download Source

Cite
@misc{OAI:The-maximal-triangular-Hilbert-transform-at-the-symmetric-point-September-24-2026,
  author = {{OpenAI}},
  title = {{The maximal triangular Hilbert transform at the symmetric point}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-maximal-triangular-Hilbert-transform-at-the-symmetric-point-September-24-2026/paper.pdf}{OAI:The-maximal-triangular-Hilbert-transform-at-the-symmetric-point-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

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

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

ResultComparator statement
Maximal triangular Hilbert transform boundTriangularHilbert.lean

Scope note on GitHub →