Tao equation (eta0): the logarithmic cutoff as a dyadic average of window indicators

For all positive reals $x,d,w$,

where $\eta_0(t)=4(\log2-|\log 2t|)_+$ is the source's logarithmic cutoff, supported on $[\tfrac14,1]$.

This is the identity that makes $\eta_0$ the right cutoff for the bilinear part of the argument: it exhibits the smooth weight $\eta_0(dw/x)$ attached to a product $dw$ as a dyadic average of products of two independent window indicators, one in $d$ and one in $w$. That is exactly what is needed to factorize the Type II sums, writing them as $4\int_0^\infty F(W)\frac{dW}{W}$ with each $F(W)$ a bilinear form over a pair of dyadic ranges, to which the large sieve applies.

The mechanism is that the two windows constrain $W$ to the interval between $\max(\frac{x}{2d},w)$ and $\min(\frac xd,2w)$, whose logarithmic length is $\log 4t$ for $\tfrac14\le t\le\tfrac12$, is $\log\frac1t$ for $\tfrac12\le t\le1$, and is negative — so the interval is empty — outside $[\tfrac14,1]$; these are the three branches of $\eta_0$.

Formalization Note The improper integral is the Lebesgue integral over $(0,\infty)$, and the product of the two indicators is written as a single conditional. The cutoff eta0 is the platform definition, extended by zero to nonpositive arguments; the identity is stated for positive $x,d,w$, for which the argument $dw/x$ is positive.