Research proof index

E₄.toFun = H₂² + H₂H₄ + H₄². Both are weight-4 level-1 modular forms tending to 1 at ∞, so their difference is a weight-4 cusp form, hence zero.

E₄ as explicit tsum (from E4_q_exp PowerSeries coefficients). Uses hasSum_qExpansion to convert from PowerSeries to tsum form.

The operator czOperator K r is bounded from L^2 ([1, 4]) to L^2 ([2, 3]), uniformly in r. This follows from the fact, proved in norm_czOperator_le_add, that it is bounded by the sum of two operators which are both bounded: one is the convolution with dirichletApprox, bounded as it is an average of Fourier projections, and the other one has a k...

Among the first $n+1$ enumerated phases, enumΘ'ArgMax returns the smallest index $i$ at which the function $g$ attains its maximum at $x$. Equivalently, every index $j\le n$ has value at most the value at $i$, and every earlier index $j<i$ has strictly smaller value.

Any set of tiles can be written as the union of disjoint subfamilies, their number being controlled by the maximal stack size.

Let $g$ have bounded finite support, let $r>0$, and suppose $d(x,x')\le r$. The truncated Calderón-Zygmund operator changes by at most a constant times the global maximal function:

$d\bigl(T_r g(x),T_r g(x')\bigr)\le C(a)\,M g(x).$