Research proof index

For a complex-valued function and a nonzero even integer $n$, discrete self-convolution has no larger $L^n$ norm than discrete self-difference-convolution: $\|f*f\|_n\le\|f\mathbin{\circleddash}f\|_n$.

A dependent-random-choice estimate. For $p \ge 2$, a nonnegative function $f$, nonempty $A$, and intersecting sets $B_1,B_2$, the support hypothesis produces subsets $A_1 \subseteq B_1$ and $A_2 \subseteq B_2$ whose normalized difference convolution has controlled correlation with $f$. Both relative sizes $|A_i|/|B_i|$ are bounded below by the same explicit quantity, namely one quarter of a normalized $2p$-th power of the weighted $L^p$ norm of $1_A \mathbin{\circleddash} 1_A$.

The project’s structural constants are chosen so that the scale-separation factor has the fixed quantitative bound

$D^{-\kappa Z}\le2^{-100}.$

E_k(it) is real for all t > 0 when k is even and k ≥ 4. This is the generalized theorem from which E₄_imag_axis_real and E₆_imag_axis_real follow.

TODO: Move this to E2.lean.

E₂(it) is real for all t > 0.