Trilinear Hilbert transform: retainedMin_holds #
Blueprint lines 2838-2888 on one root (prop:normalized, eq:before-absorption and the choice
of q, α, P): the retained-attempt estimate RetainedMin. The setup is padded so that the
vertex bound of the attempt makes the failure roots at most |R|/8; the attempt localizes the
active minima to the leaves of the guarded search, each leaf has the explicit bound of
leaf_estimate outside six cut families, the cuts and failure roots are united at most |R|/4
(root_assembly), and the parameters P = ⌈η₀^{-α}⌉, k_D, δ, τ₃, ρ absorb all costs
(retained_arith) for every large k.
Blueprint eq:active-final (prop:normalized, lines 2838-2888) for every admissible class:
RetainedMin (retainedMin_holds), the restarts at the exceptional roots
(activeMin_of_retainedMin) and the two-U term (activeFinal_of_activeMin).
Blueprint thm:main (lines 2934-2940): the trilinear Hilbert transform principal value exists
pointwise on Schwartz functions, is bounded L³ × L³ × L³ → L¹ there, and extends uniquely to a
bounded trilinear operator on L³.
Blueprint thm:main in the form of TrilinearHT.trilinear_ht_bound
(TrilinearHT/Theorems.lean): the trilinear Hilbert transform TrilinearHT.T is bounded
L³ × L³ × L³ → L¹ on Schwartz functions.