The Main Bound Computations (5.98≤L≤28)

Here we assemble bounds on the relevant pieces and combine them to accomplish the bound in the Main Theorem.

Definitions

<<IntervalTools`

{Lmin,Lmax}={6-(1/50),28};
Linterval=Interval[{Lmin,Lmax}];
η[L_]=(18/(10+9L));
c[L_]=1+(505/(111L+430));
r[L_]=(149/140)+(747/(283+36L));
(Subscript[σ, 1])[L_]=c[L]+((((c[L]-1/2))^2)/(r[L]));
δ[L_]=2c[L]-(Subscript[σ, 1])[L]-(1/2);
(Subscript[θ, -η])[L_]=ArcCos[((-η[L]-c[L])/(r[L]))];
(Subscript[θ, 1+η])[L_]=ArcCos[((1+η[L]-c[L])/(r[L]))];
(Subscript[θ, 1-c])[L_]=ArcCos[((1-2c[L])/(r[L]))];
(Subscript[θ, -1/2])[L_]=ArcCos[((-1/2-c[L])/(r[L]))];
(Subscript[θ, -3/2])[L_]=π;

Reduce[D[η[L],L]≤0&&Lmin≤L≤Lmax,L,Reals]
Reduce[D[c[L],L]≤0&&Lmin≤L≤Lmax,L,Reals]
Reduce[D[r[L],L]≤0&&Lmin≤L≤Lmax,L,Reals]
Reduce[D[(Subscript[σ, 1])[L],L]≤0&&Lmin≤L≤Lmax,L,Reals]
Reduce[D[δ[L],L]≤0&&Lmin≤L≤Lmax,L,Reals]

η[Lint_Interval]:=Block[{L},MonotoneEnclosure[η[L],L,Lint]];
c[Lint_Interval]:=Block[{L},MonotoneEnclosure[c[L],L,Lint]];
r[Lint_Interval]:=Block[{L},MonotoneEnclosure[r[L],L,Lint]];
(Subscript[σ, 1])[Lint_Interval]:=Block[{L},MonotoneEnclosure[(Subscript[σ, 1])[L],L,Lint]];
δ[Lint_Interval]:=Block[{L},MonotoneEnclosure[δ[L],L,Lint]];

Reduce[D[(Subscript[θ, -η])[L],L]≥0&&Lmin≤L≤Lmax,L,Reals]
Reduce[D[(Subscript[θ, 1+η])[L],L]≤ 0&&Lmin≤L≤Lmax,L,Reals]
Reduce[D[(Subscript[θ, 1-c])[L],L]≥0&&Lmin≤L≤Lmax,L,Reals]
Reduce[D[(Subscript[θ, -1/2])[L],L]≥0&&Lmin≤L≤Lmax,L,Reals]

Thus, the following interval enclosures are justified.  Actually, η, c,  r only contain one occurrence of L, and so are automatically sharp.

(Subscript[θ, -η])[Lint_Interval]:=Block[{L},PiecewiseMonotoneEnclosure[(Subscript[θ, -η])[L],L,{(NumericalApproximation[Root, (RowDefault["8.18", FEExpressionsNumericalApproximationElider]), Root[-400028897473100-265375772820540 #1-51872928254379 ((#1)^2)+4227068516184 ((#1)^3)+831712670784 ((#1)^4)&,2], ])},Lint]];
(Subscript[θ, 1+η])[Lint_Interval]:=Block[{L},PiecewiseMonotoneEnclosure[(Subscript[θ, 1+η])[L],L,{(NumericalApproximation[Root, (RowDefault["6.18", FEExpressionsNumericalApproximationElider]), Root[-322540649136100-126531152285940 #1+8926338680991 ((#1)^2)+2229053251464 ((#1)^3)+163781350704 ((#1)^4)&,2], ])},Lint]];
(Subscript[θ, 1-c])[Lint_Interval]:=Block[{L},PiecewiseMonotoneEnclosure[(Subscript[θ, 1-c])[L],L,{((-17617402+(Sqrt[197524318907258238]))/45811476)},Lint]];
(Subscript[θ, -1/2])[Lint_Interval]:=Block[{L},MonotoneEnclosure[(Subscript[θ, -1/2])[L],L,Lint]]

Additionally we will frequently encounter log((r/(c-1/2))), which is monotone decreasing:

Reduce[D[Log[((r[L])/(c[L]-1/2))],L]≤0&&Lmin≤L≤Lmax,L,Reals]

logrc[L_]=Log[((r[L])/(c[L]-1/2))];
logrc[Lint_Interval]:=Block[{L},PiecewiseMonotoneEnclosure[Log[((r[L])/(c[L]-1/2))],L,{((-17617402+(Sqrt[197524318907258238]))/45811476)},Lint]]

Er[a_,d_,T_]=((4 (4+3 π))/(45 ((((((17+2 a))^2)+4 (T^2)))^(3/2))))-((4 T)/(3 ((((17+2 a))^2)+4 (T^2))))+((8+6 π)/(45 ((((((17+2 a-2 d))^2)+4 (T^2)))^(3/2))))+((2 T)/(3 ((((17+2 a-2 d))^2)+4 (T^2))))+((8+6 π)/(45 ((((((17+2 a+2 d))^2)+4 (T^2)))^(3/2))))+((2 T)/(3 ((((17+2 a+2 d))^2)+4 (T^2))))+2 ArcTan[((1+2 a)/(2 T))]+2 ArcTan[((5+2 a)/(2 T))]+2 ArcTan[((9+2 a)/(2 T))]+2 ArcTan[((13+2 a)/(2 T))]-(1/2) (15+2 a) ArcTan[((17+2 a)/(2 T))]-ArcTan[((1+2 a-2 d)/(2 T))]-ArcTan[((5+2 a-2 d)/(2 T))]-ArcTan[((9+2 a-2 d)/(2 T))]-ArcTan[((13+2 a-2 d)/(2 T))]+(1/4) (15+2 a-2 d) ArcTan[((17+2 a-2 d)/(2 T))]-ArcTan[((1+2 a+2 d)/(2 T))]-ArcTan[((5+2 a+2 d)/(2 T))]-ArcTan[((9+2 a+2 d)/(2 T))]-ArcTan[((13+2 a+2 d)/(2 T))]+(1/4) (15+2 a+2 d) ArcTan[((17+2 a+2 d)/(2 T))]+(1/2) T Log[1+((((17+2 a))^2)/(4 (T^2)))]-(1/4) T Log[1+((((17+2 a-2 d))^2)/(4 (T^2)))]-(1/4) T Log[1+((((17+2 a+2 d))^2)/(4 (T^2)))];

Bounds on the pieces

Domains for L,η,c,r,(Subscript[σ, 1]),δ

ηinterval=η[Linterval]
cinterval=c[Linterval]
rinterval=r[Linterval]
N[{ηinterval,cinterval,rinterval},3]

σ1interval=(Subscript[σ, 1])[Linterval]
δinterval=δ[Linterval]
N[{σ1interval,δinterval},3]

θmeinterval=(Subscript[θ, -η])[Linterval];
θ1peinterval=(Subscript[θ, 1+η])[Linterval];
θ1mcinterval=(Subscript[θ, 1-c])[Linterval];
θm12interval=(Subscript[θ, -1/2])[Linterval];
N[{θmeinterval,θ1peinterval,θ1mcinterval,θm12interval},3]

Inequalities:	 -(3/2)<c[L]-r[L]<((-1)/2)<1-c[L]≤-η[L]<0<1<1+η[L]<c[L]<(Subscript[σ, 1])[L]<c[L]+r[L]

-(3/2)<c[L]-r[L]<((-1)/2)<1-c[L]<-η[L]<0<1<1+η[L]<c[L]<(Subscript[σ, 1])[L]<c[L]+r[L]

N[Reduce[-(3/2)<c[L]-r[L]<((-1)/2)<1-c[L]<-η[L]<0<1<1+η[L]<c[L]<(Subscript[σ, 1])[L]<c[L]+r[L],L],30]
Reduce[-(3/2)<c[L]-r[L]<((-1)/2)<1-c[L]<-η[L]<0<1<1+η[L]<c[L]<(Subscript[σ, 1])[L]<c[L]+r[L]&&Lmin≤L≤Lmax,L]

θ1peinterval≤2.1

Reduce[r[L]≥2c[L]-1&&Lmin≤L≤Lmax]

Bound:		|g(a,T)|≤((2-a)/(50T))

In the file “ZerosOfLFunctions-Prop32.nb”.

Bound:		((Subscript[E, δ])/π)≤(((640+216a)d-112-39a)/(1536(3T+3a-1)))+(1/(2^10))

This is in the file ZerosOfLFunctions-E.nb.

Bound:		|g(a,T)|+((Subscript[E, δ])/π)≤(1/(2^10))+((6/55)/(T-1/5))

bound[1]=(1/(2^10))+((6/55)/(T-1/5));

Clear[f];
f[a_,d_,T_]=bound[1]-(((2-a)/(50T))+(((640+216a)d-112-39a)/(1536(3T+3a-1)))+(1/(2^10)));
(* for each a, the function f is monotone in d, and rational in T *)
f[a_,dint_Interval,Tint_Interval]:=IntervalHull[f[a,Min[dint],Tint],f[a,Max[dint],Tint]];
f[a_,d_,Tint_Interval]:=Module[{T,tmin=Min[Tint],tmax=Max[Tint],min,max},
(* at this point, a and d are specific numbers, and what's left is rational in T *)
min=First[Minimize[{f[a,d,T],tmin≤T≤tmax},T,Reals]];
max=First[Maximize[{f[a,d,T],tmin≤T≤tmax},T,Reals]];
Interval[{min,max}]];

N[δinterval,4]

f[0,δinterval,Interval[{5/7,∞}]]
f[1,δinterval,Interval[{5/7,∞}]]

These warnings are not worrisome: they merely acknowledge that the extreme values happen as as T->∞.

Bound:		(2/π)Log[Zeta[(Subscript[σ, 1])]]-((Log[Zeta[2c]])/(Log[(r/(c-1/2))]))≤((16489+14928 L+402 (L^2))/(380433+35739 L+1024 (L^2)))

bound[2]=((16489+14928 L+402 (L^2))/(380433+35739 L+1024 (L^2)));

Clear[f];
f[L_]=bound[2]-((2/π)Log[Zeta[(Subscript[σ, 1])[L]]]-((Log[Zeta[2 c[L]]])/(Log[((r[L])/(c[L]-1/2))])));

Reduce[D[bound[2]]≥0&&Lmin≤L≤Lmax,L,Reals]

f[Lint_Interval]:=Module[{rat,rat2,rat3,L},
rat=MonotoneEnclosure[((16489+14928 L+402 (L^2))/(380433+35739 L+1024 (L^2))),L,Lint];
rat-((2/π)Log[Zeta[(Subscript[σ, 1])[Lint]]]-((Log[Zeta[2 c[Lint]]])/(logrc[Lint])))];

N[f[Interval[{10,11}]],30]

Timing[{t0,t1,t2}=ProveNonNegative[f,f,{Linterval},MaxDepth->20];]
Length/@{t0,t1,t2}

Bound:		((1/π)/(Log[r/ (c-1/2) ]))(Subscript[κ, 1]) L≤((62044+305799 L+18763 (L^2)+235 (L^3))/(2 (243814+38507 L+512 (L^2))))

bound[3]=((62044+305799 L+18763 (L^2)+235 (L^3))/(2 (243814+38507 L+512 (L^2))));

(Subscript[κ, 1])[L_]=((Subscript[θ, -η])[L]-(Subscript[θ, 1+η])[L])*((1+η[L]-c[L])/2)-(π-(Subscript[θ, -η])[L])(c[L]-(1/2))+((r[L](Sin[(Subscript[θ, -η])[L]]+Sin[(Subscript[θ, 1+η])[L]]))/2);

D[(Subscript[θ, -η])[L]-(Subscript[θ, 1+η])[L],L]
Reduce[D[(Subscript[θ, -η])[L]-(Subscript[θ, 1+η])[L],L]==0&&Lmin≤L≤Lmax]

D[((1+η[L]-c[L])/2),L]
Reduce[D[((1+η[L]-c[L])/2),L]≥0&&Lmin≤L≤Lmax]

D[((1+η[L]-c[L])/2),L]
Reduce[D[((1+η[L]-c[L])/2),L]≥0&&Lmin≤L≤Lmax]

temp=Simplify[(r[L]Sin[(Subscript[θ, -η])[L]])]
D[temp,L]
Reduce[D[temp,L]≤0&&Lmin≤L≤Lmax]

temp=Simplify[(r[L]Sin[(Subscript[θ, 1+η])[L]])]
D[temp,L]
Reduce[D[temp,L]≤0&&Lmin≤L≤Lmax]

(Subscript[κ, 1])[Lint_Interval]:=Module[{L,term1,term2,term3,term4},
term1=PiecewiseMonotoneEnclosure[(Subscript[θ, -η])[L]-(Subscript[θ, 1+η])[L],L,{(NumericalApproximation[Root, (RowDefault["7.73", FEExpressionsNumericalApproximationElider]), Root[900305963968546225236805567773000000+1826509705426578059429769259228400000 #1+1794907634483328728060569417943850000 ((#1)^2)+1024391992292832209252449624024392000 ((#1)^3)+319789090336879721298408965467508700 ((#1)^4)+38912788326621190364488248404718600 ((#1)^5)-4426974554006064736686088504168461 ((#1)^6)-1678006846867192009521495457823100 ((#1)^7)-100585450982815694112408348688812 ((#1)^8)+10446190388145213817267394838288 ((#1)^9)+1277318887539056464684224849696 ((#1)^10)+30749787465140494610180548992 ((#1)^11)&,6], ])},Lint];
term2=MonotoneEnclosure[((1+η[L]-c[L])/2),L,Lint];
term3=MonotoneEnclosure[r[L]Sin[(Subscript[θ, -η])[L]],L,Lint];
term4=MonotoneEnclosure[r[L]Sin[(Subscript[θ, 1+η])[L]],L,Lint];

term1*term2-(π-(Subscript[θ, -η])[Lint])(c[Lint]-(1/2))+((term3+term4)/2)];

Clear[f];
f[L_]=bound[3]-((1/π)/(logrc[L]))(Subscript[κ, 1])[L];

Reduce[D[bound[3],L]≥0&&Lmin≤L≤Lmax]

f[Lint_Interval]:=Module[{L,rat},
rat=MonotoneEnclosure[((62044+305799 L+18763 (L^2)+235 (L^3))/(2 (243814+38507 L+512 (L^2)))),L,Lint];
rat-((1/π)/(logrc[Lint]))(Subscript[κ, 1])[Lint]*Lint];

AbsoluteTiming[{fail,undecided,proven}=ProveNonNegative[f,f,{Linterval},MaxDepth->20];]
{fail,undecided,Length[proven]}

Bound:		((Log[Zeta[c]])/(2Log[(r/(c-1/2))]))((3/2)+(1/(2(Subscript[J, 1])))+(1/(Subscript[J, 2]))+((Subscript[θ, 1+η])/π)+(1-(1/(Subscript[J, 2])))((Subscript[θ, 1-c])/π)-((Subscript[θ, -η])/π))≤((199847+79917 L+5034 (L^2)+7 (L^3))/(2 (192512+31343 L+512 (L^2))))

bound[4]=((199847+79917 L+5034 (L^2)+7 (L^3))/(2 (192512+31343 L+512 (L^2))));

Clear[f];
f[L_]=Block[{J1=64,J2=24},
bound[4]-((Log[Zeta[c[L]]])/(2logrc[L]))((3/2)+(1/(2J1))+(1/J2)+(((Subscript[θ, 1+η])[L])/π)+(1-(1/J2))(((Subscript[θ, 1-c])[L])/π)-(((Subscript[θ, -η])[L])/π))]

{Plot[f[L],{L,Lmin,Lmax},PlotRange->All],Plot[f[L],{L,Lmin,6},PlotRange->All]}

Solve[D[bound[4],L]==0,L,Reals]

f[Lint_Interval]:=Module[{L,bound,J1=64,J2=24},
bound=MonotoneEnclosure[((199847+79917 L+5034 (L^2)+7 (L^3))/(2 (192512+31343 L+512 (L^2)))),L,Lint];
bound-((Log[Zeta[c[Lint]]])/(2logrc[Lint]))((3/2)+(1/(2J1))+(1/J2)+(((Subscript[θ, 1+η])[Lint])/π)+(1-(1/J2))(((Subscript[θ, 1-c])[Lint])/π)-(((Subscript[θ, -η])[Lint])/π))];

AbsoluteTiming[{fail,undecided,proven}=ProveNonNegative[f,f,{Linterval},MaxDepth->20];]
{fail,undecided,Length[proven]}

Bound: 		((Log[Zeta[1+η]])/(2Log[(r/(c-1/2))]))(-((Subscript[θ, 1+η])/π)+((Subscript[θ, 1-c])/π)+((Subscript[θ, -η])/π)-(1/2))≤((-82709+17494 L+3466 (L^2)-2 (L^3))/(2 (-188287+62894 L+512 (L^2))))

bound[5]=((-82709+17494 L+3466 (L^2)-2 (L^3))/(2 (-188287+62894 L+512 (L^2))));

Clear[f];
f[L_]=bound[5]-((Log[Zeta[1+η[L]]])/(2logrc[L]))(-(((Subscript[θ, 1+η])[L])/π)+(((Subscript[θ, 1-c])[L])/π)+(((Subscript[θ, -η])[L])/π)-(1/2))

Reduce[D[bound[5],L]≥0&&Lmin≤L≤Lmax]

f[Lint_Interval]:=Module[{L,rat,term},
rat=MonotoneEnclosure[((-82709+17494 L+3466 (L^2)-2 (L^3))/(2 (-188287+62894 L+512 (L^2)))),L,Lint];
term=((Log[Zeta[1+η[Lint]]])/(2logrc[Lint]))(-(((Subscript[θ, 1+η])[Lint])/π)+(((Subscript[θ, 1-c])[Lint])/π)+(((Subscript[θ, -η])[Lint])/π)-(1/2));
rat-term]

AbsoluteTiming[{fail,undecided,proven}=ProveNonNegative[f,f,{Linterval},MaxDepth->20];]
{fail,undecided,Length[proven]}

Bound: (Subscript[κ, 2])=(π/(4(Subscript[J, 1])))(Log[Zeta[c+r]]+2Sum[Log[Zeta[c+r Cos[((π j)/(2(Subscript[J, 1])))]]],{j,1,(Subscript[J, 1])-1}])
	(((Subscript[κ, 2])/π)/(Log[r/(c-1/2)]))≤((35688+11843 L+622 (L^2)+(L^3))/(689229+58176 L+1024 (L^2)))

bound[6]=((35688+11843 L+622 (L^2)+(L^3))/(689229+58176 L+1024 (L^2)));

Clear[f];
f[L_]=bound[6]-Block[{J1=64},((1/π)/(logrc[L]))(π/(4J1))(Log[Zeta[c[L]+r[L]]]+2Sum[Log[Zeta[c[L]+r[L] Cos[((π j)/(2J1))]]],{j,1,J1-1}])];

Reduce[D[((35688+11843 L+622 (L^2)+(L^3))/(689229+58176 L+1024 (L^2))),L]≥0&&Lmin≤L≤Lmax]

f[Lint_Interval]:=Module[{L,rat,J1=64},
rat=MonotoneEnclosure[((35688+11843 L+622 (L^2)+(L^3))/(689229+58176 L+1024 (L^2))),L,Lint];
rat-((1/π)/(logrc[Lint]))(π/(4J1))(Log[Zeta[c[Lint]+r[Lint]]]+2Sum[Log[Zeta[c[Lint]+r[Lint] Cos[((π j)/(2J1))]]],{j,1,J1-1}])];

AbsoluteTiming[{fail,undecided,proven}=ProveNonNegative[f,f,{Linterval},MaxDepth->20];]
{fail,undecided,Length[proven]}

Bound: (Subscript[κ, 3])=((π-(Subscript[θ, 1-c]))/(2(Subscript[J, 2])))(Log[Zeta[1-c+r]]+2Sum[Log[Zeta[1-c-r Cos[(Subscript[θ, 1-c])+(π-(Subscript[θ, 1-c]))(j/(Subscript[J, 2]))]]], {j, 1, (Subscript[J, 2])-1}])
	(((Subscript[κ, 3])/π)/(Log[r/(c-1/2)]))≤((-6171+827 L+537 (L^2))/(-92820+31635 L+1024 (L^2)))

bound[7]=((-6171+827 L+537 (L^2))/(-92820+31635 L+1024 (L^2)));

Clear[f];
f[L_]=bound[7]-Block[{J2=24},((1/π)/(logrc[L]))((π-(Subscript[θ, 1-c])[L])/(2J2))(Log[Zeta[1-c[L]+r[L]]]+2Sum[Log[Zeta[1-c[L]-r[L] Cos[(Subscript[θ, 1-c])[L](1-(j/J2))+((π j)/J2)]]], {j, 1, J2-1}])];

Reduce[D[bound[7],L]≥ 0&&L≥27]
Reduce[D[1-c[L]+r[L],L]≤0&&L≥27]

f[Lint_]:=Module[{L,rat,J2,rmcp1,insidezeta},
J2=24;
rat=MonotoneEnclosure[((-6171+827 L+537 (L^2))/(-92820+31635 L+1024 (L^2))),L,Lint];
rmcp1=Log[Zeta[MonotoneEnclosure[1-c[L]+r[L],L,Lint]]];
insidezeta[j_]:=IntervalIntersection[Interval[{Min[c[Lint]],∞}],1-c[Lint]-r[Lint]* Cos[(Subscript[θ, 1-c])[Lint]*(1-(j/J2))+((π j)/J2)]];
rat-((1/π)/(logrc[Lint]))((π-(Subscript[θ, 1-c])[Lint])/(2J2))(rmcp1+2Sum[Log[Zeta[insidezeta[j]]], {j, 1, J2-1}])];

N[f[Interval[{6,7}]],30]
N[f[Interval[{27,28}]],30]

Timing[Length/@ProveNonNegative[f,f,{Linterval},MaxDepth->25]]

Bound: 	(((Subscript[κ, 4])/π)/(Log[r/(c-1/2)]))≤((110537-2290 L-333 (L^2)+2 (L^3))/(-49052+314027 L+1024 (L^2)))

bound[8]=((110537-2290 L-333 (L^2)+2 (L^3))/(-49052+314027 L+1024 (L^2)));

The quantity (Subscript[κ, 4]) is defined by

Clear[K4];K4[c_,r_,η_]=(1/4)Block[{σ=c+r Cos[θ],t=r Sin[θ]},Integrate[(1+η-σ)(2t-4+(7/19)((((1+σ))^2)+(((t-2))^2))),{θ,ArcCos[((1+η-c)/r)],ArcCos[((-η-c)/r)]}]]

Some nontrivial rearranging work gives

(Subscript[κ, 4])[c_,r_,η_]:=Block[{α1=(Sqrt[(-1+c+r-η) (1-c+r+η)]),α2=(Sqrt[-(c-r+η) (c+r+η)])},(1/76) (α1(-48+14 c+14 (c^2)+7 (r^2)-7 η-7 c η)+α2(55-7 c-14 (c^2)-7 (r^2)+21 η+21 c η)+5 (((1+2 η))^2)+(41-55 c+7 (c^2)+7 (c^3)+14 c (r^2)+41 η-14 c η-7 (c^2) η-7 (r^2) η) (ArcTan[((-1+c-η)/(α1))]- ArcTan[((c+η)/(α2))]))]

Mathematica is unable to ascertain if the two expressions are equivalent, but they are.

FullSimplify[K4[c,r,η]-(Subscript[κ, 4])[c,r,η],Assumptions->((-3)/2)<c-r<((-1)/2)<1-c<-η<0<1<1+η<c<c+r]

MinMax[Table[Block[{k=RandomReal[{Lmin,Lmax}]},
N[K4[c[k],r[k],η[k]]-(Subscript[κ, 4])[c[k],r[k],η[k]],20]],{10000}]]

Now we turn to developing an interval enclosure for (Subscript[κ, 4]).

(* the alphas are monotone decreasing*)
Reduce[Lmin≤L≤Lmax&&D[(-1+c[L]+r[L]-η[L]) (1-c[L]+r[L]+η[L]),L]≤0,L,Reals]
Reduce[Lmin≤L≤Lmax&&D[-(c[L]-r[L]+η[L]) (c[L]+r[L]+η[L]),L]≤0,L,Reals]

(* the alpha coefficients are monotone, one decreasing and one increasing *)
Reduce[Lmin≤L≤Lmax&&D[(-48+14 c[L]+14 ((c[L])^2)+7 ((r[L])^2)-7 η[L]-7 c[L] η[L]),L]≤0,L,Reals]
Reduce[Lmin≤L≤Lmax&&D[(55-7 c[L]-14 ((c[L])^2)-7 ((r[L])^2)+21 η[L]+21 c[L] η[L]),L]≥0,L,Reals]

(*the arctan coefficient is monotone decreasing *)
Reduce[Lmin≤L≤Lmax&&D[(41-55 c[L]+7 ((c[L])^2)+7 ((c[L])^3)+14 c[L] ((r[L])^2)+41 η[L]-14 c[L] η[L]-7 ((c[L])^2) η[L]-7 ((r[L])^2) η[L]),L]≤0,L,Reals]

kappa4[L_]=(Subscript[κ, 4])[c[L],r[L],η[L]];
kappa4[Lint_Interval]:=Module[{a1c,a2c,arctanc,L,α1,α2},
α1=Sqrt[MonotoneEnclosure[(-1+c[L]+r[L]-η[L]) (1-c[L]+r[L]+η[L]),L,Lint]];
α2=Sqrt[MonotoneEnclosure[-(c[L]-r[L]+η[L]) (c[L]+r[L]+η[L]),L,Lint]];
a1c=MonotoneEnclosure[(-48+14 c[L]+14 ((c[L])^2)+7 ((r[L])^2)-7 η[L]-7 c[L] η[L]),L,Lint];
a2c=MonotoneEnclosure[(55-7 c[L]-14 ((c[L])^2)-7 ((r[L])^2)+21 η[L]+21 c[L] η[L]),L,Lint];
arctanc=MonotoneEnclosure[(41-55 c[L]+7 ((c[L])^2)+7 ((c[L])^3)+14 c[L] ((r[L])^2)+41 η[L]-14 c[L] η[L]-7 ((c[L])^2) η[L]-7 ((r[L])^2) η[L]),L,Lint];

(1/76) (α1*a1c+α2*a2c+5 (((1+2 η[Lint]))^2)+arctanc (ArcTan[((-1+c[Lint]-η[Lint])/(α1))]- ArcTan[((c[Lint]+η[Lint])/(α2))]))]

Reduce[Lmin≤L≤Lmax&&D[((110537-2290 L-333 (L^2)+2 (L^3))/(-49052+314027 L+1024 (L^2))),L]≤0,L,Reals]

Clear[f];
f[L_]=bound[8]-((kappa4[L]/π)/(logrc[L]));
f[Lint_Interval]:=Module[{L},MonotoneEnclosure[((110537-2290 L-333 (L^2)+2 (L^3))/(-49052+314027 L+1024 (L^2))),L,Lint]-((kappa4[Lint]/π)/(logrc[Lint]))];

N[f[Linterval],30]

Timing[Length/@ProveNonNegative[f,f,{Linterval},MaxDepth->20]]

Bound: 	(((Subscript[κ, 5])/π)/(Log[r/(c-1/2)]))≤((-2446-261 L+200 (L^2)-6 (L^3))/(-231541-24108 L+1024 (L^2)))

bound[9]=((-2446-261 L+200 (L^2)-6 (L^3))/(-231541-24108 L+1024 (L^2)));

For the current values of c,r, we have (Subscript[θ, -1/2])<π. The quantity (Subscript[κ, 5]) is defined by

Clear[K5];K5[c_,r_,η_]=(1/4)Block[{σ=c+r Cos[θ],t=r Sin[θ]},Integrate[(1-2σ)(2t-4+(7/19)((((1+σ))^2)+(((t-2))^2))),{θ,ArcCos[((-η-c)/r)],ArcCos[((-1/2-c)/r)]}]]

Some easy rearranging work gives

(Subscript[κ, 5])[c_,r_,η_]:=Block[{α1=(Sqrt[(r^2)-(((c+(1/2)))^2)]),α2=(Sqrt[(r^2)-(((c+η))^2)])},(1/76) (-(5/2) (-3+4 (-1+c) c+2 (r^2))- α1 (-103+7 c (3+4 c)+14 (r^2))+5 (2 (-1+c) c+(r^2)-2 η (1+η))+2 (-48+7 (r^2)+7 c (2+2 c-η)-7 η) α2+(41+7 (r^2)+c (-96+7 c (3+2 c)+28 (r^2))) (ArcCos[-((c+η)/r)]-ArcCos[-(((1/2)+c)/r)]))]

Mathematica is able to ascertain if the two expressions are equivalent, and they are.

Reduce[K5[c,r,η]==(Subscript[κ, 5])[c,r,η]&&-(3/2)<c-r<((-1)/2)<1-c<0<1<c<c+r]

%/.{c->c[L],r->r[L]}

Reduce[%&&Lmin≤L≤Lmax]

Now we turn to developing an interval enclosure for (Subscript[κ, 5]).

(* the α1 is monotone decreasing, and so is its coefficient *)
Reduce[Lmin≤L≤Lmax&&D[((r[L])^2)-(((c[L]+(1/2)))^2),L]≤0,L,Reals]
Reduce[Lmin≤L≤Lmax&&D[(-103+7 c[L] (3+4 c[L])+14 ((r[L])^2)),L]≤0,L,Reals]
(* the α2 is monotone decreasing, and so is its coefficient *)
Reduce[Lmin≤L≤Lmax&&D[((r[L])^2)-(((c[L]+η[L]))^2),L]≤0,L,Reals]
Reduce[Lmin≤L≤Lmax&&D[2 (-48+7 ((r[L])^2)+7 c[L] (2+2 c[L]-η[L])-7 η[L]),L]≤0,L,Reals]

(* the big terms are monotone increasing*)
Reduce[Lmin≤L≤Lmax&&D[-(5/2) (-3+4 (-1+c[L]) c[L]+2 ((r[L])^2))+5 (2 (-1+c[L]) c[L]+((r[L])^2)-2 η[L] (1+η[L])),L]≥0,L,Reals]

(*the arccos coefficient is monotone decreasing *)
Reduce[Lmin≤L≤Lmax&&D[(41+7 ((r[L])^2)+c[L] (-96+7 c[L] (3+2 c[L])+28 ((r[L])^2))),L]≤0,L,Reals]
(* the arccos term is monotone *)
Reduce[Lmin≤L≤Lmax&&D[(ArcCos[-((c[L]+η[L])/(r[L]))]-ArcCos[-(((1/2)+c[L])/(r[L]))]),L]≤0,L,Reals]

kappa5[L_]=(Subscript[κ, 5])[c[L],r[L],η[L]];
kappa5[Lint_Interval]:=Module[{a1c,α1,a2c,arccosc,arccos,L,bigs,α2},
α1=Sqrt[MonotoneEnclosure[((r[L])^2)-(((c[L]+(1/2)))^2),L,Lint]];
a1c=MonotoneEnclosure[(-103+7 c[L] (3+4 c[L])+14 ((r[L])^2)),L,Lint];
α2=Sqrt[MonotoneEnclosure[((r[L])^2)-(((c[L]+η[L]))^2),L,Lint]];
a2c=MonotoneEnclosure[2 (-48+7 ((r[L])^2)+7 c[L] (2+2 c[L]-η[L])-7 η[L]),L,Lint];
arccos=MonotoneEnclosure[ArcCos[-((c[L]+η[L])/(r[L]))]-ArcCos[-(((1/2)+c[L])/(r[L]))],L,Lint];
arccosc=MonotoneEnclosure[(41+7 ((r[L])^2)+c[L] (-96+7 c[L] (3+2 c[L])+28 ((r[L])^2))),L,Lint];
bigs=MonotoneEnclosure[-(5/2) (-3+4 (-1+c[L]) c[L]+2 ((r[L])^2))+5 (2 (-1+c[L]) c[L]+((r[L])^2)-2 η[L] (1+η[L])),L,Lint];

(1/76) (bigs-a1c*α1+a2c*α2+arccosc*arccos)]

Plot[kappa5[L],{L,15,16}]
N[kappa5[Interval[{15,16}]],20]

Reduce[Lmin≤L≤Lmax&&D[((-2446-261 L+200 (L^2)-6 (L^3))/(-231541-24108 L+1024 (L^2))),L]≤0,L,Reals]

Clear[f];
f[L_]=bound[9]-((kappa5[L]/π)/(logrc[L]));
f[Lint_Interval]:=Module[{L},MonotoneEnclosure[((-2446-261 L+200 (L^2)-6 (L^3))/(-231541-24108 L+1024 (L^2))),L,Lint]-((kappa5[Lint]/π)/(logrc[Lint]))];

N[f[Interval[{15+1/3,16-1/3}]],30]

Timing[Length/@ProveNonNegative[f,f,{Linterval},MaxDepth->25]]

Bound:	(((Subscript[κ, 6,1]) / π)/(Log[r/(c-1/2)]))≤ ((-1)/7)ArcCos[((L-6)/22)]

bound[10]=((-1)/7)ArcCos[((L-6)/22)];

Lstar[j_,θ_]=2r Sin[θ]-4+(7/19)((((j+c+r Cos[θ]))^2)+(((r Sin[θ]-2))^2));

Clear[K61];
K61[c_,r_]=FullSimplify[(1/4)Block[{σ=c+r Cos[θ],t=r Sin[θ]},
Integrate[(1-2σ-2)Lstar[2,θ]+2Lstar[0,θ],{θ,ArcCos[((-1/2-c)/r)],π}]],-(3/2)<c-r<((-1)/2)<1-c<0<1<c<c+r]

Some easy rearranging work gives

(Subscript[κ, 6])[c_,r_]:=Block[{α1=(Sqrt[(r^2)-(((c+(1/2)))^2)])},(1/152) (5 (-3+2 c-2 r) (1+2 c-2 r)+2 (-26+7 c (9+4 c)+14 (r^2)) α1-2 (76-12 c+49 (c^2)+14 (c^3)+7 (3+4 c) (r^2)) ArcCos[(((1/2)+c)/r)])]

Reduce[K61[c,r]==(Subscript[κ, 6])[c,r]&&-(3/2)<c-r<((-1)/2)<1-c<0<1<c<c+r]

Reduce[1<c[L]<(3/2)&&(1/2) (1+2 c[L])<r[L]<(1/2) (3+2 c[L])&&Lmin≤L≤Lmax]
Lmin≤L≤Lmax

(* Everything in sight is monotonic *)
Reduce[Lmin≤L≤Lmax&&D[5 (-3+2 c[L]-2 r[L]) (1+2 c[L]-2 r[L]),L]==0]
Reduce[Lmin≤L≤Lmax&&D[((r[L])^2)-(((c[L]+(1/2)))^2),L]==0]
Reduce[Lmin≤L≤Lmax&&D[(-26+7 c[L] (9+4 c[L])+14 ((r[L])^2)),L]==0]
Reduce[Lmin≤L≤Lmax&&D[(76-12 c[L]+49 ((c[L])^2)+14 ((c[L])^3)+7 (3+4 c[L]) ((r[L])^2)),L]==0]
Reduce[Lmin≤L≤Lmax&&D[(((1/2)+c[L])/(r[L])),L]==0]

kappa61[L_]=(Subscript[κ, 6])[c[L],r[L]];
kappa61[Lint_Interval]:=Module[{p1,α1,a1c,arccosc,arccos,L},
p1=MonotoneEnclosure[5 (-3+2 c[L]-2 r[L]) (1+2 c[L]-2 r[L]),L,Lint];
α1=MonotoneEnclosure[(Sqrt[((r[L])^2)-(((c[L]+(1/2)))^2)]),L,Lint];
a1c=MonotoneEnclosure[2(-26+7 c[L] (9+4 c[L])+14 ((r[L])^2)),L,Lint];
arccosc=MonotoneEnclosure[2 (76-12 c[L]+49 ((c[L])^2)+14 ((c[L])^3)+7 (3+4 c[L]) ((r[L])^2)) ,L,Lint];
arccos=MonotoneEnclosure[ArcCos[(((1/2)+c[L])/(r[L]))],L,Lint];

(1/152) (p1+a1c* α1-arccosc* arccos)]

Clear[f];
f[L_]:=-(1/7)ArcCos[((L-6)/22)]-((kappa61[L]/π)/(logrc[L]));

Timing[Length/@ProveNonNegative[f,f,{Linterval},MaxDepth->25]]

Assembling the final bound

sharp[L_,T_]=Sum[bound[k],{k,7}]+(1/(T+2))Sum[bound[k],{k,8,10}]

First we wrestle with the terms involving T.

Clear[f];
f[L_,T_]=((6/55)/(T-1/5))+(1/(T+2))(bound[8]+bound[9]+bound[10])

Reduce[Lmin≤L≤Lmax&&D[bound[8]+bound[9]+bound[10],L]==0]

That is, f is unimodal in L.  It is not monotone in T, but no matter.

f[Lint_Interval,Tint_Interval]:=Module[{L,Aint},
Aint=PiecewiseMonotoneEnclosure[((110537-2290 L-333 (L^2)+2 (L^3))/(-49052+314027 L+1024 (L^2)))+((-2446-261 L+200 (L^2)-6 (L^3))/(-231541-24108 L+1024 (L^2)))+((-1)/7)ArcCos[((L-6)/22)],L,{(NumericalApproximation[Root, (RowDefault["17.9", FEExpressionsNumericalApproximationElider]), Root[-75529728721541201950067118602954361647109972672-34346740259720214332104212410831719481641270444 #1-4845243537439950889739649277342754321891548775 ((#1)^2)-855291747057300725210806858372345680753841712 ((#1)^3)-142909554182042231420601752704648709656453243 ((#1)^4)+«13»+7884050355236813768901651333120 ((#1)^14)+120774757520310597737567485952 ((#1)^15)+526217511788941831177240576 ((#1)^16)+1012805729172878218231808 ((#1)^17)+903890459611768029184 ((#1)^18)&,4], ])},Lint];
((6/55)/(Tint-1/5))+(Aint/(2+Tint))]

f[Interval[{15,16}],Interval[{5/7,∞}]]

tobeprovennonneg[L_,T_]:=(13/86)-f[L,T];

ProveNonNegative[tobeprovennonneg,tobeprovennonneg,{Linterval,Interval[{5/7,∞}]}]

sharp2[L_]=(1/1024)+((-6171+827 L+537 (L^2))/(-92820+31635 L+1024 (L^2)))+((16489+14928 L+402 (L^2))/(380433+35739 L+1024 (L^2)))+((-82709+17494 L+3466 (L^2)-2 (L^3))/(2 (-188287+62894 L+512 (L^2))))+((35688+11843 L+622 (L^2)+(L^3))/(689229+58176 L+1024 (L^2)))+((199847+79917 L+5034 (L^2)+7 (L^3))/(2 (192512+31343 L+512 (L^2))))+((62044+305799 L+18763 (L^2)+235 (L^3))/(2 (243814+38507 L+512 (L^2))))+(13/86);

Plot[0.22737L+2Log[1+L]-(1/2)-sharp2[L],{L,Lmin,Lmax},PlotRange->All]

toprovenonneg[L_]=(22737/100000)L+2Log[1+L]-(1/2)-sharp2[L]

The rational part of toprovenonneg[L] is monotone decreasing:

Reduce[L≥Lmin&&D[-(28715/44032)+((22737 L)/100000)-((-6171+827 L+537 (L^2))/(-92820+31635 L+1024 (L^2)))-((16489+14928 L+402 (L^2))/(380433+35739 L+1024 (L^2)))-((-82709+17494 L+3466 (L^2)-2 (L^3))/(2 (-188287+62894 L+512 (L^2))))-((35688+11843 L+622 (L^2)+(L^3))/(689229+58176 L+1024 (L^2)))-((199847+79917 L+5034 (L^2)+7 (L^3))/(2 (192512+31343 L+512 (L^2))))-((62044+305799 L+18763 (L^2)+235 (L^3))/(2 (243814+38507 L+512 (L^2)))),L]≤0]

toprovenonneg[Lint_Interval]:=Module[{L,Lmin,Lmax,expr,min,max},
{Lmin,Lmax}={Min[Lint],Max[Lint]};
expr=-(28715/44032)+((22737 L)/100000)-((-6171+827 L+537 (L^2))/(-92820+31635 L+1024 (L^2)))-((16489+14928 L+402 (L^2))/(380433+35739 L+1024 (L^2)))-((-82709+17494 L+3466 (L^2)-2 (L^3))/(2 (-188287+62894 L+512 (L^2))))-((35688+11843 L+622 (L^2)+(L^3))/(689229+58176 L+1024 (L^2)))-((199847+79917 L+5034 (L^2)+7 (L^3))/(2 (192512+31343 L+512 (L^2))))-((62044+305799 L+18763 (L^2)+235 (L^3))/(2 (243814+38507 L+512 (L^2))));
exprint=MonotoneEnclosure[expr,L,Lint];
exprint+2 Log[1+Lint]];

N[toprovenonneg[Linterval],30]

ProveNonNegative[toprovenonneg,toprovenonneg,{Linterval},MaxDepth->15]