Boundedness of the trilinear Hilbert transform

theorem TrilinearHT.trilinear_ht_bound : ∃ (C : ℝ), ∀ (f : Fin 3 → SchwartzMap ℝ ℂ), MeasureTheory.eLpNorm (T fun (i : Fin 3) => ⇑(f i)) 1 MeasureTheory.volume ≤ ENNReal.ofReal C * ∏ i : Fin 3, MeasureTheory.eLpNorm (⇑(f i)) 3 MeasureTheory.volume

Main theorem. The trilinear Hilbert transform is bounded L³ × L³ × L³ → L¹.

Implementation notes:

• We formulate the bound as an a priori estimate on Schwartz functions as is common practice.