asympt_2.miz



    begin

    theorem :: ASYMPT_2:1

    for m,k be Nat st 1 <= m holds 1 <= (m to_power k)

    proof

      let m,n be Nat;

      per cases ;

        suppose n = 0 ;

        hence thesis by POWER: 24;

      end;

        suppose

         A1: n <> 0 ;

        assume 1 <= m;

        then 1 < m or 1 = m by XXREAL_0: 1;

        hence thesis by A1, POWER: 26, POWER: 35;

      end;

    end;

    

     LMC31X: for m,n be Nat st 2 <= m holds n < (m to_power n) by NEWTON: 86;

    theorem :: ASYMPT_2:2

    

     LMC31B: for m,n be Nat holds m <= (m to_power (n + 1))

    proof

      let m,n be Nat;

      per cases by NAT_1: 14;

        suppose m = 0 ;

        hence thesis;

      end;

        suppose

         A1: 1 <= m;

        1 <= (n + 1) by NAT_1: 11;

        then (m to_power 1) <= (m to_power (n + 1)) by A1, PRE_FF: 8;

        hence thesis by NEWTON: 5;

      end;

    end;

    theorem :: ASYMPT_2:3

    for m,n be Nat st 2 <= m holds (n + 1) <= (m to_power n) by NEWTON: 85;

    theorem :: ASYMPT_2:4

    

     LMC31D: for k be Nat holds (2 * k) <= (2 to_power k)

    proof

      defpred P[ Nat] means (2 * $1) <= (2 to_power $1);

      

       P1: P[ 0 ];

      

       P2: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A1: P[n];

        per cases ;

          suppose n = 0 ;

          hence (2 * (n + 1)) <= (2 to_power (n + 1)) by POWER: 25;

        end;

          suppose n <> 0 ;

          then (n - 1) in NAT by INT_1: 5, NAT_1: 14;

          then

          reconsider m = (n - 1) as Nat;

          

           A3: 2 <= (2 to_power (m + 1)) by LMC31B;

          

           A2: (2 to_power (n + 1)) = ((2 to_power n) * (2 to_power 1)) by POWER: 27

          .= ((2 to_power n) * 2) by POWER: 25

          .= ((2 to_power n) + (2 to_power n));

          ((2 * n) + 2) <= ((2 to_power n) + (2 to_power n)) by A3, XREAL_1: 7, A1;

          hence (2 * (n + 1)) <= (2 to_power (n + 1)) by A2;

        end;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( P1, P2);

      hence thesis;

    end;

    theorem :: ASYMPT_2:5

    

     LMC31E: for k,n be Nat st k <= n holds (n + k) <= (2 to_power n)

    proof

      let k be Nat;

      defpred P[ Nat] means (($1 + k) + k) <= (2 to_power ($1 + k));

      (2 * k) <= (2 to_power k) by LMC31D;

      then

       P1: P[ 0 ];

      

       P2: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A1: P[n];

        

         A2: (2 to_power (k + (n + 1))) = (2 to_power ((k + n) + 1))

        .= ((2 to_power (k + n)) * (2 to_power 1)) by POWER: 27

        .= ((2 to_power (k + n)) * 2) by POWER: 25

        .= ((2 to_power (k + n)) + (2 to_power (k + n)));

        1 <= (2 to_power (k + n))

        proof

          per cases ;

            suppose (k + n) = 0 ;

            hence 1 <= (2 to_power (k + n)) by POWER: 24;

          end;

            suppose (k + n) <> 0 ;

            hence 1 <= (2 to_power (k + n)) by POWER: 35;

          end;

        end;

        then (((n + k) + k) + 1) <= ((2 to_power (k + n)) + (2 to_power (k + n))) by XREAL_1: 7, A1;

        hence (((n + 1) + k) + k) <= (2 to_power ((n + 1) + k)) by A2;

      end;

      

       X1: for n be Nat holds P[n] from NAT_1:sch 2( P1, P2);

      let n be Nat;

      assume k <= n;

      then (n - k) in NAT by INT_1: 5;

      then

      reconsider m = (n - k) as Nat;

      ((m + k) + k) <= (2 to_power (m + k)) by X1;

      hence (n + k) <= (2 to_power n);

    end;

    theorem :: ASYMPT_2:6

    

     LMC31G: for k,m be Nat st ((2 * k) + 1) <= m holds (2 to_power k) <= ((2 to_power m) / m)

    proof

      let k,m be Nat;

      assume

       A1: ((2 * k) + 1) <= m;

      (2 * k) <= ((2 * k) + 1) by NAT_1: 11;

      then (k + k) <= m by A1, XXREAL_0: 2;

      then

       X1: ((k + k) - k) <= (m - k) by XREAL_1: 9;

      then (m - k) in NAT by INT_1: 3;

      then

      reconsider n = (m - k) as Nat;

      

       A2: (n + k) <= (2 to_power n) by LMC31E, X1;

      ((2 to_power (n + k)) / (2 to_power n)) <= ((2 to_power (n + k)) / (n + k)) by A1, A2, XREAL_1: 118;

      then (2 to_power ((n + k) - n)) <= ((2 to_power (n + k)) / (n + k)) by POWER: 29;

      hence (2 to_power k) <= ((2 to_power m) / m);

    end;

    

     Lm5: ( dom ( id ( [#] REAL ))) = ( [#] REAL ) & (for x be Real holds (( id ( [#] REAL )) . x) = x) & for x be Real holds ( id ( [#] REAL )) is_differentiable_in x & ( diff (( id ( [#] REAL )),x)) = 1

    proof

      set g = ( id ( [#] REAL ));

      thus ( dom g) = ( [#] REAL );

      thus for d be Real holds (g . d) = d by FUNCT_1: 17, XREAL_0:def 1;

      

       A6: for d be Real st d in REAL holds (g . d) = ((1 * d) + 0 ) by FUNCT_1: 17;

      then

       A7: g is_differentiable_on ( dom g) by FDIFF_1: 23;

      for x be Real holds g is_differentiable_in x & ( diff (g,x)) = 1

      proof

        let dd be Real;

        reconsider d = dd as Element of REAL by XREAL_0:def 1;

        g is_differentiable_in d by A7;

        hence g is_differentiable_in dd;

        

        thus ( diff (g,dd)) = ((g `| ( dom g)) . d) by A7, FDIFF_1:def 7

        .= 1 by A6, FDIFF_1: 23;

      end;

      hence thesis;

    end;

    theorem :: ASYMPT_2:7

    

     CPOWER57: for a,b,c be Real st 1 < a & 0 < b & b <= c holds ( log (a,b)) <= ( log (a,c))

    proof

      let a,b,c be Real;

      assume

       AS: 1 < a & 0 < b & b <= c;

      now

        per cases by AS, XXREAL_0: 1;

          case b < c;

          hence ( log (a,b)) < ( log (a,c)) by POWER: 57, AS;

        end;

          case b = c;

          hence ( log (a,b)) = ( log (a,c));

        end;

      end;

      hence thesis;

    end;

    

     LEMC01: for x,n,a be Nat st 0 < a & a <= x holds (a to_power n) <= (x to_power n) by PREPOWER: 9;

    theorem :: ASYMPT_2:8

    

     LC5aa: for n be Nat, a be Real st 1 < a holds (a to_power n) < (a to_power (n + 1))

    proof

      let n be Nat, a be Real;

      assume

       AS: 1 < a;

      

       LP3: (a to_power (n + 1)) = ((a to_power n) * (a to_power 1)) by FIB_NUM2: 5

      .= ((a to_power n) * a) by POWER: 25;

      (a to_power n) > 0 by POWER: 34, AS;

      then (1 * (a to_power n)) < ((a to_power n) * a) by XREAL_1: 68, AS;

      hence thesis by LP3;

    end;

    theorem :: ASYMPT_2:9

    

     LC5a: for n be Nat, a be Real st 1 <= a holds (a to_power n) <= (a to_power (n + 1))

    proof

      let n be Nat, a be Real;

      assume

       AS: 1 <= a;

      

       LP3: (a to_power (n + 1)) = ((a to_power n) * (a to_power 1)) by FIB_NUM2: 5

      .= ((a to_power n) * a) by POWER: 25;

      (a to_power n) > 0 by POWER: 34, AS;

      then (1 * (a to_power n)) <= ((a to_power n) * a) by XREAL_1: 64, AS;

      hence thesis by LP3;

    end;

    theorem :: ASYMPT_2:10

    

     Lm6: ex g be PartFunc of REAL , REAL st ( dom g) = ( right_open_halfline 0 ) & (for x be Real st x in ( right_open_halfline 0 ) holds (g . x) = ( log (2,x))) & g is_differentiable_on ( right_open_halfline 0 ) & for x be Real st x in ( right_open_halfline 0 ) holds g is_differentiable_in x & ( diff (g,x)) = (( log (2, number_e )) / x) & 0 < ( diff (g,x))

    proof

      set g = (( log (2, number_e )) (#) ln );

      take g;

      

      thus

       A3: ( dom g) = ( dom ln ) by VALUED_1:def 5

      .= ( right_open_halfline 0 ) by TAYLOR_1:def 2;

      

       E1: number_e > 1 by XXREAL_0: 2, TAYLOR_1: 11;

      thus for d be Real st d in ( right_open_halfline 0 ) holds (g . d) = ( log (2,d))

      proof

        let d be Real;

        assume

         A51: d in ( right_open_halfline 0 );

        then

        reconsider d0 = d as Element of ( right_open_halfline 0 );

        d in { y where y be Real : 0 < y } by XXREAL_1: 230, A51;

        then

         E3: ex y be Real st d = y & 0 < y;

        

        thus (g . d) = (( log (2, number_e )) * ( ln . d)) by A3, A51, VALUED_1:def 5

        .= (( log (2, number_e )) * ( log ( number_e ,d0))) by TAYLOR_1:def 2

        .= ( log (2,d)) by E1, E3, POWER: 56;

      end;

      thus g is_differentiable_on ( right_open_halfline 0 ) by FDIFF_1: 20, A3, TAYLOR_1: 18;

      thus for x be Real st x in ( right_open_halfline 0 ) holds g is_differentiable_in x & ( diff (g,x)) = (( log (2, number_e )) / x) & 0 < ( diff (g,x))

      proof

        let x be Real;

        assume

         A1: x in ( right_open_halfline 0 );

        

         A2: ln is_differentiable_in x by A1, TAYLOR_1: 18;

        hence g is_differentiable_in x by FDIFF_1: 15;

        

         A3: ( diff ( ln ,x)) = (1 / x) by A1, TAYLOR_1: 18;

        

         A4: ( diff (g,x)) = (( log (2, number_e )) * ( diff ( ln ,x))) by FDIFF_1: 15, A2;

        

        thus ( diff (g,x)) = ((1 * ( log (2, number_e ))) / x) by XCMPLX_1: 74, A4, A3

        .= (( log (2, number_e )) / x);

        

         A5: 0 < ( diff ( ln ,x)) by A1, TAYLOR_1: 18;

        ( log (2,2)) < ( log (2, number_e )) by POWER: 57, TAYLOR_1: 11;

        then 0 < ( log (2, number_e )) by POWER: 52;

        hence 0 < ( diff (g,x)) by A4, A5;

      end;

    end;

    theorem :: ASYMPT_2:11

    

     LMC31H2: ex f be PartFunc of REAL , REAL st ( right_open_halfline number_e ) = ( dom f) & (for x be Real st x in ( dom f) holds (f . x) = (x / ( log (2,x)))) & f is_differentiable_on ( right_open_halfline number_e ) & (for x0 be Real st x0 in ( right_open_halfline number_e ) holds 0 <= ( diff (f,x0))) & f is non-decreasing

    proof

      consider g be PartFunc of REAL , REAL such that

       A2: ( dom g) = ( right_open_halfline 0 ) and

       A3: (for x be Real st x in ( right_open_halfline 0 ) holds (g . x) = ( log (2,x))) and

       A4: g is_differentiable_on ( right_open_halfline 0 ) and

       A5: for x be Real st x in ( right_open_halfline 0 ) holds g is_differentiable_in x & ( diff (g,x)) = (( log (2, number_e )) / x) & 0 < ( diff (g,x)) by Lm6;

      set g0 = (g | ( right_open_halfline number_e ));

      

       AA6: for x be object st x in ( right_open_halfline number_e ) holds x in ( right_open_halfline 0 )

      proof

        let x be object;

        assume x in ( right_open_halfline number_e );

        then x in { y where y be Real : number_e < y } by XXREAL_1: 230;

        then

        consider y be Real such that

         AA2: x = y & number_e < y;

        x in { z where z be Real : 0 < z } by TAYLOR_1: 11, AA2;

        hence thesis by XXREAL_1: 230;

      end;

      then

       A6: ( right_open_halfline number_e ) c= ( right_open_halfline 0 );

      then

       A7: ( dom g0) = ( right_open_halfline number_e ) by RELAT_1: 62, A2;

      set f = (( id ( [#] REAL )) / g0);

      

       G0: (g0 " { 0 }) = {}

      proof

        assume (g0 " { 0 }) <> {} ;

        then

        consider x be object such that

         P01: x in (g0 " { 0 }) by XBOOLE_0:def 1;

        

         P02: x in ( dom g0) & (g0 . x) in { 0 } by P01, FUNCT_1:def 7;

        

         P04: (g0 . x) = 0 by TARSKI:def 1, P02;

        reconsider x0 = x as Real by P01;

        x0 in { y where y be Real : number_e < y } by XXREAL_1: 230, P02, A7;

        then ex y be Real st x = y & number_e < y;

        then

         E5: 2 < x0 by XXREAL_0: 2, TAYLOR_1: 11;

        

         F3: (g0 . x) = (g . x) by FUNCT_1: 49, P02, A7

        .= ( log (2,x0)) by A3, AA6, P02, A7;

        ( log (2,2)) <= ( log (2,x0)) by E5, PRE_FF: 10;

        hence contradiction by POWER: 52, P04, F3;

      end;

      take f;

      

      thus

       P1: ( dom f) = (( dom ( id ( [#] REAL ))) /\ (( dom g0) \ (g0 " { 0 }))) by RFUNCT_1:def 1

      .= ( right_open_halfline number_e ) by XBOOLE_1: 28, A7, G0;

      thus for x be Real st x in ( dom f) holds (f . x) = (x / ( log (2,x)))

      proof

        let x be Real;

        assume

         F1: x in ( dom f);

        

        thus (f . x) = ((( id ( [#] REAL )) . x) * ((g0 . x) " )) by F1, RFUNCT_1:def 1

        .= (x * ((g0 . x) " )) by Lm5

        .= (x * ((g . x) " )) by P1, F1, FUNCT_1: 49

        .= (x * (( log (2,x)) " )) by A3, P1, AA6, F1

        .= (x * (1 / ( log (2,x)))) by XCMPLX_1: 215

        .= ((1 * x) / ( log (2,x))) by XCMPLX_1: 74

        .= (x / ( log (2,x)));

      end;

      

       P3: g is_differentiable_on ( right_open_halfline number_e ) by FDIFF_1: 26, A4, A6;

      then

       XP: g0 is_differentiable_on ( right_open_halfline number_e ) & (g `| ( right_open_halfline number_e )) = (g0 `| ( right_open_halfline number_e )) by FDIFF_2: 16;

      

       F12: for x be Real st x in ( right_open_halfline number_e ) holds f is_differentiable_in x & ( diff (f,x)) = ((( log (2,x)) - ( log (2, number_e ))) / (( log (2,x)) ^2 ))

      proof

        let x be Real;

        assume

         F1: x in ( right_open_halfline number_e );

        then

         FA: x in ( right_open_halfline 0 ) by AA6;

        

         FB: ( diff (g,x)) = ((g `| ( right_open_halfline number_e )) . x) by P3, F1, FDIFF_1:def 7

        .= ( diff (g0,x)) by XP, F1, FDIFF_1:def 7;

        x in { y where y be Real : number_e < y } by XXREAL_1: 230, F1;

        then

         EE5: ex y be Real st x = y & number_e < y;

        then

         E5: 2 < x by XXREAL_0: 2, TAYLOR_1: 11;

        

         F3: (g0 . x) = (g . x) by F1, FUNCT_1: 49

        .= ( log (2,x)) by F1, AA6, A3;

        ( log (2,2)) <= ( log (2,x)) by E5, PRE_FF: 10;

        then

         F2: 0 < (g0 . x) by F3, POWER: 52;

        

         F3: ( id ( [#] REAL )) is_differentiable_in x by Lm5;

        

         F6: g0 is_differentiable_in x by P3, F1;

        ( diff (f,x)) = (((( diff (( id ( [#] REAL )),x)) * (g0 . x)) - (( diff (g0,x)) * (( id ( [#] REAL )) . x))) / ((g0 . x) ^2 )) by FDIFF_2: 14, F2, F3, F6

        .= (((1 * (g0 . x)) - (( diff (g0,x)) * (( id ( [#] REAL )) . x))) / ((g0 . x) ^2 )) by Lm5

        .= (((1 * (g0 . x)) - (( diff (g0,x)) * x)) / ((g0 . x) ^2 )) by Lm5

        .= (((1 * (g . x)) - (( diff (g,x)) * x)) / ((g0 . x) ^2 )) by F1, FUNCT_1: 49, FB

        .= (((1 * (g . x)) - (( diff (g,x)) * x)) / ((g . x) ^2 )) by F1, FUNCT_1: 49

        .= (((1 * ( log (2,x))) - (( diff (g,x)) * x)) / ((g . x) ^2 )) by A3, F1, AA6

        .= (((1 * ( log (2,x))) - (( diff (g,x)) * x)) / (( log (2,x)) ^2 )) by A3, AA6, F1

        .= (((1 * ( log (2,x))) - ((( log (2, number_e )) / x) * x)) / (( log (2,x)) ^2 )) by A5, FA

        .= ((( log (2,x)) - ( log (2, number_e ))) / (( log (2,x)) ^2 )) by XCMPLX_1: 87, EE5, TAYLOR_1: 11;

        hence thesis by FDIFF_2: 14, F2, F3, F6;

      end;

      hence

       P3: f is_differentiable_on ( right_open_halfline number_e ) by P1;

      thus for x be Real st x in ( right_open_halfline number_e ) holds 0 <= ( diff (f,x))

      proof

        let x be Real;

        assume

         F1: x in ( right_open_halfline number_e );

        then

         P41: ( diff (f,x)) = ((( log (2,x)) - ( log (2, number_e ))) / (( log (2,x)) ^2 )) by F12;

        x in { y where y be Real : number_e < y } by XXREAL_1: 230, F1;

        then ex y be Real st x = y & number_e < y;

        then ( log (2, number_e )) < ( log (2,x)) by POWER: 57, TAYLOR_1: 11;

        then 0 < (( log (2,x)) - ( log (2, number_e ))) by XREAL_1: 50;

        hence thesis by P41;

      end;

      hence thesis by P1, P3, FDIFF_2: 35;

    end;

    theorem :: ASYMPT_2:12

    

     LMC31H1: for x,y be Real st number_e < x & x <= y holds (x / ( log (2,x))) <= (y / ( log (2,y)))

    proof

      let x,y be Real;

      assume

       AS: number_e < x & x <= y;

      consider f be PartFunc of REAL , REAL such that

       A11: ( right_open_halfline number_e ) = ( dom f) and

       A12: (for x be Real st x in ( dom f) holds (f . x) = (x / ( log (2,x)))) and f is_differentiable_on ( right_open_halfline number_e ) and (for x0 be Real st x0 in ( right_open_halfline number_e ) holds 0 <= ( diff (f,x0))) and

       A15: f is non-decreasing by LMC31H2;

       number_e < y by AS, XXREAL_0: 2;

      then x in { g where g be Real : number_e < g } & y in { g where g be Real : number_e < g } by AS;

      then

       A3: x in ( dom f) & y in ( dom f) by A11, XXREAL_1: 230;

      then

       A4: (f . x) <= (f . y) by AS, A15, VALUED_0:def 15;

      (f . x) = (x / ( log (2,x))) by A12, A3;

      hence thesis by A4, A12, A3;

    end;

    theorem :: ASYMPT_2:13

    

     LMC31H: for k be Nat st number_e < k holds ex N be Nat st for n be Nat st N <= n holds (2 to_power k) <= (n / ( log (2,n)))

    proof

      let k be Nat;

      assume

       K1: number_e < k;

      set N = (2 to_power ((2 * k) + 1));

      (k * 1) <= (2 * k) by XREAL_1: 64;

      then

       X1: (k + 0 ) < ((2 * k) + 1) by XREAL_1: 8;

      ((2 * k) + 1) <= (2 to_power ((2 * k) + 1)) by LMC31X;

      then k < (2 to_power ((2 * k) + 1)) by X1, XXREAL_0: 2;

      then

       DD: number_e < N by K1, XXREAL_0: 2;

      take N;

      let n be Nat;

      assume N <= n;

      then

       B0: (N / ( log (2,N))) <= (n / ( log (2,n))) by LMC31H1, DD;

      

       X0: 0 < (2 to_power ((2 * k) + 1)) by POWER: 34;

      then

       X1: ((2 * k) + 1) = ( log (2,N)) by POWER:def 3;

      reconsider m = ( log (2,N)) as Nat by X0, POWER:def 3;

      

       X3: (2 to_power k) <= ((2 to_power m) / m) by LMC31G, X1;

      (2 to_power m) = N by POWER:def 3, X0;

      hence thesis by B0, XXREAL_0: 2, X3;

    end;

    

     LMC31: for r be Real holds ex N be Element of NAT st for n be Nat st N <= n holds r < (n / ( log (2,n)))

    proof

      let r0 be Real;

      ex r be Real st 0 < r & r0 <= r

      proof

        per cases ;

          suppose

           A1: 0 < r0;

          take r0;

          thus 0 < r0 & r0 <= r0 by A1;

        end;

          suppose

           A2: not 0 < r0;

          take 1;

          thus 0 < 1 & r0 <= 1 by A2;

        end;

      end;

      then

      consider r be Real such that

       AS: 0 < r & r0 <= r;

      set a0 = ( max (( log (2,r)), number_e ));

      

       A01: ( log (2,r)) <= a0 & number_e <= a0 by XXREAL_0: 25;

      set k = ( [/a0\] + 1);

      a0 < k by INT_1: 32;

      then k in NAT by INT_1: 3, TAYLOR_1: 11, A01;

      then

      reconsider k as Nat;

      

       A0: ( log (2,r)) < k & number_e < k by A01, XXREAL_0: 2, INT_1: 32;

      (2 to_power ( log (2,r))) < (2 to_power k) by A0, POWER: 39;

      then

       A1: r < (2 to_power k) by AS, POWER:def 3;

      consider N be Nat such that

       A2: for n be Nat st N <= n holds (2 to_power k) <= (n / ( log (2,n))) by LMC31H, A0;

      reconsider N as Element of NAT by ORDINAL1:def 12;

      take N;

      let n be Nat;

      assume N <= n;

      then (2 to_power k) <= (n / ( log (2,n))) by A2;

      then r < (n / ( log (2,n))) by A1, XXREAL_0: 2;

      hence r0 < (n / ( log (2,n))) by AS, XXREAL_0: 2;

    end;

    

     LMC31HC: ex N be Element of NAT st for n be Nat st N <= n holds 4 < (n / ( log (2,n)))

    proof

      reconsider k = ( [/ number_e \] + 1) as Integer;

      

       LLC2: number_e <= [/ number_e \] by INT_1:def 7;

      then

       LC2: number_e < k by XREAL_1: 145;

      then

       LC3: 2 < k by XXREAL_0: 2, TAYLOR_1: 11;

      k in NAT by INT_1: 3, LLC2, TAYLOR_1: 11;

      then

      reconsider k as Nat;

      consider N be Nat such that

       LC4: for n be Nat st N <= n holds (2 to_power k) <= (n / ( log (2,n))) by LMC31H, LC2;

      reconsider N as Element of NAT by ORDINAL1:def 12;

      take N;

      let n be Nat;

      assume N <= n;

      then

       LC5: (2 to_power k) <= (n / ( log (2,n))) by LC4;

      4 < (2 to_power k) by POWER: 60, POWER: 39, LC3;

      hence thesis by LC5, XXREAL_0: 2;

    end;

    theorem :: ASYMPT_2:14

    for x be Nat st 1 < x holds ex N be Nat st for n be Nat st N <= n holds 4 < (n / ( log (x,n)))

    proof

      let x be Nat;

      assume

       AS: 1 < x;

      ( log (2,x)) >= ( log (2,2)) by PRE_FF: 10, AS, NAT_1: 23;

      then

       AS2: 1 <= ( log (2,x)) by POWER: 52;

      consider N be Nat such that

       LL1: for n be Nat st N <= n holds 4 < (n / ( log (2,n))) by LMC31HC;

      take N;

      let n be Nat;

      assume N <= n;

      then

       CL1: 4 < (n / ( log (2,n))) by LL1;

      then 0 <> n;

      then ( log (2,n)) = (( log (2,x)) * ( log (x,n))) by POWER: 56, AS;

      then (4 * ( log (2,x))) < ((n / (( log (x,n)) * ( log (2,x)))) * ( log (2,x))) by AS2, XREAL_1: 68, CL1;

      then (4 * ( log (2,x))) < (((n / ( log (x,n))) * (1 / ( log (2,x)))) * ( log (2,x))) by XCMPLX_1: 103;

      then (4 * ( log (2,x))) < ((n / ( log (x,n))) * (( log (2,x)) * (1 / ( log (2,x)))));

      then

       TT11: (4 * ( log (2,x))) < ((n / ( log (x,n))) * 1) by XCMPLX_1: 106, AS2;

      (4 * 1) <= (4 * ( log (2,x))) by XREAL_1: 64, AS2;

      hence thesis by TT11, XXREAL_0: 2;

    end;

    theorem :: ASYMPT_2:15

    for x be Nat st 1 < x holds ex N,c be Nat st for n be Nat st N <= n holds (n to_power x) <= (c * (x to_power n))

    proof

      let x be Nat;

      assume

       AS1: 1 < x;

      consider N0 be Element of NAT such that

       P1: for n be Nat st N0 <= n holds (x / ( log (2,x))) < (n / ( log (2,n))) by LMC31;

      set N = (N0 + 2);

      reconsider N as Nat;

      reconsider c = 1 as Element of NAT ;

      take N, c;

      let n be Nat;

      assume

       AS2: N <= n;

      N0 <= N by NAT_1: 12;

      then N0 <= n by XXREAL_0: 2, AS2;

      then

       E1: (x / ( log (2,x))) < (n / ( log (2,n))) by P1;

      (1 + 1) <= x by AS1, NAT_1: 13;

      then ( log (2,2)) <= ( log (2,x)) by PRE_FF: 10;

      then

       P2: 0 < ( log (2,x)) by POWER: 52;

      2 <= N by NAT_1: 11;

      then 2 <= n by XXREAL_0: 2, AS2;

      then ( log (2,2)) <= ( log (2,n)) by PRE_FF: 10;

      then

       P3: 0 < ( log (2,n)) by POWER: 52;

      then ((x / ( log (2,x))) * ( log (2,n))) < ((n / ( log (2,n))) * ( log (2,n))) by XREAL_1: 68, E1;

      then ((x / ( log (2,x))) * ( log (2,n))) < n by P3, XCMPLX_1: 87;

      then ((( log (2,n)) * (x / ( log (2,x)))) * ( log (2,x))) < (n * ( log (2,x))) by XREAL_1: 68, P2;

      then (( log (2,n)) * ((x / ( log (2,x))) * ( log (2,x)))) < (n * ( log (2,x)));

      then

       PP4: (( log (2,n)) * x) < (n * ( log (2,x))) by P2, XCMPLX_1: 87;

      

       P5: (2 to_power (( log (2,n)) * x)) = ((2 to_power ( log (2,n))) to_power x) by POWER: 33

      .= (n to_power x) by POWER:def 3, AS2;

      (2 to_power (n * ( log (2,x)))) = ((2 to_power ( log (2,x))) to_power n) by POWER: 33

      .= (x to_power n) by AS1, POWER:def 3;

      hence thesis by PP4, P5, POWER: 39;

    end;

    theorem :: ASYMPT_2:16

    

     N2POWINPOLY: for x be Nat st 1 < x holds not ex N,c be Nat st for n be Nat st N <= n holds (2 to_power n) <= (c * (n to_power x))

    proof

      let x be Nat;

      assume

       AS1: 1 < x;

      assume

       ASC: ex N,c be Nat st for n be Nat st N <= n holds (2 to_power n) <= (c * (n to_power x));

      consider N be Nat such that

       ASC1: ex c be Nat st for n be Nat st N <= n holds (2 to_power n) <= (c * (n to_power x)) by ASC;

      N <> 0

      proof

        assume N = 0 ;

        then

        consider c be Nat such that

         LNT: for n be Nat st 0 <= n holds (2 to_power n) <= (c * (n to_power x)) by ASC1;

        (2 to_power 0 ) <= (c * ( 0 to_power x)) by LNT;

        then (2 to_power 0 ) <= (c * 0 ) by POWER: 42, AS1;

        hence contradiction by POWER: 24;

      end;

      then

       LPNN2: 0 < N;

      consider c be Nat such that

       ASC2: for n be Nat st N <= n holds (2 to_power n) <= (c * (n to_power x)) by ASC1;

      ex n be Element of NAT st N <= n & 0 < (n - (x / 4))

      proof

        now

          per cases ;

            case

             AC1: (x / 4) < N;

            reconsider n = (N + 1) as Element of NAT ;

            take n;

            thus N <= n by INT_1: 6;

            then (x / 4) < n by AC1, XXREAL_0: 2;

            hence 0 < (n - (x / 4)) by XREAL_1: 50;

          end;

            case

             AC2: N <= (x / 4);

            reconsider n = ( [/(x / 4)\] + 1) as Integer;

            

             AC33: (x / 4) <= [/(x / 4)\] by INT_1:def 7;

            then

             AC3: ((x / 4) + 0 ) < ( [/(x / 4)\] + 1) by XREAL_1: 8;

            reconsider n as Element of NAT by INT_1: 3, AC33;

            take n;

            thus 0 < (n - (x / 4)) by AC3, XREAL_1: 50;

            thus N <= n by AC3, AC2, XXREAL_0: 2;

          end;

        end;

        hence thesis;

      end;

      then

      consider n be Element of NAT such that

       ASC3: N <= n & 0 < (n - (x / 4));

      

       XC1: (2 to_power n) <= (c * (n to_power x)) by ASC2, ASC3;

      

       ZZ1: 0 < n & 1 < x by AS1, ASC3;

      

       TEZ1: 0 < c

      proof

        assume not 0 < c;

        then (2 to_power n) <= ( 0 * (n to_power x)) by XC1;

        hence contradiction by POWER: 34;

      end;

      

       ASC22: for k be Nat st 1 <= k holds (2 to_power (k * n)) <= (c * ((k * n) to_power x))

      proof

        let k be Nat;

        assume 1 <= k;

        then (1 * N) <= (k * n) by ASC3, XREAL_1: 66;

        hence thesis by ASC2;

      end;

      

       HCL1: for k be Nat st 1 <= k holds (k * n) <= ((( log (2,c)) + (x * ( log (2,k)))) + (x * ( log (2,n))))

      proof

        let k be Nat;

        assume

         ASK: 1 <= k;

        then

         L1: (2 to_power (k * n)) <= (c * ((k * n) to_power x)) by ASC22;

        

         L3: 0 < ((k * n) to_power x) by POWER: 34, LPNN2, ASC3, ASK;

         0 < (2 to_power (k * n)) by POWER: 34;

        then ( log (2,(2 to_power (k * n)))) <= ( log (2,(c * ((k * n) to_power x)))) by L1, CPOWER57;

        then ((k * n) * ( log (2,2))) <= ( log (2,(c * ((k * n) to_power x)))) by POWER: 55;

        then ((k * n) * 1) <= ( log (2,(c * ((k * n) to_power x)))) by POWER: 52;

        then (k * n) <= (( log (2,c)) + ( log (2,((k * n) to_power x)))) by POWER: 53, TEZ1, L3;

        then (k * n) <= (( log (2,c)) + (x * ( log (2,(k * n))))) by POWER: 55, LPNN2, ASC3, ASK;

        then (k * n) <= (( log (2,c)) + (x * (( log (2,k)) + ( log (2,n))))) by POWER: 53, ASK, ZZ1;

        hence (k * n) <= ((( log (2,c)) + (x * ( log (2,k)))) + (x * ( log (2,n))));

      end;

      consider Z be Element of NAT such that

       HCL2: for k be Nat st Z <= k holds 4 < (k / ( log (2,k))) by LMC31HC;

      

       HEXK: ex k be Nat st Z <= k & ((( log (2,c)) + (x * ( log (2,n)))) / (n - (x / 4))) <= k

      proof

        now

          per cases ;

            case

             AC1: ((( log (2,c)) + (x * ( log (2,n)))) / (n - (x / 4))) < Z;

            reconsider k = (Z + 1) as Element of NAT ;

            take k;

            thus Z <= k by INT_1: 6;

            hence ((( log (2,c)) + (x * ( log (2,n)))) / (n - (x / 4))) < k by AC1, XXREAL_0: 2;

          end;

            case

             AC2: Z <= ((( log (2,c)) + (x * ( log (2,n)))) / (n - (x / 4)));

            reconsider k = ( [/((( log (2,c)) + (x * ( log (2,n)))) / (n - (x / 4)))\] + 1) as Integer;

            

             AC3P: ((( log (2,c)) + (x * ( log (2,n)))) / (n - (x / 4))) <= [/((( log (2,c)) + (x * ( log (2,n)))) / (n - (x / 4)))\] by INT_1:def 7;

            then

             AC3: (((( log (2,c)) + (x * ( log (2,n)))) / (n - (x / 4))) + 0 ) <= ( [/((( log (2,c)) + (x * ( log (2,n)))) / (n - (x / 4)))\] + 1) by XREAL_1: 8;

            reconsider k as Element of NAT by AC3P, INT_1: 3, AC2;

            take k;

            thus ((( log (2,c)) + (x * ( log (2,n)))) / (n - (x / 4))) <= k by AC3;

            thus Z <= k by AC3, AC2, XXREAL_0: 2;

          end;

        end;

        hence thesis;

      end;

      ex k be Nat st Z <= k & ((( log (2,c)) + (x * ( log (2,n)))) / (n - (x / 4))) <= k & 1 < k

      proof

        consider k be Nat such that

         HEXK2: Z <= k & ((( log (2,c)) + (x * ( log (2,n)))) / (n - (x / 4))) <= k by HEXK;

        reconsider a = (k + 2) as Nat;

        take a;

        

         CC1: ( 0 + 2) <= (k + 2) by XREAL_1: 6;

        k <= a by NAT_1: 11;

        hence thesis by CC1, XXREAL_0: 2, HEXK2;

      end;

      then

      consider k be Nat such that

       HCL3: Z <= k & 1 < k & ((( log (2,c)) + (x * ( log (2,n)))) / (n - (x / 4))) <= k;

      

       FF0: (((( log (2,c)) + (x * ( log (2,n)))) / (n - (x / 4))) * (n - (x / 4))) <= (k * (n - (x / 4))) by HCL3, ASC3, XREAL_1: 64;

      

       HCL4: 4 < (k / ( log (2,k))) by HCL2, HCL3;

      

       HCL7: (k * n) <= ((( log (2,c)) + (x * ( log (2,k)))) + (x * ( log (2,n)))) by HCL1, HCL3;

      

       HCL8: 0 < ( log (2,k)) by ENTROPY1: 4, HCL3;

      then (4 * ( log (2,k))) < ((k / ( log (2,k))) * ( log (2,k))) by HCL4, XREAL_1: 68;

      then (4 * ( log (2,k))) < ((k * ( log (2,k))) / ( log (2,k))) by XCMPLX_1: 74;

      then (4 * ( log (2,k))) < (k * (( log (2,k)) / ( log (2,k)))) by XCMPLX_1: 74;

      then (4 * ( log (2,k))) < (k * 1) by XCMPLX_1: 60, HCL8;

      then ((( log (2,k)) * 4) * x) < (k * x) by XREAL_1: 68, AS1;

      then (((( log (2,k)) * x) * 4) / 4) < ((k * x) / 4) by XREAL_1: 74;

      then ((k * n) - ((k * x) / 4)) < (((( log (2,c)) + (x * ( log (2,k)))) + (x * ( log (2,n)))) - (x * ( log (2,k)))) by HCL7, XREAL_1: 15;

      hence contradiction by FF0, XCMPLX_1: 87, ASC3;

    end;

    

     FROMASYMPT1t11: for a,b be Nat st a < b holds ( seq_n^ a) in ( Big_Oh ( seq_n^ b))

    proof

      let a,b be Nat;

      assume

       AS: a < b;

      set g = ( seq_n^ b);

      set f = ( seq_n^ a);

       LL11:

      now

        let n be Element of NAT ;

        assume

         A2: n >= 2;

        then

         A3: n > 1 by XXREAL_0: 2;

        

         A4: (( seq_n^ a) . n) = (n to_power a) by A2, ASYMPT_1:def 3;

        (( seq_n^ b) . n) = (n to_power b) by A2, ASYMPT_1:def 3;

        hence (( seq_n^ a) . n) <= (1 * (( seq_n^ b) . n)) by AS, A3, A4, POWER: 39;

        thus (( seq_n^ a) . n) >= 0 by A4;

      end;

      reconsider f as Element of ( Funcs ( NAT , REAL )) by FUNCT_2: 8;

      reconsider g as eventually-nonnegative Real_Sequence;

      f in ( Big_Oh g) by LL11;

      hence thesis;

    end;

    theorem :: ASYMPT_2:17

    for a,b be Nat st a <= b holds ( seq_n^ a) in ( Big_Oh ( seq_n^ b))

    proof

      let a,b be Nat;

      assume

       AS: a <= b;

      per cases by AS, XXREAL_0: 1;

        suppose a = b;

        hence thesis by ASYMPT_0: 10;

      end;

        suppose a < b;

        hence thesis by FROMASYMPT1t11;

      end;

    end;

    theorem :: ASYMPT_2:18

    for x be Nat st 1 < x holds not ex N,c be Nat st for n be Nat st N <= n holds (x to_power n) <= (c * (n to_power x))

    proof

      let x be Nat;

      assume

       AS: 1 < x;

      assume

       CNT: ex N,c be Nat st for n be Nat st N <= n holds (x to_power n) <= (c * (n to_power x));

      ex N,c be Nat st for n be Nat st N <= n holds (2 to_power n) <= (c * (n to_power x))

      proof

        consider N,c be Nat such that

         CNT2: for n be Nat st N <= n holds (x to_power n) <= (c * (n to_power x)) by CNT;

        take N, c;

        let n be Nat;

        assume N <= n;

        then

         LCX1: (x to_power n) <= (c * (n to_power x)) by CNT2;

        (1 + 1) <= x by AS, INT_1: 7;

        then (2 to_power n) <= (x to_power n) by LEMC01;

        hence thesis by LCX1, XXREAL_0: 2;

      end;

      hence contradiction by AS, N2POWINPOLY;

    end;

    theorem :: ASYMPT_2:19

    

     LC4: for a be non negative Real, n be Nat st 1 <= n holds 0 < (( seq_n^ a) . n)

    proof

      let a be non negative Real, n be Nat;

      

       AA: n in NAT by ORDINAL1:def 12;

      assume

       AS: 1 <= n;

      then (( seq_n^ a) . n) = (n to_power a) by AA, ASYMPT_1:def 3;

      hence thesis by AS, POWER: 34;

    end;

    begin

    definition

      let p be Real_Sequence;

      :: ASYMPT_2:def1

      attr p is polynomially-bounded means ex k be Nat st p in ( Big_Oh ( seq_n^ k));

    end

    theorem :: ASYMPT_2:20

    for f be Real_Sequence st f is non polynomially-bounded holds for k be Nat holds not f in ( Big_Oh ( seq_n^ k));

    theorem :: ASYMPT_2:21

    for f be Real_Sequence st for k be Nat holds not f in ( Big_Oh ( seq_n^ k)) holds f is non polynomially-bounded;

    theorem :: ASYMPT_2:22

    for a be positive Real holds ( seq_a^ (a,1, 0 )) is positive

    proof

      let a be positive Real;

      now

        let n be Nat;

        (( seq_a^ (a,1, 0 )) . n) = (a to_power ((1 * n) + 0 )) by ASYMPT_1:def 1

        .= (a to_power n);

        hence 0 < (( seq_a^ (a,1, 0 )) . n) by POWER: 34;

      end;

      hence thesis;

    end;

    theorem :: ASYMPT_2:23

    for a be Real st 1 <= a holds ( seq_a^ (a,1, 0 )) is non-decreasing

    proof

      let a be Real;

      assume

       AS: 1 <= a;

      for n be Nat holds (( seq_a^ (a,1, 0 )) . n) <= (( seq_a^ (a,1, 0 )) . (n + 1))

      proof

        let n be Nat;

        

         L2: (( seq_a^ (a,1, 0 )) . n) = (a to_power ((1 * n) + 0 )) by ASYMPT_1:def 1

        .= (a to_power n);

        (( seq_a^ (a,1, 0 )) . (n + 1)) = (a to_power ((1 * (n + 1)) + 0 )) by ASYMPT_1:def 1

        .= (a to_power (n + 1));

        hence thesis by L2, LC5a, AS;

      end;

      hence thesis by SEQM_3:def 8;

    end;

    theorem :: ASYMPT_2:24

    for a be Real st 1 < a holds ( seq_a^ (a,1, 0 )) is increasing

    proof

      let a be Real;

      assume

       AS: 1 < a;

      

       C1: for n be Element of NAT holds (( seq_a^ (a,1, 0 )) . n) < (( seq_a^ (a,1, 0 )) . (n + 1))

      proof

        let n be Element of NAT ;

        

         L2: (( seq_a^ (a,1, 0 )) . n) = (a to_power ((1 * n) + 0 )) by ASYMPT_1:def 1

        .= (a to_power n);

        (( seq_a^ (a,1, 0 )) . (n + 1)) = (a to_power ((1 * (n + 1)) + 0 )) by ASYMPT_1:def 1

        .= (a to_power (n + 1));

        hence thesis by L2, LC5aa, AS;

      end;

      reconsider S = ( seq_a^ (a,1, 0 )) as Real_Sequence;

      for n be Nat holds (S . n) < (S . (n + 1))

      proof

        let n be Nat;

        reconsider n as Element of NAT by ORDINAL1:def 12;

        (( seq_a^ (a,1, 0 )) . n) < (( seq_a^ (a,1, 0 )) . (n + 1)) by C1;

        hence thesis;

      end;

      hence thesis by SEQM_3:def 6;

    end;

    theorem :: ASYMPT_2:25

    for a be Nat st 1 < a holds ( seq_a^ (a,1, 0 )) is non polynomially-bounded

    proof

      let a be Nat;

      assume

       AS1: 1 < a;

      assume ( seq_a^ (a,1, 0 )) is polynomially-bounded;

      then

      consider k be Nat such that

       CL1: ( seq_a^ (a,1, 0 )) in ( Big_Oh ( seq_n^ k));

      reconsider f = ( seq_n^ k) as eventually-positive Real_Sequence;

      reconsider t = ( seq_a^ (a,1, 0 )) as eventually-nonnegative Real_Sequence by AS1;

      t in ( Big_Oh f) & for n be Element of NAT st 1 <= n holds 0 < (f . n) by LC4, CL1;

      then

      consider c be Real such that

       LL1: c > 0 & for n be Element of NAT st n >= 1 holds (( seq_a^ (a,1, 0 )) . n) <= (c * (( seq_n^ k) . n)) by ASYMPT_0: 8;

      

       TLCPP: for n be Nat st n >= 1 holds (2 to_power n) <= (c * (n to_power k))

      proof

        let n be Nat;

        

         ZZ: n in NAT by ORDINAL1:def 12;

        assume

         AT1: n >= 1;

        then (( seq_a^ (a,1, 0 )) . n) <= (c * (( seq_n^ k) . n)) by ZZ, LL1;

        then (a to_power ((1 * n) + 0 )) <= (c * (( seq_n^ k) . n)) by ASYMPT_1:def 1;

        then

         TZ1: (a to_power n) <= (c * (n to_power k)) by ASYMPT_1:def 3, AT1;

        (1 + 1) <= a by AS1, INT_1: 7;

        then (2 to_power n) <= (a to_power n) by LEMC01;

        hence thesis by XXREAL_0: 2, TZ1;

      end;

      

       TLCPP2: ex N,b be Nat st for n be Nat st N <= n holds (2 to_power n) <= (b * (n to_power k))

      proof

        consider N be Nat such that

         TLCPP3: for n be Nat st N <= n holds (2 to_power n) <= (c * (n to_power k)) by TLCPP;

        set b = [/c\];

        

         TLCPP4: c <= b by INT_1:def 7;

        then

        reconsider b as Element of NAT by INT_1: 3, LL1;

        take N, b;

        for n be Nat st N <= n holds (2 to_power n) <= (b * (n to_power k))

        proof

          let n be Nat;

          assume N <= n;

          then

           TLCPP5: (2 to_power n) <= (c * (n to_power k)) by TLCPP3;

          (c * (n to_power k)) <= (b * (n to_power k)) by XREAL_1: 64, TLCPP4;

          hence thesis by TLCPP5, XXREAL_0: 2;

        end;

        hence thesis;

      end;

      per cases ;

        suppose 1 < k;

        hence contradiction by TLCPP2, N2POWINPOLY;

      end;

        suppose k <= 1;

        then

         TLCPPAA: k < 2 by XXREAL_0: 2;

        ex N,b be Nat st for n be Nat st N <= n holds (2 to_power n) <= (b * (n to_power 2))

        proof

          consider N,b be Nat such that

           TLCPPA3: for n be Nat st N <= n holds (2 to_power n) <= (b * (n to_power k)) by TLCPP2;

          reconsider M = (N + 2) as Element of NAT ;

          

           TLCPPAA1: N <= M by NAT_1: 11;

          take M, b;

          let n be Nat;

          assume

           TLCPPAS: M <= n;

          then N <= n by XXREAL_0: 2, TLCPPAA1;

          then

           TLCPPA4: (2 to_power n) <= (b * (n to_power k)) by TLCPPA3;

          2 <= (N + 2) by NAT_1: 11;

          then (1 + 1) <= n by TLCPPAS, XXREAL_0: 2;

          then 1 < n by NAT_1: 13;

          then (n to_power k) <= (n to_power 2) by POWER: 39, TLCPPAA;

          then (b * (n to_power k)) <= (b * (n to_power 2)) by XREAL_1: 64;

          hence thesis by TLCPPA4, XXREAL_0: 2;

        end;

        hence contradiction by N2POWINPOLY;

      end;

    end;

    begin

    theorem :: ASYMPT_2:26

    

     LMXFIN1: for x be XFinSequence of REAL , y be Real_Sequence holds (x (#) y) is finite Sequence of REAL & ( dom (x (#) y)) = ( dom x) & for i be object st i in ( dom x) holds ((x (#) y) . i) = ((x . i) * (y . i))

    proof

      let x be XFinSequence of REAL , y be Real_Sequence;

      

       P1: ( dom y) = NAT by FUNCT_2:def 1;

      

       P2: ( dom (x (#) y)) = (( dom x) /\ ( dom y)) by VALUED_1:def 4

      .= ( dom x) by XBOOLE_1: 28, P1;

      then (x (#) y) is Sequence of ( rng (x (#) y)) by ORDINAL1: 31;

      hence thesis by P2, VALUED_1:def 4, ORDINAL1: 32;

    end;

    definition

      let x be XFinSequence of REAL , y be Real_Sequence;

      :: original: (#)

      redefine

      func x (#) y -> XFinSequence of REAL ;

      correctness by LMXFIN1;

    end

    theorem :: ASYMPT_2:27

    

     LMXFIN2: for d be XFinSequence of REAL holds for x,i be Nat st i in ( dom d) holds ((d (#) ( seq_a^ (x,1, 0 ))) . i) = ((d . i) * (x to_power i))

    proof

      let d be XFinSequence of REAL ;

      let x,i be Nat;

      assume i in ( dom d);

      

      hence ((d (#) ( seq_a^ (x,1, 0 ))) . i) = ((d . i) * (( seq_a^ (x,1, 0 )) . i)) by LMXFIN1

      .= ((d . i) * (x to_power ((1 * i) + 0 ))) by ASYMPT_1:def 1

      .= ((d . i) * (x to_power i));

    end;

    definition

      let c be XFinSequence of REAL ;

      :: ASYMPT_2:def2

      func seq_p (c) -> Real_Sequence means

      : defseqp: for x be Nat holds (it . x) = ( Sum (c (#) ( seq_a^ (x,1, 0 ))));

      existence

      proof

        deffunc F( Nat) = ( Sum (c (#) ( seq_a^ ($1,1, 0 ))));

        consider h be Real_Sequence such that

         A1: for x be Nat holds (h . x) = F(x) from SEQ_1:sch 1;

        take h;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let s1,s2 be Real_Sequence such that

         A1: for x be Nat holds (s1 . x) = ( Sum (c (#) ( seq_a^ (x,1, 0 )))) and

         A2: for x be Nat holds (s2 . x) = ( Sum (c (#) ( seq_a^ (x,1, 0 ))));

        now

          let x be Element of NAT ;

          

          thus (s1 . x) = ( Sum (c (#) ( seq_a^ (x,1, 0 )))) by A1

          .= (s2 . x) by A2;

        end;

        hence s1 = s2;

      end;

    end

    

     LMXFIN3: for d be XFinSequence of REAL , k be Nat st ( len d) = (k + 1) holds ex a be Real, d1 be XFinSequence of REAL st ( len d1) = k & d1 = (d | k) & a = (d . k) & d = (d1 ^ <%a%>)

    proof

      let d be XFinSequence of REAL , k be Nat;

      assume

       AS: ( len d) = (k + 1);

      set d1 = (d | k);

      set a = (d . k);

      reconsider d1 as XFinSequence of REAL ;

      reconsider a as Real;

      take a, d1;

      thus thesis by AFINSQ_1: 56, AS, AFINSQ_1: 54, NAT_1: 11;

    end;

    theorem :: ASYMPT_2:28

    

     LMXFIN4: for d be XFinSequence of REAL , k be Nat st ( len d) = (k + 1) holds ex a be Real, d1 be XFinSequence of REAL , y be Real_Sequence st ( len d1) = k & d1 = (d | k) & a = (d . k) & d = (d1 ^ <%a%>) & ( seq_p d) = (( seq_p d1) + y) & for i be Nat holds (y . i) = (a * (i to_power k))

    proof

      let d be XFinSequence of REAL , k be Nat;

      assume

       AS: ( len d) = (k + 1);

      then

      consider a be Real, d1 be XFinSequence of REAL such that

       P1: ( len d1) = k & d1 = (d | k) & a = (d . k) & d = (d1 ^ <%a%>) by LMXFIN3;

      deffunc F( Nat) = (a * ($1 to_power k));

      consider y be Real_Sequence such that

       P3: for x be Nat holds (y . x) = F(x) from SEQ_1:sch 1;

      for x be Element of NAT holds (( seq_p d) . x) = ((( seq_p d1) + y) . x)

      proof

        let x be Element of NAT ;

        

         Q1: (( seq_p d) . x) = ( Sum (d (#) ( seq_a^ (x,1, 0 )))) by defseqp;

        

         Q2: (( seq_p d1) . x) = ( Sum (d1 (#) ( seq_a^ (x,1, 0 )))) by defseqp;

        

         Q3: ( len (d (#) ( seq_a^ (x,1, 0 )))) = (k + 1) by AS, LMXFIN1;

        

         K1: k < (k + 1) by NAT_1: 13;

        then k in ( Segm (k + 1)) by NAT_1: 44;

        then

         Q6: ((d (#) ( seq_a^ (x,1, 0 ))) . k) = (a * (x to_power k)) by AS, P1, LMXFIN2;

        

         Q5: (d (#) ( seq_a^ (x,1, 0 ))) = (((d (#) ( seq_a^ (x,1, 0 ))) | k) ^ <%(a * (x to_power k))%>) by Q6, Q3, AFINSQ_1: 56;

        

         Q7: ( len ((d (#) ( seq_a^ (x,1, 0 ))) | k)) = k by AFINSQ_1: 54, Q3, K1;

        for i be object st i in ( dom ((d (#) ( seq_a^ (x,1, 0 ))) | k)) holds (((d (#) ( seq_a^ (x,1, 0 ))) | k) . i) = ((d1 (#) ( seq_a^ (x,1, 0 ))) . i)

        proof

          let i be object;

          assume

           A1: i in ( dom ((d (#) ( seq_a^ (x,1, 0 ))) | k));

          then i in ( dom (d (#) ( seq_a^ (x,1, 0 )))) by RELAT_1: 57;

          then

           A2: i in ( dom d) by LMXFIN1;

          reconsider i0 = i as Nat by A1;

          

          thus (((d (#) ( seq_a^ (x,1, 0 ))) | k) . i) = ((d (#) ( seq_a^ (x,1, 0 ))) . i) by A1, FUNCT_1: 47

          .= ((d . i) * (x to_power i0)) by A2, LMXFIN2

          .= ((d1 . i) * (x to_power i0)) by FUNCT_1: 47, A1, P1, Q7

          .= ((d1 (#) ( seq_a^ (x,1, 0 ))) . i) by LMXFIN2, A1, P1, Q7;

        end;

        then ((d (#) ( seq_a^ (x,1, 0 ))) | k) = (d1 (#) ( seq_a^ (x,1, 0 ))) by P1, LMXFIN1, Q7;

        

        hence (( seq_p d) . x) = (( Sum (d1 (#) ( seq_a^ (x,1, 0 )))) + ( Sum <%(a * (x to_power k))%>)) by Q1, Q5, AFINSQ_2: 55

        .= ((( seq_p d1) . x) + (a * (x to_power k))) by AFINSQ_2: 53, Q2

        .= ((( seq_p d1) . x) + (y . x)) by P3

        .= ((( seq_p d1) + y) . x) by SEQ_1: 7;

      end;

      then ( seq_p d) = (( seq_p d1) + y);

      hence thesis by P1, P3;

    end;

    theorem :: ASYMPT_2:29

    

     LMXFIN5: for d be XFinSequence of REAL , k be Nat st ( len d) = 1 holds ex a be Real st a = (d . 0 ) & for x be Nat holds (( seq_p d) . x) = a

    proof

      let d be XFinSequence of REAL , k be Nat;

      assume

       AS: ( len d) = 1;

      reconsider a = (d . 0 ) as Real;

      take a;

      thus a = (d . 0 );

      let x be Nat;

      

       Q1: (( seq_p d) . x) = ( Sum (d (#) ( seq_a^ (x,1, 0 )))) by defseqp;

      

       Q3: 0 in ( Segm 1) by NAT_1: 44;

      

       Q4: ((d (#) ( seq_a^ (x,1, 0 ))) . 0 ) = ((d . 0 ) * (( seq_a^ (x,1, 0 )) . 0 )) by AS, Q3, LMXFIN1

      .= (a * (x to_power ((1 * 0 ) + 0 ))) by ASYMPT_1:def 1

      .= (a * 1) by POWER: 24

      .= a;

      ( len (d (#) ( seq_a^ (x,1, 0 )))) = 1 by AS, LMXFIN1;

      then (d (#) ( seq_a^ (x,1, 0 ))) = <%a%> by AFINSQ_1: 34, Q4;

      hence (( seq_p d) . x) = a by Q1, AFINSQ_2: 53;

    end;

    theorem :: ASYMPT_2:30

    

     LMXFIN6: for d be XFinSequence of REAL , k be Nat st ( len d) = 1 & d is nonnegative-yielding holds ( seq_p d) in ( Big_Oh ( seq_n^ k))

    proof

      let d be XFinSequence of REAL , k be Nat;

      assume

       AS: ( len d) = 1 & d is nonnegative-yielding;

      then

      consider a be Real such that

       P1: a = (d . 0 ) & for x be Nat holds (( seq_p d) . x) = a by LMXFIN5;

      set y = ( seq_p d);

      set c = (a + 1);

      

       XA1: (a + 0 ) < (a + 1) by XREAL_1: 8;

       0 in ( Segm 1) by NAT_1: 44;

      then

       ASX: 0 <= (d . 0 ) by AS, FUNCT_1: 3;

       A1:

      now

        let n be Element of NAT ;

        assume

         A2: n >= 2;

        then

         A3: n > 1 by XXREAL_0: 2;

        

         A4: (( seq_n^ k) . n) = (n to_power k) by A2, ASYMPT_1:def 3;

        1 <= (( seq_n^ k) . n)

        proof

          per cases ;

            suppose k = 0 ;

            hence 1 <= (( seq_n^ k) . n) by A4, POWER: 24;

          end;

            suppose 0 < k;

            hence 1 <= (( seq_n^ k) . n) by A4, A3, POWER: 35;

          end;

        end;

        then (1 * a) <= ((( seq_n^ k) . n) * c) by XA1, XREAL_1: 66, P1, ASX;

        hence (y . n) <= (c * (( seq_n^ k) . n)) by P1;

        thus (y . n) >= 0 by P1, ASX;

      end;

      y is Element of ( Funcs ( NAT , REAL )) by FUNCT_2: 8;

      hence y in ( Big_Oh ( seq_n^ k)) by A1, P1, ASX;

    end;

    

     LMXFIN7: for k be Nat, x,y be Real_Sequence st x in ( Big_Oh ( seq_n^ k)) & y in ( Big_Oh ( seq_n^ k)) holds (x + y) in ( Big_Oh ( seq_n^ k))

    proof

      let k be Nat, x,y be Real_Sequence;

      assume

       AS: x in ( Big_Oh ( seq_n^ k)) & y in ( Big_Oh ( seq_n^ k));

      consider t be Element of ( Funcs ( NAT , REAL )) such that

       P1: x = t & ex c be Real, N be Element of NAT st c > 0 & for n be Element of NAT st n >= N holds ((t . n) <= (c * (( seq_n^ k) . n)) & (t . n) >= 0 ) by AS;

      consider w be Element of ( Funcs ( NAT , REAL )) such that

       P2: y = w & ex c be Real, N be Element of NAT st c > 0 & for n be Element of NAT st n >= N holds ((w . n) <= (c * (( seq_n^ k) . n)) & (w . n) >= 0 ) by AS;

      consider c1 be Real, N1 be Element of NAT such that

       P11: c1 > 0 & for n be Element of NAT st n >= N1 holds ((x . n) <= (c1 * (( seq_n^ k) . n)) & (x . n) >= 0 ) by P1;

      consider c2 be Real, N2 be Element of NAT such that

       P21: c2 > 0 & for n be Element of NAT st n >= N2 holds ((y . n) <= (c2 * (( seq_n^ k) . n)) & (y . n) >= 0 ) by P2;

      set c = (c1 + c2);

      set N = (N1 + N2);

      

       X2: for n be Element of NAT st n >= N holds ((x + y) . n) <= (c * (( seq_n^ k) . n)) & ((x + y) . n) >= 0

      proof

        let n be Element of NAT ;

        assume

         X3: n >= N;

        N1 <= (N1 + N2) & N2 <= (N1 + N2) by NAT_1: 11;

        then

         X4: N1 <= n & N2 <= n by X3, XXREAL_0: 2;

        then

         X5: (x . n) <= (c1 * (( seq_n^ k) . n)) & (x . n) >= 0 by P11;

        

         X6: (y . n) <= (c2 * (( seq_n^ k) . n)) & (y . n) >= 0 by P21, X4;

        ((x . n) + (y . n)) <= ((c1 * (( seq_n^ k) . n)) + (c2 * (( seq_n^ k) . n))) by X5, X6, XREAL_1: 7;

        hence thesis by SEQ_1: 7, X5, X6;

      end;

      (x + y) is Element of ( Funcs ( NAT , REAL )) by FUNCT_2: 8;

      hence (x + y) in ( Big_Oh ( seq_n^ k)) by P11, P21, X2;

    end;

    theorem :: ASYMPT_2:31

    

     LMXFIN8: for k be Nat, a be Real, y be Real_Sequence st 0 <= a & for i be Nat holds (y . i) = (a * (i to_power k)) holds y in ( Big_Oh ( seq_n^ k))

    proof

      let k be Nat, a be Real, y be Real_Sequence;

      assume

       AS: 0 <= a & for n be Nat holds (y . n) = (a * (n to_power k));

      set c = (a + 1);

      

       XA1: (a + 0 ) < (a + 1) by XREAL_1: 8;

       A1:

      now

        let n be Element of NAT ;

        assume

         A2: n >= 2;

        

         A4: (( seq_n^ k) . n) = (n to_power k) by A2, ASYMPT_1:def 3;

        then

         A5: (y . n) = (a * (( seq_n^ k) . n)) by AS;

        hence (y . n) <= (c * (( seq_n^ k) . n)) by XA1, A4, XREAL_1: 64;

        thus (y . n) >= 0 by A4, A5, AS;

      end;

      y is Element of ( Funcs ( NAT , REAL )) by FUNCT_2: 8;

      hence y in ( Big_Oh ( seq_n^ k)) by AS, A1;

    end;

    

     LMXFIN9: for k be Nat holds ( Big_Oh ( seq_n^ k)) c= ( Big_Oh ( seq_n^ (k + 1)))

    proof

      let k be Nat;

      set g = ( seq_n^ (k + 1));

      set f = ( seq_n^ k);

      

       A0: k < (k + 1) by NAT_1: 13;

       A1:

      now

        let n be Element of NAT ;

        assume

         A2: n >= 2;

        then

         A3: n > 1 by XXREAL_0: 2;

        

         A4: (( seq_n^ k) . n) = (n to_power k) by A2, ASYMPT_1:def 3;

        (( seq_n^ (k + 1)) . n) = (n to_power (k + 1)) by A2, ASYMPT_1:def 3;

        hence (( seq_n^ k) . n) <= (1 * (( seq_n^ (k + 1)) . n)) by A3, A4, A0, POWER: 39;

        thus (( seq_n^ k) . n) >= 0 by A4;

      end;

      ( seq_n^ k) is Element of ( Funcs ( NAT , REAL )) by FUNCT_2: 8;

      then ( seq_n^ k) in ( Big_Oh ( seq_n^ (k + 1))) by A1;

      hence ( Big_Oh ( seq_n^ k)) c= ( Big_Oh ( seq_n^ (k + 1))) by ASYMPT_0: 11;

    end;

    theorem :: ASYMPT_2:32

    for k,n be Nat st k <= n holds ( Big_Oh ( seq_n^ k)) c= ( Big_Oh ( seq_n^ n))

    proof

      let k,n be Nat;

      assume k <= n;

      then

      consider i be Nat such that

       LA: n = (k + i) by NAT_1: 10;

      defpred P[ Nat] means ( Big_Oh ( seq_n^ k)) c= ( Big_Oh ( seq_n^ (k + $1)));

      

       P0: P[ 0 ];

      

       P1: for x be Nat st P[x] holds P[(x + 1)]

      proof

        let x be Nat;

        assume

         P1L1: P[x];

        ( Big_Oh ( seq_n^ (k + x))) c= ( Big_Oh ( seq_n^ ((k + x) + 1))) by LMXFIN9;

        hence thesis by XBOOLE_1: 1, P1L1;

      end;

      for x be Nat holds P[x] from NAT_1:sch 2( P0, P1);

      hence thesis by LA;

    end;

    theorem :: ASYMPT_2:33

    

     LMXFIN10: for k be Nat, c be nonnegative-yielding XFinSequence of REAL st ( len c) = (k + 1) holds ( seq_p c) in ( Big_Oh ( seq_n^ k))

    proof

      defpred P[ Nat] means for c be nonnegative-yielding XFinSequence of REAL st ( len c) = ($1 + 1) holds ( seq_p c) in ( Big_Oh ( seq_n^ $1));

      

       P0: P[ 0 ] by LMXFIN6;

      

       P1: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         P11: P[k];

        let d be nonnegative-yielding XFinSequence of REAL ;

        assume

         P12: ( len d) = ((k + 1) + 1);

        then

        consider a be Real, d1 be XFinSequence of REAL , y be Real_Sequence such that

         P13: ( len d1) = (k + 1) & d1 = (d | (k + 1)) & a = (d . (k + 1)) & d = (d1 ^ <%a%>) & ( seq_p d) = (( seq_p d1) + y) & for i be Nat holds (y . i) = (a * (i to_power (k + 1))) by LMXFIN4;

        

         T11: for i be Nat st i in ( dom d1) holds 0 <= (d1 . i)

        proof

          let i be Nat;

          assume

           AA1: i in ( dom d1);

          then

           AA2: (d1 . i) = (d . i) by P13, FUNCT_1: 47;

          (k + 1) <= ((k + 1) + 1) by NAT_1: 13;

          then ( Segm (k + 1)) c= ( Segm ((k + 1) + 1)) by NAT_1: 39;

          hence 0 <= (d1 . i) by PARTFUN3:def 4, AA2, FUNCT_1: 3, AA1, P12, P13;

        end;

        for r be Real st r in ( rng d1) holds 0 <= r

        proof

          let r be Real;

          assume r in ( rng d1);

          then

          consider x be object such that

           RC: x in ( dom d1) & r = (d1 . x) by FUNCT_1:def 3;

          thus thesis by RC, T11;

        end;

        then d1 is nonnegative-yielding;

        then ( seq_p d1) in ( Big_Oh ( seq_n^ k)) by P11, P13;

        then

         P14: ( seq_p d1) in ( Big_Oh ( seq_n^ (k + 1))) by LMXFIN9, TARSKI:def 3;

        (k + 1) < ((k + 1) + 1) by NAT_1: 13;

        then (k + 1) in ( Segm ((k + 1) + 1)) by NAT_1: 44;

        then (d . (k + 1)) in ( rng d) by FUNCT_1: 3, P12;

        then y in ( Big_Oh ( seq_n^ (k + 1))) by P13, LMXFIN8, PARTFUN3:def 4;

        hence ( seq_p d) in ( Big_Oh ( seq_n^ (k + 1))) by P14, P13, LMXFIN7;

      end;

      for k be Nat holds P[k] from NAT_1:sch 2( P0, P1);

      hence thesis;

    end;

    theorem :: ASYMPT_2:34

    

     LMXFIN15: for k be Nat, c be XFinSequence of REAL holds ex d be XFinSequence of REAL st ( len d) = ( len c) & for i be Nat st i in ( dom d) holds (d . i) = |.(c . i).|

    proof

      let k be Nat, c be XFinSequence of REAL ;

      deffunc F( Nat) = ( In ( |.(c . $1).|, REAL ));

      consider d be XFinSequence of REAL such that

       A1: ( len d) = ( len c) & for j be Nat st j in ( len c) holds (d . j) = F(j) from AFINSQ_2:sch 1;

      take d;

      thus ( len d) = ( len c) by A1;

      let i be Nat;

      assume i in ( dom d);

      then (d . i) = ( In ( |.(c . i).|, REAL )) by A1;

      hence (d . i) = |.(c . i).|;

    end;

    theorem :: ASYMPT_2:35

    

     LMXFIN17: for c be XFinSequence of REAL , d be XFinSequence of REAL st ( len d) = ( len c) & for i be Nat st i in ( dom d) holds (d . i) = |.(c . i).| holds for n be Nat holds (( seq_p c) . n) <= (( seq_p d) . n)

    proof

      let c be XFinSequence of REAL , d be XFinSequence of REAL ;

      assume

       AS: ( len d) = ( len c) & for i be Nat st i in ( dom d) holds (d . i) = |.(c . i).|;

      let x be Nat;

      

       P1: (( seq_p c) . x) = ( Sum (c (#) ( seq_a^ (x,1, 0 )))) by defseqp;

      

       P2: (( seq_p d) . x) = ( Sum (d (#) ( seq_a^ (x,1, 0 )))) by defseqp;

      ( dom (d (#) ( seq_a^ (x,1, 0 )))) = ( dom d) by LMXFIN1

      .= ( dom (c (#) ( seq_a^ (x,1, 0 )))) by LMXFIN1, AS;

      then

       D1: ( len (d (#) ( seq_a^ (x,1, 0 )))) = ( len (c (#) ( seq_a^ (x,1, 0 ))));

      for i be Nat st i in ( dom (c (#) ( seq_a^ (x,1, 0 )))) holds ((c (#) ( seq_a^ (x,1, 0 ))) . i) <= ((d (#) ( seq_a^ (x,1, 0 ))) . i)

      proof

        let i be Nat;

        assume i in ( dom (c (#) ( seq_a^ (x,1, 0 ))));

        then

         P6: i in ( dom c) by LMXFIN1;

        then

         P7: ((c (#) ( seq_a^ (x,1, 0 ))) . i) = ((c . i) * (x to_power i)) by LMXFIN2;

        

         P8: ((d (#) ( seq_a^ (x,1, 0 ))) . i) = ((d . i) * (x to_power i)) by P6, AS, LMXFIN2;

        (d . i) = |.(c . i).| by AS, P6;

        hence thesis by XREAL_1: 64, P7, P8, ABSVALUE: 4;

      end;

      hence (( seq_p c) . x) <= (( seq_p d) . x) by D1, AFINSQ_2: 57, P1, P2;

    end;

    theorem :: ASYMPT_2:36

    

     LMXFIN20A: for k be Nat, c be XFinSequence of REAL st ( len c) = (k + 1) & ( seq_p c) is eventually-nonnegative holds ( seq_p c) in ( Big_Oh ( seq_n^ k))

    proof

      let k be Nat, c be XFinSequence of REAL ;

      assume

       AS: ( len c) = (k + 1) & ( seq_p c) is eventually-nonnegative;

      consider d be XFinSequence of REAL such that

       P1: ( len d) = ( len c) & for i be Nat st i in ( dom d) holds (d . i) = |.(c . i).| by LMXFIN15;

      

       T11: for i be Nat st i in ( dom d) holds 0 <= (d . i)

      proof

        let i be Nat;

        assume i in ( dom d);

        then (d . i) = |.(c . i).| by P1;

        hence 0 <= (d . i) by COMPLEX1: 46;

      end;

      for r be Real st r in ( rng d) holds 0 <= r

      proof

        let r be Real;

        assume r in ( rng d);

        then

        consider x be object such that

         RC: x in ( dom d) & r = (d . x) by FUNCT_1:def 3;

        thus thesis by RC, T11;

      end;

      then d is nonnegative-yielding;

      then ( seq_p d) in ( Big_Oh ( seq_n^ k)) by LMXFIN10, P1, AS;

      then

      consider t be Element of ( Funcs ( NAT , REAL )) such that

       P5: ( seq_p d) = t & ex c be Real, N be Element of NAT st c > 0 & for n be Element of NAT st n >= N holds ((t . n) <= (c * (( seq_n^ k) . n)) & (t . n) >= 0 );

      consider N1 be Nat such that

       P4A: for n be Nat st N1 <= n holds 0 <= (( seq_p c) . n) by AS;

      consider a be Real, N2 be Element of NAT such that

       P6: a > 0 & for n be Element of NAT st n >= N2 holds ((t . n) <= (a * (( seq_n^ k) . n)) & ((t . n) >= 0 )) by P5;

      set N = (N1 + N2);

      

       P7: for n be Element of NAT st n >= N holds ((( seq_p c) . n) <= (a * (( seq_n^ k) . n)) & (( seq_p c) . n) >= 0 )

      proof

        let n be Element of NAT ;

        assume

         P8: n >= N;

        N1 <= (N1 + N2) & N2 <= (N1 + N2) by NAT_1: 11;

        then

         P9: N1 <= n & N2 <= n by P8, XXREAL_0: 2;

        then

         P10: (( seq_p c) . n) <= (( seq_p d) . n) & 0 <= (( seq_p c) . n) by P4A, P1, LMXFIN17;

        (( seq_p d) . n) <= (a * (( seq_n^ k) . n)) & ((( seq_p d) . n) >= 0 ) by P5, P9, P6;

        hence (( seq_p c) . n) <= (a * (( seq_n^ k) . n)) by P10, XXREAL_0: 2;

        thus 0 <= (( seq_p c) . n) by P4A, P9;

      end;

      ( seq_p c) is Element of ( Funcs ( NAT , REAL )) by FUNCT_2: 8;

      hence ( seq_p c) in ( Big_Oh ( seq_n^ k)) by P6, P7;

    end;

    theorem :: ASYMPT_2:37

    

     TPOWSUCC: for k,n be Nat st 0 < n holds (n * (( seq_n^ k) . n)) = (( seq_n^ (k + 1)) . n)

    proof

      let k,n be Nat;

      

       ZZ: k in NAT & n in NAT by ORDINAL1:def 12;

      assume

       AS: 0 < n;

      (( seq_n^ (k + 1)) . n) = (n to_power (k + 1)) by ZZ, ASYMPT_1:def 3, AS

      .= ((n to_power k) * (n to_power 1)) by POWER: 27, AS

      .= ((n to_power k) * n) by POWER: 25;

      hence thesis by AS, ZZ, ASYMPT_1:def 3;

    end;

    theorem :: ASYMPT_2:38

    

     TLNEG1: for c be XFinSequence of REAL st ( len c) = 0 holds for x be Nat holds (( seq_p c) . x) = 0

    proof

      let c be XFinSequence of REAL ;

      assume

       AS: ( len c) = 0 ;

      let x be Nat;

      

       L1: (( seq_p c) . x) = ( Sum (c (#) ( seq_a^ (x,1, 0 )))) by defseqp;

      reconsider f = (c (#) ( seq_a^ (x,1, 0 ))) as Sequence;

      ( dom f) = (( dom c) /\ ( dom ( seq_a^ (x,1, 0 )))) by VALUED_1:def 4;

      then

       L2: f = {} by AS;

      reconsider f as XFinSequence of REAL ;

      thus thesis by L2, L1;

    end;

    theorem :: ASYMPT_2:39

    for f be eventually-nonnegative Real_Sequence, k be Nat st f in ( Big_Oh ( seq_n^ k)) holds ex N be Nat st for n be Nat st N <= n holds (f . n) <= (( seq_n^ (k + 1)) . n)

    proof

      let f be eventually-nonnegative Real_Sequence, k be Nat;

      assume f in ( Big_Oh ( seq_n^ k));

      then

      consider t be Element of ( Funcs ( NAT , REAL )) such that

       L1: f = t & ex c be Real, N be Element of NAT st c > 0 & for n be Element of NAT st n >= N holds ((t . n) <= (c * (( seq_n^ k) . n)) & (t . n) >= 0 );

      consider c be Real, N be Element of NAT such that

       L2: c > 0 & for n be Element of NAT st n >= N holds (f . n) <= (c * (( seq_n^ k) . n)) & (f . n) >= 0 by L1;

      set n = [/( max (N,c))\];

      

       P1: N <= ( max (N,c)) & c <= ( max (N,c)) by XXREAL_0: 25;

      

       P2P: ( max (N,c)) <= n by INT_1:def 7;

      then

       P2: N <= n & c <= n by P1, XXREAL_0: 2;

      reconsider n as Element of NAT by INT_1: 3, P2P, P1;

      take n;

      let x be Nat;

      

       A: x in NAT by ORDINAL1:def 12;

      assume

       P4: n <= x;

      then

       P4r: 0 < x & N <= x & c <= x by P2, L2, XXREAL_0: 2;

      

       P5: (( seq_n^ (k + 1)) . x) = (x * (( seq_n^ k) . x)) by TPOWSUCC, P2P, L2, P4, P1;

      

       P6: (f . x) <= (c * (( seq_n^ k) . x)) & (f . x) >= 0 by A, P4r, L2;

      (( seq_n^ k) . x) = (x to_power k) by P4, P2P, L2, A, ASYMPT_1:def 3, P1;

      then (c * (( seq_n^ k) . x)) <= (x * (( seq_n^ k) . x)) by P4r, XREAL_1: 64;

      hence thesis by P5, XXREAL_0: 2, P6;

    end;

    theorem :: ASYMPT_2:40

    for c be XFinSequence of REAL holds ex absc be XFinSequence of REAL st absc = |.c.| & for n be Nat holds (( seq_p c) . n) <= (( seq_p absc) . n)

    proof

      let c be XFinSequence of REAL ;

      ( rng |.c.|) c= REAL ;

      then

      reconsider absc = |.c.| as XFinSequence of REAL by RELAT_1:def 19;

      take absc;

      thus absc = |.c.|;

      let n be Nat;

      

       CL1: (( seq_p c) . n) = ( Sum (c (#) ( seq_a^ (n,1, 0 )))) by defseqp;

      

       CL2: (( seq_p absc) . n) = ( Sum (absc (#) ( seq_a^ (n,1, 0 )))) by defseqp;

      set mc = (c (#) ( seq_a^ (n,1, 0 )));

      set mac = (absc (#) ( seq_a^ (n,1, 0 )));

      

       px0: ( dom c) = ( dom absc) by VALUED_1:def 11;

      ( dom mc) = (( dom c) /\ ( dom ( seq_a^ (n,1, 0 )))) by VALUED_1:def 4;

      then

       px: ( len mc) = ( len mac) by px0, VALUED_1:def 4;

      for x be Nat st x in ( dom mc) holds (mc . x) <= (mac . x)

      proof

        let x be Nat;

        

         CCL1: (mc . x) = ((c . x) * (( seq_a^ (n,1, 0 )) . x)) by VALUED_1: 5;

        

         CCL2: (mac . x) = ((absc . x) * (( seq_a^ (n,1, 0 )) . x)) by VALUED_1: 5;

        

         PX2: (( seq_a^ (n,1, 0 )) . x) = (n to_power ((1 * x) + 0 )) by ASYMPT_1:def 1

        .= (n to_power x);

        (absc . x) = |.(c . x).| by VALUED_1: 18;

        hence thesis by XREAL_1: 64, CCL1, CCL2, ABSVALUE: 4, PX2;

      end;

      hence thesis by CL1, CL2, AFINSQ_2: 57, px;

    end;

    theorem :: ASYMPT_2:41

    

     TLNEG41: for c,absc be XFinSequence of REAL st absc = |.c.| holds for n be Nat holds |.(( seq_p c) . n).| <= (( seq_p absc) . n)

    proof

      defpred P[ Nat] means for c,absc be XFinSequence of REAL st ( len c) = $1 & absc = |.c.| holds for x be Nat holds |.(( seq_p c) . x).| <= (( seq_p absc) . x);

      

       P0: P[ 0 ]

      proof

        let c,absc be XFinSequence of REAL ;

        assume

         A0: ( len c) = 0 & absc = |.c.|;

        

         D2: ( dom absc) = {} by A0, VALUED_1:def 11;

        let x be Nat;

        (c (#) ( seq_a^ (x,1, 0 ))) = {} by A0, LMXFIN1;

        then

         Q2: ( Sum (c (#) ( seq_a^ (x,1, 0 )))) = 0 ;

        (absc (#) ( seq_a^ (x,1, 0 ))) = {} by D2, LMXFIN1;

        then

         Q3: ( Sum (absc (#) ( seq_a^ (x,1, 0 )))) = 0 ;

         |.(( seq_p c) . x).| = 0 by COMPLEX1: 44, Q2, defseqp;

        hence |.(( seq_p c) . x).| <= (( seq_p absc) . x) by Q3, defseqp;

      end;

      

       P1: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A0: P[k];

        let c,absc be XFinSequence of REAL ;

        assume

         A1: ( len c) = (k + 1) & absc = |.c.|;

        consider a1 be Real, c1 be XFinSequence of REAL , y1 be Real_Sequence such that

         A2: ( len c1) = k & c1 = (c | k) & a1 = (c . k) & c = (c1 ^ <%a1%>) & ( seq_p c) = (( seq_p c1) + y1) & for i be Nat holds (y1 . i) = (a1 * (i to_power k)) by A1, LMXFIN4;

        ( len absc) = (k + 1) by A1, VALUED_1:def 11;

        then

        consider a2 be Real, c2 be XFinSequence of REAL , y2 be Real_Sequence such that

         A4: ( len c2) = k & c2 = (absc | k) & a2 = (absc . k) & absc = (c2 ^ <%a2%>) & ( seq_p absc) = (( seq_p c2) + y2) & for i be Nat holds (y2 . i) = (a2 * (i to_power k)) by LMXFIN4;

        

         A5: |.a1.| = a2 by A1, A2, A4, VALUED_1: 18;

        for i be object st i in ( dom c2) holds (c2 . i) = |.(c1 . i).|

        proof

          let i be object;

          assume

           B1: i in ( dom c2);

          (c2 . i) = (absc . i) by A4, B1, FUNCT_1: 47

          .= |.(c . i).| by A1, VALUED_1: 18

          .= |.(c1 . i).| by A2, B1, FUNCT_1: 47, A4;

          hence thesis;

        end;

        then

         AA7: c2 = |.c1.| by VALUED_1:def 11, A2, A4;

        let x be Nat;

        

         A8: (( seq_p c) . x) = ((( seq_p c1) . x) + (y1 . x)) by SEQ_1: 7, A2;

        

         A9: (( seq_p absc) . x) = ((( seq_p c2) . x) + (y2 . x)) by SEQ_1: 7, A4;

        

         A10: |.(( seq_p c) . x).| <= ( |.(( seq_p c1) . x).| + |.(y1 . x).|) by A8, COMPLEX1: 56;

        

         A11: |.(( seq_p c1) . x).| <= (( seq_p c2) . x) by AA7, A2, A0;

        (y1 . x) = (a1 * (x to_power k)) by A2;

        

        then |.(y1 . x).| = ( |.a1.| * |.(x to_power k).|) by COMPLEX1: 65

        .= ( |.a1.| * (x to_power k)) by ABSVALUE:def 1

        .= (y2 . x) by A4, A5;

        then ( |.(( seq_p c1) . x).| + |.(y1 . x).|) <= ((( seq_p c2) . x) + (y2 . x)) by XREAL_1: 7, A11;

        hence |.(( seq_p c) . x).| <= (( seq_p absc) . x) by A9, XXREAL_0: 2, A10;

      end;

      

       X1: for n be Nat holds P[n] from NAT_1:sch 2( P0, P1);

      let c,absc be XFinSequence of REAL ;

      assume

       X2: absc = |.c.|;

      ( len c) is Nat;

      hence for n be Nat holds |.(( seq_p c) . n).| <= (( seq_p absc) . n) by X1, X2;

    end;

    

     TLNEG42: for d be XFinSequence of REAL st (for i be Nat st i in ( dom d) holds 0 <= (d . i)) holds ex M be Real st 0 <= M & for i be Nat st i in ( dom d) holds (d . i) <= M

    proof

      defpred P[ Nat] means for d be XFinSequence of REAL st ( len d) = $1 & (for i be Nat st i in ( dom d) holds 0 <= (d . i)) holds ex M be Real st 0 <= M & for i be Nat st i in ( dom d) holds (d . i) <= M;

      

       P0: P[ 0 ]

      proof

        let d be XFinSequence of REAL ;

        assume

         A1: ( len d) = 0 & (for i be Nat st i in ( dom d) holds 0 <= (d . i));

        set M = 0 ;

        take M;

        thus 0 <= M;

        thus for i be Nat st i in ( dom d) holds (d . i) <= M by A1;

      end;

      

       P1: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A0: P[k];

        let d be XFinSequence of REAL ;

        assume

         A1: ( len d) = (k + 1) & (for i be Nat st i in ( dom d) holds 0 <= (d . i));

        consider a be Real, d1 be XFinSequence of REAL such that

         A2: ( len d1) = k & d1 = (d | k) & a = (d . k) & d = (d1 ^ <%a%>) by A1, LMXFIN3;

        for i be Nat st i in ( dom d1) holds 0 <= (d1 . i)

        proof

          let i be Nat;

          assume

           AA1: i in ( dom d1);

          then

           AA2: (d1 . i) = (d . i) by A2, FUNCT_1: 47;

          k <= (k + 1) by NAT_1: 13;

          then ( Segm k) c= ( Segm (k + 1)) by NAT_1: 39;

          hence 0 <= (d1 . i) by A1, AA2, AA1, A2;

        end;

        then

        consider M0 be Real such that

         A3: 0 <= M0 & for i be Nat st i in ( dom d1) holds (d1 . i) <= M0 by A0, A2;

        set M = [/( max (M0,a))\];

        

         Q1: M0 <= ( max (M0,a)) & a <= ( max (M0,a)) by XXREAL_0: 25;

        

         Q2P: ( max (M0,a)) <= M by INT_1:def 7;

        then

         Q2: M0 <= M & a <= M by Q1, XXREAL_0: 2;

        M in NAT by INT_1: 3, A3, Q1, Q2P;

        then

        reconsider M as Nat;

        take M;

        thus 0 <= M;

        let i be Nat;

        assume i in ( dom d);

        then i in ( Segm (k + 1)) by A1;

        then i < (k + 1) by NAT_1: 44;

        then

         Q6: i <= k by NAT_1: 13;

        per cases ;

          suppose i <> k;

          then i < k by XXREAL_0: 1, Q6;

          then

           Q8P: i in ( Segm k) by NAT_1: 44;

          then

           Q9: (d1 . i) = (d . i) by A2, FUNCT_1: 47;

          (d1 . i) <= M0 by A3, Q8P, A2;

          hence (d . i) <= M by Q9, Q2, XXREAL_0: 2;

        end;

          suppose i = k;

          hence (d . i) <= M by Q2P, A2, Q1, XXREAL_0: 2;

        end;

      end;

      

       X1: for k be Nat holds P[k] from NAT_1:sch 2( P0, P1);

      let d be XFinSequence of REAL ;

      assume

       X2: for i be Nat st i in ( dom d) holds 0 <= (d . i);

      thus ex M be Real st 0 <= M & for i be Nat st i in ( dom d) holds (d . i) <= M by X1, X2;

    end;

    theorem :: ASYMPT_2:42

    

     TLNEG36: for a be Real st 0 < a holds for k be Nat, d be nonnegative-yielding XFinSequence of REAL st ( len d) = k holds ex N be Nat st for x be Nat st N <= x holds for i be Nat st i in ( dom d) holds (((d . i) * (x to_power i)) * k) <= (a * (x to_power k))

    proof

      let a be Real;

      assume

       AS: 0 < a;

      let k be Nat, d be nonnegative-yielding XFinSequence of REAL ;

      assume

       A1: ( len d) = k;

      

       A2: for i be Nat st i in ( dom d) holds 0 <= (d . i)

      proof

        let i be Nat;

        assume i in ( dom d);

        then (d . i) in ( rng d) by FUNCT_1: 3;

        hence thesis by PARTFUN3:def 4;

      end;

      per cases ;

        suppose

         P0: k = 0 ;

        set N = 0 ;

        take N;

        let x be Nat;

        assume N <= x;

        thus for i be Nat st i in ( dom d) holds (((d . i) * (x to_power i)) * k) <= (a * (x to_power k)) by P0, A1;

      end;

        suppose

         K1P: k <> 0 ;

        then 0 <= (k - 1) by XREAL_1: 48, NAT_1: 14;

        then

        reconsider k1 = (k - 1) as Nat by INT_1: 3, ORDINAL1:def 12;

        consider M be Real such that

         Q1: 0 <= M & for i be Nat st i in ( dom d) holds (d . i) <= M by TLNEG42, A2;

        set N = ( [/((M * k) / a)\] + 2);

        

         MM1: ((M * k) / a) <= [/((M * k) / a)\] by INT_1:def 7;

        

         Q20P: 0 <= ((M * k) / a) by AS, Q1;

        then

         Q20: (1 + 0 ) < (2 + [/((M * k) / a)\]) by XREAL_1: 8, MM1;

        N in NAT by INT_1: 3, MM1, Q20P;

        then

        reconsider N as Nat;

        (( [/((M * k) / a)\] + 1) + 0 ) < (( [/((M * k) / a)\] + 1) + 1) by XREAL_1: 8;

        then ((M * k) / a) < N by XXREAL_0: 2, INT_1: 32;

        then (((M * k) / a) * a) <= (N * a) by AS, XREAL_1: 64;

        then

         Q2: (M * k) <= (a * N) & 1 < N by XCMPLX_1: 87, AS, Q20;

        take N;

        thus for x be Nat st N <= x holds for i be Nat st i in ( dom d) holds (((d . i) * (x to_power i)) * k) <= (a * (x to_power k))

        proof

          let x be Nat;

          assume

           Q3: N <= x;

          let i be Nat;

          assume

           Q4: i in ( dom d);

          then ((d . i) * k) <= (M * k) by XREAL_1: 64, Q1;

          then

           Q5: (((d . i) * k) * (x to_power i)) <= ((M * k) * (x to_power i)) by XREAL_1: 64;

          i in ( Segm k) by Q4, A1;

          then i < (k1 + 1) by NAT_1: 44;

          then

           Y1: i <= k1 by NAT_1: 13;

          

           Y2: 1 < x by Q3, XXREAL_0: 2, Q20;

          

           X1: (x to_power i) <= (x to_power k1)

          proof

            per cases ;

              suppose i = k1;

              hence (x to_power i) <= (x to_power k1);

            end;

              suppose i <> k1;

              then i < k1 by Y1, XXREAL_0: 1;

              hence (x to_power i) <= (x to_power k1) by Y2, POWER: 39;

            end;

          end;

          

           N1: (x * (x to_power k1)) = (x to_power k)

          proof

            per cases ;

              suppose x = 0 ;

              hence (x * (x to_power k1)) = (x to_power k) by K1P, POWER:def 2;

            end;

              suppose

               XX1: x <> 0 ;

              x = (x to_power 1) by POWER: 25;

              

              hence (x * (x to_power k1)) = (x to_power (1 + k1)) by XX1, POWER: 27

              .= (x to_power k);

            end;

          end;

          ((M * k) * (x to_power i)) <= ((M * k) * (x to_power k1)) by X1, XREAL_1: 64, Q1;

          then

           Q7: (((d . i) * k) * (x to_power i)) <= ((M * k) * (x to_power k1)) by XXREAL_0: 2, Q5;

          ((M * k) * (x to_power k1)) <= ((a * N) * (x to_power k1)) by Q2, XREAL_1: 64;

          then

           Q8: (((d . i) * k) * (x to_power i)) <= ((a * N) * (x to_power k1)) by XXREAL_0: 2, Q7;

          (a * N) <= (a * x) by XREAL_1: 64, AS, Q3;

          then ((a * N) * (x to_power k1)) <= ((a * x) * (x to_power k1)) by XREAL_1: 64;

          hence (((d . i) * (x to_power i)) * k) <= (a * (x to_power k)) by XXREAL_0: 2, Q8, N1;

        end;

      end;

    end;

    theorem :: ASYMPT_2:43

    

     TLNEG35: for k be Nat, d be XFinSequence of REAL , a be Real, y be Real_Sequence st 0 < a & ( len d) = k & for x be Nat holds (y . x) = (a * (x to_power k)) holds ex N be Nat st for x be Nat st N <= x holds |.(( seq_p d) . x).| <= (y . x)

    proof

      let k be Nat, d be XFinSequence of REAL , a be Real, y be Real_Sequence;

      assume that

       A1: 0 < a and

       A2: ( len d) = k and

       A3: for x be Nat holds (y . x) = (a * (x to_power k));

      per cases ;

        suppose

         K1: k = 0 ;

        set N = 0 ;

        take N;

        thus for x be Nat st N <= x holds |.(( seq_p d) . x).| <= (y . x)

        proof

          let x be Nat;

          assume N <= x;

          

           D2: |.(( seq_p d) . x).| = 0 by COMPLEX1: 44, A2, K1, TLNEG1;

          (y . x) = (a * (x to_power k)) by A3;

          hence thesis by D2, A1;

        end;

      end;

        suppose

         B4: k <> 0 ;

        ( rng |.d.|) c= REAL ;

        then

        reconsider c = |.d.| as XFinSequence of REAL by RELAT_1:def 19;

        

         B3: for i be Nat st i in ( dom c) holds 0 <= (c . i)

        proof

          let i be Nat;

          assume i in ( dom c);

          then (c . i) = |.(d . i).| by VALUED_1:def 11;

          hence 0 <= (c . i) by COMPLEX1: 46;

        end;

        for r be Real st r in ( rng c) holds 0 <= r

        proof

          let r be Real;

          assume r in ( rng c);

          then

          consider x be object such that

           RC: x in ( dom c) & r = (c . x) by FUNCT_1:def 3;

          thus thesis by RC, B3;

        end;

        then

         B3T: c is nonnegative-yielding;

        ( len c) = k by A2, VALUED_1:def 11;

        then

        consider N be Nat such that

         A4: for x be Nat st N <= x holds for i be Nat st i in ( dom c) holds (((c . i) * (x to_power i)) * k) <= (a * (x to_power k)) by A1, B3T, TLNEG36;

        take N;

        thus for x be Nat st N <= x holds |.(( seq_p d) . x).| <= (y . x)

        proof

          let x be Nat;

          assume

           A0: N <= x;

          

           NN0: ( dom (c (#) ( seq_a^ (x,1, 0 )))) = ( dom c) by LMXFIN1

          .= ( dom d) by VALUED_1:def 11;

          

           P1: (( seq_p c) . x) = ( Sum (c (#) ( seq_a^ (x,1, 0 )))) by defseqp;

          for i be Nat st i in ( dom (c (#) ( seq_a^ (x,1, 0 )))) holds ((c (#) ( seq_a^ (x,1, 0 ))) . i) <= ((y . x) / k)

          proof

            let i be Nat;

            assume i in ( dom (c (#) ( seq_a^ (x,1, 0 ))));

            then

             X5: i in ( dom c) by LMXFIN1;

            then ((((c . i) * (x to_power i)) * k) / k) <= ((a * (x to_power k)) / k) by XREAL_1: 72, A0, A4;

            then ((c . i) * (x to_power i)) <= ((a * (x to_power k)) / k) by B4, XCMPLX_1: 89;

            then ((c . i) * (x to_power i)) <= ((y . x) / k) by A3;

            hence ((c (#) ( seq_a^ (x,1, 0 ))) . i) <= ((y . x) / k) by X5, LMXFIN2;

          end;

          then ( Sum (c (#) ( seq_a^ (x,1, 0 )))) <= (((y . x) / k) * ( len (c (#) ( seq_a^ (x,1, 0 ))))) by AFINSQ_2: 59;

          then

           P6: (( seq_p c) . x) <= (y . x) by P1, NN0, A2, B4, XCMPLX_1: 87;

           |.(( seq_p d) . x).| <= (( seq_p c) . x) by TLNEG41;

          hence |.(( seq_p d) . x).| <= (y . x) by XXREAL_0: 2, P6;

        end;

      end;

    end;

    theorem :: ASYMPT_2:44

    

     TLNEG3: for k be Nat, d be XFinSequence of REAL st ( len d) = (k + 1) & 0 < (d . k) holds ( seq_p d) is eventually-nonnegative

    proof

      let k be Nat, d be XFinSequence of REAL ;

      assume

       AS: ( len d) = (k + 1) & 0 < (d . k);

      then

      consider a be Real, d1 be XFinSequence of REAL , y be Real_Sequence such that

       P1: ( len d1) = k & d1 = (d | k) & a = (d . k) & d = (d1 ^ <%a%>) & ( seq_p d) = (( seq_p d1) + y) & for i be Nat holds (y . i) = (a * (i to_power k)) by LMXFIN4;

      consider N be Nat such that

       P20: for i be Nat st N <= i holds |.(( seq_p d1) . i).| <= (y . i) by P1, TLNEG35, AS;

      for i be Nat st N <= i holds 0 <= (( seq_p d) . i)

      proof

        let i be Nat;

        assume N <= i;

        then

         P32: 0 <= ((y . i) - |.(( seq_p d1) . i).|) by XREAL_1: 48, P20;

        ( - (( seq_p d1) . i)) <= ( - ( - |.(( seq_p d1) . i).|)) by XREAL_1: 24, ABSVALUE: 4;

        then ((y . i) - |.(( seq_p d1) . i).|) <= ((y . i) - ( - (( seq_p d1) . i))) by XREAL_1: 13;

        then ((y . i) - |.(( seq_p d1) . i).|) <= ((( seq_p d1) . i) + (y . i));

        hence thesis by P1, SEQ_1: 7, P32;

      end;

      hence thesis;

    end;

    theorem :: ASYMPT_2:45

    for k be Nat, c be XFinSequence of REAL st ( len c) = (k + 1) & 0 < (c . k) holds ( seq_p c) in ( Big_Oh ( seq_n^ k)) by LMXFIN20A, TLNEG3;

    theorem :: ASYMPT_2:46

    for k be Nat, c be XFinSequence of REAL st ( len c) = (k + 1) & 0 < (c . k) holds ( seq_p c) is polynomially-bounded

    proof

      let k be Nat, c be XFinSequence of REAL ;

      assume

       AS: ( len c) = (k + 1) & 0 < (c . k);

      take k;

      thus thesis by LMXFIN20A, TLNEG3, AS;

    end;