(* Verification of inequality Log[2,E]/6<1/4 for the proof of (2.3). *)
N[1/4-Log[2,E]/6,{∞,10}]

(* Verification of inequality phi_k'[1/10]<0. *)
N[-((Log[2,10π])/2) Log[9]+(40/9),{∞,10}]

(* Verification of inequality (2.10) for 10≤k≤99. *)
Clear[k,p,t];
p[k_]=Log[2,Binomial[2k,k]];
ph[k_,t_]=((2k-p[k])t+1/2)Log[t]+((2k-p[k])(1-t)+1/2)Log[1-t]+Log[2π k]/2;
Table[N[ph[k,1/k],{∞,10}],{k,10,99}]

(* Count negative elements in the list. *)
Count[%,u_/;u<0]

(* Verification needed in the proof of inequality (2.10) for k≥100. *)
N[((Log[2π])/2)-(601/2000),{∞,10}]

(* Verification needed in the proof of inequality (2.11). *)
N[(3/(10^(41/40)))-(1/4),{∞,10}]

(* Verification needed in the proof of inequality (2.11). *)
N[((9Log[2,3])/10)-((Log[2,10])/2)+(1/4),{∞,10}]

(* Verification of inequality (2.13) for j given by (2.14) and for 2≤k≤99. *)
Clear[jk,k,p,t];
p[k_]=Log[2,Binomial[2k,k]];
w[k_]=9^(1-p[k]/k);
jk[k_]=Floor[((w[k] (k+1))/(1+w[k]))];
Table[N[Binomial[k,jk[k]] w[k]^jk[k] (9/10)^(p[k]-k),{∞,10}],{k,2,59}]

(* Count elements that exceed 1. *)
Count[%,u_/;u>1]

(* Verification needed in the proof of inequality (2.13) for k≥50. *)
N[1/7-9^(-9/10),{∞,10}]

(* Verification needed in the proof of inequality (2.13) for k≥50. *)
N[(1/(Sqrt[2(1-41/500)*(41/500)])) (50π)^((((51/400-1) Log[2,9])/2)+((Log[2,10])/2)-(1/2)),{∞,10}]

(* Verification of the differential identity needed in the proof of Lemma 5. *)
Clear[p,a,b,c,ff,k,x];
ff[x_]=(1-x)^(p[k](k-j)/k) x^(p[k] j/k);
a[x_]=(1-x)^2 x^2 ((1-x)^(p[k]/k)-x^(p[k]/k))^2;
b[x_]=(1-x) x ((1-x)^(p[k]/k)-x^(p[k]/k))((1-x)^(p[k]/k) (1+2(p[k]-1)x)+x^(p[k]/k) (1+2(p[k]-1)(1-x)));
c[x_]=(1-x)^(2 p[k]/k) x (1+(p[k]-1)x)+x^(2 p[k]/k) (1-x) (1+(p[k]-1)(1-x))-(1-x)^(p[k]/k) x^(p[k]/k) (p[k]-2(p[k]-1)(1-x)x);
Simplify[a[x] ff''[x]+b[x] ff'[x]+p[k] c[x] ff[x],Assumptions->{x>0,x<1}]

(* Verification of the differential identity needed in the proof of Lemma 5. *)
Simplify[a[x] ff''[x]+b[x] ff'[x]+p[k] c[x] ff[x]-((p[k]^2)/(k^2))((((1-x))^((p[k])/k))-(x^((p[k])/k)))(((1-x))^(((k-j) p[k])/k)) (x^((j p[k])/k)) ((j^2) (((1-x))^((p[k])/k))-(k-j)^2 (x^((p[k])/k))) ,Assumptions->{x>0,x<1}]

(* Change of variables (from x to y) used in the proof of Lemma 6. *)
Simplify[-c[(1/(y+1))],Assumptions->{y>1}]

(* Change of variables (from x to y) used in the proof of Lemma 6. *)
Simplify[((-c[(1/(y+1))])/((y^((p[k])/k))(((1+y))^(-((2 (k+p[k]))/k)))))-((y^((p[k])/k))-1) (p[k] (y^(2-((p[k])/k)))+(y^(1-((p[k])/k)))-y-p[k]),Assumptions->{y>1}]

Table[N[((2k-Log[2,Pi k]/2)/(7k/4))],{k,11,50}]

(* Verification of inequality (2.21) for 2≤k≤10. *)
Clear[k,p];
p[k_]=Log[2,Binomial[2k,k]];
Table[N[((9^(2-p[k]/k))/(1+(80/(9p[k]+1)))),{∞,10}],{k,2,10}]

(* Verification of inequality needed in the proof of (2.21) for k≥11. *)
N[Log[3] Log[2,11π]-(320/63),{∞,10}]

(* Graph of f_k for k=20 *)
Clear[k,p,x];
p[k_]=Log[2,Binomial[2k,k]];
k=20;
f[x_]=(∑_(j=0)^k)Binomial[k,j]^2 (1-x)^(p[k](k-j)/k) x^(p[k] j/k);
Plot[f[x],{x,0,1},PlotRange->{{-0.1,1.1},{-0.1,1.1}},Ticks->{{0,1/4,1/2,3/4,1},{0,1/4,1/2,3/4,1}},LabelStyle->{FontFamily->"Times New Roman",FontSize->28},PlotStyle->{RGBColor[0,0,0],Thickness[0.004]},AxesStyle->{{RGBColor[0,0,0],Thickness[0.003]},{RGBColor[0,0,0],Thickness[0.003]}},ImageSize->500]

(* Graph of c_k for k=20 *)
Clear[k,p,x];
p[k_]=Log[2,Binomial[2k,k]];
k=20;
c[x_]=(1-x)^(2 p[k]/k) x (1+(p[k]-1)x)+x^(2 p[k]/k) (1-x) (1+(p[k]-1)(1-x))-(1-x)^(p[k]/k) x^(p[k]/k) (p[k]-2(p[k]-1)(1-x)x);
Plot[c[x],{x,0,1/2},LabelStyle->{FontFamily->"Times New Roman",FontSize->28},PlotStyle->{RGBColor[0,0,0],Thickness[0.004]},Ticks->{{1/10,1/5,3/10,2/5,1/2},{-0.02,-0.04,-0.06,-0.08}},AxesStyle->{{RGBColor[0,0,0],Thickness[0.003]},{RGBColor[0,0,0],Thickness[0.003]}},ImageSize->500]