|\^/|     Maple 10 (IBM INTEL LINUX)
._|\|   |/|_. Copyright (c) Maplesoft, a division of Waterloo Maple Inc. 2005
 \  MAPLE  /  All rights reserved. Maple is a trademark of
 <____ ____>  Waterloo Maple Inc.
      |       Type ? for help.
> 
> 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);
                                       0

> expand(F(4,k,1));
                                    k           k 2
                             5 (1/2)    3 ((1/2) )
                             -------- - -----------
                                2            4

> for i to 5 do
>    evalb(H(5,i,10,20)< 2*(2/3)^i)
> od;
                                      true

                                      true

                                      true

                                      true

                                      true

> expand(G(5,k,0));
                               k           k          k
                        9 (3/5)    7 (7/15)    3 (2/3)
                        -------- + --------- + --------
                           5           5          k

> evalf(G(5,5,0)*(2/3)^(-5));
                                  1.898180000

> 
# Proof of Lemma 10
> for i to 31 do
>    evalb(F(6,i,3)< (4/5)*(1/2)^(i-1))
> od;
                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

                                      true

> G(6,k,0);
                                                                     k
                  (k + 1)          (k + 1)          (k + 1)   3 (1/2)
          3 (7/12)        + 3 (4/9)        + 3 (1/3)        + --------
                                                                 k

> f(1/2,k+1,0)+f(1/3,k+1,0)+f(1/6+1/5-1/30,k+1,0)+op(%)[4];
                                                            k
                          (k + 1)          (k + 1)   3 (1/2)
                   3 (1/2)        + 6 (1/3)        + --------
                                                        k

> evalb(subs(k=31,%)*(1/2)^(-30)<(4/5));
                                      true

> 
# Proof of Lemma 11
> evalb(H30(1200,1,30,6000)< 3/5 - 0.00356);
                                      true

> quit