Main.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The main results of “A uniform Hilbert transform estimate for Lipschitz directions” (25 September 2026). The estimates hold uniformly for Lipschitz unit vector fields depending on both coordinates, at the reciprocal-Lipschitz truncation scale.

theorem OAI.LipschitzHilbert.main line 17
Source documentation
Uniform hard truncations, the actual symmetric principal value, weak-(2,2), and bounded L2 extensions at an absolute short scale.
Distinct definitions of this name: ComparatorChallenges/LipschitzHilbert.lean:63 (same statement text; different proof or body). Qualify references as OAI.LipschitzHilbert.main@path.
```
theorem main :
    ∃ a : ℝ, a∈Ioo 0 (1/2) ∧ ∃ C : ℝ≥0, 0<C ∧ ShortHilbertConclusion a C :=
…
```
Mentions: OAI.LipschitzHilbert.ShortHilbertConclusion
theorem OAI.LipschitzHilbert.uniform_truncation line 23
Source documentation
The reciprocal-Lipschitz-scale formulation, uniform over all inner truncations and all Lipschitz unit vector fields.
Distinct definitions of this name: ComparatorChallenges/LipschitzHilbert.lean:68 (same statement text; different proof or body). Qualify references as OAI.LipschitzHilbert.uniform_truncation@path.
```
theorem uniform_truncation :
    ∃ C : ℝ, 0<C ∧ ∀ K : ℝ≥0, 0<K → ∀ epsilon R : ℝ,
      0<epsilon → epsilon≤R → R≤1/(1000000*(K:ℝ)) →
      ∀ v : Plane → Plane, LipschitzWith K v → (∀ x, ‖v x‖=1) →
      ∀ f : SchwartzMap Plane ℂ,
        eLpNorm (shortTransform v epsilon R f) 2 volume≤ENNReal.ofReal (C*‖f.toLp 2 volume‖) :=
…
```
Mentions: OAI.LipschitzHilbert.Plane, OAI.LipschitzHilbert.shortTransform