# Hilbert transforms along Lipschitz directions

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

- [A uniform Hilbert transform estimate for Lipschitz directions](../../preprints/A-uniform-Hilbert-transform-estimate-for-Lipschitz-directions-September-25-2026/main.pdf)

## Scope

The formalization proves uniform $L^2$ bounds for short Hilbert transforms along Lipschitz unit vector fields in the plane, including fields depending on both coordinates. For Lipschitz constant $K>0$, every hard truncation with $0<\varepsilon\le R\le1/(10^6K)$ has one universal $L^2$ bound on Schwartz functions, independent of the inner cutoff.

At a fixed short scale for $1$-Lipschitz fields, the formalization also gives principal-value and weak-$(2,2)$ estimates and bounded extensions to all of $L^2$. These results establish the stated short-scale form of Stein's question.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Uniform short Hilbert-transform bounds for Lipschitz directions | [LipschitzHilbert.lean](../ComparatorChallenges/LipschitzHilbert.lean) |