Definition of the trilinear Hilbert transform

noncomputable def TrilinearHT.truncatedTransform (f : Fin 3 → ℝ → ℂ) (x ε : ℝ) : ℂ

Truncated trilinear Hilbert transform of a triple of functions f at x.

Equations

• TrilinearHT.truncatedTransform f x ε = ∫ (t : ℝ) in {t : ℝ | ε < |t|}, (∏ i : Fin 3, f i (x + (↑↑i + 1) * t)) / ↑t

noncomputable def TrilinearHT.T (f : Fin 3 → ℝ → ℂ) (x : ℝ) : ℂ

Trilinear Hilbert transform.

Note: The (trivial) fact that the principal value limit exists when f are Schwartz functions is proved as the automatically generated lemma TrilinearHT.Auto.tendsto_truncatedTransform.

Equations

• TrilinearHT.T f x = (nhdsWithin 0 (Set.Ioi 0)).limUnder (TrilinearHT.truncatedTransform f x)