PartialIntegration to Smooth1ContinuousAt

LemmaPartialIntegration#

Let \(f, g\) be once differentiable functions from \(\mathbb{R}_{>0}\) to \(\mathbb{C}\) so that \(fg'\) and \(f'g\) are both integrable, and \(f\cdot g (x)\to 0\) as \(x\to 0^+,\infty\). Then

\[ \int_0^\infty f(x)g'(x) dx = -\int_0^\infty f'(x)g(x)dx. \]
Proof

Partial integration.

Lean

Formalized as PartialIntegration.

Sources
LeanPartialIntegration
Used by 1
Used byMellinOfPsi

In this section, we define the Mellin transform (already in Mathlib, thanks to David Loeffler), prove its inversion formula, and derive a number of important properties of some special functions and bumpfunctions.

Def: (Already in Mathlib) Let \(f\) be a function from \(\mathbb{R}_{>0}\) to \(\mathbb{C}\). We define the Mellin transform of \(f\) to be the function \(\mathcal{M}(f)\) from \(\mathbb{C}\) to \(\mathbb{C}\) defined by

\[ \mathcal{M}(f)(s) = \int_0^\infty f(x)x^{s-1}dx. \]

[Note: My preferred way to think about this is that we are integrating over the multiplicative group \(\mathbb{R}_{>0}\), multiplying by a (not necessarily unitary!) character \(|\cdot|^s\), and integrating with respect to the invariant Haar measure \(dx/x\). This is very useful in the kinds of calculations carried out below. But may be more difficult to formalize as things now stand. So we might have clunkier calculations, which “magically” turn out just right - of course they're explained by the aforementioned structure...]

Finally, we need Mellin Convolutions and properties thereof.

DefinitionMellinConvolution#

Let \(f\) and \(g\) be functions from \(\mathbb{R}_{>0}\) to \(\mathbb{C}\). Then we define the Mellin convolution of \(f\) and \(g\) to be the function \(f\ast g\) from \(\mathbb{R}_{>0}\) to \(\mathbb{C}\) defined by

\[ (f\ast g)(x) = \int_0^\infty f(y)g(x/y)\frac{dy}{y}. \]
Lean

Formalized as MellinConvolution.

Sources
LeanMellinConvolution
Used by 9
Used byMellinConvolutionSymmetric · MellinConvolutionTransform · MellinOfSmooth1a · Smooth1 · Smooth1ContinuousAt · Smooth1LeOne · Smooth1Nonneg · Smooth1Properties-above · Smooth1Properties-below

Let us start with a simple property of the Mellin convolution.

LemmaMellinConvolutionSymmetric#

Let \(f\) and \(g\) be functions from \(\mathbb{R}_{>0}\) to \(\mathbb{R}\) or \(\mathbb{C}\), for \(x\neq0\),

\[ (f\ast g)(x)=(g\ast f)(x) . \]
Proof

By Definition MellinConvolution,

\[ (f\ast g)(x) = \int_0^\infty f(y)g(x/y)\frac{dy}{y} \]

in which we change variables to \(z=x/y\):

\[ (f\ast g)(x) = \int_0^\infty f(x/z)g(z)\frac{dz}{z} =(g\ast f)(x) . \]
Lean

Formalized as MellinConvolutionSymmetric.

Sources
LeanMellinConvolutionSymmetric
Uses 1 · Used by 2
Statement usesMellinConvolution
Used byMellinOfSmooth1a · Smooth1ContinuousAt

The Mellin transform of a convolution is the product of the Mellin transforms.

TheoremMellinConvolutionTransform#

Let \(f\) and \(g\) be functions from \(\mathbb{R}_{>0}\) to \(\mathbb{C}\) such that

\[ (x,y)\mapsto f(y)\frac{g(x/y)}yx^{s-1}\qquad\text{(1)} \]

is absolutely integrable on \([0,\infty)^2\). Then

\[ \mathcal{M}(f\ast g)(s) = \mathcal{M}(f)(s)\mathcal{M}(g)(s). \]
Proof

By Definitions MellinTransform and MellinConvolution

\[ \mathcal M(f\ast g)(s)= \int_0^\infty \int_0^\infty f(y)g(x/y)x^{s-1}\frac{dy}ydx \]

By (1) and Fubini's theorem,

\[ \mathcal M(f\ast g)(s)= \int_0^\infty \int_0^\infty f(y)g(x/y)x^{s-1}dx\frac{dy}y \]

in which we change variables from \(x\) to \(z=x/y\):

\[ \mathcal M(f\ast g)(s)= \int_0^\infty \int_0^\infty f(y)g(z)y^{s-1}z^{s-1}dzdy \]

which, by Definition MellinTransform, is

\[ \mathcal M(f\ast g)(s)= \mathcal M(f)(s)\mathcal M(g)(s) . \]
Lean

Formalized as MellinConvolutionTransform.

Sources
LeanMellinConvolutionTransform
Uses 1 · Used by 1
Statement usesMellinConvolution
Used byMellinOfSmooth1a

The \(\nu\) function has Mellin transform \(\mathcal{M}(\nu)(s)\) which is entire and decays (at least) like \(1/|s|\).

[Of course it decays faster than any power of \(|s|\), but it turns out that we will just need one power.]

TheoremMellinOfPsi#

The Mellin transform of \(\nu\) is

\[ \mathcal{M}(\nu)(s) = O\left(\frac{1}{|s|}\right), \]

as \(|s|\to\infty\) with \(\sigma_1 \le \Re(s) \le 2\).

Proof

Integrate by parts:

\[ \left|\int_0^\infty \nu(x)x^s\frac{dx}{x}\right| = \left|-\int_0^\infty \nu'(x)\frac{x^{s}}{s}dx\right| \]
\[ \le \frac{1}{|s|} \int_{1/2}^2|\nu'(x)|x^{\Re(s)}dx. \]

Since \(\Re(s)\) is bounded, the right-hand side is bounded by a constant times \(1/|s|\).

Lean

Formalized as MellinOfPsi.

Sources
LeanMellinOfPsi
Uses 1 · Used by 1
Proof usesPartialIntegration
Used byMellinOfSmooth1b

We can make a delta spike out of this bumpfunction, as follows.

DefinitionDeltaSpike#

Let \(\nu\) be a bumpfunction supported in \([1/2,2]\). Then for any \(\epsilon>0\), we define the delta spike \(\nu_\epsilon\) to be the function from \(\mathbb{R}_{>0}\) to \(\mathbb{C}\) defined by

\[ \nu_\epsilon(x) = \frac{1}{\epsilon}\nu\left(x^{\frac{1}{\epsilon}}\right). \]
Lean

Formalized as DeltaSpike.

Sources
LeanDeltaSpike
Used by 10
Used byDeltaSpikeMass · MellinOfDeltaSpike · MellinOfDeltaSpikeAt1 · MellinOfSmooth1a · Smooth1 · Smooth1ContinuousAt · Smooth1LeOne · Smooth1Nonneg · Smooth1Properties-above · Smooth1Properties-below

This spike still has mass one:

LemmaDeltaSpikeMass#

For any \(\epsilon>0\), we have

\[ \int_0^\infty \nu_\epsilon(x)\frac{dx}{x} = 1. \]
Proof

Substitute \(y=x^{1/\epsilon}\), and use the fact that \(\nu\) has mass one, and that \(dx/x\) is Haar measure.

Lean

Formalized as DeltaSpikeMass.

Sources
LeanDeltaSpikeMass
Uses 1 · Used by 1
Statement usesDeltaSpike
Used bySmooth1Properties-below

The Mellin transform of the delta spike is easy to compute.

TheoremMellinOfDeltaSpike#

For any \(\epsilon>0\), the Mellin transform of \(\nu_\epsilon\) is

\[ \mathcal{M}(\nu_\epsilon)(s) = \mathcal{M}(\nu)\left(\epsilon s\right). \]
Proof

Substitute \(y=x^{1/\epsilon}\), use Haar measure; direct calculation.

Lean

Formalized as MellinOfDeltaSpike.

Sources
LeanMellinOfDeltaSpike
Uses 1 · Used by 2
Statement usesDeltaSpike
Used byMellinOfDeltaSpikeAt1 · MellinOfSmooth1a

In particular, for \(s=1\), we have that the Mellin transform of \(\nu_\epsilon\) is \(1+O(\epsilon)\).

CorollaryMellinOfDeltaSpikeAt1#

For any \(\epsilon>0\), we have

\[ \mathcal{M}(\nu_\epsilon)(1) = \mathcal{M}(\nu)(\epsilon). \]
Proof

This is immediate from the above theorem.

Lean

Formalized as MellinOfDeltaSpikeAt1.

Sources
LeanMellinOfDeltaSpikeAt1
Uses 2
Statement usesDeltaSpike
Proof usesMellinOfDeltaSpike

LemmaMellinOfDeltaSpikeAt1-asymp#

As \(\epsilon\to 0\), we have

\[ \mathcal{M}(\nu_\epsilon)(1) = 1+O(\epsilon). \]
Proof

By Lemma MellinOfDeltaSpikeAt1,

\[ \mathcal M(\nu_\epsilon)(1)=\mathcal M(\nu)(\epsilon) \]

which by Definition MellinTransform is

\[ \mathcal M(\nu)(\epsilon)=\int_0^\infty\nu(x)x^{\epsilon-1}dx . \]

Since \(\nu(x) x^{\epsilon-1}\) is integrable (because \(\nu\) is continuous and compactly supported),

\[ \mathcal M(\nu)(\epsilon)-\int_0^\infty\nu(x)\frac{dx}x =\int_0^\infty\nu(x)(x^{\epsilon-1}-x^{-1})dx . \]

By Taylor's theorem,

\[ x^{\epsilon-1}-x^{-1}=O(\epsilon) \]

so, since \(\nu\) is absolutely integrable,

\[ \mathcal M(\nu)(\epsilon)-\int_0^\infty\nu(x)\frac{dx}x=O(\epsilon) . \]

We conclude the proof using Theorem SmoothExistence.

Lean

Formalized as MellinOfDeltaSpikeAt1_asymp.

Sources
LeanMellinOfDeltaSpikeAt1_asymp
Used by 1
Used byMellinOfSmooth1c

Let \(1_{(0,1]}\) be the function from \(\mathbb{R}_{>0}\) to \(\mathbb{C}\) defined by

\[ 1_{(0,1]}(x) = \begin{cases} 1 & \text{ if }x\leq 1\\ 0 & \text{ if }x>1 \end{cases}. \]

This has Mellin transform: [Note: this already exists in mathlib]

TheoremMellinOf1#

The Mellin transform of \(1_{(0,1]}\) is

\[ \mathcal{M}(1_{(0,1]})(s) = \frac{1}{s}. \]
Proof

This is a straightforward calculation.

Lean

Formalized as MellinOf1.

Sources
LeanMellinOf1
Used by 1
Used byMellinOfSmooth1a

What will be essential for us is properties of the smooth version of \(1_{(0,1]}\), obtained as the Mellin convolution of \(1_{(0,1]}\) with \(\nu_\epsilon\).

DefinitionSmooth1#

Let \(\epsilon>0\). Then we define the smooth function \(\widetilde{1_{\epsilon}}\) from \(\mathbb{R}_{>0}\) to \(\mathbb{C}\) by

\[ \widetilde{1_{\epsilon}} = 1_{(0,1]}\ast\nu_\epsilon. \]
Proof

Let \(c:=2^\epsilon > 1\), in terms of which we wish to prove

\[ -1 < c \log c - c . \]

Letting \(f(x):=x\log x - x\), we can rewrite this as \(f(1) < f(c)\). Since

\[ \frac {d}{dx}f(x) = \log x > 0 , \]

\(f\) is monotone increasing on [1, \(\infty\)), and we are done.

Lean

Formalized as Smooth1.

Sources
LeanSmooth1
Uses 2 · Used by 37
Proof usesDeltaSpike · MellinConvolution
Used byGenStrengthPNT · MellinOfSmooth1a · MellinOfSmooth1b · MellinOfSmooth1c · Smooth1ContinuousAt · Smooth1LeOne · Smooth1Nonneg · Smooth1Properties-above · Smooth1Properties-below · I₁ · I₂ · I₃ · I₃₇ · I₄ · I₅ · I₆ · I₇ · I₈ · I₉ · SmoothedChebyshev · SmoothedChebyshevClose · SmoothedChebyshevDirichlet · SmoothedChebyshevDirichlet-aux-integrable · SmoothedChebyshevDirichlet-aux-tsum-integral · SmoothedChebyshevPull1-aux-integrable · I1Bound · I2GenBound · I3GenBound · I4GenBound · I5Bound · I6GenBound · I7GenBound · I8I2 · I9Bound · SmoothedChebyshevPull1 · SmoothedChebyshevPull2 · ZetaBoxEval

In particular, we have the following two properties.

LemmaSmooth1Properties-below#

Fix \(\epsilon>0\). There is an absolute constant \(c>0\) so that: If \(0 < x \leq (1-c\epsilon)\), then

\[ \widetilde{1_{\epsilon}}(x) = 1. \]
Proof

Opening the definition, we have that the Mellin convolution of \(1_{(0,1]}\) with \(\nu_\epsilon\) is

\[ \int_0^\infty 1_{(0,1]}(y)\nu_\epsilon(x/y)\frac{dy}{y} = \int_0^1 \nu_\epsilon(x/y)\frac{dy}{y}. \]

The support of \(\nu_\epsilon\) is contained in \([1/2^\epsilon,2^\epsilon]\), so it suffices to consider \(y \in [1/2^\epsilon x,2^\epsilon x]\) for nonzero contributions. If \(x < 2^{-\epsilon}\), then the integral is the same as that over \((0,\infty)\):

\[ \int_0^1 \nu_\epsilon(x/y)\frac{dy}{y} = \int_0^\infty \nu_\epsilon(x/y)\frac{dy}{y}, \]

in which we change variables to \(z=x/y\) (using \(x>0\)):

\[ \int_0^\infty \nu_\epsilon(x/y)\frac{dy}{y} = \int_0^\infty \nu_\epsilon(z)\frac{dz}{z}, \]

which is equal to one by Lemma DeltaSpikeMass. We then choose

\[ c:=\log 2, \]

which satisfies

\[ c > \frac{1-2^{-\epsilon}}\epsilon \]

by Lemma Smooth1Properties_estimate, so

\[ 1-c\epsilon < 2^{-\epsilon}. \]
Lean

Formalized as Smooth1Properties_below.

Sources
LeanSmooth1Properties_below
Uses 4 · Used by 1
Statement usesSmooth1
Proof usesDeltaSpikeMass · DeltaSpike · MellinConvolution
Used bySmoothedChebyshevClose

LemmaSmooth1Properties-above#

Fix \(0\lt \epsilon<1\). There is an absolute constant \(c>0\) so that: if \(x\geq (1+c\epsilon)\), then

\[ \widetilde{1_{\epsilon}}(x) = 0. \]
Proof

Again the Mellin convolution is

\[ \int_0^1 \nu_\epsilon(x/y)\frac{dy}{y}, \]

but now if \(x > 2^\epsilon\), then the support of \(\nu_\epsilon\) is disjoint from the region of integration, and hence the integral is zero. We choose

\[ c:=2\log 2 . \]

By Lemma Smooth1Properties_estimate,

\[ c > 2\frac{1-2^{-\epsilon}}\epsilon > 2^\epsilon\frac{1-2^{-\epsilon}}\epsilon = \frac{2^\epsilon-1}\epsilon, \]

so

\[ 1+c\epsilon > 2^\epsilon. \]
Lean

Formalized as Smooth1Properties_above.

Sources
LeanSmooth1Properties_above
Uses 3 · Used by 7
Statement usesSmooth1
Proof usesDeltaSpike · MellinConvolution
Used byGenStrengthPNT · SmoothedChebyshevClose · SmoothedChebyshevDirichlet · SmoothedChebyshevDirichlet-aux-integrable · SmoothedChebyshevDirichlet-aux-tsum-integral · SmoothedChebyshevPull1 · SmoothedChebyshevPull2

LemmaSmooth1Nonneg#

If \(\nu\) is nonnegative, then \(\widetilde{1_{\epsilon}}(x)\) is nonnegative.

Proof

By Definitions Smooth1, MellinConvolution and DeltaSpike

\[ \widetilde{1_\epsilon}(x) =\int_0^\infty 1_{(0,1]}(y)\frac1\epsilon\nu((x/y)^{\frac1\epsilon}) \frac{dy}y \]

and all the factors in the integrand are nonnegative.

Lean

Formalized as Smooth1Nonneg.

Sources
LeanSmooth1Nonneg
Uses 3 · Used by 7
Statement usesSmooth1
Proof usesDeltaSpike · MellinConvolution
Used byGenStrengthPNT · SmoothedChebyshevClose · SmoothedChebyshevDirichlet · SmoothedChebyshevDirichlet-aux-integrable · SmoothedChebyshevDirichlet-aux-tsum-integral · SmoothedChebyshevPull1 · SmoothedChebyshevPull2

LemmaSmooth1LeOne#

If \(\nu\) is nonnegative and has mass one, then \(\widetilde{1_{\epsilon}}(x)\le 1\), \(\forall x>0\).

Proof

By Definitions Smooth1, MellinConvolution and DeltaSpike

\[ \widetilde{1_\epsilon}(x) =\int_0^\infty 1_{(0,1]}(y)\frac1\epsilon\nu((x/y)^{\frac1\epsilon}) \frac{dy}y \]

and since \(1_{(0,1]}(y)\le 1\), and all the factors in the integrand are nonnegative,

\[ \widetilde{1_\epsilon}(x)\le\int_0^\infty \frac1\epsilon\nu((x/y)^{\frac1\epsilon}) \frac{dy}y \]

(because in mathlib the integral of a non-integrable function is \(0\), for the inequality above to be true, we must prove that \(\nu((x/y)^{\frac1\epsilon})/y\) is integrable; this follows from the computation below). We then change variables to \(z=(x/y)^{\frac1\epsilon}\):

\[ \widetilde{1_\epsilon}(x)\le\int_0^\infty \nu(z) \frac{dz}z \]

which by Theorem SmoothExistence is 1.

Lean

Formalized as Smooth1LeOne.

Sources
LeanSmooth1LeOne
Uses 3 · Used by 7
Statement usesSmooth1
Proof usesDeltaSpike · MellinConvolution
Used byGenStrengthPNT · SmoothedChebyshevClose · SmoothedChebyshevDirichlet · SmoothedChebyshevDirichlet-aux-integrable · SmoothedChebyshevDirichlet-aux-tsum-integral · SmoothedChebyshevPull1 · SmoothedChebyshevPull2

Combining the above, we have the following three Main Lemmata of this section on the Mellin transform of \(\widetilde{1_{\epsilon}}\).

LemmaMellinOfSmooth1a#

Fix \(\epsilon>0\). Then the Mellin transform of \(\widetilde{1_{\epsilon}}\) is

\[ \mathcal{M}(\widetilde{1_{\epsilon}})(s) = \frac{1}{s}\left(\mathcal{M}(\nu)\left(\epsilon s\right)\right). \]
Proof

By Definition Smooth1,

\[ \mathcal M(\widetilde{1_\epsilon})(s) =\mathcal M(1_{(0,1]}\ast\nu_\epsilon)(s) . \]

We wish to apply Theorem MellinConvolutionTransform. To do so, we must prove that

\[ (x,y)\mapsto 1_{(0,1]}(y)\nu_\epsilon(x/y)/y \]

is integrable on \([0,\infty)^2\). It is actually easier to do this for the convolution: \(\nu_\epsilon\ast 1_{(0,1]}\), so we use Lemma MellinConvolutionSymmetric: for \(x\neq0\),

\[ 1_{(0,1]}\ast\nu_\epsilon(x)=\nu_\epsilon\ast 1_{(0,1]}(x) . \]

Now, for \(x=0\), both sides of the equation are 0, so the equation also holds for \(x=0\). Therefore,

\[ \mathcal M(\widetilde{1_\epsilon})(s) =\mathcal M(\nu_\epsilon\ast 1_{(0,1]})(s) . \]

Now,

\[ (x,y)\mapsto \nu_\epsilon(y)1_{(0,1]}(x/y)\frac{x^{s-1}}y \]

has compact support that is bounded away from \(y=0\) (specifically \(y\in[2^{-\epsilon},2^\epsilon]\) and \(x\in(0,y]\)), so it is integrable. We can thus apply Theorem MellinConvolutionTransform and find

\[ \mathcal M(\widetilde{1_\epsilon})(s) =\mathcal M(\nu_\epsilon)(s)\mathcal M(1_{(0,1]})(s) . \]

By Lemmas MellinOf1 and MellinOfDeltaSpike,

\[ \mathcal M(\widetilde{1_\epsilon})(s) =\frac1s\mathcal M(\nu)(\epsilon s) . \]
Lean

Formalized as MellinOfSmooth1a.

Sources
LeanMellinOfSmooth1a
Uses 7 · Used by 2
Statement usesSmooth1
Proof usesMellinOf1 · MellinOfDeltaSpike · DeltaSpike · MellinConvolution · MellinConvolutionTransform · MellinConvolutionSymmetric
Used byMellinOfSmooth1b · MellinOfSmooth1c

LemmaMellinOfSmooth1b#

Given \(0\lt \sigma_1\le\sigma_2\), for any \(s\) such that \(\sigma_1\le\mathcal Re(s)\le\sigma_2\), we have

\[ \mathcal{M}(\widetilde{1_{\epsilon}})(s) = O\left(\frac{1}{\epsilon|s|^2}\right). \]
Proof

Use Lemma MellinOfSmooth1a and the bound in Lemma MellinOfPsi.

Lean

Formalized as MellinOfSmooth1b.

Sources
LeanMellinOfSmooth1b
Uses 3 · Used by 6
Statement usesSmooth1
Proof usesMellinOfSmooth1a · MellinOfPsi
Used bySmoothedChebyshevDirichlet-aux-integrable · I1Bound · I2GenBound · I3GenBound · I4GenBound · I5Bound

LemmaMellinOfSmooth1c#

At \(s=1\), we have

\[ \mathcal{M}(\widetilde{1_{\epsilon}})(1) = 1+O(\epsilon)). \]
Proof

Follows from Lemmas MellinOfSmooth1a, MellinOfDeltaSpikeAt1 and MellinOfDeltaSpikeAt1-asymp.

Lean

Formalized as MellinOfSmooth1c.

Sources
LeanMellinOfSmooth1c
Uses 3 · Used by 2
Statement usesSmooth1
Proof usesMellinOfDeltaSpikeAt1-asymp · MellinOfSmooth1a
Used byGenStrengthPNT · ZetaBoxEval

LemmaSmooth1ContinuousAt#

Fix a nonnegative, continuously differentiable function \(F\) on \(\mathbb{R}\) with support in \([1/2,2]\). Then for any \(\epsilon>0\), the function \(x \mapsto \int_{(0,\infty)} x^{1+it} \widetilde{1_{\epsilon}}(x) dx\) is continuous at any \(y>0\).

Proof

Use Lemma MellinconvolutionSymmetric to write \(\widetilde{1_{\epsilon}}(x)\) as an integral over an integral near \(1\), in particular avoiding the singularity at \(0\). The integrand may be bounded by \(2^{\epsilon}\nu_\epsilon(t)\) which is independent of \(x\) and we can use dominated convergence to prove continuity.

Lean

Formalized as Smooth1ContinuousAt.

Sources
LeanSmooth1ContinuousAt
Uses 4 · Used by 6
Statement usesSmooth1
Proof usesDeltaSpike · MellinConvolution · MellinConvolutionSymmetric
Used byGenStrengthPNT · SmoothedChebyshevDirichlet · SmoothedChebyshevDirichlet-aux-integrable · SmoothedChebyshevDirichlet-aux-tsum-integral · SmoothedChebyshevPull1 · SmoothedChebyshevPull2

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.