asympt_3.miz



    begin

    theorem :: ASYMPT_3:1

    

     TCL001: for r be Real holds r < ( |.r.| + 1)

    proof

      let r be Real;

      (r + 0 ) < ( |.r.| + 1) by XREAL_1: 8, ABSVALUE: 4;

      hence r < ( |.r.| + 1);

    end;

    theorem :: ASYMPT_3:2

    

     LMC31: for r be Real holds ex N be 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 r = r0;

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

        end;

          suppose

           A2: not 0 < r0;

          set r = 1;

          take r;

          thus 0 < r & r0 <= r 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 ASYMPT_2: 13, A0;

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

      take N;

      thus for n be Nat st N <= n holds r0 < (n / ( log (2,n)))

      proof

        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;

    end;

    theorem :: ASYMPT_3:3

    

     L1: for k be Nat holds ex N be Nat st for x be Nat st N <= x holds (x to_power k) < (2 to_power x)

    proof

      let k be Nat;

      consider N0 be Nat such that

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

      set N = (N0 + 2);

      take N;

      now

        let x be Nat;

        assume

         AS2: N <= x;

        N0 <= N by NAT_1: 12;

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

        then

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

        2 <= N by NAT_1: 11;

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

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

        then

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

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

        then

         P4: (k * ( log (2,x))) < x by P3, XCMPLX_1: 87;

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

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

        hence (x to_power k) < (2 to_power x) by P4, POWER: 39;

      end;

      hence thesis;

    end;

    theorem :: ASYMPT_3:4

    

     L2: for k be Nat holds ex N be Nat st for x be Nat st N <= x holds (1 / (2 to_power x)) < (1 / (x to_power k))

    proof

      let k be Nat;

      consider N0 be Nat such that

       P1: for x be Nat st N0 <= x holds (x to_power k) < (2 to_power x) by L1;

      set N = (N0 + 2);

      take N;

      now

        let x be Nat;

        assume

         AS: N <= x;

        N0 <= N by NAT_1: 12;

        then N0 <= x by XXREAL_0: 2, AS;

        then

         E1: (x to_power k) < (2 to_power x) by P1;

         0 < (x to_power k) by POWER: 34, AS;

        hence (1 / (2 to_power x)) < (1 / (x to_power k)) by XREAL_1: 76, E1;

      end;

      hence thesis;

    end;

    theorem :: ASYMPT_3:5

    for z be Nat st 2 <= z holds for k be Nat holds ex N be Nat st for x be Nat st N <= x holds (1 / (z to_power x)) < (1 / (x to_power k))

    proof

      let z be Nat;

      assume

       P0: 2 <= z;

      let k be Nat;

      consider N be Nat such that

       P1: for x be Nat st N <= x holds (1 / (2 to_power x)) < (1 / (x to_power k)) by L2;

      take N;

      now

        let x be Nat;

        assume N <= x;

        then

         E1: (1 / (2 to_power x)) < (1 / (x to_power k)) by P1;

        

         P3: 0 < (2 to_power x) by POWER: 34;

        (2 to_power x) <= (z to_power x)

        proof

          now

            per cases by P0, XXREAL_0: 1;

              case 2 = z;

              hence thesis;

            end;

              case

               LL1: 2 < z;

              now

                per cases ;

                  case

                   LL2: x = 0 ;

                  

                  then (2 to_power x) = 1 by POWER: 24

                  .= (z to_power x) by POWER: 24, LL2;

                  hence thesis;

                end;

                  case 0 < x;

                  hence thesis by POWER: 37, LL1;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        then (1 / (z to_power x)) <= (1 / (2 to_power x)) by P3, XREAL_1: 118;

        hence (1 / (z to_power x)) < (1 / (x to_power k)) by E1, XXREAL_0: 2;

      end;

      hence thesis;

    end;

    registration

      cluster positive-yielding for XFinSequence of REAL ;

      correctness

      proof

        1 is Element of REAL by XREAL_0:def 1;

        then

        reconsider z = <%1%> as XFinSequence of REAL ;

        now

          let r be Real;

          assume r in ( rng z);

          then r in {1} by AFINSQ_1: 33;

          hence 0 < r;

        end;

        then z is positive-yielding;

        hence thesis;

      end;

    end

    registration

      cluster non empty for positive-yielding XFinSequence of REAL ;

      correctness

      proof

        1 is Element of REAL by XREAL_0:def 1;

        then

        reconsider z = <%1%> as XFinSequence of REAL ;

        now

          let r be Real;

          assume r in ( rng z);

          then r in {1} by AFINSQ_1: 33;

          hence 0 < r;

        end;

        then z is positive-yielding;

        hence thesis;

      end;

    end

    theorem :: ASYMPT_3:6

    

     NLM1: for c be XFinSequence of REAL , a be Real holds (a (#) c) is XFinSequence of REAL

    proof

      let c be XFinSequence of REAL , a be Real;

      ( dom (a (#) c)) = ( dom c) by VALUED_1:def 5;

      then (a (#) c) is Sequence of ( rng (a (#) c)) by ORDINAL1: 31;

      hence thesis by ORDINAL1: 32;

    end;

    registration

      let c be XFinSequence of REAL , a be Real;

      cluster (a (#) c) -> finite;

      correctness ;

    end

    theorem :: ASYMPT_3:7

    

     NLM2: for c be non empty positive-yielding XFinSequence of REAL , a be Real st 0 < a holds (a (#) c) is non empty positive-yielding XFinSequence of REAL

    proof

      let c be non empty positive-yielding XFinSequence of REAL , a be Real;

      assume

       AS: 0 < a;

      

       P2: ( dom (a (#) c)) = ( dom c) by VALUED_1:def 5;

      now

        let r be Real;

        assume r in ( rng (a (#) c));

        then

        consider x be object such that

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

        (c . x) in ( rng c) by FUNCT_1: 3, P4, P2;

        then

         P5: 0 < (c . x) by PARTFUN3:def 1;

        r = (a * (c . x)) by P4, VALUED_1: 6;

        hence 0 < r by P5, AS;

      end;

      then (a (#) c) is positive-yielding;

      hence thesis by NLM1, P2;

    end;

    registration

      let c be non empty positive-yielding XFinSequence of REAL , a be positive Real;

      cluster (a (#) c) -> non empty positive-yielding;

      correctness by NLM2;

    end

    notation

      let c be XFinSequence of REAL ;

      synonym polynom (c) for seq_p (c);

    end

    theorem :: ASYMPT_3:8

    

     NLM3: for c be non empty positive-yielding XFinSequence of REAL , x be Nat holds 0 < (( polynom c) . x)

    proof

      defpred P[ Nat] means for c be non empty positive-yielding XFinSequence of REAL st ( len c) = $1 holds for x be Nat holds 0 < (( polynom c) . x);

      

       P0: P[ 0 ];

      

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

      proof

        let k be Nat;

        assume

         A1: P[k];

        let d be non empty positive-yielding XFinSequence of REAL ;

        assume

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

        then

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

         A3: ( len d1) = k & d1 = (d | k) & a = (d . k) & d = (d1 ^ <%a%>) & ( polynom d) = (( polynom d1) + y) & for i be Nat holds (y . i) = (a * (i to_power k)) by ASYMPT_2: 28;

        per cases ;

          suppose

           X1: k = 0 ;

          then

          consider a be Real such that

           A4: a = (d . 0 ) & for x be Nat holds (( polynom d) . x) = a by ASYMPT_2: 29, A2;

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

          then (d . 0 ) in ( rng d) by FUNCT_1: 3, X1, A2;

          then

           A5: 0 < (d . 0 ) by PARTFUN3:def 1;

          let x be Nat;

          reconsider n = x as Nat;

          thus 0 < (( polynom d) . x) by A5, A4;

        end;

          suppose

           A7: k <> 0 ;

          now

            let r be Real;

            assume r in ( rng d1);

            then

            consider x be object such that

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

            

             P5: (d1 . x) = (d . x) by P4, A3, FUNCT_1: 47;

            x in ( dom d) by P4, A3, RELAT_1: 60, TARSKI:def 3;

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

            hence 0 < r by PARTFUN3:def 1, P5, P4;

          end;

          then

           A8: d1 is positive-yielding;

          reconsider d1 as non empty positive-yielding XFinSequence of REAL by A7, A8, A3;

          let x be Nat;

          reconsider n = x as Nat;

          

           A9: 0 < (( polynom d1) . n) by A1, A3;

          

           A10: (( polynom d) . n) = ((( polynom d1) . n) + (y . n)) by SEQ_1: 7, A3;

          

           A11: (y . n) = (a * (n to_power k)) by A3;

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

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

          then (d . k) in ( rng d) by FUNCT_1: 3, A2;

          then 0 < (d . k) by PARTFUN3:def 1;

          hence 0 < (( polynom d) . x) by A10, A9, A11, A3;

        end;

      end;

      

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

      let c be non empty positive-yielding XFinSequence of REAL , x be Nat;

      ( len c) is Nat;

      hence 0 < (( polynom c) . x) by P2;

    end;

    theorem :: ASYMPT_3:9

    

     NLM4: for c,c1 be non empty positive-yielding XFinSequence of REAL , a be Real st c1 = (a (#) c) holds for x be Nat holds (( polynom c1) . x) = (a * (( polynom c) . x))

    proof

      let c,c1 be non empty positive-yielding XFinSequence of REAL , a be Real;

      assume

       AS: c1 = (a (#) c);

      let x be Nat;

      

       D1: ( dom (c1 (#) ( seq_a^ (x,1, 0 )))) = ( dom c1) by ASYMPT_2: 26

      .= ( dom c) by VALUED_1:def 5, AS;

      

       D2: ( dom (a (#) (c (#) ( seq_a^ (x,1, 0 ))))) = ( dom (c (#) ( seq_a^ (x,1, 0 )))) by VALUED_1:def 5

      .= ( dom c) by ASYMPT_2: 26;

      for i be object st i in ( dom (c1 (#) ( seq_a^ (x,1, 0 )))) holds ((c1 (#) ( seq_a^ (x,1, 0 ))) . i) = ((a (#) (c (#) ( seq_a^ (x,1, 0 )))) . i)

      proof

        let i be object;

        assume

         D3: i in ( dom (c1 (#) ( seq_a^ (x,1, 0 ))));

        then

         D4: i in ( dom c1) by ASYMPT_2: 26;

        

        thus ((c1 (#) ( seq_a^ (x,1, 0 ))) . i) = ((c1 . i) * (( seq_a^ (x,1, 0 )) . i)) by D4, ASYMPT_2: 26

        .= ((a * (c . i)) * (( seq_a^ (x,1, 0 )) . i)) by AS, VALUED_1: 6

        .= (a * ((c . i) * (( seq_a^ (x,1, 0 )) . i)))

        .= (a * ((c (#) ( seq_a^ (x,1, 0 ))) . i)) by D3, D1, ASYMPT_2: 26

        .= ((a (#) (c (#) ( seq_a^ (x,1, 0 )))) . i) by VALUED_1: 6;

      end;

      then

       P2: (c1 (#) ( seq_a^ (x,1, 0 ))) = (a (#) (c (#) ( seq_a^ (x,1, 0 )))) by D1, D2;

      

      thus (( polynom c1) . x) = ( Sum (c1 (#) ( seq_a^ (x,1, 0 )))) by ASYMPT_2:def 2

      .= (a * ( Sum (c (#) ( seq_a^ (x,1, 0 ))))) by AFINSQ_2: 64, P2

      .= (a * (( polynom c) . x)) by ASYMPT_2:def 2;

    end;

    begin

    definition

      let p be Real_Sequence;

      :: ASYMPT_3:def1

      attr p is polynomially-abs-bounded means

      : defabs: ex k be Nat st |.p.| in ( Big_Oh ( seq_n^ k));

    end

    registration

      cluster polynomially-bounded -> polynomially-abs-bounded for Real_Sequence;

      coherence

      proof

        let p be Real_Sequence;

        assume p is polynomially-bounded;

        then

        consider k be Nat such that

         L1: p in ( Big_Oh ( seq_n^ k));

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

         L2: p = 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 L1;

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

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

        reconsider abst = |.t.| as Element of ( Funcs ( NAT , REAL )) by FUNCT_2: 8;

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

        proof

          let n be Element of NAT ;

          assume

           LL2: n >= N;

          

          then (t . n) = |.(t . n).| by ABSVALUE:def 1, L3

          .= ( |.t.| . n) by VALUED_1: 18;

          hence thesis by LL2, L3;

        end;

        then |.p.| in ( Big_Oh ( seq_n^ k)) by L2, L3;

        hence thesis;

      end;

    end

    theorem :: ASYMPT_3:10

    

     LM1: for r be Element of NAT holds for s be Real_Sequence st s = ( NAT --> r) holds s is polynomially-abs-bounded

    proof

      let r be Element of NAT ;

      let s1 be Real_Sequence;

      assume

       AS: s1 = ( NAT --> r);

      set s = |.s1.|;

      

       P1: s in ( Funcs ( NAT , REAL )) by FUNCT_2: 8;

      now

        let n be Element of NAT ;

        assume

         A2: n >= r;

        n = 0 or n > 0 ;

        

        then

         A4: (( seq_n^ 1) . n) = (n to_power 1) by ASYMPT_1:def 3

        .= n;

        

         A5: (s . n) = |.(s1 . n).| by VALUED_1: 18

        .= |.r.| by AS

        .= r by ABSVALUE:def 1;

        hence (s . n) <= (1 * (( seq_n^ 1) . n)) by A2, A4;

        thus (s . n) >= 0 by A5;

      end;

      then s in ( Big_Oh ( seq_n^ 1)) by P1;

      hence thesis;

    end;

    reconsider rr = 0 as Element of REAL by XREAL_0:def 1;

    registration

      cluster polynomially-abs-bounded for Function of NAT , REAL ;

      existence

      proof

        take ( NAT --> rr);

        thus thesis by LM1;

      end;

    end

    registration

      let f,g be polynomially-abs-bounded Function of NAT , REAL ;

      cluster (f + g) -> polynomially-abs-bounded;

      coherence

      proof

        set h = (f + g);

        

         A3: for n be Nat holds ( |.h.| . n) <= (( |.f.| . n) + ( |.g.| . n))

        proof

          let n be Nat;

          

           S1: n in NAT by ORDINAL1:def 12;

          

           A30: ( |.h.| . n) = |.(h . n).| by VALUED_1: 18

          .= |.((f . n) + (g . n)).| by S1, VALUED_1: 1;

          ( |.(f . n).| + |.(g . n).|) = (( |.f.| . n) + |.(g . n).|) by VALUED_1: 18

          .= (( |.f.| . n) + ( |.g.| . n)) by VALUED_1: 18;

          hence thesis by COMPLEX1: 56, A30;

        end;

        consider k1 be Nat such that

         A4: |.f.| in ( Big_Oh ( seq_n^ k1)) by defabs;

        consider k2 be Nat such that

         A5: |.g.| in ( Big_Oh ( seq_n^ k2)) by defabs;

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

         A6: |.f.| = t1 & ex c1 be Real, N1 be Element of NAT st c1 > 0 & for n be Element of NAT st n >= N1 holds (t1 . n) <= (c1 * (( seq_n^ k1) . n)) & (t1 . n) >= 0 by A4;

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

         A7: |.g.| = t2 & ex c2 be Real, N2 be Element of NAT st c2 > 0 & for n be Element of NAT st n >= N2 holds (t2 . n) <= (c2 * (( seq_n^ k2) . n)) & (t2 . n) >= 0 by A5;

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

         A8: c1 > 0 & for n be Element of NAT st n >= N1 holds (t1 . n) <= (c1 * (( seq_n^ k1) . n)) & (t1 . n) >= 0 by A6;

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

         A9: c2 > 0 & for n be Element of NAT st n >= N2 holds (t2 . n) <= (c2 * (( seq_n^ k2) . n)) & (t2 . n) >= 0 by A7;

        set c = (c1 + c2);

        set N = (N1 + N2);

        set k = (k1 + k2);

        reconsider t = |.h.| as Element of ( Funcs ( NAT , REAL )) by FUNCT_2: 8;

        now

          let n be Element of NAT ;

          assume

           B11: n >= (N + 2);

          N <= (N + 2) & 2 <= (N + 2) by NAT_1: 12;

          then

           A11: N <= n & 2 <= n by B11, XXREAL_0: 2;

          N1 <= N & N2 <= N by NAT_1: 12;

          then

           A12: N1 <= n & N2 <= n by A11, XXREAL_0: 2;

          then

           A13: (t1 . n) <= (c1 * (( seq_n^ k1) . n)) & (t1 . n) >= 0 by A8;

          

           A14: (t2 . n) <= (c2 * (( seq_n^ k2) . n)) & (t2 . n) >= 0 by A12, A9;

          

           B15: 1 < n by A11, XXREAL_0: 2;

          

           B14: k1 <= k & k2 <= k by NAT_1: 12;

          

           S1: (( seq_n^ k1) . n) = (n to_power k1) by B11, ASYMPT_1:def 3;

          

           S2: (( seq_n^ k2) . n) = (n to_power k2) by B11, ASYMPT_1:def 3;

          

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

          k1 < k or k1 = k by XXREAL_0: 1, B14;

          then (( seq_n^ k1) . n) <= (( seq_n^ k) . n) by S1, S3, B15, POWER: 39;

          then

           S4: (c1 * (( seq_n^ k1) . n)) <= (c1 * (( seq_n^ k) . n)) by XREAL_1: 64, A8;

          k2 < k or k2 = k by XXREAL_0: 1, B14;

          then (( seq_n^ k2) . n) <= (( seq_n^ k) . n) by S2, S3, B15, POWER: 39;

          then (c2 * (( seq_n^ k2) . n)) <= (c2 * (( seq_n^ k) . n)) by XREAL_1: 64, A9;

          then

           S6: ((c1 * (( seq_n^ k1) . n)) + (c2 * (( seq_n^ k2) . n))) <= ((c1 * (( seq_n^ k) . n)) + (c2 * (( seq_n^ k) . n))) by S4, XREAL_1: 7;

          ((t1 . n) + (t2 . n)) <= ((c1 * (( seq_n^ k1) . n)) + (c2 * (( seq_n^ k2) . n))) by XREAL_1: 7, A13, A14;

          then

           A15: ((t1 . n) + (t2 . n)) <= (c * (( seq_n^ k) . n)) by S6, XXREAL_0: 2;

          (t . n) <= ((t1 . n) + (t2 . n)) by A3, A6, A7;

          hence (t . n) <= (c * (( seq_n^ k) . n)) by A15, XXREAL_0: 2;

          ( |.h.| . n) = |.(h . n).| by VALUED_1: 18;

          hence 0 <= (t . n);

        end;

        then |.h.| in ( Big_Oh ( seq_n^ k)) by A8, A9;

        hence thesis;

      end;

      cluster (f (#) g) -> polynomially-abs-bounded;

      coherence

      proof

        set h = (f (#) g);

        

         A3: for n be Nat holds ( |.h.| . n) = (( |.f.| . n) * ( |.g.| . n))

        proof

          let n be Nat;

          

          thus ( |.h.| . n) = |.(h . n).| by VALUED_1: 18

          .= |.((f . n) * (g . n)).| by VALUED_1: 5

          .= ( |.(f . n).| * |.(g . n).|) by COMPLEX1: 65

          .= (( |.f.| . n) * |.(g . n).|) by VALUED_1: 18

          .= (( |.f.| . n) * ( |.g.| . n)) by VALUED_1: 18;

        end;

        consider k1 be Nat such that

         A4: |.f.| in ( Big_Oh ( seq_n^ k1)) by defabs;

        consider k2 be Nat such that

         A5: |.g.| in ( Big_Oh ( seq_n^ k2)) by defabs;

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

         A6: |.f.| = t1 & ex c1 be Real, N1 be Element of NAT st c1 > 0 & for n be Element of NAT st n >= N1 holds (t1 . n) <= (c1 * (( seq_n^ k1) . n)) & (t1 . n) >= 0 by A4;

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

         A7: |.g.| = t2 & ex c2 be Real, N2 be Element of NAT st c2 > 0 & for n be Element of NAT st n >= N2 holds (t2 . n) <= (c2 * (( seq_n^ k2) . n)) & (t2 . n) >= 0 by A5;

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

         A8: c1 > 0 & for n be Element of NAT st n >= N1 holds (t1 . n) <= (c1 * (( seq_n^ k1) . n)) & (t1 . n) >= 0 by A6;

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

         A9: c2 > 0 & for n be Element of NAT st n >= N2 holds (t2 . n) <= (c2 * (( seq_n^ k2) . n)) & (t2 . n) >= 0 by A7;

        set c = (c1 * c2);

        set N = (N1 + N2);

        set k = (k1 + k2);

        reconsider t = |.h.| as Element of ( Funcs ( NAT , REAL )) by FUNCT_2: 8;

        now

          let n be Element of NAT ;

          assume

           B11: n >= (N + 2);

          N <= (N + 2) & 2 <= (N + 2) by NAT_1: 12;

          then

           A11n: N <= n & 2 <= n by B11, XXREAL_0: 2;

          N1 <= N & N2 <= N by NAT_1: 12;

          then

           A12: N1 <= n & N2 <= n by A11n, XXREAL_0: 2;

          then

           A13: (t1 . n) <= (c1 * (( seq_n^ k1) . n)) & (t1 . n) >= 0 by A8;

          

           A14: (t2 . n) <= (c2 * (( seq_n^ k2) . n)) & (t2 . n) >= 0 by A12, A9;

          

           A15: ((t1 . n) * (t2 . n)) <= ((c1 * (( seq_n^ k1) . n)) * (c2 * (( seq_n^ k2) . n))) by XREAL_1: 66, A13, A14;

          ((c1 * (( seq_n^ k1) . n)) * (c2 * (( seq_n^ k2) . n))) = ((c1 * c2) * ((( seq_n^ k1) . n) * (( seq_n^ k2) . n)))

          .= ((c1 * c2) * ((n to_power k1) * (( seq_n^ k2) . n))) by B11, ASYMPT_1:def 3

          .= ((c1 * c2) * ((n to_power k1) * (n to_power k2))) by B11, ASYMPT_1:def 3

          .= ((c1 * c2) * (n to_power (k1 + k2))) by B11, POWER: 27

          .= (c * (( seq_n^ k) . n)) by B11, ASYMPT_1:def 3;

          hence (t . n) <= (c * (( seq_n^ k) . n)) by A15, A3, A6, A7;

           0 <= ((t1 . n) * (t2 . n)) by A13, A14;

          hence 0 <= (t . n) by A3, A6, A7;

        end;

        then |.h.| in ( Big_Oh ( seq_n^ k)) by A8, A9;

        hence thesis;

      end;

    end

    registration

      let f be polynomially-abs-bounded Function of NAT , REAL ;

      let a be Element of REAL ;

      cluster (a (#) f) -> polynomially-abs-bounded;

      coherence

      proof

        set h = (a (#) f);

        per cases ;

          suppose

           CS1: a = 0 ;

          

           X0: ( dom h) = NAT by FUNCT_2:def 1;

          now

            let z be object;

            assume z in ( dom h);

            then

            reconsider n = z as Element of NAT ;

            

            thus (h . z) = ( 0 * (f . n)) by CS1, VALUED_1: 6

            .= 0 ;

          end;

          then h = ( NAT --> 0 ) by FUNCOP_1: 11, X0;

          hence thesis by LM1;

        end;

          suppose

           A0: a <> 0 ;

          

           A3: for n be Nat holds ( |.h.| . n) = ( |.a.| * ( |.f.| . n))

          proof

            let n be Nat;

            

            thus ( |.h.| . n) = |.(h . n).| by VALUED_1: 18

            .= |.(a * (f . n)).| by VALUED_1: 6

            .= ( |.a.| * |.(f . n).|) by COMPLEX1: 65

            .= ( |.a.| * ( |.f.| . n)) by VALUED_1: 18;

          end;

          consider k1 be Nat such that

           A4: |.f.| in ( Big_Oh ( seq_n^ k1)) by defabs;

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

           A6: |.f.| = t1 & ex c1 be Real, N1 be Element of NAT st c1 > 0 & for n be Element of NAT st n >= N1 holds (t1 . n) <= (c1 * (( seq_n^ k1) . n)) & (t1 . n) >= 0 by A4;

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

           A8: c1 > 0 & for n be Element of NAT st n >= N1 holds (t1 . n) <= (c1 * (( seq_n^ k1) . n)) & (t1 . n) >= 0 by A6;

          set c = ( |.a.| * c1);

          reconsider t = |.h.| as Element of ( Funcs ( NAT , REAL )) by FUNCT_2: 8;

          now

            let n be Element of NAT ;

            assume

             B11: n >= (N1 + 2);

            N1 <= (N1 + 2) & 2 <= (N1 + 2) by NAT_1: 12;

            then N1 <= n & 2 <= n by B11, XXREAL_0: 2;

            then

             A13: (t1 . n) <= (c1 * (( seq_n^ k1) . n)) & (t1 . n) >= 0 by A8;

            then

             A15: ( |.a.| * (t1 . n)) <= ( |.a.| * (c1 * (( seq_n^ k1) . n))) by XREAL_1: 66;

            thus (t . n) <= (c * (( seq_n^ k1) . n)) by A15, A3, A6;

             0 <= ( |.a.| * (t1 . n)) by A13;

            hence 0 <= (t . n) by A3, A6;

          end;

          then |.h.| in ( Big_Oh ( seq_n^ k1)) by A8, A0;

          hence thesis;

        end;

      end;

    end

    definition

      :: ASYMPT_3:def2

      func Big_Oh_poly -> Subset of ( RAlgebra NAT ) means

      : DefX1: for x be object holds x in it iff x is polynomially-abs-bounded Function of NAT , REAL ;

      existence

      proof

        defpred P[ object] means $1 is polynomially-abs-bounded Function of NAT , REAL ;

        consider IT be set such that

         A01: for x be object holds x in IT iff x in ( Funcs ( NAT , REAL )) & P[x] from XBOOLE_0:sch 1;

        

         A1: for x be object holds x in IT iff x is polynomially-abs-bounded Function of NAT , REAL

        proof

          let x be object;

          x is polynomially-abs-bounded Function of NAT , REAL implies x in ( Funcs ( NAT , REAL )) by FUNCT_2: 8;

          hence thesis by A01;

        end;

        for x be object st x in IT holds x in ( Funcs ( NAT , REAL ))

        proof

          let x be object;

          assume x in IT;

          then x is polynomially-abs-bounded Function of NAT , REAL by A1;

          hence x in ( Funcs ( NAT , REAL )) by FUNCT_2: 8;

        end;

        then IT is Subset of ( RAlgebra NAT ) by TARSKI:def 3;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of ( RAlgebra NAT );

        assume that

         A2: for x be object holds x in X1 iff x is polynomially-abs-bounded Function of NAT , REAL and

         A3: for x be object holds x in X2 iff x is polynomially-abs-bounded Function of NAT , REAL ;

        thus X1 c= X2

        proof

          let x be object;

          assume x in X1;

          then x is polynomially-abs-bounded Function of NAT , REAL by A2;

          hence thesis by A3;

        end;

        let x be object;

        assume x in X2;

        then x is polynomially-abs-bounded Function of NAT , REAL by A3;

        hence thesis by A2;

      end;

    end

    registration

      cluster Big_Oh_poly -> non empty;

      coherence

      proof

         the polynomially-abs-bounded Function of NAT , REAL in Big_Oh_poly by DefX1;

        hence thesis;

      end;

    end

    definition

      :: ASYMPT_3:def3

      func R_Algebra_of_Big_Oh_poly -> strict AlgebraStr means

      : defAlgebra: the carrier of it = Big_Oh_poly & the multF of it = (( RealFuncMult NAT ) || Big_Oh_poly ) & the addF of it = (( RealFuncAdd NAT ) || Big_Oh_poly ) & the Mult of it = (( RealFuncExtMult NAT ) | [: REAL , Big_Oh_poly :]) & the OneF of it = ( RealFuncUnit NAT ) & the ZeroF of it = ( RealFuncZero NAT );

      correctness

      proof

        set X = Big_Oh_poly ;

        set m = (( RealFuncMult NAT ) || X);

        set a = (( RealFuncAdd NAT ) || X);

        set E = (( RealFuncExtMult NAT ) | [: REAL , X:]);

        set O = ( RealFuncUnit NAT );

        set Z = ( RealFuncZero NAT );

        for x be set holds x in [:X, X:] implies (( RealFuncMult NAT ) . x) in X

        proof

          let x be set;

          assume x in [:X, X:];

          then

          consider f,g be object such that

           B2: f in X & g in X & x = [f, g] by ZFMISC_1:def 2;

          reconsider f, g as polynomially-abs-bounded Function of NAT , REAL by DefX1, B2;

          set h = (( RealFuncMult NAT ) . x);

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

          

           B5: h = (( RealFuncMult NAT ) . (f1,g1)) by B2;

          reconsider h as Function of NAT , REAL by B5;

          h = (f (#) g)

          proof

            let n be Element of NAT ;

            

            thus (h . n) = ((f . n) * (g . n)) by B5, FUNCSDOM: 2

            .= ((f (#) g) . n) by VALUED_1: 5;

          end;

          hence thesis by DefX1;

        end;

        then X is Preserv of ( RealFuncMult NAT ) by REALSET1:def 1;

        then

        reconsider m as BinOp of X by REALSET1: 2;

        for x be set holds x in [:X, X:] implies (( RealFuncAdd NAT ) . x) in X

        proof

          let x be set;

          assume x in [:X, X:];

          then

          consider f,g be object such that

           B2: f in X & g in X & x = [f, g] by ZFMISC_1:def 2;

          reconsider f, g as polynomially-abs-bounded Function of NAT , REAL by DefX1, B2;

          set h = (( RealFuncAdd NAT ) . x);

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

          

           B5: h = (( RealFuncAdd NAT ) . (f1,g1)) by B2;

          then

          reconsider h as Function of NAT , REAL ;

          h = (f + g)

          proof

            let n be Element of NAT ;

            

            thus (h . n) = ((f . n) + (g . n)) by B5, FUNCSDOM: 1

            .= ((f + g) . n) by VALUED_1: 1;

          end;

          hence thesis by DefX1;

        end;

        then X is Preserv of ( RealFuncAdd NAT ) by REALSET1:def 1;

        then

        reconsider a as BinOp of X by REALSET1: 2;

        

         Q0: [: REAL , X:] c= [: REAL , ( Funcs ( NAT , REAL )):] by ZFMISC_1: 95;

         [: REAL , ( Funcs ( NAT , REAL )):] = ( dom ( RealFuncExtMult NAT )) by FUNCT_2:def 1;

        then

         Q1: ( dom E) = [: REAL , X:] by RELAT_1: 62, Q0;

        for h be object st h in ( rng E) holds h in X

        proof

          let h be object;

          assume h in ( rng E);

          then

          consider x be object such that

           Q2: x in ( dom E) & h = (E . x) by FUNCT_1:def 3;

          consider s,f be object such that

           B2: s in REAL & f in X and

           B3: x = [s, f] by Q1, Q2, ZFMISC_1:def 2;

          reconsider f as polynomially-abs-bounded Function of NAT , REAL by DefX1, B2;

          reconsider s as Element of REAL by B2;

          

           H1: h = (( RealFuncExtMult NAT ) . x) by Q1, Q2, FUNCT_1: 49;

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

          reconsider h1 = h as Element of ( Funcs ( NAT , REAL )) by H1, FUNCT_2: 5, Q2;

          reconsider h1 as Function of NAT , REAL ;

          h1 = (s (#) f)

          proof

            let n be Element of NAT ;

            

            thus (h1 . n) = (s * (f1 . n)) by B3, H1, FUNCSDOM: 4

            .= ((s (#) f) . n) by VALUED_1: 6;

          end;

          hence h in X by DefX1;

        end;

        then ( rng E) c= X;

        then

        reconsider E as Function of [: REAL , X:], X by Q1, FUNCT_2: 2;

        reconsider O as Real_Sequence;

        O in ( Funcs ( NAT , REAL )) & ( seq_id O) is polynomially-abs-bounded by LM1;

        then

        reconsider O as Element of X by DefX1;

        reconsider Z as Real_Sequence;

        Z in ( Funcs ( NAT , REAL )) & ( seq_id Z) is polynomially-abs-bounded by LM1;

        then

        reconsider Z as Element of X by DefX1;

        set S = AlgebraStr (# X, m, a, E, O, Z #);

        S is strict AlgebraStr;

        hence thesis;

      end;

    end

    registration

      cluster R_Algebra_of_Big_Oh_poly -> non empty;

      correctness by defAlgebra;

    end

    theorem :: ASYMPT_3:11

    

     LM12: the carrier of R_Algebra_of_Big_Oh_poly c= the carrier of ( RAlgebra NAT )

    proof

      the carrier of R_Algebra_of_Big_Oh_poly = Big_Oh_poly by defAlgebra;

      hence thesis;

    end;

    theorem :: ASYMPT_3:12

    

     LM14: for f be object holds f in R_Algebra_of_Big_Oh_poly iff f is polynomially-abs-bounded Function of NAT , REAL

    proof

      let f be object;

      the carrier of R_Algebra_of_Big_Oh_poly = Big_Oh_poly by defAlgebra;

      hence f in R_Algebra_of_Big_Oh_poly iff f is polynomially-abs-bounded Function of NAT , REAL by DefX1;

    end;

    theorem :: ASYMPT_3:13

    

     LM15: for f,g be Point of R_Algebra_of_Big_Oh_poly , f1,g1 be Point of ( RAlgebra NAT ) st f = f1 & g = g1 holds (f * g) = (f1 * g1)

    proof

      let f,g be Point of R_Algebra_of_Big_Oh_poly , f1,g1 be Point of ( RAlgebra NAT );

      assume

       A1: f = f1 & g = g1;

      set X = Big_Oh_poly ;

      set S = R_Algebra_of_Big_Oh_poly ;

      

       A3a: the carrier of R_Algebra_of_Big_Oh_poly = X by defAlgebra;

      

      thus (f * g) = ((( RealFuncMult NAT ) || X) . [f, g]) by defAlgebra

      .= (f1 * g1) by A1, A3a, FUNCT_1: 49;

    end;

    theorem :: ASYMPT_3:14

    

     LM16: for f,g be Point of R_Algebra_of_Big_Oh_poly , f1,g1 be Point of ( RAlgebra NAT ) st f = f1 & g = g1 holds (f + g) = (f1 + g1)

    proof

      let f,g be Point of R_Algebra_of_Big_Oh_poly , f1,g1 be Point of ( RAlgebra NAT );

      assume

       A1: f = f1 & g = g1;

      set X = Big_Oh_poly ;

      set S = R_Algebra_of_Big_Oh_poly ;

      

       A3: the carrier of R_Algebra_of_Big_Oh_poly = X by defAlgebra;

      

      thus (f + g) = ((( RealFuncAdd NAT ) || X) . [f, g]) by defAlgebra

      .= (f1 + g1) by A1, A3, FUNCT_1: 49;

    end;

    theorem :: ASYMPT_3:15

    

     LM17: for f be Point of R_Algebra_of_Big_Oh_poly , f1 be Point of ( RAlgebra NAT ), a be Element of REAL st f = f1 holds (a * f) = (a * f1)

    proof

      let f be Point of R_Algebra_of_Big_Oh_poly , f1 be Point of ( RAlgebra NAT ), a be Element of REAL ;

      assume

       A1: f = f1;

      set X = Big_Oh_poly ;

      set S = R_Algebra_of_Big_Oh_poly ;

      

       A3: the carrier of R_Algebra_of_Big_Oh_poly = X by defAlgebra;

      

      thus (a * f) = ((( RealFuncExtMult NAT ) | [: REAL , X:]) . [a, f]) by defAlgebra

      .= (a * f1) by A1, A3, FUNCT_1: 49;

    end;

    theorem :: ASYMPT_3:16

    

     LM18: ( 0. R_Algebra_of_Big_Oh_poly ) = ( 0. ( RAlgebra NAT )) by defAlgebra;

    theorem :: ASYMPT_3:17

    

     LM19: ( 1. R_Algebra_of_Big_Oh_poly ) = ( 1. ( RAlgebra NAT )) by defAlgebra;

    registration

      cluster R_Algebra_of_Big_Oh_poly -> strict Abelian add-associative right_zeroed right_complementable commutative associative right_unital right-distributive vector-associative scalar-associative vector-distributive scalar-distributive;

      correctness

      proof

        set S = R_Algebra_of_Big_Oh_poly ;

        thus S is strict;

        thus S is Abelian

        proof

          let x,y be Element of S;

          reconsider x1 = x, y1 = y as Element of ( RAlgebra NAT ) by LM12;

          

          thus (x + y) = (x1 + y1) by LM16

          .= (y + x) by LM16;

        end;

        thus S is add-associative

        proof

          let x,y,z be Element of S;

          reconsider x1 = x, y1 = y, z1 = z as Element of ( RAlgebra NAT ) by LM12;

          

           D1: (x + y) = (x1 + y1) by LM16;

          

           D2: (y + z) = (y1 + z1) by LM16;

          

          thus ((x + y) + z) = ((x1 + y1) + z1) by D1, LM16

          .= (x1 + (y1 + z1)) by RLVECT_1:def 3

          .= (x + (y + z)) by D2, LM16;

        end;

        thus S is right_zeroed

        proof

          let x be Element of S;

          reconsider x1 = x as Element of ( RAlgebra NAT ) by LM12;

          

          thus (x + ( 0. S)) = (x1 + ( 0. ( RAlgebra NAT ))) by LM18, LM16

          .= x;

        end;

        thus S is right_complementable

        proof

          let x be Element of S;

          reconsider x1 = x as Element of ( RAlgebra NAT ) by LM12;

          set t1 = (( - 1) * x);

          take t1;

          ( - 1) is Element of REAL by XREAL_0:def 1;

          then

           D1: (( - 1) * x) = (( - 1) * x1) by LM17;

          

          thus (x + t1) = (x1 + (( - 1) * x1)) by D1, LM16

          .= ( 0. ( RAlgebra NAT )) by FUNCSDOM: 11

          .= ( 0. S) by defAlgebra;

        end;

        for x,y be Element of S holds (x * y) = (y * x)

        proof

          let x,y be Element of S;

          reconsider x1 = x, y1 = y as Element of ( RAlgebra NAT ) by LM12;

          

          thus (x * y) = (x1 * y1) by LM15

          .= (y * x) by LM15;

        end;

        hence S is commutative;

        for x,y,z be Element of S holds ((x * y) * z) = (x * (y * z))

        proof

          let x,y,z be Element of S;

          reconsider x1 = x, y1 = y, z1 = z as Element of ( RAlgebra NAT ) by LM12;

          

           D1: (x * y) = (x1 * y1) by LM15;

          

           D2: (y * z) = (y1 * z1) by LM15;

          

          thus ((x * y) * z) = ((x1 * y1) * z1) by D1, LM15

          .= (x1 * (y1 * z1)) by GROUP_1:def 3

          .= (x * (y * z)) by D2, LM15;

        end;

        hence S is associative;

        thus S is right_unital

        proof

          let x be Element of S;

          reconsider x1 = x as Element of ( RAlgebra NAT ) by LM12;

          

          thus (x * ( 1. S)) = (x1 * ( 1. ( RAlgebra NAT ))) by LM19, LM15

          .= x by VECTSP_1:def 4;

        end;

        for x,y,z be Element of S holds (x * (y + z)) = ((x * y) + (x * z))

        proof

          let x,y,z be Element of S;

          reconsider x1 = x, y1 = y, z1 = z as Element of ( RAlgebra NAT ) by LM12;

          

           D1: (x * y) = (x1 * y1) by LM15;

          

           D2: (x * z) = (x1 * z1) by LM15;

          

           D3: (y + z) = (y1 + z1) by LM16;

          

          thus (x * (y + z)) = (x1 * (y1 + z1)) by D3, LM15

          .= ((x1 * y1) + (x1 * z1)) by VECTSP_1:def 2

          .= ((x * y) + (x * z)) by D1, D2, LM16;

        end;

        hence S is right-distributive;

        for x,y be Element of S holds for s be Real holds (s * (x * y)) = ((s * x) * y)

        proof

          let x,y be Element of S;

          let s be Real;

          reconsider x1 = x, y1 = y as Element of ( RAlgebra NAT ) by LM12;

          

           D1: (x * y) = (x1 * y1) by LM15;

          

           D3: s is Element of REAL by XREAL_0:def 1;

          then

           D2: (s * x) = (s * x1) by LM17;

          

          thus (s * (x * y)) = (s * (x1 * y1)) by LM17, D1, D3

          .= ((s * x1) * y1) by FUNCSDOM:def 9

          .= ((s * x) * y) by LM15, D2;

        end;

        hence S is vector-associative;

        for s,t be Real, x be Element of S holds ((s * t) * x) = (s * (t * x))

        proof

          let s,t be Real;

          let x be Element of S;

          reconsider x1 = x as Element of ( RAlgebra NAT ) by LM12;

          

           D0: s is Element of REAL & t is Element of REAL by XREAL_0:def 1;

          

           D2: (s * t) is Element of REAL by XREAL_0:def 1;

          

           D1: (t * x) = (t * x1) by D0, LM17;

          

          thus ((s * t) * x) = ((s * t) * x1) by D2, LM17

          .= (s * (t * x1)) by RLVECT_1:def 7

          .= (s * (t * x)) by D0, D1, LM17;

        end;

        hence S is scalar-associative;

        for s be Real holds for x,y be Element of S holds (s * (x + y)) = ((s * x) + (s * y))

        proof

          let s be Real;

          let x,y be Element of S;

          reconsider x1 = x, y1 = y as Element of ( RAlgebra NAT ) by LM12;

          

           D1: (x + y) = (x1 + y1) by LM16;

          

           D3: s is Element of REAL by XREAL_0:def 1;

          then

           D2: (s * x) = (s * x1) by LM17;

          

           D4: (s * y) = (s * y1) by LM17, D3;

          

          thus (s * (x + y)) = (s * (x1 + y1)) by LM17, D1, D3

          .= ((s * x1) + (s * y1)) by RLVECT_1:def 5

          .= ((s * x) + (s * y)) by LM16, D2, D4;

        end;

        hence S is vector-distributive;

        let s,t be Real, v be Element of S;

        reconsider s, t as Element of REAL by XREAL_0:def 1;

        reconsider v1 = v as Element of ( RAlgebra NAT ) by LM12;

        

         D2: (s * v) = (s * v1) by LM17;

        

         D4: (t * v) = (t * v1) by LM17;

        ((s + t) * v) = ((s + t) * v1) by LM17

        .= ((s * v1) + (t * v1)) by RLVECT_1:def 6

        .= ((s * v) + (t * v)) by D2, D4, LM16;

        hence thesis;

      end;

    end

    theorem :: ASYMPT_3:18

     R_Algebra_of_Big_Oh_poly is Algebra;

    theorem :: ASYMPT_3:19

    

     TH11: for f,g,h be VECTOR of R_Algebra_of_Big_Oh_poly holds for f9,g9,h9 be Function of NAT , REAL st f9 = f & g9 = g & h9 = h holds (h = (f + g) iff for x be Nat holds (h9 . x) = ((f9 . x) + (g9 . x)))

    proof

      let f,g,h be VECTOR of R_Algebra_of_Big_Oh_poly ;

      reconsider f1 = f, g1 = g, h1 = h as VECTOR of ( RAlgebra NAT ) by LM12;

      let f9,g9,h9 be Function of NAT , REAL such that

       A2: f9 = f & g9 = g & h9 = h;

       A3:

      now

        assume

         A4: h = (f + g);

        let x be Nat;

        

         LXN: x in NAT by ORDINAL1:def 12;

        h1 = (f1 + g1) by A4, LM16;

        hence (h9 . x) = ((f9 . x) + (g9 . x)) by A2, FUNCSDOM: 1, LXN;

      end;

      now

        assume

         LAS: for x be Nat holds (h9 . x) = ((f9 . x) + (g9 . x));

        for x be Element of NAT holds (h9 . x) = ((f9 . x) + (g9 . x)) by LAS;

        then h1 = (f1 + g1) by A2, FUNCSDOM: 1;

        hence h = (f + g) by LM16;

      end;

      hence thesis by A3;

    end;

    theorem :: ASYMPT_3:20

    

     TH11A: for f,g,h be VECTOR of R_Algebra_of_Big_Oh_poly holds for f9,g9,h9 be Function of NAT , REAL st f9 = f & g9 = g & h9 = h holds (h = (f * g) iff for x be Nat holds (h9 . x) = ((f9 . x) * (g9 . x)))

    proof

      let f,g,h be VECTOR of R_Algebra_of_Big_Oh_poly ;

      reconsider f1 = f, g1 = g, h1 = h as VECTOR of ( RAlgebra NAT ) by LM12;

      let f9,g9,h9 be Function of NAT , REAL such that

       A2: f9 = f & g9 = g & h9 = h;

       A3:

      now

        assume

         A4: h = (f * g);

        let x be Nat;

        

         LXN: x in NAT by ORDINAL1:def 12;

        h1 = (f1 * g1) by A4, LM15;

        hence (h9 . x) = ((f9 . x) * (g9 . x)) by A2, FUNCSDOM: 2, LXN;

      end;

      now

        assume for x be Element of NAT holds (h9 . x) = ((f9 . x) * (g9 . x));

        then h1 = (f1 * g1) by A2, FUNCSDOM: 2;

        hence h = (f * g) by LM15;

      end;

      hence thesis by A3;

    end;

    theorem :: ASYMPT_3:21

    

     TH12: for f,h be VECTOR of R_Algebra_of_Big_Oh_poly holds for f9,h9 be Function of NAT , REAL st f9 = f & h9 = h holds for a be Real holds h = (a * f) iff for x be Nat holds (h9 . x) = (a * (f9 . x))

    proof

      let f,h be VECTOR of R_Algebra_of_Big_Oh_poly ;

      let f9,h9 be Function of NAT , REAL such that

       A1: f9 = f & h9 = h;

      let a be Real;

      

       A0: a is Element of REAL by XREAL_0:def 1;

      reconsider f1 = f, h1 = h as VECTOR of ( RAlgebra NAT ) by LM12;

       A3:

      now

        assume

         A4: h = (a * f);

        let x be Nat;

        

         LXN: x in NAT by ORDINAL1:def 12;

        h1 = (a * f1) by A4, LM17, A0;

        hence (h9 . x) = (a * (f9 . x)) by A1, FUNCSDOM: 4, LXN;

      end;

      now

        assume for x be Element of NAT holds (h9 . x) = (a * (f9 . x));

        then h1 = (a * f1) by A1, FUNCSDOM: 4;

        hence h = (a * f) by A0, LM17;

      end;

      hence thesis by A3;

    end;

    begin

    definition

      let f be Function of NAT , REAL ;

      :: ASYMPT_3:def4

      attr f is negligible means

      : defneg: for c be non empty positive-yielding XFinSequence of REAL holds ex N be Nat st for x be Nat st N <= x holds |.(f . x).| < (1 / (( polynom c) . x));

    end

    theorem :: ASYMPT_3:22

    

     PXR1: for r be Real st 0 < r holds ex c be non empty positive-yielding XFinSequence of REAL st for x be Nat holds (( polynom c) . x) = r

    proof

      let r be Real;

      assume

       AS: 0 < r;

      r is Element of REAL by XREAL_0:def 1;

      then

      reconsider z = <%r%> as XFinSequence of REAL ;

      now

        let x be Real;

        assume x in ( rng z);

        then x in {r} by AFINSQ_1: 33;

        hence 0 < x by AS, TARSKI:def 1;

      end;

      then

       A1: z is positive-yielding;

      reconsider z as non empty positive-yielding XFinSequence of REAL by A1;

      take z;

      ( len z) = 1 by AFINSQ_1: 34;

      then

      consider a be Real such that

       A2: a = (z . 0 ) & for x be Nat holds (( seq_p z) . x) = a by ASYMPT_2: 29;

      thus thesis by A2;

    end;

    theorem :: ASYMPT_3:23

    

     PXR2: for f be Function of NAT , REAL st f is negligible holds for r be Real st 0 < r holds ex N be Nat st for x be Nat st N <= x holds |.(f . x).| < r

    proof

      let f be Function of NAT , REAL ;

      assume

       AS: f is negligible;

      let r be Real;

      assume 0 < r;

      then

      consider c be non empty positive-yielding XFinSequence of REAL such that

       P1: for x be Nat holds (( polynom c) . x) = (1 / r) by PXR1;

      consider N be Nat such that

       P2: for x be Nat st N <= x holds |.(f . x).| < (1 / (( polynom c) . x)) by AS;

      take N;

      thus for x be Nat st N <= x holds |.(f . x).| < r

      proof

        let x be Nat;

        assume N <= x;

        then |.(f . x).| < (1 / (( polynom c) . x)) by P2;

        then |.(f . x).| < (1 / (1 / r)) by P1;

        hence |.(f . x).| < r by XCMPLX_1: 52;

      end;

    end;

    theorem :: ASYMPT_3:24

    for f be Function of NAT , REAL st f is negligible holds f is convergent & ( lim f) = 0

    proof

      let f be Function of NAT , REAL ;

      assume

       AS: f is negligible;

      

       A1: for p be Real st 0 < p holds ex n be Nat st for m be Nat st n <= m holds |.((f . m) - 0 ).| < p

      proof

        let p be Real;

        assume 0 < p;

        then

        consider N be Nat such that

         P1: for x be Nat st N <= x holds |.(f . x).| < p by AS, PXR2;

        reconsider N as Nat;

        take N;

        let m be Nat;

        assume

         P2: N <= m;

        reconsider x = m as Element of NAT by ORDINAL1:def 12;

        thus |.((f . m) - 0 ).| < p by P1, P2;

      end;

      hence f is convergent by SEQ_2:def 6;

      hence ( lim f) = 0 by A1, SEQ_2:def 7;

    end;

    registration

      cluster ( seq_const 0 ) -> negligible;

      coherence

      proof

        set f = ( seq_const 0 );

        let c be non empty positive-yielding XFinSequence of REAL ;

        take N = 0 ;

        let x be Nat;

        

         D2: |.(f . x).| = |. 0 .| by SEQ_1: 57

        .= 0 ;

         0 < (( polynom c) . x) by NLM3;

        hence thesis by D2;

      end;

    end

    registration

      cluster negligible for Function of NAT , REAL ;

      correctness

      proof

        ( seq_const 0 ) is negligible;

        hence thesis;

      end;

    end

    registration

      let f be negligible Function of NAT , REAL ;

      cluster |.f.| -> negligible;

      coherence

      proof

        let g be Function of NAT , REAL such that

         A1: g = |.f.|;

        let c be non empty positive-yielding XFinSequence of REAL ;

        consider N be Nat such that

         D3: for x be Nat st N <= x holds |.(f . x).| < (1 / (( polynom c) . x)) by defneg;

        take N;

        let x be Nat;

        assume

         B1: N <= x;

         |.( |.f.| . x).| = |. |.(f . x).|.| by SEQ_1: 12

        .= |.(f . x).|;

        hence thesis by A1, D3, B1;

      end;

    end

    registration

      let f be negligible Function of NAT , REAL , a be Real;

      cluster (a (#) f) -> negligible;

      coherence

      proof

        let g be Function of NAT , REAL such that

         A1: g = (a (#) f);

        let c be non empty positive-yielding XFinSequence of REAL ;

        per cases ;

          suppose

           D1: a = 0 ;

          take N = 0 ;

          let x be Nat;

          assume N <= x;

          

           D2: |.((a (#) f) . x).| = |.(a * (f . x)).| by VALUED_1: 6

          .= 0 by D1;

           0 < (( polynom c) . x) by NLM3;

          hence thesis by A1, D2;

        end;

          suppose

           F1: a <> 0 ;

          reconsider c1 = ( |.a.| (#) c) as non empty positive-yielding XFinSequence of REAL by NLM2, F1;

          consider N be Nat such that

           F3: for x be Nat st N <= x holds |.(f . x).| < (1 / (( polynom c1) . x)) by defneg;

          take N;

          let x be Nat;

          assume

           F4: N <= x;

          

           K2: 0 < (( polynom c) . x) by NLM3;

          

           F6: (( polynom c1) . x) = ( |.a.| * (( polynom c) . x)) by NLM4;

          

           K4: 0 < (( polynom c1) . x) by NLM3;

           |.(f . x).| < (1 / (( polynom c1) . x)) by F3, F4;

          then ( |.(f . x).| * (( polynom c1) . x)) < ((1 / (( polynom c1) . x)) * (( polynom c1) . x)) by K4, XREAL_1: 68;

          then (( |.(f . x).| * |.a.|) * (( polynom c) . x)) < 1 by F6, K4, XCMPLX_1: 87;

          then ( |.(a * (f . x)).| * (( polynom c) . x)) < 1 by COMPLEX1: 65;

          then ( |.((a (#) f) . x).| * (( polynom c) . x)) < 1 by VALUED_1: 6;

          then (( |.((a (#) f) . x).| * (( polynom c) . x)) / (( polynom c) . x)) < (1 / (( polynom c) . x)) by K2, XREAL_1: 74;

          hence thesis by A1, K2, XCMPLX_1: 89;

        end;

      end;

    end

    registration

      let f,g be negligible Function of NAT , REAL ;

      cluster (f + g) -> negligible;

      coherence

      proof

        let h be Function of NAT , REAL such that

         A0: h = (f + g);

        let c be non empty positive-yielding XFinSequence of REAL ;

        reconsider c1 = (2 (#) c) as non empty positive-yielding XFinSequence of REAL by NLM2;

        consider N1 be Nat such that

         D1: for x be Nat st N1 <= x holds |.(f . x).| < (1 / (( polynom c1) . x)) by defneg;

        consider N2 be Nat such that

         D2: for x be Nat st N2 <= x holds |.(g . x).| < (1 / (( polynom c1) . x)) by defneg;

        take N = (N1 + N2);

        let x be Nat;

        assume

         D3: N <= x;

        N1 <= N by NAT_1: 12;

        then N1 <= x by D3, XXREAL_0: 2;

        then

         D4: |.(f . x).| < (1 / (( polynom c1) . x)) by D1;

        N2 <= N by NAT_1: 12;

        then N2 <= x by D3, XXREAL_0: 2;

        then

         D5: |.(g . x).| < (1 / (( polynom c1) . x)) by D2;

        

         F6: (( polynom c1) . x) = (2 * (( polynom c) . x)) by NLM4;

         |.((f + g) . x).| = |.((f . x) + (g . x)).|

        proof

          x in NAT by ORDINAL1:def 12;

          hence thesis by VALUED_1: 1;

        end;

        then

         D6: |.((f + g) . x).| <= ( |.(f . x).| + |.(g . x).|) by COMPLEX1: 56;

        ( |.(f . x).| + |.(g . x).|) < ((1 / (( polynom c1) . x)) + (1 / (( polynom c1) . x))) by D4, D5, XREAL_1: 8;

        then |.((f + g) . x).| < (2 * (1 / (( polynom c1) . x))) by XXREAL_0: 2, D6;

        hence thesis by A0, XCMPLX_1: 92, F6;

      end;

    end

    registration

      let f,g be negligible Function of NAT , REAL ;

      cluster (f (#) g) -> negligible;

      coherence

      proof

        let h be Function of NAT , REAL such that

         A0: h = (f (#) g);

        let c1 be non empty positive-yielding XFinSequence of REAL ;

        consider N1 be Nat such that

         D1: for x be Nat st N1 <= x holds |.(f . x).| < (1 / 2) by PXR2;

        consider N2 be Nat such that

         D2: for x be Nat st N2 <= x holds |.(g . x).| < (1 / (( polynom c1) . x)) by defneg;

        take N = (N1 + N2);

        let x be Nat;

        assume

         D3: N <= x;

        N1 <= N by NAT_1: 12;

        then N1 <= x by D3, XXREAL_0: 2;

        then

         D4: |.(f . x).| < (1 / 2) by D1;

        N2 <= N by NAT_1: 12;

        then N2 <= x by D3, XXREAL_0: 2;

        then

         D5: |.(g . x).| < (1 / (( polynom c1) . x)) by D2;

        then

         F6: ((1 / 2) * (1 / (( polynom c1) . x))) < (1 * (1 / (( polynom c1) . x))) by XREAL_1: 97;

         |.((f (#) g) . x).| = |.((f . x) * (g . x)).| by VALUED_1: 5;

        then

         D6: |.((f (#) g) . x).| = ( |.(f . x).| * |.(g . x).|) by COMPLEX1: 65;

        ( |.(f . x).| * |.(g . x).|) <= ((1 / 2) * (1 / (( polynom c1) . x))) by D4, D5, XREAL_1: 66;

        hence thesis by A0, F6, XXREAL_0: 2, D6;

      end;

    end

    theorem :: ASYMPT_3:25

    

     TH3: for f be Function of NAT , REAL st for x be Nat holds (f . x) = (1 / (2 to_power x)) holds f is negligible

    proof

      let f be Function of NAT , REAL ;

      assume

       AS: for x be Nat holds (f . x) = (1 / (2 to_power x));

      let c be non empty positive-yielding XFinSequence of REAL ;

      set k = ( len c);

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

      consider y be Real_Sequence such that

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

      consider N1 be Nat such that

       P2: for x be Nat st N1 <= x holds |.(( seq_p c) . x).| <= (y . x) by ASYMPT_2: 43, P1;

      consider N2 be Nat such that

       P3: for x be Nat st N2 <= x holds (1 / (2 to_power x)) < (1 / (x to_power k)) by L2;

      set N = (N1 + N2);

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

      take N;

      thus for x be Nat st N <= x holds |.(f . x).| < (1 / (( polynom c) . x))

      proof

        let x be Nat;

        assume

         D3: N <= x;

        

         K1: (f . x) = (1 / (2 to_power x)) by AS;

        N2 <= N by NAT_1: 12;

        then N2 <= x by D3, XXREAL_0: 2;

        then (1 / (2 to_power x)) < (1 / (x to_power k)) by P3;

        then

         P4: |.(f . x).| < (1 / (x to_power k)) by K1, ABSVALUE:def 1;

        N1 <= N by NAT_1: 12;

        then N1 <= x by D3, XXREAL_0: 2;

        then |.(( polynom c) . x).| <= (y . x) by P2;

        then (( polynom c) . x) <= (y . x) by ABSVALUE:def 1;

        then (( polynom c) . x) <= (1 * (x to_power k)) by P1;

        then (1 / (x to_power k)) <= (1 / (( polynom c) . x)) by XREAL_1: 118, NLM3;

        hence |.(f . x).| < (1 / (( polynom c) . x)) by P4, XXREAL_0: 2;

      end;

    end;

    theorem :: ASYMPT_3:26

    

     TH4: for f,g be Function of NAT , REAL st f is negligible & for x be Nat holds |.(g . x).| <= |.(f . x).| holds g is negligible

    proof

      let f,g be Function of NAT , REAL ;

      assume

       AS: f is negligible & for x be Nat holds |.(g . x).| <= |.(f . x).|;

      thus g is negligible

      proof

        let c be non empty positive-yielding XFinSequence of REAL ;

        consider N be Nat such that

         D3: for x be Nat st N <= x holds |.(f . x).| < (1 / (( polynom c) . x)) by AS;

        take N;

        let x be Nat;

        assume N <= x;

        then

         D2: |.(f . x).| < (1 / (( polynom c) . x)) by D3;

         |.(g . x).| <= |.(f . x).| by AS;

        hence thesis by D2, XXREAL_0: 2;

      end;

    end;

    registration

      cluster negligible -> polynomially-abs-bounded for Function of NAT , REAL ;

      coherence

      proof

        let f be Function of NAT , REAL ;

        assume

         A0: f is negligible;

        consider c be non empty positive-yielding XFinSequence of REAL such that

         P1: for x be Nat holds (( polynom c) . x) = 1 by PXR1;

        consider N be Nat such that

         P2: for x be Nat st N <= x holds |.(f . x).| < (1 / (( polynom c) . x)) by A0;

        set s = |.f.|;

        

         ZP1: s in ( Funcs ( NAT , REAL )) by FUNCT_2: 8;

        now

          let n be Element of NAT ;

          assume

           A2: n >= (N + 2);

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

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

          then

           A3: n > 1 by XXREAL_0: 2;

          

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

          .= n;

          

           A5: (s . n) = |.(f . n).| by VALUED_1: 18;

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

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

          then (s . n) < (1 / (( polynom c) . n)) by A5, P2;

          then (s . n) < (1 / 1) by P1;

          hence (s . n) <= (1 * (( seq_n^ 1) . n)) by XXREAL_0: 2, A3, A4;

          thus (s . n) >= 0 by A5;

        end;

        then s in ( Big_Oh ( seq_n^ 1)) by ZP1;

        hence thesis;

      end;

    end

    definition

      :: ASYMPT_3:def5

      func negligibleFuncs -> Subset of Big_Oh_poly means

      : Def1: for x be object holds x in it iff x is negligible Function of NAT , REAL ;

      existence

      proof

        defpred P[ object] means $1 is negligible Function of NAT , REAL ;

        consider IT be set such that

         A01: for x be object holds x in IT iff x in ( Funcs ( NAT , REAL )) & P[x] from XBOOLE_0:sch 1;

        

         A1: for x be object holds x in IT iff x is negligible Function of NAT , REAL

        proof

          let x be object;

          x is negligible Function of NAT , REAL implies x in ( Funcs ( NAT , REAL )) by FUNCT_2: 8;

          hence thesis by A01;

        end;

        for x be object st x in IT holds x in Big_Oh_poly

        proof

          let x be object;

          assume x in IT;

          then x is negligible Function of NAT , REAL by A1;

          hence x in Big_Oh_poly by DefX1;

        end;

        then IT is Subset of Big_Oh_poly by TARSKI:def 3;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of Big_Oh_poly ;

        assume that

         A2: for x be object holds x in X1 iff x is negligible Function of NAT , REAL and

         A3: for x be object holds x in X2 iff x is negligible Function of NAT , REAL ;

        thus X1 c= X2

        proof

          let x be object;

          assume x in X1;

          then x is negligible Function of NAT , REAL by A2;

          hence thesis by A3;

        end;

        let x be object;

        assume x in X2;

        then x is negligible Function of NAT , REAL by A3;

        hence thesis by A2;

      end;

    end

    registration

      cluster negligibleFuncs -> non empty;

      coherence

      proof

         the negligible Function of NAT , REAL in negligibleFuncs by Def1;

        hence thesis;

      end;

    end

    theorem :: ASYMPT_3:27

    

     RSSPAC2: for v,w be VECTOR of R_Algebra_of_Big_Oh_poly , v1,w1 be Function of NAT , REAL st v = v1 & w1 = w holds (v + w) = (v1 + w1)

    proof

      let v,w be VECTOR of R_Algebra_of_Big_Oh_poly , v1,w1 be Function of NAT , REAL ;

      assume

       A0: v = v1 & w1 = w;

      (v + w) in the carrier of R_Algebra_of_Big_Oh_poly ;

      then (v + w) in Big_Oh_poly by defAlgebra;

      then

      reconsider h = (v + w) as Function of NAT , REAL by DefX1;

      h = (v1 + w1)

      proof

        let n be Element of NAT ;

        

        thus (h . n) = ((v1 . n) + (w1 . n)) by A0, TH11

        .= ((v1 + w1) . n) by VALUED_1: 1;

      end;

      hence (v + w) = (v1 + w1);

    end;

    theorem :: ASYMPT_3:28

    

     RSSPAC2A: for v,w be VECTOR of R_Algebra_of_Big_Oh_poly , v1,w1 be Function of NAT , REAL st v = v1 & w1 = w holds (v * w) = (v1 (#) w1)

    proof

      let v,w be VECTOR of R_Algebra_of_Big_Oh_poly , v1,w1 be Function of NAT , REAL ;

      assume

       A0: v = v1 & w1 = w;

      (v * w) in the carrier of R_Algebra_of_Big_Oh_poly ;

      then (v * w) in Big_Oh_poly by defAlgebra;

      then

      reconsider h = (v * w) as Function of NAT , REAL by DefX1;

      h = (v1 (#) w1)

      proof

        let n be Element of NAT ;

        

        thus (h . n) = ((v1 . n) * (w1 . n)) by TH11A, A0

        .= ((v1 (#) w1) . n) by VALUED_1: 5;

      end;

      hence (v * w) = (v1 (#) w1);

    end;

    theorem :: ASYMPT_3:29

    

     RSSPAC3: for a be Real, v be VECTOR of R_Algebra_of_Big_Oh_poly , v1 be Function of NAT , REAL st v = v1 holds (a * v) = (a (#) v1)

    proof

      let a be Real;

      let v be VECTOR of R_Algebra_of_Big_Oh_poly , v1 be Function of NAT , REAL ;

      assume

       A0: v = v1;

      (a * v) in the carrier of R_Algebra_of_Big_Oh_poly ;

      then (a * v) in Big_Oh_poly by defAlgebra;

      then

      reconsider h = (a * v) as Function of NAT , REAL by DefX1;

      h = (a (#) v1)

      proof

        let n be Element of NAT ;

        

        thus (h . n) = (a * (v1 . n)) by TH12, A0

        .= ((a (#) v1) . n) by VALUED_1: 6;

      end;

      hence (a * v) = (a (#) v1);

    end;

    theorem :: ASYMPT_3:30

    for a be Real holds for v be VECTOR of R_Algebra_of_Big_Oh_poly st v in negligibleFuncs holds (a * v) in negligibleFuncs

    proof

      let a be Real;

      let v be VECTOR of R_Algebra_of_Big_Oh_poly ;

      assume v in negligibleFuncs ;

      then

      reconsider v1 = v as negligible Function of NAT , REAL by Def1;

      (a (#) v1) is negligible;

      then (a * v) is negligible Function of NAT , REAL by RSSPAC3;

      hence thesis by Def1;

    end;

    theorem :: ASYMPT_3:31

    for v,u be VECTOR of R_Algebra_of_Big_Oh_poly st v in negligibleFuncs & u in negligibleFuncs holds (v + u) in negligibleFuncs

    proof

      let v,u be VECTOR of R_Algebra_of_Big_Oh_poly ;

      assume v in negligibleFuncs & u in negligibleFuncs ;

      then

      reconsider v1 = v, u1 = u as negligible Function of NAT , REAL by Def1;

      (v1 + u1) is negligible;

      then (v + u) is negligible Function of NAT , REAL by RSSPAC2;

      hence thesis by Def1;

    end;

    theorem :: ASYMPT_3:32

    for v,u be VECTOR of R_Algebra_of_Big_Oh_poly st v in negligibleFuncs & u in negligibleFuncs holds (v * u) in negligibleFuncs

    proof

      let v,u be VECTOR of R_Algebra_of_Big_Oh_poly ;

      assume v in negligibleFuncs & u in negligibleFuncs ;

      then

      reconsider v1 = v, u1 = u as negligible Function of NAT , REAL by Def1;

      (v1 (#) u1) is negligible;

      then (v * u) is negligible Function of NAT , REAL by RSSPAC2A;

      hence thesis by Def1;

    end;

    definition

      let f,g be Function of NAT , REAL ;

      :: ASYMPT_3:def6

      pred f negligibleEQ g means ex h be Function of NAT , REAL st h is negligible & for x be Nat holds |.((f . x) - (g . x)).| <= |.(h . x).|;

      reflexivity

      proof

        let f be Function of NAT , REAL ;

        deffunc F( Nat) = (1 / (2 to_power $1));

        consider h be Real_Sequence such that

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

        take h;

        thus h is negligible by TH3, P1;

        let x be Nat;

         |.((f . x) - (f . x)).| = 0 ;

        hence |.((f . x) - (f . x)).| <= |.(h . x).|;

      end;

      symmetry

      proof

        let f,g be Function of NAT , REAL ;

        given h be Function of NAT , REAL such that

         P1: h is negligible & for x be Nat holds |.((f . x) - (g . x)).| <= |.(h . x).|;

        take h;

        thus h is negligible by P1;

        let x be Nat;

         |.((f . x) - (g . x)).| <= |.(h . x).| by P1;

        hence |.((g . x) - (f . x)).| <= |.(h . x).| by COMPLEX1: 60;

      end;

    end

    theorem :: ASYMPT_3:33

    for f,g,h be Function of NAT , REAL st f negligibleEQ g & g negligibleEQ h holds f negligibleEQ h

    proof

      let f,g,h be Function of NAT , REAL ;

      given v be Function of NAT , REAL such that

       B1: v is negligible & for x be Nat holds |.((f . x) - (g . x)).| <= |.(v . x).|;

      given w be Function of NAT , REAL such that

       B2: w is negligible & for x be Nat holds |.((g . x) - (h . x)).| <= |.(w . x).|;

      take u = ( |.v.| + |.w.|);

      thus u is negligible by B1, B2;

      let x be Nat;

      

       B4: |.((f . x) - (g . x)).| <= |.(v . x).| by B1;

      

       B5: |.((g . x) - (h . x)).| <= |.(w . x).| by B2;

       |.((f . x) - (h . x)).| = |.(((f . x) - (g . x)) + ((g . x) - (h . x))).|;

      then

       B6: |.((f . x) - (h . x)).| <= ( |.((f . x) - (g . x)).| + |.((g . x) - (h . x)).|) by COMPLEX1: 56;

      ( |.((f . x) - (g . x)).| + |.((g . x) - (h . x)).|) <= ( |.(v . x).| + |.(w . x).|) by B4, B5, XREAL_1: 7;

      then

       B7: |.((f . x) - (h . x)).| <= ( |.(v . x).| + |.(w . x).|) by B6, XXREAL_0: 2;

      x in NAT by ORDINAL1:def 12;

      then

      consider y be Element of NAT such that

       LXY: x = y;

      ( |.(v . x).| + |.(w . x).|) = (( |.v.| . x) + |.(w . x).|) by SEQ_1: 12

      .= (( |.v.| . x) + ( |.w.| . x)) by SEQ_1: 12

      .= (( |.v.| + |.w.|) . x) by LXY, VALUED_1: 1;

      hence |.((f . x) - (h . x)).| <= |.(u . x).| by B7, ABSVALUE:def 1;

    end;

    theorem :: ASYMPT_3:34

    for f,g be Function of NAT , REAL holds f negligibleEQ g iff (f - g) is negligible

    proof

      let f,g be Function of NAT , REAL ;

      hereby

        assume

         A1: f negligibleEQ g;

        consider v be Function of NAT , REAL such that

         B1: v is negligible & for x be Nat holds |.((f . x) - (g . x)).| <= |.(v . x).| by A1;

        for x be Nat holds |.((f - g) . x).| <= |.(v . x).|

        proof

          let x be Nat;

          x in NAT by ORDINAL1:def 12;

          then

          consider y be Element of NAT such that

           LXY: x = y;

           |.((f - g) . y).| = |.((f . y) - (g . y)).| by VALUED_1: 15;

          hence thesis by B1, LXY;

        end;

        hence (f - g) is negligible by B1, TH4;

      end;

      set v = (f - g);

      for x be Nat holds |.((f . x) - (g . x)).| <= |.(v . x).|

      proof

        let x be Nat;

        x in NAT by ORDINAL1:def 12;

        hence thesis by VALUED_1: 15;

      end;

      hence thesis;

    end;

    theorem :: ASYMPT_3:35

    

     LRNG1: for c be non empty positive-yielding XFinSequence of REAL holds ex a be Real, k,N be Nat st 0 < a & 0 < k & for x be Nat st N <= x holds (( polynom c) . x) <= (a * (x to_power k))

    proof

      let c be non empty positive-yielding XFinSequence of REAL ;

      (1 - 1) <= (( len c) - 1) by XREAL_1: 9, NAT_1: 14;

      then (( len c) - 1) in NAT by INT_1: 3;

      then

      reconsider k = (( len c) - 1) as Nat;

      

       C1: ( len c) = (k + 1);

      ((k + 1) - 1) < (( len c) - 0 ) by XREAL_1: 15;

      then k in ( Segm ( len c)) by NAT_1: 44;

      then

       C2: (c . k) in ( rng c) by FUNCT_1: 3;

      for n be Nat st 0 <= n holds 0 <= (( seq_p c) . n) by NLM3;

      then

      reconsider f = ( seq_p c) as eventually-nonnegative Real_Sequence by ASYMPT_0:def 2;

      f in ( Big_Oh ( seq_n^ k)) by ASYMPT_2: 45, C1, C2, PARTFUN3:def 1;

      then

      consider N be Nat such that

       C5: for x be Nat st N <= x holds (f . x) <= (( seq_n^ (k + 1)) . x) by ASYMPT_2: 39;

      reconsider m = (k + 1) as Nat;

      reconsider M = (N + 1) as Nat;

      take 1, m, M;

      for x be Nat st M <= x holds (f . x) <= (1 * (x to_power m))

      proof

        let x be Nat;

        assume

         C8: M <= x;

        

         CX: x is Element of NAT by ORDINAL1:def 12;

        ((N + 1) - 1) < (M - 0 ) by XREAL_1: 15;

        then N < x by C8, XXREAL_0: 2;

        then (f . x) <= (( seq_n^ m) . x) by C5;

        hence thesis by C8, ASYMPT_1:def 3, CX;

      end;

      hence thesis;

    end;

    registration

      let a be nonnegative-yielding XFinSequence of REAL , b be nonnegative-yielding Real_Sequence;

      cluster (a (#) b) -> nonnegative-yielding;

      coherence

      proof

        for r be Real st r in ( rng (a (#) b)) holds 0 <= r

        proof

          let r be Real;

          assume r in ( rng (a (#) b));

          then

          consider x be object such that

           AS1: x in ( dom (a (#) b)) & r = ((a (#) b) . x) by FUNCT_1:def 3;

          x in (( dom a) /\ ( dom b)) by AS1, VALUED_1:def 4;

          then x in ( dom a) & x in ( dom b) by XBOOLE_0:def 4;

          then (a . x) in ( rng a) & (b . x) in ( rng b) by FUNCT_1: 3;

          then

           L1: 0 <= (a . x) & 0 <= (b . x) by PARTFUN3:def 4;

          ((a (#) b) . x) = ((a . x) * (b . x)) by AS1, VALUED_1:def 4;

          hence thesis by L1, AS1;

        end;

        hence thesis;

      end;

    end

    registration

      let a,b be nonnegative-yielding XFinSequence of REAL ;

      cluster (a ^ b) -> nonnegative-yielding;

      coherence

      proof

        for r be Real st r in ( rng (a ^ b)) holds 0 <= r

        proof

          let r be Real;

          assume r in ( rng (a ^ b));

          then r in (( rng a) \/ ( rng b)) by AFINSQ_1: 26;

          then r in ( rng a) or r in ( rng b) by XBOOLE_0:def 3;

          hence thesis by PARTFUN3:def 4;

        end;

        hence thesis;

      end;

    end

    registration

      let a,b,c be non negative Real;

      cluster ( seq_a^ (a,b,c)) -> nonnegative-yielding;

      coherence

      proof

        set f = ( seq_a^ (a,b,c));

        for r be Real st r in ( rng f) holds r >= 0

        proof

          let r be Real;

          assume r in ( rng f);

          then

          consider n be object such that

           A2: n in ( dom f) & r = (f . n) by FUNCT_1:def 3;

          reconsider n as Element of NAT by A2;

          

           LL1: r = (a to_power ((b * n) + c)) by ASYMPT_1:def 1, A2;

          now

            per cases ;

              case

               CA0: a = 0 ;

              now

                per cases ;

                  case ((b * n) + c) <> 0 ;

                  hence thesis by CA0, LL1, POWER:def 2;

                end;

                  case ((b * n) + c) = 0 ;

                  hence thesis by POWER: 24, LL1;

                end;

              end;

              hence thesis;

            end;

              case 0 < a;

              hence thesis by LL1, POWER: 34;

            end;

          end;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: ASYMPT_3:36

    

     LRNG2: for a be Real, k be Nat holds ex c be non empty positive-yielding XFinSequence of REAL st for x be Nat holds (a * (x to_power k)) <= (( polynom c) . x)

    proof

      let a be Real, k be Nat;

      reconsider c = (( Segm (k + 1)) --> ( |.a.| + 1)) as XFinSequence of REAL by AFINSQ_1: 63, XREAL_0:def 1;

      reconsider c as non empty positive-yielding XFinSequence of REAL ;

      take c;

      for x be Nat holds (a * (x to_power k)) <= (( polynom c) . x)

      proof

        let x be Nat;

        set c2 = (c (#) ( seq_a^ (x,1, 0 )));

        

         T0: (( polynom c) . x) = ( Sum c2) by ASYMPT_2:def 2;

        

         LN2: (k + 0 ) < (k + 1) by XREAL_1: 8;

        

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

        .= (( dom c) /\ NAT ) by SEQ_1: 1

        .= (( Segm (k + 1)) /\ NAT );

        

         T3: (c2 . k) = ((c . k) * (( seq_a^ (x,1, 0 )) . k)) by VALUED_1: 5

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

        .= (( |.a.| + 1) * (x to_power k)) by FUNCOP_1: 7, NAT_1: 44, LN2;

        a < ( |.a.| + 1) by TCL001;

        then

         T4: (a * (x to_power k)) <= (( |.a.| + 1) * (x to_power k)) by XREAL_1: 64;

        ( len c2) = (k + 1) by T1, XBOOLE_1: 28;

        then ( Sum c2) >= (( |.a.| + 1) * (x to_power k)) by T3, AFINSQ_2: 61, NAT_1: 44, LN2;

        hence thesis by T4, XXREAL_0: 2, T0;

      end;

      hence thesis;

    end;

    theorem :: ASYMPT_3:37

    

     RNG0: for c,s be non empty positive-yielding XFinSequence of REAL holds ex d be non empty positive-yielding XFinSequence of REAL , N be Nat st for x be Nat st N <= x holds ((( polynom c) . x) * (( polynom s) . x)) <= (( polynom d) . x)

    proof

      let c,s be non empty positive-yielding XFinSequence of REAL ;

      consider a1 be Real, k1,N1 be Nat such that

       P1: 0 < a1 & 0 < k1 & for x be Nat st N1 <= x holds (( polynom c) . x) <= (a1 * (x to_power k1)) by LRNG1;

      consider a2 be Real, k2,N2 be Nat such that

       P2: 0 < a2 & 0 < k2 & for x be Nat st N2 <= x holds (( polynom s) . x) <= (a2 * (x to_power k2)) by LRNG1;

      consider d be non empty positive-yielding XFinSequence of REAL such that

       P3: for x be Nat holds ((a1 * a2) * (x to_power (k1 + k2))) <= (( polynom d) . x) by LRNG2;

      set N = (N1 + N2);

      take d, N;

      let x be Nat;

      assume

       P4: N <= x;

      N1 <= N by NAT_1: 12;

      then N1 <= x by XXREAL_0: 2, P4;

      then

       P5: (( polynom c) . x) <= (a1 * (x to_power k1)) by P1;

      N2 <= N by NAT_1: 12;

      then N2 <= x by XXREAL_0: 2, P4;

      then

       P6: (( polynom s) . x) <= (a2 * (x to_power k2)) by P2;

      

       P7: 0 < (( polynom c) . x) by NLM3;

      

       P8: 0 < (( polynom s) . x) by NLM3;

      

       P9: ((( polynom c) . x) * (( polynom s) . x)) <= ((a1 * (x to_power k1)) * (a2 * (x to_power k2))) by XREAL_1: 66, P5, P6, P7, P8;

      

       P10: ((a1 * (x to_power k1)) * (a2 * (x to_power k2))) = ((a1 * a2) * (x to_power (k1 + k2)))

      proof

        per cases ;

          suppose

           P11: x = 0 ;

          

           P12: (x to_power k1) = 0 by P1, P11, POWER:def 2;

          (x to_power (k1 + k2)) = 0 by P2, P11, POWER:def 2;

          hence thesis by P12;

        end;

          suppose x <> 0 ;

          then ((x to_power k1) * (x to_power k2)) = (x to_power (k1 + k2)) by POWER: 27;

          hence thesis;

        end;

      end;

      ((a1 * a2) * (x to_power (k1 + k2))) <= (( polynom d) . x) by P3;

      hence ((( polynom c) . x) * (( polynom s) . x)) <= (( polynom d) . x) by P9, P10, XXREAL_0: 2;

    end;

    registration

      let f be negligible Function of NAT , REAL , c be non empty positive-yielding XFinSequence of REAL ;

      cluster (( polynom c) (#) f) -> negligible;

      coherence

      proof

        let g be Function of NAT , REAL such that

         A0: g = (( polynom c) (#) f);

        let s be non empty positive-yielding XFinSequence of REAL ;

        consider d be non empty positive-yielding XFinSequence of REAL , N0 be Nat such that

         P1: for x be Nat st N0 <= x holds ((( polynom c) . x) * (( polynom s) . x)) <= (( polynom d) . x) by RNG0;

        consider N1 be Nat such that

         P2: for x be Nat st N1 <= x holds |.(f . x).| < (1 / (( polynom d) . x)) by defneg;

        take N = (N0 + N1);

        let x be Nat;

        assume

         P3: N <= x;

        

         P4: 0 < (( polynom c) . x) by NLM3;

        

         Q4: 0 < (( polynom d) . x) by NLM3;

        N1 <= N by NAT_1: 12;

        then N1 <= x by P3, XXREAL_0: 2;

        then

         P7: |.(f . x).| < (1 / (( polynom d) . x)) by P2;

        

         P6: ( |.(f . x).| * (( polynom c) . x)) < ((1 / (( polynom d) . x)) * (( polynom c) . x)) by P7, P4, XREAL_1: 97;

        

         Q6: 0 < (( polynom s) . x) by NLM3;

        N0 <= N by NAT_1: 12;

        then N0 <= x by P3, XXREAL_0: 2;

        then ((( polynom c) . x) * (( polynom s) . x)) <= (( polynom d) . x) by P1;

        then (1 / (( polynom d) . x)) <= (1 / ((( polynom c) . x) * (( polynom s) . x))) by P4, Q6, XREAL_1: 118;

        then

         P8: ((1 / (( polynom d) . x)) * (( polynom c) . x)) <= ((1 / ((( polynom c) . x) * (( polynom s) . x))) * (( polynom c) . x)) by Q4, P4, XREAL_1: 66;

        

         P5: ((1 / ((( polynom c) . x) * (( polynom s) . x))) * (( polynom c) . x)) = (1 / (( polynom s) . x)) by P4, XCMPLX_1: 92;

        ( |.(f . x).| * (( polynom c) . x)) = ( |.(f . x).| * |.(( polynom c) . x).|) by P4, ABSVALUE:def 1

        .= |.((( polynom c) . x) * (f . x)).| by COMPLEX1: 65

        .= |.((( polynom c) (#) f) . x).| by VALUED_1: 5;

        hence thesis by A0, P5, XXREAL_0: 2, P6, P8;

      end;

    end

    theorem :: ASYMPT_3:38

    

     RNG2: for g be polynomially-abs-bounded Function of NAT , REAL holds ex d be non empty positive-yielding XFinSequence of REAL , N be Nat st for x be Nat st N <= x holds |.(g . x).| <= (( polynom d) . x)

    proof

      let g be polynomially-abs-bounded Function of NAT , REAL ;

      consider k1 be Nat such that

       A4: |.g.| in ( Big_Oh ( seq_n^ k1)) by defabs;

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

       A6: |.g.| = t1 & ex c1 be Real, N1 be Element of NAT st c1 > 0 & for n be Element of NAT st n >= N1 holds (t1 . n) <= (c1 * (( seq_n^ k1) . n)) & (t1 . n) >= 0 by A4;

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

       A7: c1 > 0 & for n be Element of NAT st n >= N1 holds (t1 . n) <= (c1 * (( seq_n^ k1) . n)) & (t1 . n) >= 0 by A6;

      consider d be non empty positive-yielding XFinSequence of REAL such that

       A8: for x be Nat holds (c1 * (x to_power k1)) <= (( polynom d) . x) by LRNG2;

      reconsider N = (N1 + 1) as Nat;

      take d, N;

      let x be Nat;

      assume

       B1: N <= x;

      

       LXN: x is Element of NAT by ORDINAL1:def 12;

      N1 <= N by NAT_1: 12;

      then N1 <= x by XXREAL_0: 2, B1;

      then

       A9: (t1 . x) <= (c1 * (( seq_n^ k1) . x)) & (t1 . x) >= 0 by A7, LXN;

      

       A10: (( seq_n^ k1) . x) = (x to_power k1) by ASYMPT_1:def 3, LXN, B1;

      (c1 * (x to_power k1)) <= (( polynom d) . x) by A8;

      then (t1 . x) <= (( polynom d) . x) by A10, A9, XXREAL_0: 2;

      hence |.(g . x).| <= (( polynom d) . x) by A6, VALUED_1: 18;

    end;

    registration

      let f be negligible Function of NAT , REAL , g be polynomially-abs-bounded Function of NAT , REAL ;

      cluster (g (#) f) -> negligible;

      coherence

      proof

        let h be Function of NAT , REAL such that

         A0: h = (g (#) f);

        consider s be non empty positive-yielding XFinSequence of REAL , N0 be Nat such that

         P1: for x be Nat st N0 <= x holds |.(g . x).| <= (( polynom s) . x) by RNG2;

        let d be non empty positive-yielding XFinSequence of REAL ;

        (( polynom s) (#) f) is negligible;

        then

        consider N1 be Nat such that

         P2: for x be Nat st N1 <= x holds |.((( polynom s) (#) f) . x).| < (1 / (( polynom d) . x));

        take N = (N1 + N0);

        let x be Nat;

        assume

         P3: N <= x;

        

         P4: |.((g (#) f) . x).| = |.((g . x) * (f . x)).| by VALUED_1: 5

        .= ( |.(g . x).| * |.(f . x).|) by COMPLEX1: 65;

        N0 <= N by NAT_1: 12;

        then N0 <= x by XXREAL_0: 2, P3;

        then

         P6: |.(g . x).| <= (( polynom s) . x) by P1;

        

         Q7: 0 < (( polynom s) . x) by NLM3;

        ((( polynom s) . x) * |.(f . x).|) = ( |.(( polynom s) . x).| * |.(f . x).|) by Q7, ABSVALUE:def 1

        .= |.((( polynom s) . x) * (f . x)).| by COMPLEX1: 65

        .= |.((( polynom s) (#) f) . x).| by VALUED_1: 5;

        then

         P8: |.((g (#) f) . x).| <= |.((( polynom s) (#) f) . x).| by P4, XREAL_1: 66, P6;

        N1 <= N by NAT_1: 12;

        then N1 <= x by P3, XXREAL_0: 2;

        then |.((( polynom s) (#) f) . x).| < (1 / (( polynom d) . x)) by P2;

        hence thesis by A0, P8, XXREAL_0: 2;

      end;

    end

    theorem :: ASYMPT_3:39

    for v,w be VECTOR of R_Algebra_of_Big_Oh_poly st w in negligibleFuncs holds (v * w) in negligibleFuncs

    proof

      let v,w be VECTOR of R_Algebra_of_Big_Oh_poly ;

      assume w in negligibleFuncs ;

      then

      reconsider w1 = w as negligible Function of NAT , REAL by Def1;

      v in R_Algebra_of_Big_Oh_poly ;

      then

      reconsider v1 = v as polynomially-abs-bounded Function of NAT , REAL by LM14;

      (v1 (#) w1) is negligible;

      then (v * w) is negligible Function of NAT , REAL by RSSPAC2A;

      hence thesis by Def1;

    end;