<<IntervalTools`

Example: g(a,T) from Counting Zeros of Dirichlet L-Functions

In “Counting Zeros of Dirichlet L-Functions”, we define a function g(a,T):=(2/π)Im[LogGamma[(1/4)+(a/2)+I*(T/2)]]-(T/π)Log[(T/(2E))]-((2a-1)/4). Using Stirling’s Approximation, we get upper and lower bounds on g(a,T), and need to prove the simplifying ((a-2)/(50T))≤g(a,T)≤((2-a)/(50T)), for a∈{0,1} and T≥5/7. That’s 4 inequalities, if you are counting: upper and lower bounds for a=0 and for a=1.

Plot[{((0-2)/50),T*((2/π)Im[LogGamma[(1/4)+(0/2)+I*(T/2)]]-(T/π)Log[(T/(2E))]-((2 0-1)/4)),((2-0)/50)},{T,5/7,4},PlotLegends->{((2-a)/(50T)),"T g(a,T)",((a-2)/(50T))},PlotLabel->"a=0"]

Plot[{((1-2)/50),T*((2/π)Im[LogGamma[(1/4)+(1/2)+I*(T/2)]]-(T/π)Log[(T/(2E))]-((2 1-1)/4)),((2-1)/50)},{T,5/7,4},PlotLegends->{((2-a)/(50T)),"T g(a,T)",((a-2)/(50T))},PlotLabel->"a=1"]

The pieces

The upper bound on T*g(a,T) is

(T/(240 (((((((9/4)+(a/2)))^2)+((T^2)/4)))^(3/2))))+(T/(180 π (((((((9/4)+(a/2)))^2)+((T^2)/4)))^(3/2))))-((T^2)/(12 π (((((9/4)+(a/2)))^2)+((T^2)/4))))+((2 T ArcTan[((2 ((1/4)+(a/2)))/T)])/π)+((2 T ArcTan[((2 ((5/4)+(a/2)))/T)])/π)-((7 T ArcTan[((2 ((9/4)+(a/2)))/T)])/(2 π))-((a T ArcTan[((2 ((9/4)+(a/2)))/T)])/π)+(((T^2) Log[1+((4 ((((9/4)+(a/2)))^2))/(T^2))])/(2 π))

Which we presciently express as

g11[a_,T_]=((T/2)/(((((((9/4)+(a/2)))^2)+((T^2)/4)))^(3/2)));
g12[a_,T_]=(((T^2)/4)/((((((9/4)+(a/2)))^2)+((T^2)/4))));
g13[c_,T_]=T ArcTan[(c/T)];
g14[a_,T_]=(T^2) Log[1+((4 ((((9/4)+(a/2)))^2))/(T^2))];
gUpper[a_,T_]:=((1/120)+(1/(90π)))g11[a,T]-(1/(3π))g12[a,T]+(1/π)(2g13[(1/2)+a,T]+2g13[(5/2)+a,T]-((7/2)+a)g13[(9/2)+a,T])+(1/(2π))g14[a,T];

Manipulate[Plot[{gUpper[a,T],T*((2/π)Im[LogGamma[(1/4)+(a/2)+I*(T/2)]]-(T/π)Log[(T/(2E))]-((2 a-1)/4))},{T,5/7,4},PlotRange->All,PlotLegends->{"upper bound","T g(a,T)"}],{a,{0,1}}]

We now proceed to find sharper interval enclosures for g11,g12,g13,g14. Both g11 and g12 are essentially polynomials in one variable, and so are easy to handle. The arctangent presents some awkwardness in g13, but the logarithm in g14 is easy.

g11

(*g11[a,T] has only one positive  critical value *)
Solve[D[g11[a,T],T]==0]

g11[a_,Tint_Interval]:=PiecewiseMonotoneEnclosure[((T/2)/(((((((9/4)+(a/2)))^2)+((T^2)/4)))^(3/2))),T,{((9+2 a)/(2 (Sqrt[2])))},Tint];

g12

(*g12[a,T] has no positive critical values *)
Solve[D[g12[a,T],T]==0]

g12[a_,Tint_Interval]:=MonotoneEnclosure[(((T^2)/4)/((((((9/4)+(a/2)))^2)+((T^2)/4)))),T,Tint];

g13 (the hard one)

(*g13 is somewhat trickier, but it is also strickly increasing. *)
(* We care about (1/2)≤c≤(11/2) and T≥5/7 *)
D[g13[c,T],T]/.c->x T//Simplify

As x=(c/T), we should consider 0<x≤((11/2)/(5/7))=(77/10). We need to show on this domain that
	ArcTan[x]-(x/(1+(x^2)))>0.

Plot[ArcTan[x]-(x/(1+(x^2))),{x,0,(77/10)}]

We can restrict our attention to 0<x<∞. 
By Alirezaei’s Arctangent Bound,
	ArcTan[x]-(x/(1+(x^2)))≥(x/((4/(π^2))+Sqrt[(((1-(4/(π^2))))^2)+(4/(π^2)) (x^2)]))-(x/(1+(x^2)))=((x (1-(4/(π^2))+(x^2)-(Sqrt[(((1-(4/(π^2))))^2)+(4/(π^2)) (x^2)])))/((1+(x^2)) ((4/(π^2))+(Sqrt[(((1-(4/(π^2))))^2)+(4/(π^2)) (x^2)])))).
Clearly x, 1+(x^2), and (4/(π^2))+(Sqrt[(((1-(4/(π^2))))^2)+(4/(π^2)) (x^2)]) are positive for positive x.  The remaining term is positive as x->∞, is continuous, and is never 0 (a polynomial root problem):

Solve[1-(4/(π^2))+(x^2)-(Sqrt[(((1-(4/(π^2))))^2)+((4 (x^2))/(π^2))])==0]

g13[c_,Tint_Interval]:=MonotoneEnclosure[T ArcTan[(c/T)],T,Tint];

g14

g14[a_,T_]=(T^2) Log[1+((4 ((((9/4)+(a/2)))^2))/(T^2))];

Simplify[D[g14[a,T],T]]

A picture showing the standard bounds on logarithms.

Plot[{(x/(1+x)),Log[1+x],x},{x,-1/2,1/2}]

Recall that (x/(1+x))≤Log[1+x]. For positive T, the derivative D[g14[a,T],T] has the same sign as -((((9+2 a))^2)/(81+36 a+4 (a^2)+4 (T^2)))+Log[1+((((9+2 a))^2)/(4 (T^2)))]≥-((((9+2 a))^2)/(81+36 a+4 (a^2)+4 (T^2)))+(((((9+2 a))^2)/(4 (T^2)))/(1+((((9+2 a))^2)/(4 (T^2))))) =0.

Simplify[-((((9+2 a))^2)/(81+36 a+4 (a^2)+4 (T^2)))+(((((9+2 a))^2)/(4 (T^2)))/(1+((((9+2 a))^2)/(4 (T^2)))))]

Limit[g14[a,T],T->Infinity]

(*we thus  have the following interval version of g14*)
g14[a_,Tint_Interval]:=MonotoneEnclosure[(T^2) Log[1+((4 ((((9/4)+(a/2)))^2))/(T^2))],T,Tint];

The proof for the upper bound

{fails,uncertains,proved}=ProveNonNegative[(((2-0)/50)-gUpper[0,#])&,(((2-0)/50)-gUpper[0,#])&,{Interval[{5/7,Infinity}]},MaxDepth->50];
fails
uncertains
Length[proved]
Last[proved]

So the proof for a=0 works, splitting the interval [(5/7),∞] into 361 pieces, with the infinite one being [64,∞].

{fails,uncertains,proved}=ProveNonNegative[(((2-1)/50)-gUpper[1,#])&,(((2-1)/50)-gUpper[1,#])&,{Interval[{5/7,Infinity}]},MaxDepth->50];
{fails,uncertains}
{Length[proved],Last[proved]}

We have T*g(a,T)≤((2-a)/50).

The lower bound

The expression from Stirling’s Approximation that we need to show is at least ((a-2)/50) is

gLower[a_,T_]:=(((-1)/120)+((-1)/(90π)))g11[a,T]-(1/(3π))g12[a,T]+(1/π)(2g13[(1/2)+a,T]+2g13[(5/2)+a,T]-((7/2)+a)g13[(9/2)+a,T])+(1/(2π))g14[a,T];

Manipulate[Plot[{gLower[a,T],T*((2/π)Im[LogGamma[(1/4)+(a/2)+I*(T/2)]]-(T/π)Log[(T/(2E))]-((2 a-1)/4))},{T,5/7,4},PlotRange->All,PlotLegends->{"lower bound","T g(a,T)"}],{a,{0,1}}]

The proof for the lower bound

{fails,uncertains,proved}=ProveNonNegative[(gLower[0,#]+((2-0)/50))&,(gLower[0,#]+((2-0)/50))&,{Interval[{5/7,Infinity}]},MaxDepth->15];
{fails,uncertains}
{Length[proved],Last[proved]}

{fails,uncertains,proved}=ProveNonNegative[(((2-1)/50)+gLower[1,#])&,(((2-1)/50)+gLower[1,#])&,{Interval[{5/7,Infinity}]},MaxDepth->15];
{fails,uncertains}
{Length[proved],Last[proved]}