######################################################## f := proc(x,s,t) option remember; local xs; xs := x^s; 1-(1-3*xs*x^t)*mul(1-xs*x^i,i=0..t-1) end: F := proc(y,k,t) option remember; local T,i,p; T := 0; for i to infinity do p := ithprime(i); if p>=y then break fi; T := T+f(ceil(y/p)/y,k+1,t) od; return T end: F30 := proc(y,k,t) option remember; local T,i,p; if modp(y,30)>0 then error fi; T := 1-(1-f(1/2,k+1,t))*(1-f(1/3,k+1,t))*(1-f(1/5,k+1,t)); for i from 4 to infinity do p := ithprime(i); if p>=y then break fi; T := T+f(ceil(y/p)/y,k+1,t) od; return T end: G := proc(L,k,t) option remember; local T, i, p, x; T := 0; for i to infinity do p := ithprime(i); if p>=L then break fi; x := 1/L+1/p-1/(p*L); T := T + f(x,k+1,t) od; T+(3/k)*(1/(L/2-1))^k end: G30 := proc(L,k,t) option remember; local T, i, p, x; if modp(L,30)>0 then error fi; T := 1-(1-f(1/2,k+1,t))*(1-f(1/3,k+1,t))*(1-f(1/5,k+1,t)); for i from 4 to infinity do p := ithprime(i); if p>=L then break fi; x := 1/L+1/p-1/(p*L); T := T + f(x,k+1,t) od; T+(3/k)*(1/(L/2-1))^k end: H := proc(L,k,t,B) max(seq(F(L+i,k,t),i=0..B-1),G(L+B,k,t)) end: H30 := proc(L,k,t,B) if modp(L,30)>0 then error fi; if modp(B,30)>0 then error fi; max(seq(F30(L+i*30,k,t),i=0..B/30-1),G30(L+B,k,t)) end: ######################################################## # Proof of Lemma 9 simplify(F(3,k,0)-2*(2/3)^k,symbolic); expand(F(4,k,1)); for i to 5 do evalb(H(5,i,10,20)< 2*(2/3)^i) od; expand(G(5,k,0)); evalf(G(5,5,0)*(2/3)^(-5)); # Proof of Lemma 10 for i to 31 do evalb(F(6,i,3)< (4/5)*(1/2)^(i-1)) od; G(6,k,0); f(1/2,k+1,0)+f(1/3,k+1,0)+f(1/6+1/5-1/30,k+1,0)+op(%)[4]; evalb(subs(k=31,%)*(1/2)^(-30)<(4/5)); # Proof of Lemma 11 evalb(H30(1200,1,30,6000)< 3/5 - 0.00356);