If[!TrueQ[Private`$ev],Block[{Private`$ev=True},Print["Total time: ",First@AbsoluteTiming[ClearAll["Global`*"];
NotebookEvaluate[EvaluationNotebook[],InsertResults->True]]," s"]]]

ClearAll["Global`*"];
(*(Subscript[Q, *]^2) in (A.3)*)
Qanew[t_]:=-32389/844*t^14+692573/1409*t^13-14647839/5182*t^12+13634891/1418*t^11-31307644/1461*t^10+22954676/703*t^9-1268792/37*t^8+34165996/1415*t^7-12679168/1223*t^6+2124876/1117*t^5+78128/353*t^4+15317/829*t^3-138192/1231*t^2+15295/813;
(* (Subscript[W, 1]) in (A.4)*)
W1[t_]:=-126751 t^22/80621266+998813 t^21/24102701-44784703 t^20/90944085+532787760 t^19/154914809-1478230681 t^18/97178472+1104148971 t^17/27114439-6386998649 t^16/165889120-4563349408 t^15/24620175+12295664789 t^14/11848354-25742069395 t^13/8929817+22711315187 t^12/4190364-21505639879 t^11/2916474+32713853029 t^10/4462850-12946708519 t^9/2496198+3403022733 t^8/1411424-6729001962 t^7/11651297-626483074 t^5/65670795+752248559 t^4/20846520-89936485 t^2/6984383+93423/21539;
(* (Subscript[W, 2]) in (A.5)*)
W2[t_]:=157*t^8/1255706-5215*t^7/1535379+25008*t^6/610441-1118777*t^5/3886821+1230788*t^4/949047-784873*t^3/202656+10232110*t^2/1348117-2084185*t/228972+43251/8233;
(* (Subscript[P, 1]), (Subscript[P, 2]) in (B.2)*)
P1[t_]:=2(W1[t]-75 10^(-6))^2;P2[t_]:=(W1[t]+75 10^(-6))(W1'[t]-42 10^(-5));
(* (Subscript[P, 3]), (Subscript[P, 4]) in (B.3)*)
P3[t_]:=2(W1[t]+75 10^(-6))^2;P4[t_]:=(W1[t]+75 10^(-6))^4;
(* for example, Dig5[312]=31200; Dig5[3123423]=31234*)
Dig5[x_]:=IntegerPart[x*10^5/10^(IntegerLength[x])];
(* for example, FU[401256/309977]=(40126/30997) gives an upper bound of 401256/309977*)
FU[s_]:=If[s>0,(Dig5[Numerator[s]]+1)/Dig5[Denominator[s]]*10^(IntegerLength[Numerator[s]]-IntegerLength[Denominator[s]]),Print["Error: Input must be a positive number."];
$Failed]
(* for example, NL[401256/3077]=6;  DL[401256/3077]=4*)
NL[x_]:=IntegerLength[Numerator[x]]; DL[x_]:=IntegerLength[Denominator[x]];
(*The following function  polyMax corresponds to formula (1.24) in Lemma 1.4. *)
polyMax[p_,a_,b_,dx_]:=Module[{d,pValues,M2,Lam,Nsub,coeffList},If[!PolynomialQ[p,x],Return["Error: p must be a polynomial in x."];];
coeffList=CoefficientList[p,x];
d=Exponent[p,x];
Nsub=Ceiling[(b-a)/dx];
If[6 Nsub^2-d^2 (d^2-1)<=0,Return["Error: lambda must be positive."];];
pValues=ParallelTable[FromDigits[Reverse[coeffList],a+k*dx],{k,0,Nsub}];
M2=Max[Abs[pValues]];
Lam=((6Nsub^2)/(6Nsub^2-d^2(d^2-1)));
Lam*M2]
(*The following function  polynomialMin corresponds to formula (1.25) in Lemma 1.4. *)
polynomialMin[p_,a_,b_,dx_]:=Module[{d,pValues,m1,m2,lam,Nsub,coeffList},If[!PolynomialQ[p,x],Return["Error: p must be a polynomial in x."];];
coeffList=CoefficientList[p,x];
d=Exponent[p,x];
Nsub=Ceiling[(b-a)/dx];
If[6 Nsub^2-d^2 (d^2-1)<=0,Return["Error: lambda must be positive."];];
pValues=ParallelTable[FromDigits[Reverse[coeffList],a+k*dx],{k,0,Nsub}];
m1=Min[pValues];
m2=Max[Abs[pValues]];
lam=(d^2 (d^2-1))/(6 Nsub^2-d^2 (d^2-1));
m1-lam*m2] 
(*The following functions are used in Lemma 4.4*)
H[x1_,x2_,x3_,x4_,y1_,y2_,y3_,y4_,p1_,p2_]:=4*p1*x3^2*y1^2+4*p1*p2*x2*x4*y1^2-4*p1*p2*x1*x4*y1*y2-p2^2*x4^2*y2^2-8*p1*x1*x3*y1*y3-4*p2*x3*x4*y2*y3+4*p1*x1^2*y3^2+4*p2*x2*x4*y3^2-4*p1*p2*x1*x2*y1*y4+4*p1*p2*x1^2*y2*y4+4*p2*x3^2*y2*y4+2*p2^2*x2*x4*y2*y4-4*p2*x2*x3*y3*y4-p2^2*x2^2*y4^2;
HM[x1_,x2_,x3_,x4_,y1_,y2_,y3_,y4_,p1_,p2_]:=4*p1*x3^2*y1^2+4*p1*p2*x2*x4*y1^2+4*p1*p2*x1*x4*y1*y2+p2^2*x4^2*y2^2+8*p1*x1*x3*y1*y3+4*p2*x3*x4*y2*y3+4*p1*x1^2*y3^2+4*p2*x2*x4*y3^2+4*p1*p2*x1*x2*y1*y4+4*p1*p2*x1^2*y2*y4+4*p2*x3^2*y2*y4+2*p2^2*x2*x4*y2*y4+4*p2*x2*x3*y3*y4+p2^2*x2^2*y4^2;

Toy Examples

toy example 1

polynomialMin[3 x P2[x]+3(W1[x]-75 10^(-6))^2-1,0,(1/2),(5/(10^5))]>0

toy example 2

Clear[U,Ud,U2d,p,R];T=3/10;U[x_,t_]:=t-31/5 t^3+1/3 t^4+472/21 t^5-25 t^6+(-1/6 t^3+21/20 t^5-8/7 t^6)x;
Ud[x_,t_]:=Derivative[0,1][U][x,t];U2d[x_,t_]:=Derivative[0,2][U][x,t];
R[x_,t_]:=U2d[x,t]+(x+2 Qanew[t]-1) U[x,t];
p=Integrate[R[x,t]^2,{t,0,T}];
Ud[x,T]
2 75/10^5 T+T^(1/2)(polyMax[p,144/10,192/10,1/10])^(1/2)<7/10^3

Case l=0: Theorem 5.1

Proposition 5.2: τ∈[12.4,19.2]

Clear[Uaapp,Vaapp,Ubapp,Vbapp,Uad,Vad,Ubd,Vbd,Ua2d,Va2d,Ub2d,Vb2d];
Uaapp[τ_,t_]:=(4550*t^7)/131-(5787*t^6)/91+(3986*t^5)/105-(334*t^4)/211-(727*t^3)/120+(t^2)/242+t+((58*t^7)/49-(305*t^6)/129+(90*t^5)/59-(6*t^4)/61-(10*t^3)/63-(t^2)/3170)*τ;
Vaapp[τ_,t_]:=-(2251*t^7)/81+(4841*t^6)/99-(11060*t^5)/403+(89*t^4)/102+(429*t^3)/136-(t^2)/140+((-9*t^7)/92+(17*t^6)/162+(5*t^5)/111-(3*t^4)/133+(t^3)/260-(t^2)/3409)*τ;
Ubapp[τ_,t_]:=-(3423*t^7)/124+(4105*t^6)/84-(3577*t^5)/130+(72*t^4)/79+(129*t^3)/41-(t^2)/155+((5*t^7)/83-(t^6)/52-(4*t^5)/95+(t^4)/61-(t^3)/382+(t^2)/5233)*τ;
Vbapp[τ_,t_]:=(5468*t^7)/155-(8018*t^6)/121+(3078*t^5)/79-(406*t^4)/225-(1417*t^3)/235+(t^2)/461+t+((-241*t^7)/443+(288*t^6)/253-(95*t^5)/148+(15*t^4)/374+(61*t^3)/372+(t^2)/15381)*τ;
Uad[x_,t_]:=Derivative[0,1][Uaapp][x,t];
Vad[x_,t_]:=Derivative[0,1][Vaapp][x,t];
Ubd[x_,t_]:=Derivative[0,1][Ubapp][x,t];
Vbd[x_,t_]:=Derivative[0,1][Vbapp][x,t];
Ua2d[x_,t_]:=Derivative[0,2][Uaapp][x,t];
Va2d[x_,t_]:=Derivative[0,2][Vaapp][x,t];
Ub2d[x_,t_]:=Derivative[0,2][Ubapp][x,t];
Vb2d[x_,t_]:=Derivative[0,2][Vbapp][x,t];

(5.2 )

Clear[pa,pb,x,es,du,tauL,tauR,Ya1,Ya2,Ya3,Ya4,Yb1,Yb2,Yb3,Yb4,T];
tauL=124/10;tauR=192/10;pa=1/10;pb=427/100;es=45/10^3;du=2*(10^(-2));T=475/1000;
Ya1[x_]:=Uaapp[x,T];Ya2[x_]:= Vaapp[x,T]; Ya3[x_]:=Uad[x,T];Ya4[x_]:=Vad[x,T];
Yb1[x_]:=Ubapp[x,T]; Yb2[x_]:= Vbapp[x,T]; Yb3[x_]:= Ubd[x,T];Yb4[x_]:=Vbd[x,T];
Hepsilon[x_]:=Simplify[H[Ya1[x],Ya2[x],Ya3[x],Ya4[x],Yb1[x],Yb2[x],Yb3[x],Yb4[x],pa,pb]-(HM[Abs[Ya1[x]]+es,Abs[Ya2[x]]+es,Abs[Ya3[x]]+es,Abs[Ya4[x]]+es,Abs[Yb1[x]]+es,Abs[Yb2[x]]+es,Abs[Yb3[x]]+es,Abs[Yb4[x]]+es,pa,pb]-HM[Abs[Ya1[x]],Abs[Ya2[x]],Abs[Ya3[x]],Abs[Ya4[x]],Abs[Yb1[x]],Abs[Yb2[x]],Abs[Yb3[x]],Abs[Yb4[x]],pa,pb])];
Ya2[x]-es
Ya4[x]-es
HepsilonExpanded=Expand[Hepsilon[x]];
xvals=Range[tauL,tauR,du];  
minValue=Min[HepsilonExpanded/. x->xvals];
minValue>0

(5.3)

Clear[tauL,tauR,dx,T,Za,Zb,x,Ra,Rb,A1,A2,B1,B2];tauL=124/10;tauR=192/10;dx=2*(10^(-2));T=475/1000;
A1[x_,t_]:=Ua2d[x,t]-(1-x-2 Qanew[t]) Uaapp[x,t]-Qanew[t] Vaapp[x,t];
A2[x_,t_]:=Va2d[x,t]-(1+x-2 Qanew[t]) Vaapp[x,t]-Qanew[t] Uaapp[x,t];
B1[x_,t_]:=Ub2d[x,t]-(1-x-2 Qanew[t]) Ubapp[x,t]-Qanew[t] Vbapp[x,t];
B2[x_,t_]:=Vb2d[x,t]-(1+x-2 Qanew[t]) Vbapp[x,t]-Qanew[t] Ubapp[x,t];
Za=Integrate[ExpandAll[A1[x,t]^2+A2[x,t]^2],{t,0,T}];
Zb=Integrate[ExpandAll[B1[x,t]^2+B2[x,t]^2],{t,0,T}];
Ra=polyMax[Za,tauL,tauR,dx];
Rb=polyMax[Zb,tauL,tauR,dx];
Max[FU[Ra],FU[Rb]]

(5.4)

k=(Sqrt[tauR+1]);{(1/2) (Sqrt[((2 k T+Sinh[2 k T])/k)])<(1493/1000),((3T Sinh[k T])/(2 k))<(6690/(10^4)), (1493/1000)(Sqrt[(14039/18384000)])+(6690/(10^4))(75/(10^5))≤(418/(10^4))}

(5.5)

(dx/2)Max[Abs[Ya1'[tauL]],Abs[Ya1'[tauR]],Abs[Ya2'[tauL]],Abs[Ya2'[tauR]],Abs[Ya3'[tauL]],Abs[Ya3'[tauR]],Abs[Ya4'[tauL]],Abs[Ya4'[tauR]],Abs[Yb1'[tauL]],Abs[Yb1'[tauR]],Abs[Yb2'[tauL]],Abs[Yb2'[tauR]],Abs[Yb3'[tauL]],Abs[Yb3'[tauR]],Abs[Yb4'[tauL]],Abs[Yb4'[tauR]]]<(1/1000)

(5.1)

k=(Sqrt[tauR+1]);
(1/2) (Sqrt[((2 k T+Sinh[2 k T])/k)])(Sqrt[Max[FU[Ra],FU[Rb]]])+((3T Sinh[k T])/(2 k)) (75/(10^5))+(1/20)  dx<es

Proposition C.1: τ∈[5.4,12.4]

Clear[Uaapp,Vaapp,Ubapp,Vbapp,Uad,Vad,Ubd,Vbd,Ua2d,Va2d,Ub2d,Vb2d];Uaapp[τ_,t_]:=(250858*t^10)/4155-(42245*t^9)/226+(7428*t^8)/35-(8522*t^7)/109-(9443*t^6)/240+(11239*t^5)/283-(698*t^4)/265-(1186*t^3)/203-(10*t^2)/749+t+(5*t^10/402-14*t^9/341+7*t^8/135-5*t^7/214-t^6/96+t^5/81-t^4/1295+t^3/12292)*τ^2+(303*t^10/272-642*t^9/179+843*t^8/199-111*t^7/68-207*t^6/244+584*t^5/629-26*t^4/435-48*t^3/299-t^2/3075)*τ;
Vaapp[τ_,t_]:=-(13012*t^10)/297+(50423*t^9)/387-(35597*t^8)/261+(11461*t^7)/333+(13129*t^6)/321-(20636*t^5)/669+(431*t^4)/177+(255*t^3)/88+(2*t^2)/167+(t^10/5317-t^9/336+4*t^8/435-t^7/90+3*t^6/389-t^5/459+t^4/2762-t^3/28556)*τ^2+(15*t^10/256-99*t^9/232+493*t^8/450-534*t^7/389+248*t^6/285-25*t^5/102+7*t^4/172-t^3/255+t^2/4980)*τ;
Ubapp[τ_,t_]:=-(3355*t^10)/78+(51257*t^9)/401-(55000*t^8)/413+(7825*t^7)/244+(12499*t^6)/298-(11800*t^5)/379+(236*t^4)/95+(1727*t^3)/597+(4*t^2)/327+(-t^10/167+5*t^9/288-5*t^8/249+5*t^7/466-t^6/503+t^5/2013-t^4/10812+t^3/94132)*τ^2+((103*t^10)/334-(122*t^9)/165+(95*t^8)/201+(35*t^7)/172-(115*t^6)/337+(23*t^5)/240-(6*t^4)/409+(t^3)/805-(t^2)/18830)*τ;
Vbapp[τ_,t_]:=(18556*t^10)/313-(107695*t^9)/587+(66232*t^8)/319-(23047*t^7)/308-(13337*t^6)/328+(7012*t^5)/175-(167*t^4)/62-(1249*t^3)/214-(4*t^2)/293+t+((14*t^10)/741-(18*t^9)/301+(13*t^8)/171-(7*t^7)/166+(2*t^6)/375+(t^5)/132+(t^4)/12270)*τ^2+((-376*t^10)/245+(634*t^9)/129-(2809*t^8)/465+(1457*t^7)/491+(21*t^6)/85-(268*t^5)/353+(t^4)/33+(35*t^3)/214+(t^2)/6317)*τ;
Uad[x_,t_]:=Derivative[0,1][Uaapp][x,t];
Vad[x_,t_]:=Derivative[0,1][Vaapp][x,t];
Ubd[x_,t_]:=Derivative[0,1][Ubapp][x,t];
Vbd[x_,t_]:=Derivative[0,1][Vbapp][x,t];
Ua2d[x_,t_]:=Derivative[0,2][Uaapp][x,t];
Va2d[x_,t_]:=Derivative[0,2][Vaapp][x,t];
Ub2d[x_,t_]:=Derivative[0,2][Ubapp][x,t];
Vb2d[x_,t_]:=Derivative[0,2][Vbapp][x,t];

(C.2)

Clear[pa,pb,x,es,du,tauL,tauR,Ya1,Ya2,Ya3,Ya4,Yb1,Yb2,Yb3,Yb4,T];
tauL=54/10;tauR=124/10;pa=96/10;pb=343/100;es=26/10^3;du=(10^(-2));T=2/3;
Ya1[x_]:=Uaapp[x,T];Ya2[x_]:= Vaapp[x,T]; Ya3[x_]:=Uad[x,T];Ya4[x_]:=Vad[x,T];
Yb1[x_]:=Ubapp[x,T]; Yb2[x_]:= Vbapp[x,T]; Yb3[x_]:= Ubd[x,T];Yb4[x_]:=Vbd[x,T];
Hepsilon[x_]:=H[Ya1[x],Ya2[x],Ya3[x],Ya4[x],Yb1[x],Yb2[x],Yb3[x],Yb4[x],pa,pb]-(HM[Abs[Ya1[x]]+es,Abs[Ya2[x]]+es,Abs[Ya3[x]]+es,Abs[Ya4[x]]+es,Abs[Yb1[x]]+es,Abs[Yb2[x]]+es,Abs[Yb3[x]]+es,Abs[Yb4[x]]+es,pa,pb]-HM[Abs[Ya1[x]],Abs[Ya2[x]],Abs[Ya3[x]],Abs[Ya4[x]],Abs[Yb1[x]],Abs[Yb2[x]],Abs[Yb3[x]],Abs[Yb4[x]],pa,pb]);
Ya2[x]-es
Ya4[x]-es
HepsilonExpanded=Expand[Hepsilon[x]];
xvals=Range[tauL,tauR,du];  
minValue=Min[HepsilonExpanded/. x->xvals];
minValue>0

(C.3)

Max[Abs[Ya1'[tauL]],Abs[Ya1'[tauR]],Abs[Ya2'[tauL]],Abs[Ya2'[tauR]],Abs[Ya3'[tauL]],Abs[Ya3'[tauR]],Abs[Ya4'[tauL]],Abs[Ya4'[tauR]],Abs[Yb1'[tauL]],Abs[Yb1'[tauR]],Abs[Yb2'[tauL]],Abs[Yb2'[tauR]],Abs[Yb3'[tauL]],Abs[Yb3'[tauR]],Abs[Yb4'[tauL]],Abs[Yb4'[tauR]]]<(2/5)

(C.4)

Clear[tauL,tauR,dx,T,Za,Zb,x,Ra,Rb,A1,A2,B1,B2];tauL=54/10;tauR=124/10;T=2/3;dx=(10^(-2));
A1[x_,t_]:=Ua2d[x,t]-(1-x-2 Qanew[t]) Uaapp[x,t]-Qanew[t] Vaapp[x,t];
A2[x_,t_]:=Va2d[x,t]-(1+x-2 Qanew[t]) Vaapp[x,t]-Qanew[t] Uaapp[x,t];
B1[x_,t_]:=Ub2d[x,t]-(1-x-2 Qanew[t]) Ubapp[x,t]-Qanew[t] Vbapp[x,t];
B2[x_,t_]:=Vb2d[x,t]-(1+x-2 Qanew[t]) Vbapp[x,t]-Qanew[t] Ubapp[x,t];
Za=Integrate[ExpandAll[A1[x,t]^2+A2[x,t]^2],{t,0,T}];
Zb=Integrate[ExpandAll[B1[x,t]^2+B2[x,t]^2],{t,0,T}];
Ra=polyMax[Za,tauL,tauR,dx];
Rb=polyMax[Zb,tauL,tauR,dx];
k=(Sqrt[tauR+1]);
(1/2) (Sqrt[((2 k T+Sinh[2 k T])/k)])(Sqrt[Max[FU[Ra],FU[Rb]]])+((3T Sinh[k T])/(2 k)) (75/(10^5))+(1/5) dx<es

Proposition C.1: τ∈[2.1,5.4]

Clear[Uaapp,Vaapp,Ubapp,Vbapp,Uad,Vad,Ubd,Vbd,Ua2d,Va2d,Ub2d,Vb2d];Uaapp[τ_,t_]:=(42673*t^12)/692-(1055462*t^11)/3005+(424795*t^10)/488-(435706*t^9)/359+(419355*t^8)/413-(130882*t^7)/269+(20712*t^6)/211+(3913*t^5)/423+(405*t^4)/241-(4633*t^3)/746+t^2/278+t+((89*t^12)/67-(1981*t^11)/262+(4426*t^10)/235-(21136*t^9)/795+(5435*t^8)/239-(6325*t^7)/559+(437*t^6)/176+(23*t^5)/135+(15*t^4)/296-(95*t^3)/558+t^2/7198)*τ+((-2*t^12)/231+(13*t^11)/401-t^10/23+(5*t^9)/276+(4*t^8)/451-t^7/383-(5*t^6)/328+(3*t^5)/227-t^4/1153+t^3/11554)*τ^2;
Vaapp[τ_,t_]:=-(26307*t^12)/491+(81288*t^11)/271-(257262*t^10)/353+(290879*t^9)/293-(214088*t^8)/265+(91013*t^7)/243-(19248*t^6)/263-(1193*t^5)/211-(267*t^4)/238+(1981*t^3)/619-t^2/519+((-233*t^12)/354+(1250*t^11)/367-(1958*t^10)/259+(3649*t^9)/394-(6277*t^8)/944+(888*t^7)/329-(228*t^6)/409+(21*t^5)/244-(3*t^4)/347+t^3/1861-t^2/53354)*τ+((3*t^12)/152-(20*t^11)/207+(58*t^10)/279-(20*t^9)/77+(101*t^8)/481-(23*t^7)/200+(9*t^6)/206-t^5/96+t^4/636-t^3/7055)*τ^2;
Ubapp[τ_,t_]:=-(23768*t^12)/441+(30452*t^11)/101-(91512*t^10)/125+(987850*t^9)/991-(236014*t^8)/291+(129403*t^7)/344-(160111*t^6)/2171-(4746*t^5)/859-(397*t^4)/348+(1284*t^3)/401-t^2/498+((179*t^12)/278-(2323*t^11)/697+(2951*t^10)/399-(1077*t^9)/119+(1509*t^8)/233-(521*t^7)/200+(34*t^6)/65-(15*t^5)/193+(3*t^4)/409-(t^3)/2412+(t^2)/79649)*τ+((-4*t^12)/423+(16*t^11)/343-(39*t^10)/392+(38*t^9)/319-(19*t^8)/219+(27*t^7)/703-(2*t^6)/215+t^5/592-(t^4)/4961+(t^3)/67049)*τ^2;
Vbapp[τ_,t_]:=(27683*t^12)/447-(214333*t^11)/608+(289907*t^10)/332-(320070*t^9)/263+(845926*t^8)/831-(18539*t^7)/38+(25544*t^6)/259+(1335*t^5)/146+(765*t^4)/451-(733*t^3)/118+t^2/273+t+((-369*t^12)/280+(4729*t^11)/630-(4883*t^10)/261+(7160*t^9)/271-(3865*t^8)/171+(3944*t^7)/351-(547*t^6)/223-(148*t^5)/831-(4*t^4)/81+(74*t^3)/435-t^2/7602)*τ+((t^12)/72-(74*t^11)/961+(79*t^10)/420-(107*t^9)/408+(74*t^8)/331-(22*t^7)/197+(8*t^6)/323+(t^5)/255+(t^4)/1959-(t^3)/27802)*τ^2;
Uad[x_,t_]:=Derivative[0,1][Uaapp][x,t];
Vad[x_,t_]:=Derivative[0,1][Vaapp][x,t];
Ubd[x_,t_]:=Derivative[0,1][Ubapp][x,t];
Vbd[x_,t_]:=Derivative[0,1][Vbapp][x,t];
Ua2d[x_,t_]:=Derivative[0,2][Uaapp][x,t];
Va2d[x_,t_]:=Derivative[0,2][Vaapp][x,t];
Ub2d[x_,t_]:=Derivative[0,2][Ubapp][x,t];
Vb2d[x_,t_]:=Derivative[0,2][Vbapp][x,t];

(C.2)

Clear[pa,pb,x,es,du,tauL,tauR,Ya1,Ya2,Ya3,Ya4,Yb1,Yb2,Yb3,Yb4,T];
tauL=21/10;tauR=54/10;pa=4;pb=182/100;es=2/100;du=(10^(-2));T=856/1000;
Ya1[x_]:=Uaapp[x,T];Ya2[x_]:= Vaapp[x,T]; Ya3[x_]:=Uad[x,T];Ya4[x_]:=Vad[x,T];
Yb1[x_]:=Ubapp[x,T]; Yb2[x_]:= Vbapp[x,T]; Yb3[x_]:= Ubd[x,T];Yb4[x_]:=Vbd[x,T];
Hepsilon[x_]:=H[Ya1[x],Ya2[x],Ya3[x],Ya4[x],Yb1[x],Yb2[x],Yb3[x],Yb4[x],pa,pb]-(HM[Abs[Ya1[x]]+es,Abs[Ya2[x]]+es,Abs[Ya3[x]]+es,Abs[Ya4[x]]+es,Abs[Yb1[x]]+es,Abs[Yb2[x]]+es,Abs[Yb3[x]]+es,Abs[Yb4[x]]+es,pa,pb]-HM[Abs[Ya1[x]],Abs[Ya2[x]],Abs[Ya3[x]],Abs[Ya4[x]],Abs[Yb1[x]],Abs[Yb2[x]],Abs[Yb3[x]],Abs[Yb4[x]],pa,pb]);
Ya2[x]-es
Ya4[x]-es
HepsilonExpanded=Expand[Hepsilon[x]];
xvals=Range[tauL,tauR,du];  
minValue=Min[HepsilonExpanded/. x->xvals];
minValue>0

(C.3)

Max[Abs[Ya1'[tauL]],Abs[Ya1'[tauR]],Abs[Ya2'[tauL]],Abs[Ya2'[tauR]],Abs[Ya3'[tauL]],Abs[Ya3'[tauR]],Abs[Ya4'[tauL]],Abs[Ya4'[tauR]],Abs[Yb1'[tauL]],Abs[Yb1'[tauR]],Abs[Yb2'[tauL]],Abs[Yb2'[tauR]],Abs[Yb3'[tauL]],Abs[Yb3'[tauR]],Abs[Yb4'[tauL]],Abs[Yb4'[tauR]]]<(2/5)

(C.4)

Clear[tauL,tauR,dx,T,Za,Zb,x,Ra,Rb,A1,A2,B1,B2];tauL=21/10;tauR=54/10;T=856/1000;dx=(10^(-2));
A1[x_,t_]:=Ua2d[x,t]-(1-x-2 Qanew[t]) Uaapp[x,t]-Qanew[t] Vaapp[x,t];
A2[x_,t_]:=Va2d[x,t]-(1+x-2 Qanew[t]) Vaapp[x,t]-Qanew[t] Uaapp[x,t];
B1[x_,t_]:=Ub2d[x,t]-(1-x-2 Qanew[t]) Ubapp[x,t]-Qanew[t] Vbapp[x,t];
B2[x_,t_]:=Vb2d[x,t]-(1+x-2 Qanew[t]) Vbapp[x,t]-Qanew[t] Ubapp[x,t];
Za=Integrate[ExpandAll[A1[x,t]^2+A2[x,t]^2],{t,0,T}];
Zb=Integrate[ExpandAll[B1[x,t]^2+B2[x,t]^2],{t,0,T}];
Ra=polyMax[Za,tauL,tauR,dx];
Rb=polyMax[Zb,tauL,tauR,dx];
k=(Sqrt[tauR+1]);
(1/2) (Sqrt[((2 k T+Sinh[2 k T])/k)])(Sqrt[Max[FU[Ra],FU[Rb]]])+((3T Sinh[k T])/(2 k)) (75/(10^5))+(1/5) dx<es

Proposition C.1: τ∈[1,1.2]

Clear[Uaapp,Vaapp,Ubapp,Vbapp,Uad,Vad,Ubd,Vbd,Ua2d,Va2d,Ub2d,Vb2d];Uaapp[τ_,t_]:=t+(112*t^2)/7071-(84069*t^3)/12941+(19306*t^4)/3625-(156439*t^5)/8122+(4529108*t^6)/18517-(12407469*t^7)/12391+(13802505*t^8)/6041-(19938272*t^9)/5805+(53183415*t^10)/14657-(42924858*t^11)/15571+(8404358*t^12)/5591-(3526473*t^13)/6148+(1591789*t^14)/11029-(278264*t^15)/13315+(3326*t^16)/3039+(2680*t^17)/49349+ (-(249*t^17)/5389+(4374*t^16)/6893-(15398*t^15)/3823+(219958*t^14)/14015-(212295*t^13)/5051+(688472*t^12)/8401-(1117303*t^11)/9315+(1588706*t^10)/11909 -(4482105*t^9)/39941+(501013*t^8)/7201-(359491*t^7)/12021+(30645*t^6)/3956-(5614*t^5)/6493+(1923*t^4)/10346-(1271*t^3)/7015+(3*t^2)/4790)*τ+((54*t^17)/7553-(1012*t^16)/11019+(6161*t^15)/11484-(39423*t^14)/20906+(260558*t^13)/58587-(121265*t^12)/16324+(57598*t^11)/6371-(64982*t^10)/7999+(68601*t^9)/12683-(17790*t^8)/6677+(7547*t^7)/7746-(2944*t^6)/10785+(2152*t^5)/35229-(33*t^4)/4823+(7*t^3)/12667-(t^2)/40643)*τ^2;
Vaapp[τ_,t_]:=(3681*t^17)/15061-(57636*t^16)/11473+(825829*t^15)/18764-(57112156*t^14)/255125+(11597999*t^13)/15502-(20590648*t^12)/11777+(25621273*t^11)/8685-(51191939*t^10)/14066+(39140407*t^9)/11979-(5210419*t^8)/2505+(13541181*t^7)/15350-(352048*t^6)/1631+(183459*t^5)/8386-(43947*t^4)/9515+(43703*t^3)/12583-(205*t^2)/15119+((271*t^17)/5454-(6838*t^16)/10085+(52723*t^15)/12435-(43681*t^14)/2714+(243056*t^13)/5871-(2308060*t^12)/30281+(771033*t^11)/7463-(949681*t^10)/9110+(1067194*t^9)/13673-(126229*t^8)/2964+(127476*t^7)/7783-(33624*t^6)/7837+(12196*t^5)/15311-(531*t^4)/5368+(89*t^3)/11587-(4*t^2)/12041)*τ+((-80*t^17)/14649+(945*t^16)/13466-(221639*t^15)/540245+(12380*t^14)/8571-(232353*t^13)/67993+(74064*t^12)/12901-(58461*t^11)/8284+(65299*t^10)/10126-(41500*t^9)/9413+(4898*t^8)/2173-(13581*t^7)/15874+(2569*t^6)/10804-(305*t^5)/6601+(56*t^4)/9319-(2*t^3)/4113+t^2/46045)*τ^2;
Ubapp[τ_,t_]:=(2463*t^17)/9715-(36251*t^16)/7047+(285916*t^15)/6391-(2011509*t^14)/8881+(8515714*t^13)/11285-(23298569*t^12)/13241+(119068063*t^11)/40167-(44459792*t^10)/12171+(21775652*t^9)/6645-(17028738*t^8)/8167+(8508863*t^7)/9624-(1251442*t^6)/5783+(792161*t^5)/36032-(54532*t^4)/11771+(34531*t^3)/9939-(156*t^2)/11465+((68*t^17)/6929-(745*t^16)/7468+(6177*t^15)/15824-(6535*t^14)/12444-(4174*t^13)/3315+(66375*t^12)/9109-(146303*t^11)/8824+(212006*t^10)/9193-(201460*t^9)/9491+(43291*t^8)/3347-(88537*t^7)/17825+(19981*t^6)/17933-(1831*t^5)/10383+(147*t^4)/8275-(35*t^3)/33337+(t^2)/32146)*τ+((-28*t^17)/9343+(365*t^16)/9599-(2944*t^15)/13441+(12991*t^14)/17140-(32497*t^13)/18494+(24623*t^12)/8543-(16321*t^11)/4738+(17317*t^10)/5685-(8489*t^9)/4231+(90568*t^8)/91895-(2930*t^7)/8137+(1761*t^6)/18083-(143*t^5)/7848+(162*t^4)/71441-(t^3)/5726+(t^2)/135052)*τ^2;
Vbapp[τ_,t_]:=(281*t^17)/6789+(29119*t^16)/23022-(134735*t^15)/6146+(1565941*t^14)/10578-(6744679*t^13)/11576+(9325931*t^12)/6140-(21688406*t^11)/7811+(11901372*t^10)/3263-(36827911*t^9)/10681+(28814971*t^8)/12573-(11522451*t^7)/11476+(609949*t^6)/2486-(47380*t^5)/2441+(53649*t^4)/10037-(70099*t^3)/10788+(243*t^2)/15278+t+(-(431*t^17)/12307+(1891*t^16)/4423-(17301*t^15)/7532+(79657*t^14)/11355-(75969*t^13)/5918+(128952*t^12)/10477+(15653*t^11)/11987-(186559*t^10)/8361+(394344*t^9)/11453-(395025*t^8)/13636+(260073*t^7)/18221-(29944*t^6)/8821+(271*t^5)/18282-(807*t^4)/10802+(1133*t^3)/6583-(2*t^2)/9289)*τ+((27*t^17)/6227-(1706*t^16)/30739+(4549*t^15)/14101-(14721*t^14)/13070+(52013*t^13)/19762-(52482*t^12)/12091+(30786*t^11)/5933-(64433*t^10)/14173+(24681*t^9)/8450-(10701*t^8)/7799+(2498*t^7)/5227-(973*t^6)/7295+(267*t^5)/7960-(22*t^4)/6887+(3*t^3)/11911-(t^2)/91156)*τ^2;
Uad[x_,t_]:=Derivative[0,1][Uaapp][x,t];
Vad[x_,t_]:=Derivative[0,1][Vaapp][x,t];
Ubd[x_,t_]:=Derivative[0,1][Ubapp][x,t];
Vbd[x_,t_]:=Derivative[0,1][Vbapp][x,t];
Ua2d[x_,t_]:=Derivative[0,2][Uaapp][x,t];
Va2d[x_,t_]:=Derivative[0,2][Vaapp][x,t];
Ub2d[x_,t_]:=Derivative[0,2][Ubapp][x,t];
Vb2d[x_,t_]:=Derivative[0,2][Vbapp][x,t];

(C.2)

Clear[pa,pb,x,es,du,tauL,tauR,Ya1,Ya2,Ya3,Ya4,Yb1,Yb2,Yb3,Yb4,T];
tauL=1;tauR=12/10;pa=2/10;pb=1/10;es=26/10^3;du=2*(10^(-3));T=16/10;
Ya1[x_]:=Uaapp[x,T];Ya2[x_]:= Vaapp[x,T]; Ya3[x_]:=Uad[x,T];Ya4[x_]:=Vad[x,T];
Yb1[x_]:=Ubapp[x,T]; Yb2[x_]:= Vbapp[x,T]; Yb3[x_]:= Ubd[x,T];Yb4[x_]:=Vbd[x,T];
Hepsilon[x_]:=H[Ya1[x],Ya2[x],Ya3[x],Ya4[x],Yb1[x],Yb2[x],Yb3[x],Yb4[x],pa,pb]-(HM[Abs[Ya1[x]]+es,Abs[Ya2[x]]+es,Abs[Ya3[x]]+es,Abs[Ya4[x]]+es,Abs[Yb1[x]]+es,Abs[Yb2[x]]+es,Abs[Yb3[x]]+es,Abs[Yb4[x]]+es,pa,pb]-HM[Abs[Ya1[x]],Abs[Ya2[x]],Abs[Ya3[x]],Abs[Ya4[x]],Abs[Yb1[x]],Abs[Yb2[x]],Abs[Yb3[x]],Abs[Yb4[x]],pa,pb]);
Ya2[x]-es
Ya4[x]-es
HepsilonExpanded=Expand[Hepsilon[x]];
xvals=Range[tauL,tauR,du];  
minValue=Min[HepsilonExpanded/. x->xvals];
minValue>0

(C.3)

Max[Abs[Ya1'[tauL]],Abs[Ya1'[tauR]],Abs[Ya2'[tauL]],Abs[Ya2'[tauR]],Abs[Ya3'[tauL]],Abs[Ya3'[tauR]],Abs[Ya4'[tauL]],Abs[Ya4'[tauR]],Abs[Yb1'[tauL]],Abs[Yb1'[tauR]],Abs[Yb2'[tauL]],Abs[Yb2'[tauR]],Abs[Yb3'[tauL]],Abs[Yb3'[tauR]],Abs[Yb4'[tauL]],Abs[Yb4'[tauR]]]<(2/5)

(C.4)

Clear[tauL,tauR,dx,T,Za,Zb,x,Ra,Rb,A1,A2,B1,B2];tauL=1;tauR=12/10;T=16/10;dx=2*(10^(-3));
A1[x_,t_]:=Ua2d[x,t]-(1-x-2 Qanew[t]) Uaapp[x,t]-Qanew[t] Vaapp[x,t];
A2[x_,t_]:=Va2d[x,t]-(1+x-2 Qanew[t]) Vaapp[x,t]-Qanew[t] Uaapp[x,t];
B1[x_,t_]:=Ub2d[x,t]-(1-x-2 Qanew[t]) Ubapp[x,t]-Qanew[t] Vbapp[x,t];
B2[x_,t_]:=Vb2d[x,t]-(1+x-2 Qanew[t]) Vbapp[x,t]-Qanew[t] Ubapp[x,t];
Za=Integrate[ExpandAll[A1[x,t]^2+A2[x,t]^2],{t,0,T}];
Zb=Integrate[ExpandAll[B1[x,t]^2+B2[x,t]^2],{t,0,T}];
Ra=polyMax[Za,tauL,tauR,dx];
Rb=polyMax[Zb,tauL,tauR,dx];
k=(Sqrt[tauR+1]);
(1/2) (Sqrt[((2 k T+Sinh[2 k T])/k)])(Sqrt[Max[FU[Ra],FU[Rb]]])+((3T Sinh[k T])/(2 k)) (75/(10^5))+(1/5) dx<es

Proposition C.1: τ∈[1.2,2.1]

(C.2)

Clear[pa,pb,x,es,du,tauL,tauR,Ya1,Ya2,Ya3,Ya4,Yb1,Yb2,Yb3,Yb4,T];
tauL=12/10;tauR=21/10;pa=1;pb=1/2;es=23/10^3;du=(10^(-2));T=11/10;
Ya1[x_]:=Uaapp[x,T];Ya2[x_]:= Vaapp[x,T]; Ya3[x_]:=Uad[x,T];Ya4[x_]:=Vad[x,T];
Yb1[x_]:=Ubapp[x,T]; Yb2[x_]:= Vbapp[x,T]; Yb3[x_]:= Ubd[x,T];Yb4[x_]:=Vbd[x,T];
Hepsilon[x_]:=H[Ya1[x],Ya2[x],Ya3[x],Ya4[x],Yb1[x],Yb2[x],Yb3[x],Yb4[x],pa,pb]-(HM[Abs[Ya1[x]]+es,Abs[Ya2[x]]+es,Abs[Ya3[x]]+es,Abs[Ya4[x]]+es,Abs[Yb1[x]]+es,Abs[Yb2[x]]+es,Abs[Yb3[x]]+es,Abs[Yb4[x]]+es,pa,pb]-HM[Abs[Ya1[x]],Abs[Ya2[x]],Abs[Ya3[x]],Abs[Ya4[x]],Abs[Yb1[x]],Abs[Yb2[x]],Abs[Yb3[x]],Abs[Yb4[x]],pa,pb]);
Ya2[x]-es
Ya4[x]-es
HepsilonExpanded=Expand[Hepsilon[x]];
xvals=Range[tauL,tauR,du];  
minValue=Min[HepsilonExpanded/. x->xvals];
minValue>0

(C.3)

Max[Abs[Ya1'[tauL]],Abs[Ya1'[tauR]],Abs[Ya2'[tauL]],Abs[Ya2'[tauR]],Abs[Ya3'[tauL]],Abs[Ya3'[tauR]],Abs[Ya4'[tauL]],Abs[Ya4'[tauR]],Abs[Yb1'[tauL]],Abs[Yb1'[tauR]],Abs[Yb2'[tauL]],Abs[Yb2'[tauR]],Abs[Yb3'[tauL]],Abs[Yb3'[tauR]],Abs[Yb4'[tauL]],Abs[Yb4'[tauR]]]<(2/5)

(C.4)

Clear[tauL,tauR,dx,T,Za,Zb,x,Ra,Rb,A1,A2,B1,B2];tauL=12/10;tauR=21/10;T=11/10;dx=(10^(-2));
A1[x_,t_]:=Ua2d[x,t]-(1-x-2 Qanew[t]) Uaapp[x,t]-Qanew[t] Vaapp[x,t];
A2[x_,t_]:=Va2d[x,t]-(1+x-2 Qanew[t]) Vaapp[x,t]-Qanew[t] Uaapp[x,t];
B1[x_,t_]:=Ub2d[x,t]-(1-x-2 Qanew[t]) Ubapp[x,t]-Qanew[t] Vbapp[x,t];
B2[x_,t_]:=Vb2d[x,t]-(1+x-2 Qanew[t]) Vbapp[x,t]-Qanew[t] Ubapp[x,t];
Za=Integrate[ExpandAll[A1[x,t]^2+A2[x,t]^2],{t,0,T}];
Zb=Integrate[ExpandAll[B1[x,t]^2+B2[x,t]^2],{t,0,T}];
Ra=polyMax[Za,tauL,tauR,dx];
Rb=polyMax[Zb,tauL,tauR,dx];
k=(Sqrt[tauR+1]);
(1/2) (Sqrt[((2 k T+Sinh[2 k T])/k)])(Sqrt[Max[FU[Ra],FU[Rb]]])+((3T Sinh[k T])/(2 k)) (75/(10^5))+(1/5) dx<es

Case l=1: Section 7

(7.15), please check toy example 1

(7.18)

polynomialMin[2+(867/100) x^2+3 x^3P2[x],(1/2),1,(1/(10^5))]>0

(7.21)

polynomialMin[2+3 x^3P2[x]+3 x^2,1,(17/10),(5/(10^5))]>0

(7.34)

Clear[y1,y];y1[t_]:=-((3 (t^8))/341)+((46 (t^7))/525)-((487 (t^6))/1404)+((1801 (t^5))/2640)-((2669 (t^4))/4312)+((81 (t^2))/185);y[t_]:=t^2 y1[t];
polynomialMin[ExpandAll[(y''[x]-2 y1[x]-x^2(W1[x]+75/10^6))/x^2],0,17/10,1/10^3]>0

(7.35)

polynomialMin[ExpandAll[(2/x^2+3 x P2[x])y1[x]+W1[x]-75/10^6],0,17/10,2/10^4]>0

l=1: Section 8

Check (SubMinus[I])(t)>0, t∈[0, 1.8]

gtilde[t_]:=29/5+(5324 t^2)/11721-(5242 t^3)/6305-(453401 t^4)/8690-(1372577 t^5)/5985+(11561100 t^6)/5101-(104060861 t^7)/8909+(269766735 t^8)/5476-(1847962994 t^9)/11735+(3127972553 t^10)/8468-(117464741599 t^11)/181890+(272712958583 t^12)/316809-(188840245805 t^13)/212143+(59891505057 t^14)/83009-(82501815384 t^15)/179359+(88378047540 t^16)/384383-(13934342915 t^17)/156279+(22540646527 t^18)/857154-(4889665718 t^19)/857587+(1193343423 t^20)/1392527-(61031641 t^21)/765161+(2655007 t^22)/766661;
Iminus[t_]:=t^2(gtilde[t]-t/1600);
Iplus[t_]:=t^2(gtilde[t]+t/1600);
Itilde[t_]:=t^2gtilde[t];
polynomialMin[gtilde[x]-x/1600,0,18/10,6*10^(-4)]>0

(8.3)

Clear[p,x];P2plus[t_]:=(W1[t]-75 10^(-6))(W1'[t]+42 10^(-5));p=Simplify[ExpandAll[(Iplus''[x]*x^2*Iminus[x]-(2+3x^3P2plus[x])*Iplus[x]*Iminus[x]-x^4(W1[x]+75/10^6)*Iplus[x])/x^5]];
polynomialMin[p,0,12/10,6*10^(-5)]>0
Clear[p,x];p=Simplify[ExpandAll[(-Iminus''[x]*x^2*Iplus[x]+(2+3x^3P2[x])*Iplus[x]*Iminus[x]+x^4(W1[x]-75/10^6)*Iminus[x])/x^5]];
polynomialMin[p,0,12/10,6*10^(-5)]>0

(8.4)

Max[Abs[Itilde'[6/5]-Iplus'[6/5]/Iplus[6/5]*Iminus[6/5]],
Abs[Itilde'[6/5]-Iminus'[6/5]/Iminus[6/5]*Iplus[6/5]]]<62/10^4

(8.5)

(* Check 1st inequality in (8.5) *)
Fminus[t_]:=Itilde''[t]-2gtilde[t]-3t*P2plus[t]*Itilde[t]-t^2(W1[t]+75/10^6)
Fplus[t_]:=Itilde''[t]-2gtilde[t]-3t*P2[t]*Itilde[t]-t^2(W1[t]-75/10^6);
polynomialMin[Fminus[x],12/10,18/10,6*10^(-5)]>0   
{polyMax[Fminus[x],12/10,18/10,15*10^(-5)]<39/10^4,polyMax[Fplus[x],12/10,18/10,5*10^(-5)]<39/10^4}

(* Check 2nd inequality in (8.5) *)
Clear[p];p=7/5*x^2-2-3x^3P2plus[x];polynomialMin[p,12/10,18/10,10^(-4)]>0
Clear[p];p=7/5*x^2+2+3x^3P2[x];  polynomialMin[p,12/10,18/10,4*10^(-5)]>0

(8.7)

Clear[t,y];DSolve[{y''[t]==7/5y[t]+39/10^4 ,y[6/5]==(12/10)^3/1600,y'[6/5]==62/10^4},y[t],t]

Clear[yz];yz[t_]:=(1/700000)(E^(-((6 (Sqrt[(7/5)]))/5)-(Sqrt[(7/5)]) t)) (1353 (E^((12 (Sqrt[(7/5)]))/5))-310 (Sqrt[35]) (E^((12 (Sqrt[(7/5)]))/5))+1353 (E^(2 (Sqrt[(7/5)]) t))+310 (Sqrt[35]) (E^(2 (Sqrt[(7/5)]) t))-1950 (E^(((6 (Sqrt[(7/5)]))/5)+(Sqrt[(7/5)]) t)));
{yz[9/5]<62/10^4,yz'[9/5]<114/10^4}

(8.8)

polynomialMin[-2-3x^3P2plus[x],12/10,16/10,10^(-4)]>0
Integrate[-2/t^2-3t P2[t],{t,12/10,16/10}]<244/10^3
polynomialMin[3/20x^2+2+3x^3P2[x],16/10,18/10,5 10^(-5)]>0
polynomialMin[3/20x^2-2-3x^3P2plus[x],16/10,18/10, 8 10^(-5)]>0
Integrate[Fplus[t],{t,12/10,18/10}]<165/10^5
62/10^4+(244/10^3+2/10*15/100)*62/10^4+165/10^5<96/10^4

(8.9)

Integrate[t^2(Itilde[t]-62/10^4)(W1[t]-75/10^6),{t,0,18/10}]>107/100

(SubPlus[J])((9/5))≥I((9/5))≥(SubMinus[J])((9/5)),  (Subscript[J, +]^′)((9/5))>I'((9/5))≥(Subscript[J, -]^′)((9/5)).

Clear[Jp,Jm];Jp[x_]:=-(46355/4182)+((162617 x)/2916)-((215987 (x^2))/2017)+((428192 (x^3))/3543)-((38323 (x^4))/412)+((104356 (x^5))/2011)-((37198 (x^6))/1725)+((20181 (x^7))/2999)-((5962 (x^8))/3809)+((923 (x^9))/3491)-((17 (x^10))/556)+((11 (x^11))/5279)-((x^12)/27017)-((x^13)/189311)+((x^14)/3302419);
Jm[x_]:=-(12413/1105)+((171747 x)/3038)-((174823 (x^2))/1612)+((47397503 (x^3))/388000)-((307187 (x^4))/3277)+((540785 (x^5))/10386)-((28489 (x^6))/1325)+((20281 (x^7))/3051)-((5023 (x^8))/3296)+((1218 (x^9))/4849)-((187 (x^10))/6760)+((4 (x^11))/2441)+((x^12)/121108)-((x^13)/124156)+((x^14)/2629395);
{Jp[(9/5)]>Iplus[(9/5)]>Iminus[(9/5)]>Jm[(9/5)],Jp'[(9/5)]>Iplus'[(9/5)]>Iminus'[(9/5)]>Jm'[(9/5)]}

(8.11) and note that  (Subscript[J, m])(t)<(Subscript[J, p])(t), then -(Subscript[J, p])(t)<-(Subscript[J, m])(t)

{(83/100)<-Jp[(35/10)]<-Jm[(35/10)]<(1051/1000),(16/100)<-Jp'[(35/10)]<-Jm'[(35/10)]<(57/100)}

(8.13)

Clear[x,Bt1,Bt2,pt1,pt2,pt3,pt4];Bt1=(W1'[x]+5/10^5)(W1[x]-6/10^6);Bt2=(W1'[x]-5/10^5)(W1[x]+6/10^6);
pt1=x^2Jp''[x]-2Jp[x]-3x^3Bt1*Jp[x]-x^4(W1[x]+6/10^6);
pt2=x^2Jp''[x]-2Jp[x]-3x^3Bt2*Jp[x]-x^4(W1[x]+6/10^6);
pt3=x^2Jm''[x]-2Jm[x]-3x^3Bt1*Jm[x]-x^4(W1[x]-6/10^6);
pt4=x^2Jm''[x]-2Jm[x]-3x^3Bt2*Jm[x]-x^4(W1[x]-6/10^6);
{polynomialMin[pt1,18/10,25/10,7*10^(-5)]>0,polynomialMin[pt2,18/10,25/10,7*10^(-5)]>0,
polynomialMin[-pt3,18/10,25/10,10^(-4)]>0,polynomialMin[-pt4,18/10,25/10,10^(-4)]>0}

Check (Subscript[J, ±])<0 on [2.5, 3.5]

{polynomialMin[-Jp[x],25/10,35/10,7*10^(-3)]>0,polynomialMin[-Jm[x],25/10,35/10,7*10^(-3)]>0}

(8.14) and (8.15)

Clear[x,Ct1,Ct2,pt1,pt2];Ct1=(-W2'[x]+5/10^5)(W2[x]+6/10^6);
Ct2=(-W2'[x]-5/10^5)(W2[x]-6/10^6);
pt1=x^2Jp''[x]-2Jp[x]+3x^3Ct1*Jp[x]-x^4(W2[x]+6/10^6);
pt2=x^2Jm''[x]-2Jm[x]+3x^3Ct2*Jm[x]-x^4(W2[x]-6/10^6);
{polynomialMin[pt1,25/10,35/10,2*10^(-4)]>0,polynomialMin[-pt2,25/10,35/10,2*10^(-4)]>0}

(8.16)

polyMax[Jm[x],9/5,7/2,10^(-4)]<(106/100)

Integrate[Jm[t]t^2 W1[t],{t,(9/5),(5/2)}]+Integrate[Jm[t]t^2W2[t],{t,(5/2),(7/2)}]-(6/(10^6))*(106/100) Integrate[t^2,{t,(9/5),(7/2)}]>-(401/1000)

(SubMinus[H])(t) in Lemma 8.3

Clear[t];DSolve[{Hm''[t]==18525/10^4 1/t^2 Hm[t]- 28/10 t Exp[-t],Hm[7/2]==83/100,Hm'[7/2]==16/100},Hm[t],t]

(8.19)

10788 (2^(19/20)) (7^(1/20)) -548800   Gamma[(21/20),(7/2)]>0

(SubPlus[H])(t) in Lemma 8.3

Clear[t];DSolve[{Hp''[t]==2/t^2 Hp[t]- 27/10 t Exp[-t],Hp[7/2]==1051/1000,Hp'[7/2]==57/100},Hp[t],t]

Integrate[ExpandAll[(((E^(-(7/2)-t)) (-1587600 (E^(7/2))+28212975 (E^t)+36701 (E^((7/2)+t))-1587600 (E^(7/2)) t-793800 (E^(7/2)) (t^2)-264600 (E^t) (t^3)+24368 (E^((7/2)+t)) (t^3)))/(294000 t))t 19/7 Exp[-t]],{t,7/2,Infinity}]<(65/100)

Proposition 8.4

(107/100)-(401/1000)+(65/100)>0