Let the square contain the Euclidean ball of radius , set , and define the logarithmic cutoff
Then and on the boundary. On an edge at radius comparable to , the mean value theorem gives . There are edges in the annulus of radius , hence the discrete Dirichlet energy satisfies
This logarithmic cutoff is the discrete manifestation of recurrence in two dimensions.
The Liouville approximation theorem states that if is an irrational algebraic number of degree , then there is a constant such that every reduced rational satisfies
Let be the minimal polynomial of , of degree . Since is irreducible of degree greater than one, . Moreover,
and hence
On the compact interval , put
If , the mean value theorem gives a point between and such that
Thus . If , then . Taking any
proves the stated strict inequality.
Since is bounded and smooth, the Sobolev embedding theorem gives continuous embeddings and . Because ,
Taking the norm in time gives
For , the mean value theorem and imply
Apply the Generalized Holder inequality in space, using for the quadratic products and for the cubic products, and then use the two Sobolev embeddings. Pointwise in time this yields
Taking the norm in time proves the required estimate with the factor .
If , the mean value theorem gives . Conversely, if is increasing, every difference quotient with positive or negative increment is nonnegative; taking its limit gives .
For , apply the mean value theorem to : for some . Since is increasing, . Therefore
and part (c) proves that the quotient is increasing.
Put . It is nonzero by unique prime factorization. If or , the claimed inequality follows immediately after increasing the effective constant. We may therefore assume
which implies .
The Baker lower bound for a homogeneous linear form in logarithms, with the fixed algebraic numbers and , gives
for an effective absolute constant . If , the desired conclusion is again immediate. Otherwise, the mean value theorem applied to the exponential function on gives . Hence
Absorbing the fixed factor into a larger exponent proves .
If , monotonicity already gives , so assume . Suppose for a contradiction that . By the mean value theorem, some satisfies
The Margulis–Russo formula identifies this derivative with the appropriately normalized total influence, so is bounded solely in terms of . The -biased Friedgut junta theorem then supplies, for any small , a Boolean -junta with and
Because is monotone, , hence when . It follows that
For some assignment on with , therefore, . Monotonicity and imply . Choose , set , and take . Then
contradicting -quasirandomness. Thus .
Choose a radial mollifier with integral one and support in the unit ball, and a radial cutoff function equal to one there. For a radial tempered distribution , the functions
are radial Schwartz functions. Smoothness comes from convolution of a tempered distribution with a Schwartz function, and compact support comes from the cutoff. Pairing with gives . With , the cutoff tail and the mean value theorem give
The continuity estimate for therefore proves even in the strong dual topology. Inserting a cutoff is essential because convolution alone need not give rapid decay.
Uniform error bound for nearby decaying exponentials Created 2026-10-06 Updated 2026-10-07
For positive rates , the mean value theorem in the rate gives a bound by . Its maximum is . Combining this estimate with coefficient errors bounds a finite spectral sum uniformly on a half-line, including slow scales much longer than one. Positivity of both rates is essential: unstable exponentials need a different time-window or relative-error analysis.
If a twice differentiable real function on satisfies for some fixed , then it has a unique global maximum. The mean value theorem shows that is strictly decreasing, and that is nonincreasing. Hence for and for . These inequalities force opposite derivative signs at the two ends. The intermediate value theorem supplies a unique zero of , at which changes from increasing to decreasing. Merely having does not guarantee existence: is increasing and approaches its unattained supremum zero.