asympt_0.miz



    begin

    reserve c,c1,d for Real,

k for Nat,

n,m,N,n1,N1,N2,N3,N4,N5,M for Element of NAT ,

x for set;

    scheme :: ASYMPT_0:sch1

    FinSegRng1 { m,n() -> Nat , X() -> non empty set , F( set) -> Element of X() } :

{ F(i) where i be Element of NAT : m() <= i & i <= n() } is finite non empty Subset of X()

      provided

       A1: m() <= n();

      defpred P[ Nat] means m() <= $1;

      set S = { F(i) where i be Nat : i <= n() & P[i] };

      

       A2: F(m) in S by A1;

      set S1 = { F(i) where i be Element of NAT : m() <= i & i <= n() };

       A3:

      now

        let x be object;

        hereby

          assume x in S;

          then

          consider i be Nat such that

           A4: x = F(i) & i <= n() & P[i];

          reconsider j = i as Element of NAT by ORDINAL1:def 12;

          x = F(j) by A4;

          hence x in S1 by A4;

        end;

        assume x in S1;

        then ex i be Element of NAT st x = F(i) & m() <= i & i <= n();

        hence x in S;

      end;

      

       A5: S c= X()

      proof

        let x be object;

        assume x in S;

        then ex n1 be Nat st x = F(n1) & n1 <= n() & n1 >= m();

        hence thesis;

      end;

      S is finite from FINSEQ_1:sch 6;

      hence thesis by A3, A2, A5, TARSKI: 2;

    end;

    scheme :: ASYMPT_0:sch2

    FinImInit1 { N() -> Nat , X() -> non empty set , F( set) -> Element of X() } :

{ F(n) where n be Element of NAT : n <= N() } is finite non empty Subset of X();

      set T = { F(n) where n be Element of NAT : 0 <= n & n <= N() };

      set S = { F(n) where n be Element of NAT : n <= N() };

       A1:

      now

        let x be object;

        hereby

          assume x in S;

          then ex n be Element of NAT st x = F(n) & n <= N();

          hence x in T;

        end;

        assume x in T;

        then ex n be Element of NAT st x = F(n) & 0 <= n & n <= N();

        hence x in S;

      end;

      

       A2: 0 <= N();

      T is finite non empty Subset of X() from FinSegRng1( A2);

      hence thesis by A1, TARSKI: 2;

    end;

    scheme :: ASYMPT_0:sch3

    FinImInit2 { N() -> Nat , X() -> non empty set , F( set) -> Element of X() } :

{ F(n) where n be Element of NAT : n < N() } is finite non empty Subset of X()

      provided

       A1: N() > 0 ;

      set S = { F(n) where n be Element of NAT : n < N() };

      consider m be Nat such that

       A2: N() = (m + 1) by A1, NAT_1: 6;

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

      set T = { F(n) where n be Element of NAT : n <= m };

       A3:

      now

        let x be object;

        hereby

          assume x in S;

          then

          consider n be Element of NAT such that

           A4: x = F(n) and

           A5: n < N();

          n <= m by A2, A5, NAT_1: 13;

          hence x in T by A4;

        end;

        assume x in T;

        then

        consider n be Element of NAT such that

         A6: x = F(n) and

         A7: n <= m;

        n < (m + 1) by A7, NAT_1: 13;

        hence x in S by A2, A6;

      end;

      T is finite non empty Subset of X() from FinImInit1;

      hence thesis by A3, TARSKI: 2;

    end;

    definition

      let c be Real;

      :: ASYMPT_0:def1

      attr c is logbase means c > 0 & c <> 1;

    end

    reconsider jj = 1, dwa = 2 as Element of REAL by XREAL_0:def 1;

    registration

      cluster positive for Real;

      existence

      proof

        take jj;

        thus thesis;

      end;

      cluster negative for Real;

      existence

      proof

        take ( - jj);

        thus thesis by XXREAL_0:def 7;

      end;

      cluster logbase for Real;

      existence

      proof

        take dwa;

        thus thesis;

      end;

      cluster non negative for Real;

      existence by XXREAL_0:def 7;

      cluster non positive for Real;

      existence by XXREAL_0:def 6;

      cluster non logbase for Real;

      existence

      proof

        take jj;

        thus thesis;

      end;

    end

    definition

      let f be Real_Sequence;

      :: ASYMPT_0:def2

      attr f is eventually-nonnegative means

      : Def2: ex N be Nat st for n be Nat st n >= N holds (f . n) >= 0 ;

      :: ASYMPT_0:def3

      attr f is positive means

      : Def3: for n be Nat holds (f . n) > 0 ;

      :: ASYMPT_0:def4

      attr f is eventually-positive means

      : Def4: ex N be Nat st for n be Nat st n >= N holds (f . n) > 0 ;

      :: ASYMPT_0:def5

      attr f is eventually-nonzero means

      : Def5: ex N be Nat st for n be Nat st n >= N holds (f . n) <> 0 ;

      :: ASYMPT_0:def6

      attr f is eventually-nondecreasing means

      : Def6: ex N be Nat st for n be Nat st n >= N holds (f . n) <= (f . (n + 1));

    end

    registration

      cluster eventually-nonnegative eventually-nonzero positive eventually-positive eventually-nondecreasing for Real_Sequence;

      existence

      proof

        take f = ( seq_const 1);

        thus f is eventually-nonnegative

        proof

          take 0 ;

          let n be Nat;

          assume n >= 0 ;

          thus thesis by SEQ_1: 57;

        end;

        thus f is eventually-nonzero

        proof

          take 0 ;

          let n be Nat;

          thus thesis by SEQ_1: 57;

        end;

        thus f is positive by SEQ_1: 57;

        thus f is eventually-positive

        proof

          take 0 ;

          let n be Nat;

          assume n >= 0 ;

          thus thesis by SEQ_1: 57;

        end;

        thus f is eventually-nondecreasing

        proof

          take 0 ;

          let n be Nat;

          assume n >= 0 ;

          (f . n) = 1 by SEQ_1: 57;

          hence thesis by SEQ_1: 57;

        end;

      end;

    end

    registration

      cluster positive -> eventually-positive for Real_Sequence;

      coherence

      proof

        let f be Real_Sequence;

        assume

         A1: f is positive;

        take 0 ;

        let n be Nat;

        assume n >= 0 ;

        thus thesis by A1;

      end;

      cluster eventually-positive -> eventually-nonnegative eventually-nonzero for Real_Sequence;

      coherence

      proof

        let f be Real_Sequence;

        assume f is eventually-positive;

        then

        consider N be Nat such that

         A2: for n be Nat st n >= N holds (f . n) > 0 ;

        thus f is eventually-nonnegative

        proof

          take N;

          let n be Nat;

          assume n >= N;

          hence thesis by A2;

        end;

        thus f is eventually-nonzero

        proof

          take N;

          let n be Nat;

          assume n >= N;

          hence thesis by A2;

        end;

      end;

      cluster eventually-nonnegative eventually-nonzero -> eventually-positive for Real_Sequence;

      coherence

      proof

        let f be Real_Sequence;

        assume that

         A3: f is eventually-nonnegative and

         A4: f is eventually-nonzero;

        consider N be Nat such that

         A5: for n be Nat st n >= N holds (f . n) >= 0 by A3;

        consider M be Nat such that

         A6: for n be Nat st n >= M holds (f . n) <> 0 by A4;

        reconsider a = ( max (N,M)) as Nat by TARSKI: 1;

        take a;

        let n be Nat;

        assume

         A7: n >= a;

        a >= N by XXREAL_0: 25;

        then

         A8: n >= N by A7, XXREAL_0: 2;

        a >= M by XXREAL_0: 25;

        then (f . n) <> 0 by A6, A7, XXREAL_0: 2;

        hence thesis by A5, A8;

      end;

    end

    definition

      let f,g be eventually-nonnegative Real_Sequence;

      :: original: +

      redefine

      func f + g -> eventually-nonnegative Real_Sequence ;

      coherence

      proof

        consider M be Nat such that

         A1: for n be Nat st n >= M holds (g . n) >= 0 by Def2;

        consider N be Nat such that

         A2: for n be Nat st n >= N holds (f . n) >= 0 by Def2;

        reconsider a = ( max (N,M)) as Nat by TARSKI: 1;

        (f + g) is eventually-nonnegative

        proof

          take a;

          let n be Nat;

          assume

           A3: n >= a;

          a >= M by XXREAL_0: 25;

          then n >= M by A3, XXREAL_0: 2;

          then

           A4: (g . n) >= 0 by A1;

          a >= N by XXREAL_0: 25;

          then n >= N by A3, XXREAL_0: 2;

          then (f . n) >= 0 by A2;

          then ( 0 + 0 ) <= ((f . n) + (g . n)) by A4;

          hence thesis by SEQ_1: 7;

        end;

        hence thesis;

      end;

    end

    definition

      let f be eventually-nonnegative Real_Sequence, c be positive Real;

      :: original: (#)

      redefine

      func c (#) f -> eventually-nonnegative Real_Sequence ;

      coherence

      proof

        consider N be Nat such that

         A1: for n be Nat st n >= N holds (f . n) >= 0 by Def2;

        (c (#) f) is eventually-nonnegative

        proof

          take N;

          let n be Nat;

          assume n >= N;

          then (f . n) >= 0 by A1;

          then (c * (f . n)) >= (c * 0 );

          hence thesis by SEQ_1: 9;

        end;

        hence thesis;

      end;

    end

    definition

      let f be eventually-nonnegative Real_Sequence, c be non negative Real;

      :: original: +

      redefine

      func c + f -> eventually-nonnegative Real_Sequence ;

      coherence

      proof

        consider N be Nat such that

         A1: for n be Nat st n >= N holds (f . n) >= 0 by Def2;

        (c + f) is eventually-nonnegative

        proof

          take N;

          let n be Nat;

          

           A2: n in NAT by ORDINAL1:def 12;

          assume n >= N;

          then (f . n) >= 0 by A1;

          then (c + (f . n)) >= ( 0 + 0 );

          hence thesis by VALUED_1: 2, A2;

        end;

        hence thesis;

      end;

    end

    definition

      let f be eventually-nonnegative Real_Sequence, c be positive Real;

      :: original: +

      redefine

      func c + f -> eventually-positive Real_Sequence ;

      coherence

      proof

        consider N be Nat such that

         A1: for n be Nat st n >= N holds (f . n) >= 0 by Def2;

        (c + f) is eventually-positive

        proof

          take N;

          let n be Nat;

          

           A2: n in NAT by ORDINAL1:def 12;

          assume n >= N;

          then (f . n) >= 0 by A1;

          then (c + (f . n)) > ( 0 + 0 );

          hence thesis by VALUED_1: 2, A2;

        end;

        hence thesis;

      end;

    end

    definition

      let f,g be Real_Sequence;

      :: ASYMPT_0:def7

      func max (f,g) -> Real_Sequence means

      : Def7: for n be Nat holds (it . n) = ( max ((f . n),(g . n)));

      existence

      proof

        deffunc F( Nat) = ( In (( max ((f . $1),(g . $1))), REAL ));

        consider h be sequence of REAL such that

         A1: for n be Element of NAT holds (h . n) = F(n) from FUNCT_2:sch 4;

        take h;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        then (h . n) = F(n) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let j,k be Real_Sequence such that

         A2: for n be Nat holds (j . n) = ( max ((f . n),(g . n))) and

         A3: for n be Nat holds (k . n) = ( max ((f . n),(g . n)));

        now

          let n;

          

          thus (j . n) = ( max ((f . n),(g . n))) by A2

          .= (k . n) by A3;

        end;

        hence j = k by FUNCT_2: 63;

      end;

      commutativity ;

    end

    registration

      let f be Real_Sequence, g be eventually-nonnegative Real_Sequence;

      cluster ( max (f,g)) -> eventually-nonnegative;

      coherence

      proof

        consider N be Nat such that

         A1: for n be Nat st n >= N holds (g . n) >= 0 by Def2;

        take N;

        let n be Nat;

        assume n >= N;

        then

         A2: (g . n) >= 0 by A1;

        ( max ((f . n),(g . n))) >= (g . n) by XXREAL_0: 25;

        hence thesis by A2, Def7;

      end;

    end

    registration

      let f be Real_Sequence, g be eventually-positive Real_Sequence;

      cluster ( max (f,g)) -> eventually-positive;

      coherence

      proof

        consider N be Nat such that

         A1: for n be Nat st n >= N holds (g . n) > 0 by Def4;

        take N;

        let n be Nat;

        assume n >= N;

        then (g . n) > 0 by A1;

        then ( max ((f . n),(g . n))) > 0 by XXREAL_0: 25;

        hence thesis by Def7;

      end;

    end

    definition

      let f,g be Real_Sequence;

      :: ASYMPT_0:def8

      pred g majorizes f means ex N st for n st n >= N holds (f . n) <= (g . n);

    end

    

     Lm1: for f,g be Real_Sequence, n be Nat holds ((f /" g) . n) = ((f . n) / (g . n))

    proof

      let f,g be Real_Sequence, n be Nat;

      

      thus ((f /" g) . n) = ((f . n) * ((g " ) . n)) by SEQ_1: 8

      .= ((f . n) * ((g . n) " )) by VALUED_1: 10

      .= ((f . n) / (g . n)) by XCMPLX_0:def 9;

    end;

    theorem :: ASYMPT_0:1

    

     Th1: for f be Real_Sequence, N be Nat st for n be Nat st n >= N holds (f . n) <= (f . (n + 1)) holds for n,m be Nat st N <= n & n <= m holds (f . n) <= (f . m)

    proof

      let f be Real_Sequence, N be Nat;

      assume

       A1: for n be Nat st n >= N holds (f . n) <= (f . (n + 1));

      let n,m be Nat;

      defpred P[ Nat] means (f . n) <= (f . $1);

      assume

       A2: n >= N;

      

       A3: for m be Nat st m >= n & P[m] holds P[(m + 1)]

      proof

        let m be Nat;

        assume that

         A4: m >= n and

         A5: (f . n) <= (f . m);

        m in NAT & m >= N by A2, A4, ORDINAL1:def 12, XXREAL_0: 2;

        then (f . m) <= (f . (m + 1)) by A1;

        hence thesis by A5, XXREAL_0: 2;

      end;

      

       A6: P[n];

      for m be Nat st m >= n holds P[m] from NAT_1:sch 8( A6, A3);

      hence thesis;

    end;

    theorem :: ASYMPT_0:2

    

     Th2: for f,g be eventually-positive Real_Sequence st (f /" g) is convergent & ( lim (f /" g)) <> 0 holds (g /" f) is convergent & ( lim (g /" f)) = (( lim (f /" g)) " )

    proof

      let f,g be eventually-positive Real_Sequence;

      set s = (f /" g);

      set als = |.( lim s).|;

      set ls = ( lim s);

      assume that

       A1: (f /" g) is convergent and

       A2: ( lim (f /" g)) <> 0 ;

      consider n1 be Nat such that

       A3: for m be Nat st n1 <= m holds (als / 2) < |.(s . m).| by A1, A2, SEQ_2: 16;

      

       A4: 0 < als by A2, COMPLEX1: 47;

      then ( 0 * 0 ) < (als * als) by XREAL_1: 96;

      then

       A5: 0 < ((als * als) / 2) by XREAL_1: 215;

      consider N2 be Nat such that

       A6: for n be Nat st n >= N2 holds (g . n) > 0 by Def4;

      consider N1 be Nat such that

       A7: for n be Nat st n >= N1 holds (f . n) > 0 by Def4;

      

       A8: 0 <> als by A2, COMPLEX1: 47;

       A9:

      now

        set N3 = (N1 + N2);

        let p be Real;

        set N4 = (N3 + n1);

        

         A10: 0 <> (als / 2) by A2, COMPLEX1: 47;

        

         A11: ((p * (als / 2)) / (als / 2)) = ((p * (als / 2)) * ((als / 2) " )) by XCMPLX_0:def 9

        .= (p * ((als / 2) * ((als / 2) " )))

        .= (p * 1) by A10, XCMPLX_0:def 7

        .= p;

        assume

         A12: 0 < p;

        then ( 0 * 0 ) < (p * ((als * als) / 2)) by A5, XREAL_1: 96;

        then

        consider n2 be Nat such that

         A13: for m be Nat st n2 <= m holds |.((s . m) - ls).| < (p * ((als * als) / 2)) by A1, SEQ_2:def 7;

        take n = (N4 + n2);

        let m be Nat such that

         A14: n <= m;

        set asm = |.(s . m).|;

        

         A15: ((p * ((als * als) / 2)) / (asm * als)) = ((p * ((2 " ) * (als * als))) * ((asm * als) " )) by XCMPLX_0:def 9

        .= ((p * (2 " )) * ((als * als) * ((als * asm) " )))

        .= ((p * (2 " )) * ((als * als) * ((als " ) * (asm " )))) by XCMPLX_1: 204

        .= ((p * (2 " )) * ((als * (als * (als " ))) * (asm " )))

        .= ((p * (2 " )) * ((als * 1) * (asm " ))) by A8, XCMPLX_0:def 7

        .= ((p * (als / 2)) * (asm " ))

        .= ((p * (als / 2)) / asm) by XCMPLX_0:def 9;

        n1 <= N4 by NAT_1: 12;

        then n1 <= n by NAT_1: 12;

        then n1 <= m by A14, XXREAL_0: 2;

        then

         A16: (als / 2) < asm by A3;

        

         A17: 0 < (als / 2) by A4, XREAL_1: 215;

        then ( 0 * 0 ) < (p * (als / 2)) by A12, XREAL_1: 96;

        then

         A18: ((p * (als / 2)) / asm) < ((p * (als / 2)) / (als / 2)) by A16, A17, XREAL_1: 76;

        N2 <= N3 by NAT_1: 12;

        then N2 <= N4 by NAT_1: 12;

        then N2 <= n by NAT_1: 12;

        then N2 <= m by A14, XXREAL_0: 2;

        then

         A19: (g . m) <> 0 by A6;

        N1 <= N3 by NAT_1: 12;

        then N1 <= N4 by NAT_1: 12;

        then N1 <= n by NAT_1: 12;

        then N1 <= m by A14, XXREAL_0: 2;

        then (f . m) <> 0 by A7;

        then ((f . m) / (g . m)) <> 0 by A19, XCMPLX_1: 50;

        then

         A20: (s . m) <> 0 by Lm1;

        then ((s . m) * ls) <> 0 by A2, XCMPLX_1: 6;

        then 0 < |.((s . m) * ls).| by COMPLEX1: 47;

        then

         A21: 0 < (asm * als) by COMPLEX1: 65;

        n2 <= n by NAT_1: 12;

        then n2 <= m by A14, XXREAL_0: 2;

        then |.((s . m) - ls).| < (p * ((als * als) / 2)) by A13;

        then

         A22: ( |.((s . m) - ls).| / (asm * als)) < ((p * ((als * als) / 2)) / (asm * als)) by A21, XREAL_1: 74;

         |.(((g /" f) . m) - (ls " )).| = |.(((g . m) / (f . m)) - (ls " )).| by Lm1

        .= |.((((f . m) / (g . m)) " ) - (ls " )).| by XCMPLX_1: 213

        .= |.(((s . m) " ) - (ls " )).| by Lm1

        .= ( |.((s . m) - ls).| / (asm * als)) by A2, A20, SEQ_2: 2;

        hence |.(((g /" f) . m) - (ls " )).| < p by A22, A15, A18, A11, XXREAL_0: 2;

      end;

      hence (g /" f) is convergent by SEQ_2:def 6;

      hence thesis by A9, SEQ_2:def 7;

    end;

    theorem :: ASYMPT_0:3

    

     Th3: for f be eventually-nonnegative Real_Sequence st f is convergent holds 0 <= ( lim f)

    proof

      let f be eventually-nonnegative Real_Sequence such that

       A1: f is convergent and

       A2: not 0 <= ( lim f);

       0 < ( - ( lim f)) by A2, XREAL_1: 58;

      then

      consider N1 be Nat such that

       A3: for m be Nat st N1 <= m holds |.((f . m) - ( lim f)).| < ( - ( lim f)) by A1, SEQ_2:def 7;

      consider N be Nat such that

       A4: for n be Nat st n >= N holds 0 <= (f . n) by Def2;

      set n1 = ( max (N,N1));

      

       A0: n1 is Nat by TARSKI: 1;

       A5:

      now

        assume (f . n1) = 0 ;

        then |.((f . n1) - ( lim f)).| = ( - ( lim f)) by A2, ABSVALUE:def 1;

        hence contradiction by A0, A3, XXREAL_0: 25;

      end;

       |.((f . n1) - ( lim f)).| <= ( - ( lim f)) by A0, A3, XXREAL_0: 25;

      then ((f . n1) - ( lim f)) <= ( - ( lim f)) by ABSVALUE: 5;

      then (((f . n1) - ( lim f)) + ( lim f)) <= (( - ( lim f)) + ( lim f)) by XREAL_1: 6;

      hence contradiction by A0, A4, A5, XXREAL_0: 25;

    end;

    theorem :: ASYMPT_0:4

    

     Th4: for f,g be Real_Sequence st f is convergent & g is convergent & g majorizes f holds ( lim f) <= ( lim g)

    proof

      let f,g be Real_Sequence;

      assume that

       A1: f is convergent & g is convergent and

       A2: ex N st for n st n >= N holds (f . n) <= (g . n);

      consider N such that

       A3: for n st n >= N holds (f . n) <= (g . n) by A2;

      now

        let n be Nat;

        

         A4: n in NAT by ORDINAL1:def 12;

        assume n >= N;

        then (f . n) <= (g . n) by A3, A4;

        then

         A5: ((f . n) - (f . n)) <= ((g . n) - (f . n)) by XREAL_1: 9;

        ((g - f) . n) = ((g . n) + (( - f) . n)) by SEQ_1: 7

        .= ((g . n) + ( - (f . n))) by SEQ_1: 10

        .= ((g . n) - (f . n));

        hence 0 <= ((g - f) . n) by A5;

      end;

      then

       A6: (g - f) is eventually-nonnegative;

      

       A7: ( lim (g - f)) = (( lim g) - ( lim f)) by A1, SEQ_2: 12;

      (g - f) is convergent by A1, SEQ_2: 11;

      then 0 <= ( lim (g - f)) by A6, Th3;

      then ( 0 + ( lim f)) <= ((( lim g) - ( lim f)) + ( lim f)) by A7, XREAL_1: 6;

      hence thesis;

    end;

    theorem :: ASYMPT_0:5

    

     Th5: for f be Real_Sequence, g be eventually-nonzero Real_Sequence st (f /" g) is divergent_to+infty holds (g /" f) is convergent & ( lim (g /" f)) = 0

    proof

      let f be Real_Sequence, g be eventually-nonzero Real_Sequence;

      consider N1 be Nat such that

       A1: for n be Nat st n >= N1 holds (g . n) <> 0 by Def5;

      assume

       A2: (f /" g) is divergent_to+infty;

       A3:

      now

        let p be Real such that

         A4: p > 0 ;

        reconsider w = (1 / p) as Real;

        consider N be Nat such that

         A5: for n be Nat st n >= N holds w < ((f /" g) . n) by A2, LIMFUNC1:def 4;

        reconsider a = ( max (N,N1)) as Nat by TARSKI: 1;

        take a;

        let n be Nat;

        assume

         A6: n >= a;

        a >= N by XXREAL_0: 25;

        then n >= N by A6, XXREAL_0: 2;

        then (1 / p) < ((f /" g) . n) by A5;

        then ((1 / p) * p) < (p * ((f /" g) . n)) by A4, XREAL_1: 68;

        then 1 < (p * ((f /" g) . n)) by A4, XCMPLX_1: 106;

        then

         A7: 1 < (p * ((f . n) / (g . n))) by Lm1;

        then

         A8: 1 < (p * ((f . n) * ((g . n) " ))) by XCMPLX_0:def 9;

         A9:

        now

          assume ((g . n) * ((f . n) " )) > ((g . n) * 0 );

          then ((g . n) * ((f " ) . n)) > 0 by VALUED_1: 10;

          hence (((g /" f) . n) - 0 ) >= 0 by SEQ_1: 8;

        end;

        a >= N1 by XXREAL_0: 25;

        then

         A10: (g . n) <> 0 by A1, A6, XXREAL_0: 2;

        

         A11: (f . n) <> 0 by A7;

         A12:

        now

          assume ((g . n) * ((f . n) " )) < ((p * (f . n)) * ((f . n) " ));

          then ((g . n) * ((f " ) . n)) < ((p * (f . n)) * ((f . n) " )) by VALUED_1: 10;

          then ((g (#) (f " )) . n) < (p * ((f . n) * ((f . n) " ))) by SEQ_1: 8;

          then ((g (#) (f " )) . n) < (p * 1) by A11, XCMPLX_0:def 7;

          hence (((g /" f) . n) - 0 ) < p;

        end;

        per cases by A10;

          suppose

           A13: (g . n) > 0 ;

          then (1 * (g . n)) < (((p * (f . n)) * ((g . n) " )) * (g . n)) by A8, XREAL_1: 68;

          then (g . n) < ((p * (f . n)) * (((g . n) " ) * (g . n)));

          then

           A14: (g . n) < ((p * (f . n)) * 1) by A10, XCMPLX_0:def 7;

          (f . n) > 0 by A4, A7, A13;

          hence |.(((g /" f) . n) - 0 ).| < p by A12, A9, A13, A14, ABSVALUE:def 1, XREAL_1: 68;

        end;

          suppose

           A15: (g . n) < 0 ;

          then (1 * (g . n)) > (((p * (f . n)) * ((g . n) " )) * (g . n)) by A8, XREAL_1: 69;

          then (g . n) > ((p * (f . n)) * (((g . n) " ) * (g . n)));

          then

           A16: (g . n) > ((p * (f . n)) * 1) by A10, XCMPLX_0:def 7;

          (f . n) < 0 by A4, A7, A15;

          hence |.(((g /" f) . n) - 0 ).| < p by A12, A9, A15, A16, ABSVALUE:def 1, XREAL_1: 69;

        end;

      end;

      hence (g /" f) is convergent by SEQ_2:def 6;

      hence thesis by A3, SEQ_2:def 7;

    end;

    begin

    definition

      let f be eventually-nonnegative Real_Sequence;

      :: ASYMPT_0:def9

      func Big_Oh (f) -> FUNCTION_DOMAIN of NAT , REAL equals { t where t be Element of ( Funcs ( NAT , REAL )) : ex c, N st c > 0 & for n st n >= N holds (t . n) <= (c * (f . n)) & (t . n) >= 0 };

      coherence

      proof

        set IT = { t where t be Element of ( Funcs ( NAT , REAL )) : ex c, N st c > 0 & for n st n >= N holds (t . n) <= (c * (f . n)) & (t . n) >= 0 };

        

         A1: IT is functional

        proof

          let x be object;

          assume x in IT;

          then ex t be Element of ( Funcs ( NAT , REAL )) st x = t & ex c, N st c > 0 & for n st n >= N holds (t . n) <= (c * (f . n)) & (t . n) >= 0 ;

          hence thesis;

        end;

        consider N be Nat such that

         A2: for n be Nat st n >= N holds (f . n) >= 0 by Def2;

        

         A3: N in NAT by ORDINAL1:def 12;

        

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

        for n st n >= N holds (f . n) <= (1 * (f . n)) & (f . n) >= 0 by A2;

        then ex c, N st c > 0 & for n st n >= N holds (f . n) <= (c * (f . n)) & (f . n) >= 0 by A3;

        then f in IT by A4;

        then

        reconsider IT1 = IT as functional non empty set by A1;

        now

          let x be Element of IT1;

          x in IT;

          then ex t be Element of ( Funcs ( NAT , REAL )) st x = t & ex c, N st c > 0 & for n st n >= N holds (t . n) <= (c * (f . n)) & (t . n) >= 0 ;

          hence x is sequence of REAL ;

        end;

        hence thesis by FUNCT_2:def 12;

      end;

    end

    theorem :: ASYMPT_0:6

    

     Th6: for x be set, f be eventually-nonnegative Real_Sequence st x in ( Big_Oh f) holds x is eventually-nonnegative Real_Sequence

    proof

      let t be set, f be eventually-nonnegative Real_Sequence;

      assume t in ( Big_Oh f);

      then

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

       A1: s = t and

       A2: ex c, N st c > 0 & for n st n >= N holds (s . n) <= (c * (f . n)) & (s . n) >= 0 ;

      reconsider t9 = t as Real_Sequence by A1;

      consider c, N such that c > 0 and

       A3: for n st n >= N holds (s . n) <= (c * (f . n)) & (s . n) >= 0 by A2;

      now

        take N;

        let n be Nat;

        

         A4: n in NAT by ORDINAL1:def 12;

        assume n >= N;

        hence (t9 . n) >= 0 by A1, A3, A4;

      end;

      hence thesis by Def2;

    end;

    theorem :: ASYMPT_0:7

    for f be positive Real_Sequence, t be eventually-nonnegative Real_Sequence holds t in ( Big_Oh f) iff ex c st c > 0 & for n holds (t . n) <= (c * (f . n))

    proof

      let f be positive Real_Sequence, t be eventually-nonnegative Real_Sequence;

      hereby

        assume t in ( Big_Oh f);

        then

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

         A1: t = s and

         A2: ex c, N st c > 0 & for n st n >= N holds (s . n) <= (c * (f . n)) & (s . n) >= 0 ;

        consider c, N such that

         A3: c > 0 and

         A4: for n st n >= N holds (s . n) <= (c * (f . n)) & (s . n) >= 0 by A2;

        per cases ;

          suppose

           A5: N = 0 ;

          take c;

          thus c > 0 by A3;

          let n;

          thus (t . n) <= (c * (f . n)) by A1, A4, A5;

        end;

          suppose

           A6: N > 0 ;

          deffunc F( Element of NAT ) = ((t . $1) / (f . $1));

          reconsider B = { F(n) : n < N } as finite non empty Subset of REAL from FinImInit2( A6);

          set b = ( max B);

          

           A7: for n st n < N holds (t . n) <= (b * (f . n))

          proof

            let n;

            

             A8: (f . n) > 0 by Def3;

            assume n < N;

            then ((t . n) / (f . n)) in B;

            then ((t . n) / (f . n)) <= b by XXREAL_2:def 8;

            then (((t . n) / (f . n)) * (f . n)) <= (b * (f . n)) by A8, XREAL_1: 64;

            hence thesis by A8, XCMPLX_1: 87;

          end;

          thus ex c st c > 0 & for n holds (t . n) <= (c * (f . n))

          proof

            per cases ;

              suppose

               A9: b <= c;

              take c;

              thus c > 0 by A3;

              let n;

              thus (t . n) <= (c * (f . n))

              proof

                per cases ;

                  suppose

                   A10: n < N;

                  (f . n) > 0 by Def3;

                  then

                   A11: (b * (f . n)) <= (c * (f . n)) by A9, XREAL_1: 64;

                  (t . n) <= (b * (f . n)) by A7, A10;

                  hence thesis by A11, XXREAL_0: 2;

                end;

                  suppose n >= N;

                  hence thesis by A1, A4;

                end;

              end;

            end;

              suppose

               A12: b > c;

              reconsider b as Element of REAL by XREAL_0:def 1;

              take b;

              thus b > 0 by A3, A12;

              let n;

              thus (t . n) <= (b * (f . n))

              proof

                per cases ;

                  suppose n < N;

                  hence thesis by A7;

                end;

                  suppose

                   A13: n >= N;

                  (f . n) > 0 by Def3;

                  then

                   A14: (c * (f . n)) <= (b * (f . n)) by A12, XREAL_1: 64;

                  (t . n) <= (c * (f . n)) by A1, A4, A13;

                  hence thesis by A14, XXREAL_0: 2;

                end;

              end;

            end;

          end;

        end;

      end;

      given c such that

       A15: c > 0 and

       A16: for n holds (t . n) <= (c * (f . n));

      consider N be Nat such that

       A17: for n be Nat st n >= N holds (t . n) >= 0 by Def2;

      

       A18: N in NAT by ORDINAL1:def 12;

      t is Element of ( Funcs ( NAT , REAL )) & for n st n >= N holds (t . n) <= (c * (f . n)) & (t . n) >= 0 by A16, A17, FUNCT_2: 8;

      hence t in ( Big_Oh f) by A15, A18;

    end;

    theorem :: ASYMPT_0:8

    for f be eventually-positive Real_Sequence, t be eventually-nonnegative Real_Sequence, N be Element of NAT st t in ( Big_Oh f) & for n st n >= N holds (f . n) > 0 holds ex c st c > 0 & for n st n >= N holds (t . n) <= (c * (f . n))

    proof

      let f be eventually-positive Real_Sequence, t be eventually-nonnegative Real_Sequence, N be Element of NAT ;

      assume that

       A1: t in ( Big_Oh f) and

       A2: for n st n >= N holds (f . n) > 0 ;

      deffunc T( Element of NAT ) = (t . $1);

      deffunc F( Element of NAT ) = (f . $1);

      ex s be Element of ( Funcs ( NAT , REAL )) st t = s & ex c, N st c > 0 & for n st n >= N holds (s . n) <= (c * (f . n)) & (s . n) >= 0 by A1;

      then

      consider c2 be Real, M such that

       A3: c2 > 0 and

       A4: for n st n >= M holds (t . n) <= (c2 * (f . n)) & (t . n) >= 0 ;

      set fset = { F(n) : N <= n & n <= ( max (M,N)) };

      

       A5: N <= ( max (M,N)) by XXREAL_0: 25;

      fset is finite non empty Subset of REAL from FinSegRng1( A5);

      then

      reconsider fset as finite non empty Subset of REAL ;

      set F = ( min fset);

      

       A6: M <= ( max (M,N)) by XXREAL_0: 25;

      set tset = { T(n) : N <= n & n <= ( max (M,N)) };

      tset is finite non empty Subset of REAL from FinSegRng1( A5);

      then

      reconsider tset as finite non empty Subset of REAL ;

      set T = ( max tset);

      set c1 = (T / F);

      reconsider c = ( max (c1,c2)) as Element of REAL by XREAL_0:def 1;

      take c;

      thus c > 0 by A3, XXREAL_0: 25;

      let n;

      assume

       A7: n >= N;

      then

       A8: (f . n) > 0 by A2;

      

       A9: (f . n) <> 0 by A2, A7;

      F in fset by XXREAL_2:def 7;

      then

       A10: ex n1 be Element of NAT st (f . n1) = F & n1 >= N & n1 <= ( max (M,N));

      then

       A11: F > 0 by A2;

      

       A12: F <> 0 by A2, A10;

      per cases ;

        suppose N >= M;

        then n >= M by A7, XXREAL_0: 2;

        then

         A13: (t . n) <= (c2 * (f . n)) by A4;

        (c2 * (f . n)) <= (c * (f . n)) by A8, XREAL_1: 64, XXREAL_0: 25;

        hence thesis by A13, XXREAL_0: 2;

      end;

        suppose

         A14: N <= M;

        thus (t . n) <= (c * (f . n))

        proof

          per cases ;

            suppose n <= M;

            then

             A15: n <= ( max (M,N)) by A6, XXREAL_0: 2;

            then (t . n) in tset by A7;

            then

             A16: (t . n) <= T by XXREAL_2:def 8;

            (f . n) in fset by A7, A15;

            then

             A17: (f . n) >= F by XXREAL_2:def 7;

            (t . M) in tset by A6, A14;

            then

             A18: (t . M) <= T by XXREAL_2:def 8;

            (t . M) >= 0 by A4;

            then

             A19: (c1 * (f . n)) >= (c1 * F) by A11, A18, A17, XREAL_1: 64;

            now

              assume ((t . n) / (f . n)) > c1;

              then (((t . n) / (f . n)) * (f . n)) > (c1 * (f . n)) by A8, XREAL_1: 68;

              then (t . n) > (c1 * (f . n)) by A9, XCMPLX_1: 87;

              then T > (c1 * (f . n)) by A16, XXREAL_0: 2;

              hence contradiction by A12, A19, XCMPLX_1: 87;

            end;

            then (((t . n) / (f . n)) * (f . n)) <= (c1 * (f . n)) by A8, XREAL_1: 64;

            then

             A20: (t . n) <= (c1 * (f . n)) by A9, XCMPLX_1: 87;

            (c1 * (f . n)) <= (c * (f . n)) by A8, XREAL_1: 64, XXREAL_0: 25;

            hence thesis by A20, XXREAL_0: 2;

          end;

            suppose

             A21: n >= M;

            

             A22: (c2 * (f . n)) <= (c * (f . n)) by A8, XREAL_1: 64, XXREAL_0: 25;

            (t . n) <= (c2 * (f . n)) by A4, A21;

            hence thesis by A22, XXREAL_0: 2;

          end;

        end;

      end;

    end;

    theorem :: ASYMPT_0:9

    for f,g be eventually-nonnegative Real_Sequence holds ( Big_Oh (f + g)) = ( Big_Oh ( max (f,g)))

    proof

      let f,g be eventually-nonnegative Real_Sequence;

      now

        let x be object;

        hereby

          assume x in ( Big_Oh (f + g));

          then

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

           A1: t = x and

           A2: ex c, N st c > 0 & for n st n >= N holds (t . n) <= (c * ((f + g) . n)) & (t . n) >= 0 ;

          consider c, N such that

           A3: c > 0 and

           A4: for n st n >= N holds (t . n) <= (c * ((f + g) . n)) & (t . n) >= 0 by A2;

           A5:

          now

            let n;

            

             A6: (f . n) <= ( max ((f . n),(g . n))) & (g . n) <= ( max ((f . n),(g . n))) by XXREAL_0: 25;

            

             A7: ((1 * (( max (f,g)) . n)) + (1 * (( max (f,g)) . n))) = ((1 + 1) * (( max (f,g)) . n));

            ((f + g) . n) = ((f . n) + (g . n)) & (( max (f,g)) . n) = ( max ((f . n),(g . n))) by Def7, SEQ_1: 7;

            then ((f + g) . n) <= (2 * (( max (f,g)) . n)) by A6, A7, XREAL_1: 7;

            then

             A8: (c * ((f + g) . n)) <= (c * (2 * (( max (f,g)) . n))) by A3, XREAL_1: 64;

            assume

             A9: n >= N;

            then (t . n) <= (c * ((f + g) . n)) by A4;

            hence (t . n) <= ((2 * c) * (( max (f,g)) . n)) by A8, XXREAL_0: 2;

            thus (t . n) >= 0 by A4, A9;

          end;

          (2 * c) > (2 * 0 ) by A3, XREAL_1: 68;

          hence x in ( Big_Oh ( max (f,g))) by A1, A5;

        end;

        assume x in ( Big_Oh ( max (f,g)));

        then

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

         A10: t = x and

         A11: ex c, N st c > 0 & for n st n >= N holds (t . n) <= (c * (( max (f,g)) . n)) & (t . n) >= 0 ;

        consider c, N1 such that

         A12: c > 0 and

         A13: for n st n >= N1 holds (t . n) <= (c * (( max (f,g)) . n)) & (t . n) >= 0 by A11;

        consider M1 be Nat such that

         A14: for n be Nat st n >= M1 holds (f . n) >= 0 by Def2;

        consider M2 be Nat such that

         A15: for n be Nat st n >= M2 holds (g . n) >= 0 by Def2;

        set N = ( max (N1,( max (M1,M2))));

        

         A16: ( max (M1,M2)) <= N by XXREAL_0: 25;

        M2 <= ( max (M1,M2)) by XXREAL_0: 25;

        then

         A17: M2 <= N by A16, XXREAL_0: 2;

        

         A18: N1 <= N by XXREAL_0: 25;

        M1 <= ( max (M1,M2)) by XXREAL_0: 25;

        then

         A19: M1 <= N by A16, XXREAL_0: 2;

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

        ex c, N st c > 0 & for n st n >= N holds (t . n) <= (c * ((f + g) . n)) & (t . n) >= 0

        proof

          take c, N;

          thus c > 0 by A12;

          let n;

          

           A20: ( max ((f . n),(g . n))) = (f . n) or ( max ((f . n),(g . n))) = (g . n) by XXREAL_0: 16;

          assume

           A21: n >= N;

          then n >= M1 by A19, XXREAL_0: 2;

          then (f . n) >= 0 by A14;

          then

           A22: ((f . n) + (g . n)) >= ( 0 + (g . n)) by XREAL_1: 7;

          n >= M2 by A17, A21, XXREAL_0: 2;

          then (g . n) >= 0 by A15;

          then

           A23: ((f . n) + (g . n)) >= ((f . n) + 0 ) by XREAL_1: 7;

          (( max (f,g)) . n) = ( max ((f . n),(g . n))) & ((f + g) . n) = ((f . n) + (g . n)) by Def7, SEQ_1: 7;

          then

           A24: (c * (( max (f,g)) . n)) <= (c * ((f + g) . n)) by A12, A23, A22, A20, XREAL_1: 64;

          

           A25: n >= N1 by A18, A21, XXREAL_0: 2;

          then (t . n) <= (c * (( max (f,g)) . n)) by A13;

          hence (t . n) <= (c * ((f + g) . n)) by A24, XXREAL_0: 2;

          thus (t . n) >= 0 by A13, A25;

        end;

        hence x in ( Big_Oh (f + g)) by A10;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: ASYMPT_0:10

    

     Th10: for f be eventually-nonnegative Real_Sequence holds f in ( Big_Oh f)

    proof

      let f be eventually-nonnegative Real_Sequence;

      consider N be Nat such that

       A1: for n be Nat st n >= N holds (f . n) >= 0 by Def2;

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

      f is Element of ( Funcs ( NAT , REAL )) & for n st n >= N holds (f . n) <= (1 * (f . n)) & (f . n) >= 0 by A1, FUNCT_2: 8;

      hence thesis;

    end;

    theorem :: ASYMPT_0:11

    

     Th11: for f,g be eventually-nonnegative Real_Sequence st f in ( Big_Oh g) holds ( Big_Oh f) c= ( Big_Oh g)

    proof

      let f,g be eventually-nonnegative Real_Sequence;

      assume f in ( Big_Oh g);

      then

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

       A1: t = f and

       A2: ex c, N st c > 0 & for n st n >= N holds (t . n) <= (c * (g . n)) & (t . n) >= 0 ;

      consider ct be Real, Nt be Element of NAT such that ct > 0 and

       A3: for n st n >= Nt holds (t . n) <= (ct * (g . n)) & (t . n) >= 0 by A2;

      consider Ng be Nat such that

       A4: for n be Nat st n >= Ng holds (g . n) >= 0 by Def2;

      let x be object;

      assume x in ( Big_Oh f);

      then

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

       A5: s = x and

       A6: ex c, N st c > 0 & for n st n >= N holds (s . n) <= (c * (f . n)) & (s . n) >= 0 ;

      consider cs be Real, Ns be Element of NAT such that

       A7: cs > 0 and

       A8: for n st n >= Ns holds (s . n) <= (cs * (f . n)) & (s . n) >= 0 by A6;

      now

        take c = ( max ((cs * ct),( max (cs,ct))));

        c >= ( max (cs,ct)) by XXREAL_0: 25;

        hence c > 0 by A7, XXREAL_0: 25;

        reconsider N = ( max (( max (Ns,Nt)),Ng)) as Element of NAT by ORDINAL1:def 12;

        take N;

        let n;

        assume

         A9: n >= N;

        

         A10: N >= ( max (Ns,Nt)) by XXREAL_0: 25;

        ( max (Ns,Nt)) >= Nt by XXREAL_0: 25;

        then N >= Nt by A10, XXREAL_0: 2;

        then n >= Nt by A9, XXREAL_0: 2;

        then (t . n) <= (ct * (g . n)) by A3;

        then

         A11: (cs * (t . n)) <= (cs * (ct * (g . n))) by A7, XREAL_1: 64;

        N >= Ng by XXREAL_0: 25;

        then n >= Ng by A9, XXREAL_0: 2;

        then (g . n) >= 0 by A4;

        then ((cs * ct) * (g . n)) <= (c * (g . n)) by XREAL_1: 64, XXREAL_0: 25;

        then

         A12: (cs * (t . n)) <= (c * (g . n)) by A11, XXREAL_0: 2;

        ( max (Ns,Nt)) >= Ns by XXREAL_0: 25;

        then N >= Ns by A10, XXREAL_0: 2;

        then

         A13: n >= Ns by A9, XXREAL_0: 2;

        then (s . n) <= (cs * (f . n)) by A8;

        hence (s . n) <= (c * (g . n)) by A1, A12, XXREAL_0: 2;

        thus (s . n) >= 0 by A8, A13;

      end;

      hence thesis by A5;

    end;

    theorem :: ASYMPT_0:12

    

     Th12: for f,g,h be eventually-nonnegative Real_Sequence holds f in ( Big_Oh g) & g in ( Big_Oh h) implies f in ( Big_Oh h)

    proof

      let f,g,h be eventually-nonnegative Real_Sequence;

      assume that

       A1: f in ( Big_Oh g) and

       A2: g in ( Big_Oh h);

      ( Big_Oh g) c= ( Big_Oh h) by A2, Th11;

      hence thesis by A1;

    end;

    

     Lm2: for f,g be eventually-nonnegative Real_Sequence holds f in ( Big_Oh g) & g in ( Big_Oh f) iff ( Big_Oh f) = ( Big_Oh g)

    proof

      let f,g be eventually-nonnegative Real_Sequence;

      hereby

        assume f in ( Big_Oh g) & g in ( Big_Oh f);

        then ( Big_Oh f) c= ( Big_Oh g) & ( Big_Oh g) c= ( Big_Oh f) by Th11;

        hence ( Big_Oh f) = ( Big_Oh g) by XBOOLE_0:def 10;

      end;

      assume ( Big_Oh f) = ( Big_Oh g);

      hence thesis by Th10;

    end;

    theorem :: ASYMPT_0:13

    for f be eventually-nonnegative Real_Sequence, c be positive Real holds ( Big_Oh f) = ( Big_Oh (c (#) f))

    proof

      let f be eventually-nonnegative Real_Sequence, c be positive Real;

      now

        let x be object;

        hereby

          assume x in ( Big_Oh f);

          then

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

           A1: x = t and

           A2: ex c, N st c > 0 & for n st n >= N holds (t . n) <= (c * (f . n)) & (t . n) >= 0 ;

          consider c1, N such that

           A3: c1 > 0 and

           A4: for n st n >= N holds (t . n) <= (c1 * (f . n)) & (t . n) >= 0 by A2;

           A5:

          now

            let n;

            assume

             A6: n >= N;

            then (t . n) <= ((c1 * 1) * (f . n)) by A4;

            then (t . n) <= ((c1 * ((c " ) * c)) * (f . n)) by XCMPLX_0:def 7;

            then (t . n) <= ((c1 * (c " )) * (c * (f . n)));

            hence (t . n) <= ((c1 * (c " )) * ((c (#) f) . n)) & (t . n) >= 0 by A4, A6, SEQ_1: 9;

          end;

          (c1 * (c " )) > ( 0 * (c " )) by A3, XREAL_1: 68;

          hence x in ( Big_Oh (c (#) f)) by A1, A5;

        end;

        assume x in ( Big_Oh (c (#) f));

        then

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

         A7: x = t and

         A8: ex c1, N st c1 > 0 & for n st n >= N holds (t . n) <= (c1 * ((c (#) f) . n)) & (t . n) >= 0 ;

        consider c1, N such that

         A9: c1 > 0 and

         A10: for n st n >= N holds (t . n) <= (c1 * ((c (#) f) . n)) & (t . n) >= 0 by A8;

         A11:

        now

          let n;

          assume

           A12: n >= N;

          then (t . n) <= (c1 * ((c (#) f) . n)) by A10;

          then (t . n) <= (c1 * (c * (f . n))) by SEQ_1: 9;

          hence (t . n) <= ((c1 * c) * (f . n)) & (t . n) >= 0 by A10, A12;

        end;

        (c1 * c) > ( 0 * c) by A9, XREAL_1: 68;

        hence x in ( Big_Oh f) by A7, A11;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: ASYMPT_0:14

    for c be non negative Real, x,f be eventually-nonnegative Real_Sequence holds x in ( Big_Oh f) implies x in ( Big_Oh (c + f))

    proof

      let c be non negative Real, x,f be eventually-nonnegative Real_Sequence;

      assume x in ( Big_Oh f);

      then

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

       A1: x = t and

       A2: ex c1, N st c1 > 0 & for n st n >= N holds (t . n) <= (c1 * (f . n)) & (t . n) >= 0 ;

      consider c1, N such that

       A3: c1 > 0 and

       A4: for n st n >= N holds (t . n) <= (c1 * (f . n)) & (t . n) >= 0 by A2;

      now

        let n;

        ((f . n) + 0 ) <= ((f . n) + c) by XREAL_1: 7;

        then (f . n) <= ((c + f) . n) by VALUED_1: 2;

        then

         A5: (c1 * (f . n)) <= (c1 * ((c + f) . n)) by A3, XREAL_1: 64;

        assume

         A6: n >= N;

        then (t . n) <= (c1 * (f . n)) by A4;

        hence (t . n) <= (c1 * ((c + f) . n)) & (t . n) >= 0 by A4, A6, A5, XXREAL_0: 2;

      end;

      hence thesis by A1, A3;

    end;

    

     Lm3: for f,g be eventually-positive Real_Sequence st (f /" g) is convergent & ( lim (f /" g)) > 0 holds f in ( Big_Oh g)

    proof

      let f,g be eventually-positive Real_Sequence;

      assume that

       A1: (f /" g) is convergent and

       A2: ( lim (f /" g)) > 0 ;

      set l = ( lim (f /" g)), delta = l, c = (2 * l);

      consider N be Nat such that

       A3: for n be Nat st N <= n holds |.(((f /" g) . n) - l).| < delta by A1, A2, SEQ_2:def 7;

      consider N2 be Nat such that

       A4: for n be Nat st n >= N2 holds (g . n) > 0 by Def4;

      consider N1 be Nat such that

       A5: for n be Nat st n >= N1 holds (f . n) >= 0 by Def2;

      reconsider b = ( max (N,N1)) as Element of NAT by ORDINAL1:def 12;

      reconsider a = ( max (b,N2)) as Element of NAT by ORDINAL1:def 12;

       A6:

      now

        let n;

        assume

         A7: n >= a;

        a >= N2 by XXREAL_0: 25;

        then n >= N2 by A7, XXREAL_0: 2;

        then

         A8: (g . n) > 0 by A4;

        a >= b by XXREAL_0: 25;

        then

         A9: n >= b by A7, XXREAL_0: 2;

        b >= N by XXREAL_0: 25;

        then n >= N by A9, XXREAL_0: 2;

        then |.(((f /" g) . n) - l).| < delta by A3;

        then (((f /" g) . n) - l) <= delta by ABSVALUE: 5;

        then ((f /" g) . n) <= ((1 * l) + (1 * l)) by XREAL_1: 20;

        then ((f . n) * ((g " ) . n)) <= c by SEQ_1: 8;

        then ((f . n) * ((g . n) " )) <= c by VALUED_1: 10;

        then (((f . n) * ((g . n) " )) * (g . n)) <= (c * (g . n)) by A8, XREAL_1: 64;

        then ((f . n) * (((g . n) " ) * (g . n))) <= (c * (g . n));

        then ((f . n) * 1) <= (c * (g . n)) by A8, XCMPLX_0:def 7;

        hence (f . n) <= (c * (g . n));

        b >= N1 by XXREAL_0: 25;

        then n >= N1 by A9, XXREAL_0: 2;

        hence (f . n) >= 0 by A5;

      end;

      

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

      (2 * l) > (2 * 0 ) by A2, XREAL_1: 68;

      hence thesis by A10, A6;

    end;

    theorem :: ASYMPT_0:15

    

     Th15: for f,g be eventually-positive Real_Sequence st (f /" g) is convergent & ( lim (f /" g)) > 0 holds ( Big_Oh f) = ( Big_Oh g)

    proof

      let f,g be eventually-positive Real_Sequence;

      assume

       A1: (f /" g) is convergent & ( lim (f /" g)) > 0 ;

      then ( lim (g /" f)) = (( lim (f /" g)) " ) by Th2;

      then

       A2: g in ( Big_Oh f) by A1, Lm3, Th2;

      f in ( Big_Oh g) by A1, Lm3;

      hence thesis by A2, Lm2;

    end;

    theorem :: ASYMPT_0:16

    

     Th16: for f,g be eventually-positive Real_Sequence st (f /" g) is convergent & ( lim (f /" g)) = 0 holds f in ( Big_Oh g) & not g in ( Big_Oh f)

    proof

      let f,g be eventually-positive Real_Sequence;

      assume

       A1: (f /" g) is convergent & ( lim (f /" g)) = 0 ;

      then

      consider N be Nat such that

       A2: for n be Nat st N <= n holds |.(((f /" g) . n) - 0 ).| < 1 by SEQ_2:def 7;

      consider N1 be Nat such that

       A3: for n be Nat st n >= N1 holds (f . n) >= 0 by Def2;

      consider N2 be Nat such that

       A4: for n be Nat st n >= N2 holds (g . n) > 0 by Def4;

      

       A5: not g in ( Big_Oh f)

      proof

        assume g in ( Big_Oh f);

        then

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

         A6: t = g and

         A7: ex c, N st c > 0 & for n st n >= N holds (t . n) <= (c * (f . n)) & (t . n) >= 0 ;

        consider c, N such that

         A8: c > 0 and

         A9: for n st n >= N holds (t . n) <= (c * (f . n)) & (t . n) >= 0 by A7;

        reconsider c as Element of REAL by XREAL_0:def 1;

        set q = ( seq_const (1 / c));

        reconsider a = ( max (N,N2)) as Element of NAT by ORDINAL1:def 12;

        

         A10: a >= N2 by XXREAL_0: 25;

        

         A11: a >= N by XXREAL_0: 25;

        now

          take a;

          let n;

          assume

           A12: n >= a;

          then n >= N by A11, XXREAL_0: 2;

          then (g . n) <= (c * (f . n)) & (g . n) >= 0 by A6, A9;

          then

           A13: ((g . n) * ((g . n) " )) <= ((c * (f . n)) * ((g . n) " )) by XREAL_1: 64;

          n >= N2 by A10, A12, XXREAL_0: 2;

          then (g . n) > 0 by A4;

          then 1 <= ((c * (f . n)) * ((g . n) " )) by A13, XCMPLX_0:def 7;

          then ((c " ) * 1) <= ((c " ) * (c * ((f . n) * ((g . n) " )))) by A8, XREAL_1: 64;

          then ((c " ) * 1) <= (((c " ) * c) * ((f . n) * ((g . n) " )));

          then ((c " ) * 1) <= (1 * ((f . n) * ((g . n) " ))) by A8, XCMPLX_0:def 7;

          then (1 / c) <= ((1 * (f . n)) * ((g . n) " )) by XCMPLX_0:def 9;

          then (1 / c) <= ((1 * (f . n)) / (g . n)) by XCMPLX_0:def 9;

          then (1 / c) <= ((f /" g) . n) by Lm1;

          hence (q . n) <= ((f /" g) . n) by SEQ_1: 57;

        end;

        then

         A14: (f /" g) majorizes q;

        now

          set p = (1 / c);

          let p1 be Real;

          assume

           A15: p1 > 0 ;

          reconsider N as Nat;

          take N;

          let n be Nat;

          assume n >= N;

           |.((q . n) - p).| = |.((1 / c) - (1 / c)).| by SEQ_1: 57

          .= |. 0 .|;

          hence |.((q . n) - p).| < p1 by A15, ABSVALUE: 2;

        end;

        then

         A16: q is convergent by SEQ_2:def 6;

        now

          let p1 be Real;

          assume

           A17: p1 > 0 ;

          reconsider N as Nat;

          take N;

          let n be Nat;

          assume n >= N;

           |.((q . n) - (1 / c)).| = |.((1 / c) - (1 / c)).| by SEQ_1: 57

          .= |. 0 .|;

          hence |.((q . n) - (1 / c)).| < p1 by A17, ABSVALUE: 2;

        end;

        then ( lim q) = (1 / c) by A16, SEQ_2:def 7;

        then (1 / c) <= 0 by A1, A14, A16, Th4;

        then ((1 / c) * c) <= ( 0 * c) by A8;

        hence contradiction by A8, XCMPLX_1: 106;

      end;

      reconsider b = ( max (N,N1)) as Element of NAT by ORDINAL1:def 12;

      reconsider a = ( max (b,N2)) as Element of NAT by ORDINAL1:def 12;

       A18:

      now

        let n;

        assume

         A19: n >= a;

        a >= b by XXREAL_0: 25;

        then

         A20: n >= b by A19, XXREAL_0: 2;

        b >= N by XXREAL_0: 25;

        then n >= N by A20, XXREAL_0: 2;

        then |.(((f /" g) . n) - 0 ).| < 1 by A2;

        then ((f /" g) . n) <= 1 by ABSVALUE: 5;

        then ((f . n) * ((g " ) . n)) <= 1 by SEQ_1: 8;

        then

         A21: ((f . n) * ((g . n) " )) <= 1 by VALUED_1: 10;

        a >= N2 by XXREAL_0: 25;

        then

         A22: n >= N2 by A19, XXREAL_0: 2;

        then

         A23: (g . n) <> 0 by A4;

        (g . n) > 0 by A4, A22;

        then (((f . n) * ((g . n) " )) * (g . n)) <= (1 * (g . n)) by A21, XREAL_1: 64;

        then ((f . n) * (((g . n) " ) * (g . n))) <= (1 * (g . n));

        then ((f . n) * 1) <= (1 * (g . n)) by A23, XCMPLX_0:def 7;

        hence (f . n) <= (1 * (g . n));

        b >= N1 by XXREAL_0: 25;

        then n >= N1 by A20, XXREAL_0: 2;

        hence (f . n) >= 0 by A3;

      end;

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

      hence thesis by A18, A5;

    end;

    theorem :: ASYMPT_0:17

    

     Th17: for f,g be eventually-positive Real_Sequence st (f /" g) is divergent_to+infty holds not f in ( Big_Oh g) & g in ( Big_Oh f)

    proof

      let f,g be eventually-positive Real_Sequence;

      assume (f /" g) is divergent_to+infty;

      then (g /" f) is convergent & ( lim (g /" f)) = 0 by Th5;

      hence thesis by Th16;

    end;

    begin

    definition

      let f be eventually-nonnegative Real_Sequence;

      :: ASYMPT_0:def10

      func Big_Omega (f) -> FUNCTION_DOMAIN of NAT , REAL equals { t where t be Element of ( Funcs ( NAT , REAL )) : ex d, N st d > 0 & for n st n >= N holds (t . n) >= (d * (f . n)) & (t . n) >= 0 };

      coherence

      proof

        set IT = { t where t be Element of ( Funcs ( NAT , REAL )) : ex d, N st d > 0 & for n st n >= N holds (t . n) >= (d * (f . n)) & (t . n) >= 0 };

        

         A1: IT is functional

        proof

          let x be object;

          assume x in IT;

          then ex t be Element of ( Funcs ( NAT , REAL )) st x = t & ex d, N st d > 0 & for n st n >= N holds (t . n) >= (d * (f . n)) & (t . n) >= 0 ;

          hence thesis;

        end;

        consider N be Nat such that

         A2: for n be Nat st n >= N holds (f . n) >= 0 by Def2;

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

        f is Element of ( Funcs ( NAT , REAL )) & for n st n >= N holds (f . n) >= (1 * (f . n)) & (f . n) >= 0 by A2, FUNCT_2: 8;

        then f in IT;

        then

        reconsider IT1 = IT as functional non empty set by A1;

        now

          let x be Element of IT1;

          x in IT;

          then ex t be Element of ( Funcs ( NAT , REAL )) st x = t & ex d, N st d > 0 & for n st n >= N holds (t . n) >= (d * (f . n)) & (t . n) >= 0 ;

          hence x is sequence of REAL ;

        end;

        hence thesis by FUNCT_2:def 12;

      end;

    end

    theorem :: ASYMPT_0:18

    for x be set, f be eventually-nonnegative Real_Sequence st x in ( Big_Omega f) holds x is eventually-nonnegative Real_Sequence

    proof

      let t be set, f be eventually-nonnegative Real_Sequence;

      assume t in ( Big_Omega f);

      then

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

       A1: s = t and

       A2: ex d, N st d > 0 & for n st n >= N holds (s . n) >= (d * (f . n)) & (s . n) >= 0 ;

      reconsider t9 = t as Real_Sequence by A1;

      consider d, N such that d > 0 and

       A3: for n st n >= N holds (s . n) >= (d * (f . n)) & (s . n) >= 0 by A2;

      now

        reconsider N as Nat;

        take N;

        let n be Nat;

        

         A4: n in NAT by ORDINAL1:def 12;

        assume n >= N;

        hence (t9 . n) >= 0 by A1, A3, A4;

      end;

      hence thesis by Def2;

    end;

    theorem :: ASYMPT_0:19

    

     Th19: for f,g be eventually-nonnegative Real_Sequence holds f in ( Big_Omega g) iff g in ( Big_Oh f)

    proof

      let f,g be eventually-nonnegative Real_Sequence;

      

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

      hereby

        consider N1 be Nat such that

         A2: for n be Nat st n >= N1 holds (g . n) >= 0 by Def2;

        assume f in ( Big_Omega g);

        then

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

         A3: f = t and

         A4: ex d, N st d > 0 & for n st n >= N holds (t . n) >= (d * (g . n)) & (t . n) >= 0 ;

        consider d, N such that

         A5: d > 0 and

         A6: for n st n >= N holds (t . n) >= (d * (g . n)) & (t . n) >= 0 by A4;

        reconsider a = ( max (N,N1)) as Element of NAT by ORDINAL1:def 12;

        

         A7: a >= N1 by XXREAL_0: 25;

        

         A8: a >= N by XXREAL_0: 25;

        now

          take a;

          let n;

          assume

           A9: n >= a;

          then n >= N by A8, XXREAL_0: 2;

          then (t . n) >= (d * (g . n)) by A6;

          then ((d " ) * (t . n)) >= ((d " ) * (d * (g . n))) by A5, XREAL_1: 64;

          then ((d " ) * (t . n)) >= (((d " ) * d) * (g . n));

          then ((d " ) * (t . n)) >= (1 * (g . n)) by A5, XCMPLX_0:def 7;

          hence (g . n) <= ((d " ) * (f . n)) by A3;

          n >= N1 by A7, A9, XXREAL_0: 2;

          hence (g . n) >= 0 by A2;

        end;

        hence g in ( Big_Oh f) by A1, A5;

      end;

      assume g in ( Big_Oh f);

      then

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

       A10: g = t and

       A11: ex c, N st c > 0 & for n st n >= N holds (t . n) <= (c * (f . n)) & (t . n) >= 0 ;

      consider c, N such that

       A12: c > 0 and

       A13: for n st n >= N holds (t . n) <= (c * (f . n)) & (t . n) >= 0 by A11;

      consider N1 be Nat such that

       A14: for n be Nat st n >= N1 holds (f . n) >= 0 by Def2;

      reconsider a = ( max (N,N1)) as Element of NAT by ORDINAL1:def 12;

      

       A15: a >= N1 by XXREAL_0: 25;

      

       A16: a >= N by XXREAL_0: 25;

       A17:

      now

        take a;

        let n;

        assume

         A18: n >= a;

        then n >= N by A16, XXREAL_0: 2;

        then (t . n) <= (c * (f . n)) by A13;

        then ((c " ) * (t . n)) <= ((c " ) * (c * (f . n))) by A12, XREAL_1: 64;

        then ((c " ) * (t . n)) <= (((c " ) * c) * (f . n));

        then ((c " ) * (t . n)) <= (1 * (f . n)) by A12, XCMPLX_0:def 7;

        hence (f . n) >= ((c " ) * (g . n)) by A10;

        n >= N1 by A15, A18, XXREAL_0: 2;

        hence (f . n) >= 0 by A14;

      end;

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

      hence thesis by A12, A17;

    end;

    theorem :: ASYMPT_0:20

    

     Th20: for f be eventually-nonnegative Real_Sequence holds f in ( Big_Omega f)

    proof

      let f be eventually-nonnegative Real_Sequence;

      f in ( Big_Oh f) by Th10;

      hence thesis by Th19;

    end;

    theorem :: ASYMPT_0:21

    

     Th21: for f,g,h be eventually-nonnegative Real_Sequence holds f in ( Big_Omega g) & g in ( Big_Omega h) implies f in ( Big_Omega h)

    proof

      let f,g,h be eventually-nonnegative Real_Sequence;

      assume f in ( Big_Omega g) & g in ( Big_Omega h);

      then h in ( Big_Oh g) & g in ( Big_Oh f) by Th19;

      then h in ( Big_Oh f) by Th12;

      hence thesis by Th19;

    end;

    theorem :: ASYMPT_0:22

    for f,g be eventually-positive Real_Sequence st (f /" g) is convergent & ( lim (f /" g)) > 0 holds ( Big_Omega f) = ( Big_Omega g)

    proof

      let f,g be eventually-positive Real_Sequence;

      assume

       A1: (f /" g) is convergent & ( lim (f /" g)) > 0 ;

      now

        let x be object;

        hereby

          g in ( Big_Oh g) by Th10;

          then g in ( Big_Oh f) by A1, Th15;

          then

           A2: f in ( Big_Omega g) by Th19;

          assume x in ( Big_Omega f);

          then

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

           A3: x = t and

           A4: ex d, N st d > 0 & for n st n >= N holds (d * (f . n)) <= (t . n) & (t . n) >= 0 ;

          consider d, N such that d > 0 and

           A5: for n st n >= N holds (d * (f . n)) <= (t . n) & (t . n) >= 0 by A4;

          now

            reconsider N as Nat;

            take N;

            let n be Nat;

            

             A6: n in NAT by ORDINAL1:def 12;

            assume n >= N;

            hence (t . n) >= 0 by A5, A6;

          end;

          then

           A7: t is eventually-nonnegative;

          t in ( Big_Omega f) by A4;

          hence x in ( Big_Omega g) by A3, A7, A2, Th21;

        end;

        assume x in ( Big_Omega g);

        then

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

         A8: x = t and

         A9: ex d, N st d > 0 & for n st n >= N holds (d * (g . n)) <= (t . n) & (t . n) >= 0 ;

        consider d, N such that d > 0 and

         A10: for n st n >= N holds (d * (g . n)) <= (t . n) & (t . n) >= 0 by A9;

        now

          reconsider N as Nat;

          take N;

          let n be Nat;

          

           A11: n in NAT by ORDINAL1:def 12;

          assume n >= N;

          hence (t . n) >= 0 by A10, A11;

        end;

        then

         A12: t is eventually-nonnegative;

        f in ( Big_Oh f) by Th10;

        then f in ( Big_Oh g) by A1, Th15;

        then

         A13: g in ( Big_Omega f) by Th19;

        t in ( Big_Omega g) by A9;

        hence x in ( Big_Omega f) by A8, A12, A13, Th21;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: ASYMPT_0:23

    

     Th23: for f,g be eventually-positive Real_Sequence st (f /" g) is convergent & ( lim (f /" g)) = 0 holds g in ( Big_Omega f) & not f in ( Big_Omega g)

    proof

      let f,g be eventually-positive Real_Sequence;

      assume (f /" g) is convergent & ( lim (f /" g)) = 0 ;

      then f in ( Big_Oh g) & not g in ( Big_Oh f) by Th16;

      hence thesis by Th19;

    end;

    theorem :: ASYMPT_0:24

    for f,g be eventually-positive Real_Sequence st (f /" g) is divergent_to+infty holds not g in ( Big_Omega f) & f in ( Big_Omega g)

    proof

      let f,g be eventually-positive Real_Sequence;

      assume (f /" g) is divergent_to+infty;

      then (g /" f) is convergent & ( lim (g /" f)) = 0 by Th5;

      hence thesis by Th23;

    end;

    theorem :: ASYMPT_0:25

    for f,t be positive Real_Sequence holds t in ( Big_Omega f) iff ex d st d > 0 & for n holds (d * (f . n)) <= (t . n)

    proof

      let f,t be positive Real_Sequence;

      hereby

        assume t in ( Big_Omega f);

        then

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

         A1: s = t and

         A2: ex d, N st d > 0 & for n st n >= N holds (d * (f . n)) <= (s . n) & (s . n) >= 0 ;

        consider d, N such that

         A3: d > 0 and

         A4: for n st n >= N holds (d * (f . n)) <= (s . n) & (s . n) >= 0 by A2;

        per cases ;

          suppose

           A5: N = 0 ;

          take d;

          thus d > 0 by A3;

          let n;

          thus (d * (f . n)) <= (t . n) by A1, A4, A5;

        end;

          suppose

           A6: N > 0 ;

          deffunc F( Element of NAT ) = ((t . $1) / (f . $1));

          reconsider B = { F(n) : n < N } as finite non empty Subset of REAL from FinImInit2( A6);

          set b = ( min B);

          

           A7: for n st n < N holds (b * (f . n)) <= (t . n)

          proof

            let n;

            

             A8: (f . n) > 0 by Def3;

            assume n < N;

            then ((t . n) / (f . n)) in B;

            then ((t . n) / (f . n)) >= b by XXREAL_2:def 7;

            then (((t . n) / (f . n)) * (f . n)) >= (b * (f . n)) by A8, XREAL_1: 64;

            hence thesis by A8, XCMPLX_1: 87;

          end;

          thus ex d st d > 0 & for n holds (d * (f . n)) <= (t . n)

          proof

            per cases ;

              suppose

               A9: b <= d;

              reconsider b as Element of REAL by XREAL_0:def 1;

              take b;

              b in B by XXREAL_2:def 7;

              then

              consider n1 such that

               A10: b = ((t . n1) / (f . n1)) and n1 < N;

              (t . n1) > 0 & (f . n1) > 0 by Def3;

              then ((t . n1) * ((f . n1) " )) > ( 0 * ((f . n1) " )) by XREAL_1: 68;

              hence b > 0 by A10, XCMPLX_0:def 9;

              let n;

              thus (b * (f . n)) <= (t . n)

              proof

                per cases ;

                  suppose n < N;

                  hence thesis by A7;

                end;

                  suppose

                   A11: n >= N;

                  (f . n) > 0 by Def3;

                  then

                   A12: (b * (f . n)) <= (d * (f . n)) by A9, XREAL_1: 64;

                  (d * (f . n)) <= (t . n) by A1, A4, A11;

                  hence thesis by A12, XXREAL_0: 2;

                end;

              end;

            end;

              suppose

               A13: b > d;

              take d;

              thus d > 0 by A3;

              let n;

              thus (d * (f . n)) <= (t . n)

              proof

                per cases ;

                  suppose

                   A14: n < N;

                  (f . n) > 0 by Def3;

                  then

                   A15: (d * (f . n)) <= (b * (f . n)) by A13, XREAL_1: 64;

                  (b * (f . n)) <= (t . n) by A7, A14;

                  hence thesis by A15, XXREAL_0: 2;

                end;

                  suppose n >= N;

                  hence thesis by A1, A4;

                end;

              end;

            end;

          end;

        end;

      end;

      given d such that

       A16: d > 0 and

       A17: for n holds (d * (f . n)) <= (t . n);

      t is Element of ( Funcs ( NAT , REAL )) & for n st n >= 0 holds (d * (f . n)) <= (t . n) & (t . n) >= 0 by A17, Def3, FUNCT_2: 8;

      hence thesis by A16;

    end;

    theorem :: ASYMPT_0:26

    for f,g be eventually-nonnegative Real_Sequence holds ( Big_Omega (f + g)) = ( Big_Omega ( max (f,g)))

    proof

      let f,g be eventually-nonnegative Real_Sequence;

      consider N1 be Nat such that

       A1: for n be Nat st n >= N1 holds (f . n) >= 0 by Def2;

      consider N2 be Nat such that

       A2: for n be Nat st n >= N2 holds (g . n) >= 0 by Def2;

      now

        let x be object;

        hereby

          assume x in ( Big_Omega (f + g));

          then

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

           A3: t = x and

           A4: ex d, N st d > 0 & for n st n >= N holds (d * ((f + g) . n)) <= (t . n) & (t . n) >= 0 ;

          consider d, N such that

           A5: d > 0 and

           A6: for n st n >= N holds (d * ((f + g) . n)) <= (t . n) & (t . n) >= 0 by A4;

          reconsider a = ( max (N,( max (N1,N2)))) as Element of NAT by ORDINAL1:def 12;

          

           A7: a >= N by XXREAL_0: 25;

          

           A8: a >= ( max (N1,N2)) by XXREAL_0: 25;

          ( max (N1,N2)) >= N2 by XXREAL_0: 25;

          then

           A9: a >= N2 by A8, XXREAL_0: 2;

          ( max (N1,N2)) >= N1 by XXREAL_0: 25;

          then

           A10: a >= N1 by A8, XXREAL_0: 2;

          now

            let n;

            assume

             A11: n >= a;

            then n >= N1 by A10, XXREAL_0: 2;

            then

             A12: (f . n) >= 0 by A1;

            n >= N2 by A9, A11, XXREAL_0: 2;

            then

             A13: (g . n) >= 0 by A2;

            

             A14: (( max (f,g)) . n) = ( max ((f . n),(g . n))) by Def7;

            (( max (f,g)) . n) <= ((f + g) . n)

            proof

              per cases by A14, XXREAL_0: 16;

                suppose (( max (f,g)) . n) = (f . n);

                then ((( max (f,g)) . n) + 0 ) <= ((f . n) + (g . n)) by A13, XREAL_1: 7;

                hence thesis by SEQ_1: 7;

              end;

                suppose (( max (f,g)) . n) = (g . n);

                then ((( max (f,g)) . n) + 0 ) <= ((g . n) + (f . n)) by A12, XREAL_1: 7;

                hence thesis by SEQ_1: 7;

              end;

            end;

            then

             A15: (d * (( max (f,g)) . n)) <= (d * ((f + g) . n)) by A5, XREAL_1: 64;

            

             A16: n >= N by A7, A11, XXREAL_0: 2;

            then (d * ((f + g) . n)) <= (t . n) by A6;

            hence (d * (( max (f,g)) . n)) <= (t . n) by A15, XXREAL_0: 2;

            thus (t . n) >= 0 by A6, A16;

          end;

          hence x in ( Big_Omega ( max (f,g))) by A3, A5;

        end;

        assume x in ( Big_Omega ( max (f,g)));

        then

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

         A17: t = x and

         A18: ex d, N st d > 0 & for n st n >= N holds (d * (( max (f,g)) . n)) <= (t . n) & (t . n) >= 0 ;

        consider d, N such that

         A19: d > 0 and

         A20: for n st n >= N holds (d * (( max (f,g)) . n)) <= (t . n) & (t . n) >= 0 by A18;

        reconsider a = ( max (N,( max (N1,N2)))) as Element of NAT by ORDINAL1:def 12;

        

         A21: N <= a by XXREAL_0: 25;

         A22:

        now

          let n;

          (f . n) <= ( max ((f . n),(g . n))) & (g . n) <= ( max ((f . n),(g . n))) by XXREAL_0: 25;

          then ((f . n) + (g . n)) <= ((1 * ( max ((f . n),(g . n)))) + (1 * ( max ((f . n),(g . n))))) by XREAL_1: 7;

          then ((2 " ) * ((f . n) + (g . n))) <= ((2 " ) * (2 * ( max ((f . n),(g . n))))) by XREAL_1: 64;

          then ((2 " ) * ((f + g) . n)) <= ( max ((f . n),(g . n))) by SEQ_1: 7;

          then (d * ((2 " ) * ((f + g) . n))) <= (d * ( max ((f . n),(g . n)))) by A19, XREAL_1: 64;

          then

           A23: (d * ((2 " ) * ((f + g) . n))) <= (d * (( max (f,g)) . n)) by Def7;

          assume n >= a;

          then

           A24: n >= N by A21, XXREAL_0: 2;

          then (d * (( max (f,g)) . n)) <= (t . n) by A20;

          hence ((d * (2 " )) * ((f + g) . n)) <= (t . n) by A23, XXREAL_0: 2;

          thus (t . n) >= 0 by A20, A24;

        end;

        (d * (2 " )) > (d * 0 ) by A19, XREAL_1: 68;

        hence x in ( Big_Omega (f + g)) by A17, A22;

      end;

      hence thesis by TARSKI: 2;

    end;

    definition

      let f be eventually-nonnegative Real_Sequence;

      :: ASYMPT_0:def11

      func Big_Theta (f) -> FUNCTION_DOMAIN of NAT , REAL equals (( Big_Oh f) /\ ( Big_Omega f));

      coherence

      proof

        f in ( Big_Oh f) & f in ( Big_Omega f) by Th10, Th20;

        then

         A1: (( Big_Oh f) /\ ( Big_Omega f)) is non empty by XBOOLE_0:def 4;

        now

          let x be Element of (( Big_Oh f) /\ ( Big_Omega f));

          x in ( Big_Oh f) by A1, XBOOLE_0:def 4;

          hence x is sequence of REAL by Th6;

        end;

        hence thesis by A1, FUNCT_2:def 12;

      end;

    end

    theorem :: ASYMPT_0:27

    

     Th27: for f be eventually-nonnegative Real_Sequence holds ( Big_Theta f) = { t where t be Element of ( Funcs ( NAT , REAL )) : ex c, d, N st c > 0 & d > 0 & for n st n >= N holds (d * (f . n)) <= (t . n) & (t . n) <= (c * (f . n)) }

    proof

      let f be eventually-nonnegative Real_Sequence;

      set BT = { t where t be Element of ( Funcs ( NAT , REAL )) : ex c, d, N st c > 0 & d > 0 & for n st n >= N holds (d * (f . n)) <= (t . n) & (t . n) <= (c * (f . n)) };

      now

        let x be object;

        hereby

          assume

           A1: x in ( Big_Theta f);

          then x in ( Big_Oh f) by XBOOLE_0:def 4;

          then

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

           A2: x = t and

           A3: ex c, N st c > 0 & for n st n >= N holds (t . n) <= (c * (f . n)) & (t . n) >= 0 ;

          x in ( Big_Omega f) by A1, XBOOLE_0:def 4;

          then

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

           A4: x = s and

           A5: ex d, N st d > 0 & for n st n >= N holds (s . n) >= (d * (f . n)) & (s . n) >= 0 ;

          consider c, N such that

           A6: c > 0 and

           A7: for n st n >= N holds (t . n) <= (c * (f . n)) & (t . n) >= 0 by A3;

          consider d, N1 such that

           A8: d > 0 and

           A9: for n st n >= N1 holds (s . n) >= (d * (f . n)) & (s . n) >= 0 by A5;

          set a = ( max (N,N1));

          

           A10: a >= N & a >= N1 by XXREAL_0: 25;

          now

            take a;

            let n;

            assume n >= a;

            then n >= N & n >= N1 by A10, XXREAL_0: 2;

            hence (d * (f . n)) <= (t . n) & (t . n) <= (c * (f . n)) by A2, A4, A7, A9;

          end;

          hence x in BT by A2, A6, A8;

        end;

        assume x in BT;

        then

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

         A11: x = t and

         A12: ex c, d, N st c > 0 & d > 0 & for n st n >= N holds (d * (f . n)) <= (t . n) & (t . n) <= (c * (f . n));

        consider c, d, N such that

         A13: c > 0 and

         A14: d > 0 and

         A15: for n st n >= N holds (d * (f . n)) <= (t . n) & (t . n) <= (c * (f . n)) by A12;

        consider N1 be Nat such that

         A16: for n be Nat st n >= N1 holds (f . n) >= 0 by Def2;

        reconsider a = ( max (N,N1)) as Element of NAT by ORDINAL1:def 12;

        

         A17: a >= N1 by XXREAL_0: 25;

        

         A18: a >= N by XXREAL_0: 25;

        now

          take a;

          let n;

          assume

           A19: n >= a;

          then

           A20: n >= N by A18, XXREAL_0: 2;

          hence (d * (f . n)) <= (t . n) by A15;

          n >= N1 by A17, A19, XXREAL_0: 2;

          then (f . n) >= 0 by A16;

          then (d * (f . n)) >= (d * 0 ) by A14;

          hence (t . n) >= 0 by A15, A20;

        end;

        then

         A21: x in ( Big_Omega f) by A11, A14;

        now

          take a;

          let n;

          assume

           A22: n >= a;

          then

           A23: n >= N by A18, XXREAL_0: 2;

          hence (t . n) <= (c * (f . n)) by A15;

          n >= N1 by A17, A22, XXREAL_0: 2;

          then (f . n) >= 0 by A16;

          then (d * (f . n)) >= (d * 0 ) by A14;

          hence (t . n) >= 0 by A15, A23;

        end;

        then x in ( Big_Oh f) by A11, A13;

        hence x in ( Big_Theta f) by A21, XBOOLE_0:def 4;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: ASYMPT_0:28

    for f be eventually-nonnegative Real_Sequence holds f in ( Big_Theta f)

    proof

      let f be eventually-nonnegative Real_Sequence;

      f in ( Big_Oh f) & f in ( Big_Omega f) by Th10, Th20;

      hence thesis by XBOOLE_0:def 4;

    end;

    theorem :: ASYMPT_0:29

    for f,g be eventually-nonnegative Real_Sequence st f in ( Big_Theta g) holds g in ( Big_Theta f)

    proof

      let f,g be eventually-nonnegative Real_Sequence;

      assume

       A1: f in ( Big_Theta g);

      then f in ( Big_Omega g) by XBOOLE_0:def 4;

      then

       A2: g in ( Big_Oh f) by Th19;

      f in ( Big_Oh g) by A1, XBOOLE_0:def 4;

      then g in ( Big_Omega f) by Th19;

      hence thesis by A2, XBOOLE_0:def 4;

    end;

    theorem :: ASYMPT_0:30

    for f,g,h be eventually-nonnegative Real_Sequence st f in ( Big_Theta g) & g in ( Big_Theta h) holds f in ( Big_Theta h)

    proof

      let f,g,h be eventually-nonnegative Real_Sequence;

      assume

       A1: f in ( Big_Theta g) & g in ( Big_Theta h);

      then f in ( Big_Omega g) & g in ( Big_Omega h) by XBOOLE_0:def 4;

      then

       A2: f in ( Big_Omega h) by Th21;

      f in ( Big_Oh g) & g in ( Big_Oh h) by A1, XBOOLE_0:def 4;

      then f in ( Big_Oh h) by Th12;

      hence thesis by A2, XBOOLE_0:def 4;

    end;

    theorem :: ASYMPT_0:31

    for f,t be positive Real_Sequence holds t in ( Big_Theta f) iff ex c, d st c > 0 & d > 0 & for n holds (d * (f . n)) <= (t . n) & (t . n) <= (c * (f . n))

    proof

      let f,t be positive Real_Sequence;

      

       A1: ( Big_Theta f) = { s where s be Element of ( Funcs ( NAT , REAL )) : ex c, d, N st c > 0 & d > 0 & for n st n >= N holds (d * (f . n)) <= (s . n) & (s . n) <= (c * (f . n)) } by Th27;

      hereby

        assume t in ( Big_Theta f);

        then

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

         A2: s = t and

         A3: ex c, d, N st c > 0 & d > 0 & for n st n >= N holds (d * (f . n)) <= (s . n) & (s . n) <= (c * (f . n)) by A1;

        consider c, d, N such that

         A4: c > 0 and

         A5: d > 0 and

         A6: for n st n >= N holds (d * (f . n)) <= (s . n) & (s . n) <= (c * (f . n)) by A3;

        per cases ;

          suppose

           A7: N = 0 ;

          take c, d;

          thus c > 0 by A4;

          thus d > 0 by A5;

          let n;

          thus (d * (f . n)) <= (t . n) & (t . n) <= (c * (f . n)) by A2, A6, A7;

        end;

          suppose

           A8: N > 0 ;

          deffunc F( Element of NAT ) = ((t . $1) / (f . $1));

          reconsider B = { F(n) : n < N } as finite non empty Subset of REAL from FinImInit2( A8);

          set b = ( max B);

          set a = ( min B);

          

           A9: for n st n < N holds (t . n) >= (a * (f . n))

          proof

            let n;

            

             A10: (f . n) > 0 by Def3;

            assume n < N;

            then ((t . n) / (f . n)) in B;

            then ((t . n) / (f . n)) >= a by XXREAL_2:def 7;

            then (((t . n) / (f . n)) * (f . n)) >= (a * (f . n)) by A10, XREAL_1: 64;

            hence thesis by A10, XCMPLX_1: 87;

          end;

          

           A11: for n st n < N holds (t . n) <= (b * (f . n))

          proof

            let n;

            

             A12: (f . n) > 0 by Def3;

            assume n < N;

            then ((t . n) / (f . n)) in B;

            then ((t . n) / (f . n)) <= b by XXREAL_2:def 8;

            then (((t . n) / (f . n)) * (f . n)) <= (b * (f . n)) by A12, XREAL_1: 64;

            hence thesis by A12, XCMPLX_1: 87;

          end;

          thus ex c, d st c > 0 & d > 0 & for n holds (d * (f . n)) <= (t . n) & (t . n) <= (c * (f . n))

          proof

            set D = ( min (a,d));

            set C = ( max (b,c));

            reconsider C, D as Element of REAL by XREAL_0:def 1;

            take C, D;

            thus C > 0 by A4, XXREAL_0: 25;

             A13:

            now

              let n;

              (f . n) > 0 & (t . n) > 0 by Def3;

              then ( 0 * ((f . n) " )) < ((t . n) * ((f . n) " )) by XREAL_1: 68;

              hence 0 < ((t . n) / (f . n)) by XCMPLX_0:def 9;

            end;

            a > 0

            proof

              a in B by XXREAL_2:def 7;

              then ex n st a = ((t . n) / (f . n)) & n < N;

              hence thesis by A13;

            end;

            hence D > 0 by A5, XXREAL_0: 15;

            let n;

            

             A14: (f . n) > 0 by Def3;

            per cases ;

              suppose

               A15: n < N;

              

               A16: (D * (f . n)) <= (a * (f . n)) by A14, XREAL_1: 64, XXREAL_0: 17;

              (a * (f . n)) <= (t . n) by A9, A15;

              hence (D * (f . n)) <= (t . n) by A16, XXREAL_0: 2;

              

               A17: (b * (f . n)) <= (C * (f . n)) by A14, XREAL_1: 64, XXREAL_0: 25;

              (t . n) <= (b * (f . n)) by A11, A15;

              hence thesis by A17, XXREAL_0: 2;

            end;

              suppose

               A18: n >= N;

              

               A19: (D * (f . n)) <= (d * (f . n)) by A14, XREAL_1: 64, XXREAL_0: 17;

              (d * (f . n)) <= (t . n) by A2, A6, A18;

              hence (D * (f . n)) <= (t . n) by A19, XXREAL_0: 2;

              

               A20: (c * (f . n)) <= (C * (f . n)) by A14, XREAL_1: 64, XXREAL_0: 25;

              (t . n) <= (c * (f . n)) by A2, A6, A18;

              hence thesis by A20, XXREAL_0: 2;

            end;

          end;

        end;

      end;

      given c, d such that

       A21: c > 0 & d > 0 and

       A22: for n holds (d * (f . n)) <= (t . n) & (t . n) <= (c * (f . n));

      t is Element of ( Funcs ( NAT , REAL )) & for n st n >= 0 holds (d * (f . n)) <= (t . n) & (t . n) <= (c * (f . n)) by A22, FUNCT_2: 8;

      hence thesis by A1, A21;

    end;

    theorem :: ASYMPT_0:32

    for f,g be eventually-nonnegative Real_Sequence holds ( Big_Theta (f + g)) = ( Big_Theta ( max (f,g)))

    proof

      let f,g be eventually-nonnegative Real_Sequence;

      

       A1: ( Big_Theta ( max (f,g))) = { s where s be Element of ( Funcs ( NAT , REAL )) : ex c, d, N st c > 0 & d > 0 & for n st n >= N holds (d * (( max (f,g)) . n)) <= (s . n) & (s . n) <= (c * (( max (f,g)) . n)) } by Th27;

      consider N2 be Nat such that

       A2: for n be Nat st n >= N2 holds (g . n) >= 0 by Def2;

      consider N1 be Nat such that

       A3: for n be Nat st n >= N1 holds (f . n) >= 0 by Def2;

      

       A4: ( Big_Theta (f + g)) = { s where s be Element of ( Funcs ( NAT , REAL )) : ex c, d, N st c > 0 & d > 0 & for n st n >= N holds (d * ((f + g) . n)) <= (s . n) & (s . n) <= (c * ((f + g) . n)) } by Th27;

      now

        let x be object;

        hereby

          assume x in ( Big_Theta (f + g));

          then

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

           A5: t = x and

           A6: ex c, d, N st c > 0 & d > 0 & for n st n >= N holds (d * ((f + g) . n)) <= (t . n) & (t . n) <= (c * ((f + g) . n)) by A4;

          consider c, d, N such that

           A7: c > 0 and

           A8: d > 0 and

           A9: for n st n >= N holds (d * ((f + g) . n)) <= (t . n) & (t . n) <= (c * ((f + g) . n)) by A6;

          reconsider a = ( max (N,( max (N1,N2)))) as Element of NAT by ORDINAL1:def 12;

          

           A10: a >= N by XXREAL_0: 25;

          

           A11: a >= ( max (N1,N2)) by XXREAL_0: 25;

          ( max (N1,N2)) >= N2 by XXREAL_0: 25;

          then

           A12: a >= N2 by A11, XXREAL_0: 2;

          ( max (N1,N2)) >= N1 by XXREAL_0: 25;

          then

           A13: a >= N1 by A11, XXREAL_0: 2;

           A14:

          now

            let n;

            

             A15: (g . n) <= ( max ((f . n),(g . n))) & ((1 * (( max (f,g)) . n)) + (1 * (( max (f,g)) . n))) = ((1 + 1) * (( max (f,g)) . n)) by XXREAL_0: 25;

            

             A16: (( max (f,g)) . n) = ( max ((f . n),(g . n))) by Def7;

            ((f + g) . n) = ((f . n) + (g . n)) & (f . n) <= ( max ((f . n),(g . n))) by SEQ_1: 7, XXREAL_0: 25;

            then ((f + g) . n) <= (2 * (( max (f,g)) . n)) by A16, A15, XREAL_1: 7;

            then

             A17: (c * ((f + g) . n)) <= (c * (2 * (( max (f,g)) . n))) by A7, XREAL_1: 64;

            assume

             A18: n >= a;

            then n >= N2 by A12, XXREAL_0: 2;

            then

             A19: (g . n) >= 0 by A2;

            n >= N1 by A13, A18, XXREAL_0: 2;

            then

             A20: (f . n) >= 0 by A3;

            (( max (f,g)) . n) <= ((f + g) . n)

            proof

              per cases by A16, XXREAL_0: 16;

                suppose (( max (f,g)) . n) = (f . n);

                then ((( max (f,g)) . n) + 0 ) <= ((f . n) + (g . n)) by A19, XREAL_1: 7;

                hence thesis by SEQ_1: 7;

              end;

                suppose (( max (f,g)) . n) = (g . n);

                then ((( max (f,g)) . n) + 0 ) <= ((g . n) + (f . n)) by A20, XREAL_1: 7;

                hence thesis by SEQ_1: 7;

              end;

            end;

            then

             A21: (d * (( max (f,g)) . n)) <= (d * ((f + g) . n)) by A8, XREAL_1: 64;

            n >= N by A10, A18, XXREAL_0: 2;

            then (t . n) <= (c * ((f + g) . n)) & (d * ((f + g) . n)) <= (t . n) by A9;

            hence (d * (( max (f,g)) . n)) <= (t . n) & (t . n) <= ((2 * c) * (( max (f,g)) . n)) by A17, A21, XXREAL_0: 2;

          end;

          (2 * c) > (2 * 0 ) by A7, XREAL_1: 68;

          hence x in ( Big_Theta ( max (f,g))) by A1, A5, A8, A14;

        end;

        consider N1 be Nat such that

         A22: for n be Nat st n >= N1 holds (f . n) >= 0 by Def2;

        consider N2 be Nat such that

         A23: for n be Nat st n >= N2 holds (g . n) >= 0 by Def2;

        assume x in ( Big_Theta ( max (f,g)));

        then

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

         A24: t = x and

         A25: ex c, d, N st c > 0 & d > 0 & for n st n >= N holds (d * (( max (f,g)) . n)) <= (t . n) & (t . n) <= (c * (( max (f,g)) . n)) by A1;

        consider c, d, N such that

         A26: c > 0 and

         A27: d > 0 and

         A28: for n st n >= N holds (d * (( max (f,g)) . n)) <= (t . n) & (t . n) <= (c * (( max (f,g)) . n)) by A25;

        reconsider a = ( max (N,( max (N1,N2)))) as Element of NAT by ORDINAL1:def 12;

        

         A29: ( max (N1,N2)) <= a by XXREAL_0: 25;

        N2 <= ( max (N1,N2)) by XXREAL_0: 25;

        then

         A30: N2 <= a by A29, XXREAL_0: 2;

        

         A31: N <= a by XXREAL_0: 25;

        N1 <= ( max (N1,N2)) by XXREAL_0: 25;

        then

         A32: N1 <= a by A29, XXREAL_0: 2;

         A33:

        now

          let n;

          assume

           A34: n >= a;

          then n >= N1 by A32, XXREAL_0: 2;

          then (f . n) >= 0 by A22;

          then

           A35: ((f . n) + (g . n)) >= ( 0 + (g . n)) by XREAL_1: 7;

          (f . n) <= ( max ((f . n),(g . n))) & (g . n) <= ( max ((f . n),(g . n))) by XXREAL_0: 25;

          then ((f . n) + (g . n)) <= ((1 * ( max ((f . n),(g . n)))) + (1 * ( max ((f . n),(g . n))))) by XREAL_1: 7;

          then ((2 " ) * ((f . n) + (g . n))) <= ((2 " ) * (2 * ( max ((f . n),(g . n))))) by XREAL_1: 64;

          then ((2 " ) * ((f + g) . n)) <= ( max ((f . n),(g . n))) by SEQ_1: 7;

          then (d * ((2 " ) * ((f + g) . n))) <= (d * ( max ((f . n),(g . n)))) by A27, XREAL_1: 64;

          then

           A36: (d * ((2 " ) * ((f + g) . n))) <= (d * (( max (f,g)) . n)) by Def7;

          n >= N2 by A30, A34, XXREAL_0: 2;

          then (g . n) >= 0 by A23;

          then

           A37: ((f . n) + (g . n)) >= ((f . n) + 0 ) by XREAL_1: 7;

          (( max (f,g)) . n) = ( max ((f . n),(g . n))) & ((f + g) . n) = ((f . n) + (g . n)) by Def7, SEQ_1: 7;

          then (( max (f,g)) . n) <= ((f + g) . n) by A37, A35, XXREAL_0: 16;

          then

           A38: (c * (( max (f,g)) . n)) <= (c * ((f + g) . n)) by A26, XREAL_1: 64;

          n >= N by A31, A34, XXREAL_0: 2;

          then (t . n) <= (c * (( max (f,g)) . n)) & (d * (( max (f,g)) . n)) <= (t . n) by A28;

          hence ((d * (2 " )) * ((f + g) . n)) <= (t . n) & (t . n) <= (c * ((f + g) . n)) by A38, A36, XXREAL_0: 2;

        end;

        (d * (2 " )) > (d * 0 ) by A27, XREAL_1: 68;

        hence x in ( Big_Theta (f + g)) by A4, A24, A26, A33;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: ASYMPT_0:33

    for f,g be eventually-positive Real_Sequence st (f /" g) is convergent & ( lim (f /" g)) > 0 holds f in ( Big_Theta g)

    proof

      let f,g be eventually-positive Real_Sequence;

      assume (f /" g) is convergent & ( lim (f /" g)) > 0 ;

      then

       A1: ( Big_Oh f) = ( Big_Oh g) by Th15;

      then g in ( Big_Oh f) by Th10;

      then

       A2: f in ( Big_Omega g) by Th19;

      f in ( Big_Oh g) by A1, Th10;

      hence thesis by A2, XBOOLE_0:def 4;

    end;

    theorem :: ASYMPT_0:34

    for f,g be eventually-positive Real_Sequence st (f /" g) is convergent & ( lim (f /" g)) = 0 holds f in ( Big_Oh g) & not f in ( Big_Theta g)

    proof

      let f,g be eventually-positive Real_Sequence;

      assume

       A1: (f /" g) is convergent & ( lim (f /" g)) = 0 ;

      now

        assume f in ( Big_Theta g);

        then f in ( Big_Omega g) by XBOOLE_0:def 4;

        then g in ( Big_Oh f) by Th19;

        hence contradiction by A1, Th16;

      end;

      hence thesis by A1, Th16;

    end;

    theorem :: ASYMPT_0:35

    for f,g be eventually-positive Real_Sequence st (f /" g) is divergent_to+infty holds f in ( Big_Omega g) & not f in ( Big_Theta g)

    proof

      let f,g be eventually-positive Real_Sequence;

      assume (f /" g) is divergent_to+infty;

      then ( not f in ( Big_Oh g)) & g in ( Big_Oh f) by Th17;

      hence thesis by Th19, XBOOLE_0:def 4;

    end;

    begin

    definition

      let f be eventually-nonnegative Real_Sequence, X be set;

      :: ASYMPT_0:def12

      func Big_Oh (f,X) -> FUNCTION_DOMAIN of NAT , REAL equals { t where t be Element of ( Funcs ( NAT , REAL )) : ex c, N st c > 0 & for n st n >= N & n in X holds (t . n) <= (c * (f . n)) & (t . n) >= 0 };

      coherence

      proof

        set IT = { t where t be Element of ( Funcs ( NAT , REAL )) : ex c, N st c > 0 & for n st n >= N & n in X holds (t . n) <= (c * (f . n)) & (t . n) >= 0 };

        

         A1: IT is functional

        proof

          let x be object;

          assume x in IT;

          then ex t be Element of ( Funcs ( NAT , REAL )) st x = t & ex c, N st c > 0 & for n st n >= N & n in X holds (t . n) <= (c * (f . n)) & (t . n) >= 0 ;

          hence thesis;

        end;

        consider N be Nat such that

         A2: for n be Nat st n >= N holds (f . n) >= 0 by Def2;

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

        f is Element of ( Funcs ( NAT , REAL )) & for n st n >= N & n in X holds (f . n) <= (1 * (f . n)) & (f . n) >= 0 by A2, FUNCT_2: 8;

        then f in IT;

        then

        reconsider IT1 = IT as functional non empty set by A1;

        now

          let x be Element of IT1;

          x in IT;

          then ex t be Element of ( Funcs ( NAT , REAL )) st x = t & ex c, N st c > 0 & for n st n >= N & n in X holds (t . n) <= (c * (f . n)) & (t . n) >= 0 ;

          hence x is sequence of REAL ;

        end;

        hence thesis by FUNCT_2:def 12;

      end;

    end

    definition

      let f be eventually-nonnegative Real_Sequence, X be set;

      :: ASYMPT_0:def13

      func Big_Omega (f,X) -> FUNCTION_DOMAIN of NAT , REAL equals { t where t be Element of ( Funcs ( NAT , REAL )) : ex d, N st d > 0 & for n st n >= N & n in X holds (t . n) >= (d * (f . n)) & (t . n) >= 0 };

      coherence

      proof

        set IT = { t where t be Element of ( Funcs ( NAT , REAL )) : ex d, N st d > 0 & for n st n >= N & n in X holds (t . n) >= (d * (f . n)) & (t . n) >= 0 };

        

         A1: IT is functional

        proof

          let x be object;

          assume x in IT;

          then ex t be Element of ( Funcs ( NAT , REAL )) st x = t & ex d, N st d > 0 & for n st n >= N & n in X holds (t . n) >= (d * (f . n)) & (t . n) >= 0 ;

          hence thesis;

        end;

        consider N be Nat such that

         A2: for n be Nat st n >= N holds (f . n) >= 0 by Def2;

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

        f is Element of ( Funcs ( NAT , REAL )) & for n st n >= N & n in X holds (f . n) >= (1 * (f . n)) & (f . n) >= 0 by A2, FUNCT_2: 8;

        then f in IT;

        then

        reconsider IT1 = IT as functional non empty set by A1;

        now

          let x be Element of IT1;

          x in IT;

          then ex t be Element of ( Funcs ( NAT , REAL )) st x = t & ex d, N st d > 0 & for n st n >= N & n in X holds (t . n) >= (d * (f . n)) & (t . n) >= 0 ;

          hence x is sequence of REAL ;

        end;

        hence thesis by FUNCT_2:def 12;

      end;

    end

    definition

      let f be eventually-nonnegative Real_Sequence, X be set;

      :: ASYMPT_0:def14

      func Big_Theta (f,X) -> FUNCTION_DOMAIN of NAT , REAL equals { t where t be Element of ( Funcs ( NAT , REAL )) : ex c, d, N st c > 0 & d > 0 & for n st n >= N & n in X holds (d * (f . n)) <= (t . n) & (t . n) <= (c * (f . n)) };

      coherence

      proof

        set IT = { t where t be Element of ( Funcs ( NAT , REAL )) : ex c, d, N st c > 0 & d > 0 & for n st n >= N & n in X holds (d * (f . n)) <= (t . n) & (t . n) <= (c * (f . n)) };

        

         A1: IT is functional

        proof

          let x be object;

          assume x in IT;

          then ex t be Element of ( Funcs ( NAT , REAL )) st x = t & ex c, d, N st c > 0 & d > 0 & for n st n >= N & n in X holds (d * (f . n)) <= (t . n) & (t . n) <= (c * (f . n));

          hence thesis;

        end;

        f is Element of ( Funcs ( NAT , REAL )) & for n st n >= 0 & n in X holds (1 * (f . n)) <= (f . n) & (f . n) <= (1 * (f . n)) by FUNCT_2: 8;

        then f in IT;

        then

        reconsider IT1 = IT as functional non empty set by A1;

        now

          let x be Element of IT1;

          x in IT;

          then ex t be Element of ( Funcs ( NAT , REAL )) st x = t & ex c, d, N st c > 0 & d > 0 & for n st n >= N & n in X holds (d * (f . n)) <= (t . n) & (t . n) <= (c * (f . n));

          hence x is sequence of REAL ;

        end;

        hence thesis by FUNCT_2:def 12;

      end;

    end

    theorem :: ASYMPT_0:36

    

     Th36: for f be eventually-nonnegative Real_Sequence, X be set holds ( Big_Theta (f,X)) = (( Big_Oh (f,X)) /\ ( Big_Omega (f,X)))

    proof

      let f be eventually-nonnegative Real_Sequence, X be set;

      now

        let x be object;

        hereby

          consider N1 be Nat such that

           A1: for n be Nat st n >= N1 holds (f . n) >= 0 by Def2;

          assume x in ( Big_Theta (f,X));

          then

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

           A2: x = t and

           A3: ex c, d, N st c > 0 & d > 0 & for n st n >= N & n in X holds (d * (f . n)) <= (t . n) & (t . n) <= (c * (f . n));

          consider c, d, N such that

           A4: c > 0 and

           A5: d > 0 and

           A6: for n st n >= N & n in X holds (d * (f . n)) <= (t . n) & (t . n) <= (c * (f . n)) by A3;

          reconsider a = ( max (N,N1)) as Element of NAT by ORDINAL1:def 12;

          

           A7: a >= N1 by XXREAL_0: 25;

          

           A8: a >= N by XXREAL_0: 25;

          now

            take a;

            let n;

            assume that

             A9: n >= a and

             A10: n in X;

            

             A11: n >= N by A8, A9, XXREAL_0: 2;

            hence (d * (f . n)) <= (t . n) by A6, A10;

            n >= N1 by A7, A9, XXREAL_0: 2;

            then (f . n) >= 0 by A1;

            then (d * (f . n)) >= (d * 0 ) by A5;

            hence (t . n) >= 0 by A6, A10, A11;

          end;

          then

           A12: x in ( Big_Omega (f,X)) by A2, A5;

          now

            take a;

            let n;

            assume that

             A13: n >= a and

             A14: n in X;

            

             A15: n >= N by A8, A13, XXREAL_0: 2;

            hence (t . n) <= (c * (f . n)) by A6, A14;

            n >= N1 by A7, A13, XXREAL_0: 2;

            then (f . n) >= 0 by A1;

            then (d * (f . n)) >= (d * 0 ) by A5;

            hence (t . n) >= 0 by A6, A14, A15;

          end;

          then x in ( Big_Oh (f,X)) by A2, A4;

          hence x in (( Big_Oh (f,X)) /\ ( Big_Omega (f,X))) by A12, XBOOLE_0:def 4;

        end;

        assume

         A16: x in (( Big_Oh (f,X)) /\ ( Big_Omega (f,X)));

        then x in ( Big_Oh (f,X)) by XBOOLE_0:def 4;

        then

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

         A17: x = t and

         A18: ex c, N st c > 0 & for n st n >= N & n in X holds (t . n) <= (c * (f . n)) & (t . n) >= 0 ;

        x in ( Big_Omega (f,X)) by A16, XBOOLE_0:def 4;

        then

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

         A19: x = s and

         A20: ex d, N st d > 0 & for n st n >= N & n in X holds (s . n) >= (d * (f . n)) & (s . n) >= 0 ;

        consider c, N such that

         A21: c > 0 and

         A22: for n st n >= N & n in X holds (t . n) <= (c * (f . n)) & (t . n) >= 0 by A18;

        consider d, N1 such that

         A23: d > 0 and

         A24: for n st n >= N1 & n in X holds (s . n) >= (d * (f . n)) & (s . n) >= 0 by A20;

        set a = ( max (N,N1));

        

         A25: a >= N & a >= N1 by XXREAL_0: 25;

        now

          take a;

          let n;

          assume that

           A26: n >= a and

           A27: n in X;

          n >= N & n >= N1 by A25, A26, XXREAL_0: 2;

          hence (d * (f . n)) <= (t . n) & (t . n) <= (c * (f . n)) by A17, A19, A22, A24, A27;

        end;

        hence x in ( Big_Theta (f,X)) by A17, A21, A23;

      end;

      hence thesis by TARSKI: 2;

    end;

    definition

      let f be Real_Sequence, b be Nat;

      :: ASYMPT_0:def15

      func f taken_every b -> Real_Sequence means

      : Def15: for n holds (it . n) = (f . (b * n));

      existence

      proof

        deffunc F( Element of NAT ) = (f . (b * $1));

        consider h be sequence of REAL such that

         A1: for n be Element of NAT holds (h . n) = F(n) from FUNCT_2:sch 4;

        take h;

        let n;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let j,k be Real_Sequence such that

         A2: for n holds (j . n) = (f . (b * n)) and

         A3: for n holds (k . n) = (f . (b * n));

        now

          let n;

          

          thus (j . n) = (f . (b * n)) by A2

          .= (k . n) by A3;

        end;

        hence j = k by FUNCT_2: 63;

      end;

    end

    definition

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

      :: ASYMPT_0:def16

      pred f is_smooth_wrt b means f is eventually-nondecreasing & (f taken_every b) in ( Big_Oh f);

    end

    definition

      let f be eventually-nonnegative Real_Sequence;

      :: ASYMPT_0:def17

      attr f is smooth means for b be Element of NAT st b >= 2 holds f is_smooth_wrt b;

    end

    theorem :: ASYMPT_0:37

    for f be eventually-nonnegative Real_Sequence st ex b be Element of NAT st b >= 2 & f is_smooth_wrt b holds f is smooth

    proof

      let f be eventually-nonnegative Real_Sequence;

      given b be Element of NAT such that

       A1: b >= 2 and

       A2: f is_smooth_wrt b;

      

       A3: f is eventually-nondecreasing by A2;

      then

      consider N3 be Nat such that

       A4: for n be Nat st n >= N3 holds (f . n) <= (f . (n + 1));

      (f taken_every b) in ( Big_Oh f) by A2;

      then

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

       A5: (f taken_every b) = t and

       A6: ex c, N st c > 0 & for n st n >= N holds (t . n) <= (c * (f . n)) & (t . n) >= 0 ;

      consider c, N2 such that

       A7: c > 0 and

       A8: for n st n >= N2 holds (t . n) <= (c * (f . n)) & (t . n) >= 0 by A6;

      reconsider N = ( max (N2,N3)) as Element of NAT by ORDINAL1:def 12;

      

       A9: N >= N2 by XXREAL_0: 25;

      

       A10: N >= N3 by XXREAL_0: 25;

      now

        let a be Element of NAT ;

        set i = [/( log (b,a))\];

        

         A11: [/( log (b,a))\] >= ( log (b,a)) by INT_1:def 7;

        

         A12: b > 1 by A1, XXREAL_0: 2;

        

         A13: b <> 1 by A1;

        assume

         A14: a >= 2;

        then a > 1 by XXREAL_0: 2;

        then ( log (b,a)) > ( log (b,1)) by A12, POWER: 57;

        then ( log (b,a)) > 0 by A1, A13, POWER: 51;

        then

        reconsider i as Element of NAT by A11, INT_1: 3;

        reconsider i1 = (b |^ i) as Element of NAT ;

         A15:

        now

          let n;

          defpred P[ Nat] means (f . ((b |^ $1) * n)) <= ((c |^ $1) * (f . n));

          a >= 1 by A14, XXREAL_0: 2;

          then

           A16: (a * n) >= (1 * n) by XREAL_1: 64;

          (b to_power ( log (b,a))) <= (b to_power i) by A12, A11, PRE_FF: 8;

          then a <= (b |^ i) by A1, A13, POWER:def 3;

          then

           A17: (a * n) <= (i1 * n) by XREAL_1: 64;

          assume

           A18: n >= N;

          then

           A19: n >= N2 by A9, XXREAL_0: 2;

          then

           A20: (t . n) <= (c * (f . n)) by A8;

           A21:

          now

            assume (f . n) < 0 ;

            then (c * (f . n)) < (c * 0 ) by A7, XREAL_1: 68;

            hence contradiction by A8, A19, A20;

          end;

          

           A22: for k st P[k] holds P[(k + 1)]

          proof

            let k;

            set m = ((b |^ k) * n);

            assume

             A23: (f . m) <= ((c |^ k) * (f . n));

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

            (c * (f . m)) <= (c * ((c |^ k) * (f . n))) by A7, A23, XREAL_1: 64;

            then (c * (f . m)) <= ((c * (c |^ k)) * (f . n));

            then (c * (f . m)) <= (((c to_power 1) * (c to_power k)) * (f . n));

            then

             A24: (c * (f . m)) <= ((c to_power (k + 1)) * (f . n)) by A7, POWER: 27;

            m >= N2

            proof

              per cases ;

                suppose k = 0 ;

                

                then ((b |^ k) * n) = ((b to_power 0 ) * n)

                .= (1 * n) by POWER: 24

                .= n;

                hence thesis by A9, A18, XXREAL_0: 2;

              end;

                suppose k > 0 ;

                then (b to_power k) > 1 by A12, POWER: 35;

                then ((b |^ k) * n) >= (1 * n) by XREAL_1: 64;

                hence thesis by A19, XXREAL_0: 2;

              end;

            end;

            then ((f taken_every b) . m) <= (c * (f . m)) by A5, A8;

            then

             A25: (f . (b * m)) <= (c * (f . m)) by Def15;

            (f . ((b |^ (k + 1)) * n)) = (f . ((b to_power (k + 1)) * n))

            .= (f . (((b to_power 1) * (b to_power k)) * n)) by A1, POWER: 27

            .= (f . ((b * (b |^ k)) * n))

            .= (f . (b * ((b |^ k) * n)));

            hence thesis by A25, A24, XXREAL_0: 2;

          end;

          (f . ((b |^ 0 ) * n)) = (f . ((b to_power 0 ) * n))

          .= (f . (1 * n)) by POWER: 24

          .= (1 * (f . n))

          .= ((c to_power 0 ) * (f . n)) by POWER: 24;

          then

           A26: P[ 0 ];

          for k holds P[k] from NAT_1:sch 2( A26, A22);

          then (f . ((b |^ i) * n)) <= ((c |^ i) * (f . n));

          then

           A27: ((f taken_every i1) . n) <= ((c |^ i) * (f . n)) by Def15;

          

           A28: n >= N3 by A10, A18, XXREAL_0: 2;

          then (a * n) >= N3 by A16, XXREAL_0: 2;

          then (f . (a * n)) <= (f . (i1 * n)) by A4, A17, Th1;

          then ((f taken_every a) . n) <= (f . (i1 * n)) by Def15;

          then ((f taken_every a) . n) <= ((f taken_every i1) . n) by Def15;

          hence ((f taken_every a) . n) <= ((c |^ i) * (f . n)) by A27, XXREAL_0: 2;

          (f . n) <= (f . (a * n)) by A4, A28, A16, Th1;

          hence ((f taken_every a) . n) >= 0 by A21, Def15;

        end;

        (c |^ i) = (c to_power i);

        then (f taken_every a) is Element of ( Funcs ( NAT , REAL )) & (c |^ i) > 0 by A7, FUNCT_2: 8, POWER: 34;

        then (f taken_every a) in ( Big_Oh f) by A15;

        hence f is_smooth_wrt a by A3;

      end;

      hence thesis;

    end;

    theorem :: ASYMPT_0:38

    

     Th38: for f be eventually-nonnegative Real_Sequence, t be eventually-nonnegative eventually-nondecreasing Real_Sequence, b be Nat st f is smooth & b >= 2 & t in ( Big_Oh (f, the set of all (b |^ n) where n be Element of NAT )) holds t in ( Big_Oh f)

    proof

      let f be eventually-nonnegative Real_Sequence, t be eventually-nonnegative eventually-nondecreasing Real_Sequence, b be Nat;

      assume that

       A1: f is smooth and

       A2: b >= 2 and

       A3: t in ( Big_Oh (f, the set of all (b |^ n) where n be Element of NAT ));

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

      

       A4: f is_smooth_wrt b by A1, A2;

      then (f taken_every b) in ( Big_Oh f);

      then

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

       A5: (f taken_every b) = s and

       A6: ex c, N st c > 0 & for n st n >= N holds (s . n) <= (c * (f . n)) & (s . n) >= 0 ;

      consider c, N3 such that

       A7: c > 0 and

       A8: for n st n >= N3 holds (s . n) <= (c * (f . n)) & (s . n) >= 0 by A6;

      

       A9: b > 1 by A2, XXREAL_0: 2;

      f is eventually-nondecreasing by A4;

      then

      consider N1 be Nat such that

       A10: for m be Nat st m >= N1 holds (f . m) <= (f . (m + 1));

      consider N2 be Nat such that

       A11: for m be Nat st m >= N2 holds (t . m) <= (t . (m + 1)) by Def6;

      set X = the set of all (b |^ n) where n be Element of NAT ;

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

       A12: r = t and

       A13: ex c, N st c > 0 & for n st n >= N & n in X holds (r . n) <= (c * (f . n)) & (r . n) >= 0 by A3;

      consider a be Real, N4 such that

       A14: a > 0 and

       A15: for n st n >= N4 & n in X holds (r . n) <= (a * (f . n)) & (r . n) >= 0 by A13;

      reconsider N0 = ( max (( max (N1,N2)),( max (N3,N4)))) as Element of NAT by ORDINAL1:def 12;

      

       A16: N0 >= ( max (N1,N2)) by XXREAL_0: 25;

      ( max (N1,N2)) >= N2 by XXREAL_0: 25;

      then

       A17: N0 >= N2 by A16, XXREAL_0: 2;

      ( max (N1,N2)) >= N1 by XXREAL_0: 25;

      then

       A18: N0 >= N1 by A16, XXREAL_0: 2;

      

       A19: N0 >= ( max (N3,N4)) by XXREAL_0: 25;

      ( max (N3,N4)) >= N4 by XXREAL_0: 25;

      then

       A20: N0 >= N4 by A19, XXREAL_0: 2;

      ( max (N3,N4)) >= N3 by XXREAL_0: 25;

      then

       A21: N0 >= N3 by A19, XXREAL_0: 2;

      consider N5 be Nat such that

       A22: for n be Nat st n >= N5 holds (t . n) >= 0 by Def2;

      reconsider N = ( max (N5,( max (1,(b * N0))))) as Element of NAT by ORDINAL1:def 12;

      

       A23: N >= ( max (1,(b * N0))) by XXREAL_0: 25;

      ( max (1,(b * N0))) >= (b * N0) by XXREAL_0: 25;

      then

       A24: N >= (b * N0) by A23, XXREAL_0: 2;

      b >= 1 by A2, XXREAL_0: 2;

      then (b * N0) >= (1 * N0) by XREAL_1: 64;

      then

       A25: N >= N0 by A24, XXREAL_0: 2;

      

       A26: N >= N5 by XXREAL_0: 25;

      

       A27: ( max (1,(b * N0))) >= 1 by XXREAL_0: 25;

      then

       A28: N >= 1 by A23, XXREAL_0: 2;

       A29:

      now

        (N * (b " )) >= ((b " ) * (b * N0)) by A24, XREAL_1: 64;

        then (N * (b " )) >= (((b " ) * b) * N0);

        then

         A30: (N * (b " )) >= (1 * N0) by A2, XCMPLX_0:def 7;

        let n;

        set n1 = (b to_power [\( log (b,n))/]);

        assume

         A31: n >= N;

        then

         A32: n = (b to_power ( log (b,n))) by A23, A27, A9, POWER:def 3;

        n >= 1 by A28, A31, XXREAL_0: 2;

        then ( log (b,n)) >= ( log (b,1)) by A9, PRE_FF: 10;

        then

         A33: ( log (b,n)) >= 0 by A9, POWER: 51;

         A34:

        now

          (( log (b,n)) - 1) < [\( log (b,n))/] by INT_1:def 6;

          then (1 + (( log (b,n)) - 1)) < ( [\( log (b,n))/] + 1) by XREAL_1: 6;

          then

           A35: ((1 + ( - 1)) + ( log (b,n))) < ( [\( log (b,n))/] + 1);

          assume [\( log (b,n))/] < 0 ;

          then [\( log (b,n))/] <= ( - 1) by INT_1: 8;

          hence contradiction by A33, A35, XREAL_1: 6;

        end;

        then

        reconsider i = [\( log (b,n))/] as Element of NAT by INT_1: 3;

        reconsider n3 = ( [\( log (b,n))/] + 1) as Element of NAT by A34, INT_1: 3;

        n1 = (b |^ i) by POWER: 41;

        then

        reconsider n1 as Element of NAT ;

        set n2 = (b * n1);

        

         A36: n2 = ((b to_power 1) * (b to_power [\( log (b,n))/]))

        .= (b to_power ( [\( log (b,n))/] + 1)) by A2, POWER: 27;

        then n2 = (b |^ n3) by POWER: 41;

        then

         A37: n2 in X;

        (n * (b " )) >= (N * (b " )) by A31, XREAL_1: 64;

        then (n * (b " )) >= N0 by A30, XXREAL_0: 2;

        then

         A38: (n / b) >= N0 by XCMPLX_0:def 9;

        ( log (b,n)) <= ( [\( log (b,n))/] + 1) by INT_1: 29;

        then

         A39: n <= n2 by A9, A32, A36, PRE_FF: 8;

        then (n * (b " )) <= ((b " ) * (b * (b to_power [\( log (b,n))/]))) by XREAL_1: 64;

        then (n * (b " )) <= (((b " ) * b) * (b to_power [\( log (b,n))/]));

        then (n * (b " )) <= (1 * (b to_power [\( log (b,n))/])) by A2, XCMPLX_0:def 7;

        then (n / b) <= n1 by XCMPLX_0:def 9;

        then

         A40: n1 >= N0 by A38, XXREAL_0: 2;

        then

         A41: n1 >= N3 by A21, XXREAL_0: 2;

        

         A42: n >= N0 by A25, A31, XXREAL_0: 2;

        then n >= N4 by A20, XXREAL_0: 2;

        then n2 >= N4 by A39, XXREAL_0: 2;

        then

         A43: (t . n2) <= (a * (f . n2)) by A12, A15, A37;

        (f . (b * n1)) = (s . n1) by A5, Def15;

        then (f . (b * n1)) <= (c * (f . n1)) by A8, A41;

        then

         A44: (a * (f . (b * n1))) <= (a * (c * (f . n1))) by A14, XREAL_1: 64;

        n >= N2 by A17, A42, XXREAL_0: 2;

        then (t . n) <= (t . n2) by A11, A39, Th1;

        then (t . n) <= (a * (f . n2)) by A43, XXREAL_0: 2;

        then

         A45: (t . n) <= ((a * c) * (f . n1)) by A44, XXREAL_0: 2;

        

         A46: n1 >= N1 by A18, A40, XXREAL_0: 2;

         [\( log (b,n))/] <= ( log (b,n)) by INT_1:def 6;

        then n1 <= n by A9, A32, PRE_FF: 8;

        then ((a * c) * (f . n1)) <= ((a * c) * (f . n)) by A10, A7, A14, A46, Th1, XREAL_1: 64;

        hence (t . n) <= ((a * c) * (f . n)) by A45, XXREAL_0: 2;

        n >= N5 by A26, A31, XXREAL_0: 2;

        hence (t . n) >= 0 by A22;

      end;

      

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

      (a * c) > (c * 0 ) by A7, A14, XREAL_1: 68;

      hence thesis by A47, A29;

    end;

    theorem :: ASYMPT_0:39

    

     Th39: for f be eventually-nonnegative Real_Sequence, t be eventually-nonnegative eventually-nondecreasing Real_Sequence, b be Element of NAT st f is smooth & b >= 2 & t in ( Big_Omega (f, the set of all (b |^ n) where n be Element of NAT )) holds t in ( Big_Omega f)

    proof

      let f be eventually-nonnegative Real_Sequence, t be eventually-nonnegative eventually-nondecreasing Real_Sequence, b be Element of NAT ;

      assume that

       A1: f is smooth and

       A2: b >= 2 and

       A3: t in ( Big_Omega (f, the set of all (b |^ n) where n be Element of NAT ));

      consider N2 be Nat such that

       A4: for m be Nat st m >= N2 holds (t . m) <= (t . (m + 1)) by Def6;

      

       A5: f is_smooth_wrt b by A1, A2;

      then (f taken_every b) in ( Big_Oh f);

      then

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

       A6: (f taken_every b) = s and

       A7: ex c, N st c > 0 & for n st n >= N holds (s . n) <= (c * (f . n)) & (s . n) >= 0 ;

      consider c, N3 such that

       A8: c > 0 and

       A9: for n st n >= N3 holds (s . n) <= (c * (f . n)) & (s . n) >= 0 by A7;

      f is eventually-nondecreasing by A5;

      then

      consider N1 be Nat such that

       A10: for m be Nat st m >= N1 holds (f . m) <= (f . (m + 1));

      consider N5 be Nat such that

       A11: for n be Nat st n >= N5 holds (t . n) >= 0 by Def2;

      set X = the set of all (b |^ n) where n be Element of NAT ;

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

       A12: r = t and

       A13: ex d, N st d > 0 & for n st n >= N & n in X holds (d * (f . n)) <= (r . n) & (r . n) >= 0 by A3;

      consider a be Real, N4 such that

       A14: a > 0 and

       A15: for n st n >= N4 & n in X holds (a * (f . n)) <= (r . n) & (r . n) >= 0 by A13;

      

       A16: b > 1 by A2, XXREAL_0: 2;

      reconsider N0 = ( max (( max (N1,N2)),( max (N3,N4)))) as Element of NAT by ORDINAL1:def 12;

      

       A17: N0 >= ( max (N1,N2)) by XXREAL_0: 25;

      ( max (N1,N2)) >= N2 by XXREAL_0: 25;

      then

       A18: N0 >= N2 by A17, XXREAL_0: 2;

      ( max (N1,N2)) >= N1 by XXREAL_0: 25;

      then

       A19: N0 >= N1 by A17, XXREAL_0: 2;

      

       A20: N0 >= ( max (N3,N4)) by XXREAL_0: 25;

      ( max (N3,N4)) >= N4 by XXREAL_0: 25;

      then

       A21: N0 >= N4 by A20, XXREAL_0: 2;

      ( max (N3,N4)) >= N3 by XXREAL_0: 25;

      then

       A22: N0 >= N3 by A20, XXREAL_0: 2;

      reconsider N = ( max (N5,( max (1,(b * N0))))) as Element of NAT by ORDINAL1:def 12;

      

       A23: N >= ( max (1,(b * N0))) by XXREAL_0: 25;

      ( max (1,(b * N0))) >= (b * N0) by XXREAL_0: 25;

      then

       A24: N >= (b * N0) by A23, XXREAL_0: 2;

      b >= 1 by A2, XXREAL_0: 2;

      then (b * N0) >= (1 * N0) by XREAL_1: 64;

      then

       A25: N >= N0 by A24, XXREAL_0: 2;

      

       A26: N >= N5 by XXREAL_0: 25;

      

       A27: ( max (1,(b * N0))) >= 1 by XXREAL_0: 25;

      then

       A28: N >= 1 by A23, XXREAL_0: 2;

       A29:

      now

        (N * (b " )) >= ((b " ) * (b * N0)) by A24, XREAL_1: 64;

        then (N * (b " )) >= (((b " ) * b) * N0);

        then

         A30: (N * (b " )) >= (1 * N0) by A2, XCMPLX_0:def 7;

        let n;

        set n1 = (b to_power [\( log (b,n))/]);

        

         A31: ( log (b,n)) <= ( [\( log (b,n))/] + 1) by INT_1: 29;

        assume

         A32: n >= N;

        then

         A33: n = (b to_power ( log (b,n))) by A23, A27, A16, POWER:def 3;

        n >= 1 by A28, A32, XXREAL_0: 2;

        then

         A34: ( log (b,n)) >= ( log (b,1)) by A16, PRE_FF: 10;

         [\( log (b,n))/] >= 0

        proof

          (( log (b,n)) - 1) < [\( log (b,n))/] by INT_1:def 6;

          then (1 + (( log (b,n)) - 1)) < ( [\( log (b,n))/] + 1) by XREAL_1: 6;

          then

           A35: ((1 + ( - 1)) + ( log (b,n))) < ( [\( log (b,n))/] + 1);

          assume [\( log (b,n))/] < 0 ;

          then [\( log (b,n))/] <= ( - 1) by INT_1: 8;

          then ( log (b,n)) < 0 by A35, XREAL_1: 6;

          hence contradiction by A16, A34, POWER: 51;

        end;

        then

        reconsider i = [\( log (b,n))/] as Element of NAT by INT_1: 3;

        

         A36: n1 = (b |^ i) by POWER: 41;

        (n * (b " )) >= (N * (b " )) by A32, XREAL_1: 64;

        then (n * (b " )) >= N0 by A30, XXREAL_0: 2;

        then

         A37: (n / b) >= N0 by XCMPLX_0:def 9;

        reconsider n1 as Element of NAT by A36;

        

         A38: n1 in X by A36;

        set n2 = (b * n1);

        n2 = ((b to_power 1) * (b to_power [\( log (b,n))/]))

        .= (b to_power ( [\( log (b,n))/] + 1)) by A2, POWER: 27;

        then

         A39: n <= n2 by A16, A33, A31, PRE_FF: 8;

        then (n * (b " )) <= ((b " ) * (b * (b to_power [\( log (b,n))/]))) by XREAL_1: 64;

        then (n * (b " )) <= (((b " ) * b) * (b to_power [\( log (b,n))/]));

        then (n * (b " )) <= (1 * (b to_power [\( log (b,n))/])) by A2, XCMPLX_0:def 7;

        then (n / b) <= n1 by XCMPLX_0:def 9;

        then

         A40: n1 >= N0 by A37, XXREAL_0: 2;

        then n1 >= N4 by A21, XXREAL_0: 2;

        then

         A41: (a * (f . n1)) <= (t . n1) by A12, A15, A38;

        n1 >= N3 by A22, A40, XXREAL_0: 2;

        then (s . n1) <= (c * (f . n1)) by A9;

        then ((c " ) * (s . n1)) <= ((c " ) * (c * (f . n1))) by A8, XREAL_1: 64;

        then ((c " ) * (s . n1)) <= (((c " ) * c) * (f . n1));

        then ((c " ) * (s . n1)) <= (1 * (f . n1)) by A8, XCMPLX_0:def 7;

        then ((c " ) * (f . (b * n1))) <= (f . n1) by A6, Def15;

        then

         A42: (a * ((c " ) * (f . (b * n1)))) <= (a * (f . n1)) by A14, XREAL_1: 64;

         [\( log (b,n))/] <= ( log (b,n)) by INT_1:def 6;

        then

         A43: (b to_power [\( log (b,n))/]) <= (b to_power ( log (b,n))) by A16, PRE_FF: 8;

        n >= N0 by A25, A32, XXREAL_0: 2;

        then n >= N1 by A19, XXREAL_0: 2;

        then (f . n) <= (f . n2) by A10, A39, Th1;

        then

         A44: ((a * (c " )) * (f . n)) <= ((a * (c " )) * (f . n2)) by A8, A14, XREAL_1: 64;

        n1 >= N2 by A18, A40, XXREAL_0: 2;

        then (t . n1) <= (t . n) by A4, A33, A43, Th1;

        then (a * (f . n1)) <= (t . n) by A41, XXREAL_0: 2;

        then ((a * (c " )) * (f . n2)) <= (t . n) by A42, XXREAL_0: 2;

        hence ((a * (c " )) * (f . n)) <= (t . n) by A44, XXREAL_0: 2;

        n >= N5 by A26, A32, XXREAL_0: 2;

        hence (t . n) >= 0 by A11;

      end;

      

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

      (a * (c " )) > ((c " ) * 0 ) by A8, A14, XREAL_1: 68;

      hence thesis by A45, A29;

    end;

    theorem :: ASYMPT_0:40

    for f be eventually-nonnegative Real_Sequence, t be eventually-nonnegative eventually-nondecreasing Real_Sequence, b be Element of NAT st f is smooth & b >= 2 & t in ( Big_Theta (f, the set of all (b |^ n) where n be Element of NAT )) holds t in ( Big_Theta f)

    proof

      let f be eventually-nonnegative Real_Sequence, t be eventually-nonnegative eventually-nondecreasing Real_Sequence, b be Element of NAT ;

      assume that

       A1: f is smooth & b >= 2 and

       A2: t in ( Big_Theta (f, the set of all (b |^ n) where n be Element of NAT ));

      set X = the set of all (b |^ n) where n be Element of NAT ;

      

       A3: t in (( Big_Oh (f,X)) /\ ( Big_Omega (f,X))) by A2, Th36;

      then t in ( Big_Omega (f,X)) by XBOOLE_0:def 4;

      then

       A4: t in ( Big_Omega f) by A1, Th39;

      t in ( Big_Oh (f,X)) by A3, XBOOLE_0:def 4;

      then t in ( Big_Oh f) by A1, Th38;

      hence thesis by A4, XBOOLE_0:def 4;

    end;

    begin

    definition

      let X be non empty set, F,G be FUNCTION_DOMAIN of X, REAL ;

      :: ASYMPT_0:def18

      func F + G -> FUNCTION_DOMAIN of X, REAL equals { t where t be Element of ( Funcs (X, REAL )) : ex f,g be Element of ( Funcs (X, REAL )) st f in F & g in G & for n be Element of X holds (t . n) = ((f . n) + (g . n)) };

      coherence

      proof

        set IT = { t where t be Element of ( Funcs (X, REAL )) : ex f,g be Element of ( Funcs (X, REAL )) st f in F & g in G & for n be Element of X holds (t . n) = ((f . n) + (g . n)) };

         A1:

        now

          consider g be object such that

           A2: g in G by XBOOLE_0:def 1;

          g is Function of X, REAL by A2, FUNCT_2:def 12;

          then

          reconsider g as Element of ( Funcs (X, REAL )) by FUNCT_2: 8;

          consider f be object such that

           A3: f in F by XBOOLE_0:def 1;

          f is Function of X, REAL by A3, FUNCT_2:def 12;

          then

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

          defpred P[ Element of X, Real] means $2 = ((f . $1) + (g . $1));

          

           A4: for x be Element of X holds ex y be Element of REAL st P[x, y];

          consider t be Function of X, REAL such that

           A5: for x be Element of X holds P[x, (t . x)] from FUNCT_2:sch 3( A4);

          reconsider t as Element of ( Funcs (X, REAL )) by FUNCT_2: 8;

          t in IT by A3, A2, A5;

          hence IT is non empty;

        end;

        IT is functional

        proof

          let x be object;

          assume x in IT;

          then ex t be Element of ( Funcs (X, REAL )) st x = t & ex f,g be Element of ( Funcs (X, REAL )) st f in F & g in G & for n be Element of X holds (t . n) = ((f . n) + (g . n));

          hence thesis;

        end;

        then

        reconsider IT1 = IT as functional non empty set by A1;

        now

          let x be Element of IT1;

          x in IT;

          then ex t be Element of ( Funcs (X, REAL )) st x = t & ex f,g be Element of ( Funcs (X, REAL )) st f in F & g in G & for n be Element of X holds (t . n) = ((f . n) + (g . n));

          hence x is Function of X, REAL ;

        end;

        hence thesis by FUNCT_2:def 12;

      end;

    end

    definition

      let X be non empty set, F,G be FUNCTION_DOMAIN of X, REAL ;

      :: ASYMPT_0:def19

      func max (F,G) -> FUNCTION_DOMAIN of X, REAL equals { t where t be Element of ( Funcs (X, REAL )) : ex f,g be Element of ( Funcs (X, REAL )) st f in F & g in G & for n be Element of X holds (t . n) = ( max ((f . n),(g . n))) };

      coherence

      proof

        set IT = { t where t be Element of ( Funcs (X, REAL )) : ex f,g be Element of ( Funcs (X, REAL )) st f in F & g in G & for n be Element of X holds (t . n) = ( max ((f . n),(g . n))) };

         A1:

        now

          consider g be object such that

           A2: g in G by XBOOLE_0:def 1;

          g is Function of X, REAL by A2, FUNCT_2:def 12;

          then

          reconsider g as Element of ( Funcs (X, REAL )) by FUNCT_2: 8;

          consider f be object such that

           A3: f in F by XBOOLE_0:def 1;

          f is Function of X, REAL by A3, FUNCT_2:def 12;

          then

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

          defpred P[ Element of X, Real] means $2 = ( max ((f . $1),(g . $1)));

          

           A4: for x be Element of X holds ex y be Element of REAL st P[x, y]

          proof

            let x be Element of X;

            consider y be Real such that

             A5: P[x, y];

            reconsider y as Element of REAL by XREAL_0:def 1;

            take y;

            thus thesis by A5;

          end;

          consider t be Function of X, REAL such that

           A6: for x be Element of X holds P[x, (t . x)] from FUNCT_2:sch 3( A4);

          reconsider t as Element of ( Funcs (X, REAL )) by FUNCT_2: 8;

          t in IT by A3, A2, A6;

          hence IT is non empty;

        end;

        IT is functional

        proof

          let x be object;

          assume x in IT;

          then ex t be Element of ( Funcs (X, REAL )) st x = t & ex f,g be Element of ( Funcs (X, REAL )) st f in F & g in G & for n be Element of X holds (t . n) = ( max ((f . n),(g . n)));

          hence thesis;

        end;

        then

        reconsider IT1 = IT as functional non empty set by A1;

        now

          let x be Element of IT1;

          x in IT;

          then ex t be Element of ( Funcs (X, REAL )) st x = t & ex f,g be Element of ( Funcs (X, REAL )) st f in F & g in G & for n be Element of X holds (t . n) = ( max ((f . n),(g . n)));

          hence x is Function of X, REAL ;

        end;

        hence thesis by FUNCT_2:def 12;

      end;

    end

    theorem :: ASYMPT_0:41

    for f,g be eventually-nonnegative Real_Sequence holds (( Big_Oh f) + ( Big_Oh g)) = ( Big_Oh (f + g))

    proof

      let f,g be eventually-nonnegative Real_Sequence;

      now

        let x be object;

        hereby

          assume x in (( Big_Oh f) + ( Big_Oh g));

          then

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

           A1: x = t and

           A2: ex f9,g9 be Element of ( Funcs ( NAT , REAL )) st f9 in ( Big_Oh f) & g9 in ( Big_Oh g) & for n be Element of NAT holds (t . n) = ((f9 . n) + (g9 . n));

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

           A3: f9 in ( Big_Oh f) and

           A4: g9 in ( Big_Oh g) and

           A5: for n be Element of NAT holds (t . n) = ((f9 . n) + (g9 . n)) by A2;

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

           A6: r = f9 and

           A7: ex c, N st c > 0 & for n st n >= N holds (r . n) <= (c * (f . n)) & (r . n) >= 0 by A3;

          consider c, N1 such that

           A8: c > 0 and

           A9: for n st n >= N1 holds (r . n) <= (c * (f . n)) & (r . n) >= 0 by A7;

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

           A10: s = g9 and

           A11: ex c, N st c > 0 & for n st n >= N holds (s . n) <= (c * (g . n)) & (s . n) >= 0 by A4;

          consider d, N2 such that

           A12: d > 0 and

           A13: for n st n >= N2 holds (s . n) <= (d * (g . n)) & (s . n) >= 0 by A11;

          set N = ( max (N1,N2));

          set e = ( max (c,d));

          

           A14: N >= N2 by XXREAL_0: 25;

          

           A15: N >= N1 by XXREAL_0: 25;

           A16:

          now

            let n;

            assume

             A17: n >= N;

            then

             A18: n >= N1 by A15, XXREAL_0: 2;

            then (f9 . n) >= 0 by A6, A9;

            then

             A19: ((f9 . n) + (g9 . n)) >= ( 0 + (g9 . n)) by XREAL_1: 6;

            (r . n) <= (c * (f . n)) by A9, A18;

            then ((f . n) * c) >= ( 0 * c) by A9, A18;

            then (f . n) >= 0 by A8, XREAL_1: 68;

            then

             A20: (c * (f . n)) <= (e * (f . n)) by XREAL_1: 64, XXREAL_0: 25;

            (r . n) <= (c * (f . n)) by A9, A18;

            then (r . n) <= (e * (f . n)) by A20, XXREAL_0: 2;

            then

             A21: ((r . n) + (s . n)) <= ((e * (f . n)) + (s . n)) by XREAL_1: 6;

            

             A22: n >= N2 by A14, A17, XXREAL_0: 2;

            then (s . n) <= (d * (g . n)) by A13;

            then ((g . n) * d) >= ( 0 * d) by A13, A22;

            then (g . n) >= 0 by A12, XREAL_1: 68;

            then

             A23: (d * (g . n)) <= (e * (g . n)) by XREAL_1: 64, XXREAL_0: 25;

            (s . n) <= (d * (g . n)) by A13, A22;

            then (s . n) <= (e * (g . n)) by A23, XXREAL_0: 2;

            then ((e * (f . n)) + (s . n)) <= ((e * (f . n)) + (e * (g . n))) by XREAL_1: 6;

            then ((r . n) + (s . n)) <= (e * ((f . n) + (g . n))) by A21, XXREAL_0: 2;

            then ((r . n) + (s . n)) <= (e * ((f + g) . n)) by SEQ_1: 7;

            hence (t . n) <= (e * ((f + g) . n)) by A5, A6, A10;

            ( 0 + (g9 . n)) >= 0 by A10, A13, A22;

            hence (t . n) >= 0 by A5, A19;

          end;

          e > 0 by A8, XXREAL_0: 25;

          hence x in ( Big_Oh (f + g)) by A1, A16;

        end;

        assume x in ( Big_Oh (f + g));

        then

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

         A24: x = t and

         A25: ex c, N st c > 0 & for n st n >= N holds (t . n) <= (c * ((f + g) . n)) & (t . n) >= 0 ;

        consider c, N3 such that

         A26: c > 0 and

         A27: for n st n >= N3 holds (t . n) <= (c * ((f + g) . n)) & (t . n) >= 0 by A25;

        consider N1 be Nat such that

         A28: for n be Nat st n >= N1 holds (f . n) >= 0 by Def2;

        consider N2 be Nat such that

         A29: for n be Nat st n >= N2 holds (g . n) >= 0 by Def2;

        reconsider N = ( max (N3,( max (N1,N2)))) as Element of NAT by ORDINAL1:def 12;

        

         A30: N >= ( max (N1,N2)) by XXREAL_0: 25;

        defpred Q[ Element of NAT , Real] means ((t . $1) <= (c * (f . $1)) implies $2 = 0 ) & ((c * (f . $1)) < (t . $1) implies $2 = ((t . $1) - (c * (f . $1))));

        

         A31: for x be Element of NAT holds ex y be Element of REAL st Q[x, y]

        proof

          let n;

          per cases ;

            suppose

             A32: (t . n) <= (c * (f . n));

             0 in REAL by XREAL_0:def 1;

            hence thesis by A32;

          end;

            suppose

             A33: (c * (f . n)) < (t . n);

            reconsider y = ((t . n) - (c * (f . n))) as Element of REAL by XREAL_0:def 1;

            take y;

            thus thesis by A33;

          end;

        end;

        consider g9 be sequence of REAL such that

         A34: for x be Element of NAT holds Q[x, (g9 . x)] from FUNCT_2:sch 3( A31);

        

         A35: N >= N3 by XXREAL_0: 25;

        

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

        ( max (N1,N2)) >= N2 by XXREAL_0: 25;

        then

         A37: N >= N2 by A30, XXREAL_0: 2;

        now

          let n;

          assume

           A38: n >= N;

          then n >= N3 by A35, XXREAL_0: 2;

          then

           A39: (t . n) <= (c * ((f + g) . n)) by A27;

          n >= N2 by A37, A38, XXREAL_0: 2;

          then (g . n) >= 0 by A29;

          then

           A40: ( 0 * (g . n)) <= (c * (g . n)) by A26;

          per cases ;

            suppose (t . n) <= (c * (f . n));

            hence (g9 . n) <= (c * (g . n)) & (g9 . n) >= 0 by A34, A40;

          end;

            suppose

             A41: (t . n) > (c * (f . n));

            (t . n) <= (c * ((f . n) + (g . n))) by A39, SEQ_1: 7;

            then (t . n) <= ((c * (f . n)) + (c * (g . n)));

            then

             A42: ((t . n) - (c * (f . n))) <= (c * (g . n)) by XREAL_1: 20;

            (t . n) > ( 0 + (c * (f . n))) by A41;

            then ((t . n) - (c * (f . n))) >= 0 by XREAL_1: 19;

            hence (g9 . n) <= (c * (g . n)) & (g9 . n) >= 0 by A34, A42;

          end;

        end;

        then

         A43: g9 in ( Big_Oh g) by A26, A36;

        defpred P[ Element of NAT , Real] means ((t . $1) <= (c * (f . $1)) implies $2 = (t . $1)) & ((c * (f . $1)) < (t . $1) implies $2 = (c * (f . $1)));

        

         A44: for x be Element of NAT holds ex y be Element of REAL st P[x, y]

        proof

          let n;

          per cases ;

            suppose (t . n) <= (c * (f . n));

            hence thesis;

          end;

            suppose

             A45: (c * (f . n)) < (t . n);

            reconsider y = (c * (f . n)) as Element of REAL by XREAL_0:def 1;

            take y;

            thus thesis by A45;

          end;

        end;

        consider f9 be sequence of REAL such that

         A46: for x be Element of NAT holds P[x, (f9 . x)] from FUNCT_2:sch 3( A44);

         A47:

        now

          let n be Element of NAT ;

          per cases ;

            suppose

             A48: (t . n) <= (c * (f . n));

            then (g9 . n) = 0 by A34;

            hence (t . n) = ((f9 . n) + (g9 . n)) by A46, A48;

          end;

            suppose (c * (f . n)) < (t . n);

            then (f9 . n) = (c * (f . n)) & (g9 . n) = ((t . n) - (c * (f . n))) by A46, A34;

            hence ((f9 . n) + (g9 . n)) = (t . n);

          end;

        end;

        

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

        ( max (N1,N2)) >= N1 by XXREAL_0: 25;

        then

         A50: N >= N1 by A30, XXREAL_0: 2;

        now

          let n;

          assume

           A51: n >= N;

          then n >= N3 by A35, XXREAL_0: 2;

          then

           A52: (t . n) >= 0 by A27;

          n >= N1 by A50, A51, XXREAL_0: 2;

          then

           A53: (f . n) >= 0 by A28;

          per cases ;

            suppose (t . n) <= (c * (f . n));

            hence (f9 . n) <= (c * (f . n)) & (f9 . n) >= 0 by A46, A52;

          end;

            suppose (t . n) > (c * (f . n));

            hence (f9 . n) <= (c * (f . n)) & (f9 . n) >= 0 by A26, A46, A53;

          end;

        end;

        then f9 in ( Big_Oh f) by A26, A49;

        hence x in (( Big_Oh f) + ( Big_Oh g)) by A24, A49, A36, A43, A47;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: ASYMPT_0:42

    for f,g be eventually-nonnegative Real_Sequence holds ( max (( Big_Oh f),( Big_Oh g))) = ( Big_Oh ( max (f,g)))

    proof

      let f,g be eventually-nonnegative Real_Sequence;

      now

        let x be object;

        hereby

          assume x in ( max (( Big_Oh f),( Big_Oh g)));

          then

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

           A1: x = t and

           A2: ex f9,g9 be Element of ( Funcs ( NAT , REAL )) st f9 in ( Big_Oh f) & g9 in ( Big_Oh g) & for n be Element of NAT holds (t . n) = ( max ((f9 . n),(g9 . n)));

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

           A3: f9 in ( Big_Oh f) and

           A4: g9 in ( Big_Oh g) and

           A5: for n be Element of NAT holds (t . n) = ( max ((f9 . n),(g9 . n))) by A2;

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

           A6: s = g9 and

           A7: ex c, N st c > 0 & for n st n >= N holds (s . n) <= (c * (g . n)) & (s . n) >= 0 by A4;

          consider d, N2 such that

           A8: d > 0 and

           A9: for n st n >= N2 holds (s . n) <= (d * (g . n)) & (s . n) >= 0 by A7;

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

           A10: r = f9 and

           A11: ex c, N st c > 0 & for n st n >= N holds (r . n) <= (c * (f . n)) & (r . n) >= 0 by A3;

          consider c, N1 such that

           A12: c > 0 and

           A13: for n st n >= N1 holds (r . n) <= (c * (f . n)) & (r . n) >= 0 by A11;

          set e = ( max (c,d));

          

           A14: e > 0 by A12, XXREAL_0: 25;

          reconsider N = ( max (N1,N2)) as Element of NAT ;

          

           A15: N >= N2 by XXREAL_0: 25;

          

           A16: N >= N1 by XXREAL_0: 25;

          now

            let n;

            assume

             A17: n >= N;

            then

             A18: n >= N1 by A16, XXREAL_0: 2;

            then (r . n) <= (c * (f . n)) by A13;

            then ((f . n) * c) >= ( 0 * c) by A13, A18;

            then (f . n) >= 0 by A12, XREAL_1: 68;

            then

             A19: (c * (f . n)) <= (e * (f . n)) by XREAL_1: 64, XXREAL_0: 25;

            

             A20: n >= N2 by A15, A17, XXREAL_0: 2;

            then (s . n) <= (d * (g . n)) by A9;

            then ((g . n) * d) >= ( 0 * d) by A9, A20;

            then (g . n) >= 0 by A8, XREAL_1: 68;

            then

             A21: (d * (g . n)) <= (e * (g . n)) by XREAL_1: 64, XXREAL_0: 25;

            (s . n) <= (d * (g . n)) by A9, A20;

            then

             A22: (s . n) <= (e * (g . n)) by A21, XXREAL_0: 2;

            (e * (g . n)) <= (e * ( max ((f . n),(g . n)))) by A14, XREAL_1: 64, XXREAL_0: 25;

            then

             A23: (s . n) <= (e * ( max ((f . n),(g . n)))) by A22, XXREAL_0: 2;

            (r . n) <= (c * (f . n)) by A13, A18;

            then

             A24: (r . n) <= (e * (f . n)) by A19, XXREAL_0: 2;

            (e * (f . n)) <= (e * ( max ((f . n),(g . n)))) by A14, XREAL_1: 64, XXREAL_0: 25;

            then (r . n) <= (e * ( max ((f . n),(g . n)))) by A24, XXREAL_0: 2;

            then ( max ((r . n),(s . n))) <= (e * ( max ((f . n),(g . n)))) by A23, XXREAL_0: 28;

            then ( max ((r . n),(s . n))) <= (e * (( max (f,g)) . n)) by Def7;

            hence (t . n) <= (e * (( max (f,g)) . n)) by A5, A10, A6;

            ( max ((f9 . n),(g9 . n))) >= (f9 . n) & (f9 . n) >= 0 by A10, A13, A18, XXREAL_0: 25;

            hence (t . n) >= 0 by A5;

          end;

          hence x in ( Big_Oh ( max (f,g))) by A1, A14;

        end;

        assume x in ( Big_Oh ( max (f,g)));

        then

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

         A25: x = t and

         A26: ex c, N st c > 0 & for n st n >= N holds (t . n) <= (c * (( max (f,g)) . n)) & (t . n) >= 0 ;

        consider c, N3 such that

         A27: c > 0 and

         A28: for n st n >= N3 holds (t . n) <= (c * (( max (f,g)) . n)) & (t . n) >= 0 by A26;

        consider N1 be Nat such that

         A29: for n be Nat st n >= N1 holds (f . n) >= 0 by Def2;

        consider N2 be Nat such that

         A30: for n be Nat st n >= N2 holds (g . n) >= 0 by Def2;

        reconsider N = ( max (N3,( max (N1,N2)))) as Element of NAT by ORDINAL1:def 12;

        defpred P[ Element of NAT , Real] means ((f . $1) >= (g . $1) or $1 < N implies $2 = (t . $1)) & ((f . $1) < (g . $1) & $1 >= N implies $2 = 0 );

        defpred Q[ Element of NAT , Real] means ((f . $1) >= (g . $1) & $1 >= N implies $2 = 0 ) & ((f . $1) < (g . $1) or $1 < N implies $2 = (t . $1));

        

         A31: for x be Element of NAT holds ex y be Element of REAL st P[x, y]

        proof

          let n;

          per cases ;

            suppose (f . n) >= (g . n);

            hence thesis;

          end;

            suppose

             A32: (f . n) < (g . n);

            thus thesis

            proof

              per cases ;

                suppose n < N;

                hence thesis;

              end;

                suppose

                 A33: n >= N;

                 0 in REAL by XREAL_0:def 1;

                hence thesis by A32, A33;

              end;

            end;

          end;

        end;

        consider f9 be sequence of REAL such that

         A34: for x be Element of NAT holds P[x, (f9 . x)] from FUNCT_2:sch 3( A31);

        

         A35: for x be Element of NAT holds ex y be Element of REAL st Q[x, y]

        proof

          let n;

          per cases ;

            suppose

             A36: (f . n) >= (g . n);

            thus thesis

            proof

              per cases ;

                suppose n < N;

                hence thesis;

              end;

                suppose

                 A37: n >= N;

                 0 in REAL by XREAL_0:def 1;

                hence thesis by A36, A37;

              end;

            end;

          end;

            suppose (f . n) < (g . n);

            hence thesis;

          end;

        end;

        consider g9 be sequence of REAL such that

         A38: for x be Element of NAT holds Q[x, (g9 . x)] from FUNCT_2:sch 3( A35);

        

         A39: N >= N3 by XXREAL_0: 25;

         A40:

        now

          let n be Element of NAT ;

          per cases ;

            suppose n < N;

            then (f9 . n) = (t . n) & (g9 . n) = (t . n) by A34, A38;

            hence (t . n) = ( max ((f9 . n),(g9 . n)));

          end;

            suppose

             A41: n >= N;

            then

             A42: n >= N3 by A39, XXREAL_0: 2;

            thus (t . n) = ( max ((f9 . n),(g9 . n)))

            proof

              per cases ;

                suppose

                 A43: (f . n) >= (g . n);

                

                 A44: (t . n) >= 0 by A28, A42;

                (f9 . n) = (t . n) & (g9 . n) = 0 by A34, A38, A41, A43;

                hence thesis by A44, XXREAL_0:def 10;

              end;

                suppose

                 A45: (f . n) < (g . n);

                

                 A46: (t . n) >= 0 by A28, A42;

                (f9 . n) = 0 & (g9 . n) = (t . n) by A34, A38, A41, A45;

                hence thesis by A46, XXREAL_0:def 10;

              end;

            end;

          end;

        end;

        

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

        

         A48: N >= ( max (N1,N2)) by XXREAL_0: 25;

        ( max (N1,N2)) >= N2 by XXREAL_0: 25;

        then

         A49: N >= N2 by A48, XXREAL_0: 2;

        now

          let n;

          assume

           A50: n >= N;

          then n >= N3 by A39, XXREAL_0: 2;

          then

           A51: (t . n) >= 0 & (t . n) <= (c * (( max (f,g)) . n)) by A28;

          n >= N2 by A49, A50, XXREAL_0: 2;

          then (g . n) >= 0 by A30;

          then

           A52: ( 0 * (g . n)) <= (c * (g . n)) by A27;

          per cases ;

            suppose (f . n) >= (g . n);

            hence (g9 . n) <= (c * (g . n)) & (g9 . n) >= 0 by A38, A50, A52;

          end;

            suppose

             A53: (f . n) < (g . n);

            then ( max ((f . n),(g . n))) = (g . n) by XXREAL_0:def 10;

            then (( max (f,g)) . n) = (g . n) by Def7;

            hence (g9 . n) <= (c * (g . n)) & (g9 . n) >= 0 by A38, A51, A53;

          end;

        end;

        then

         A54: g9 in ( Big_Oh g) by A27, A47;

        

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

        ( max (N1,N2)) >= N1 by XXREAL_0: 25;

        then

         A56: N >= N1 by A48, XXREAL_0: 2;

        now

          let n;

          assume

           A57: n >= N;

          then n >= N3 by A39, XXREAL_0: 2;

          then

           A58: (t . n) >= 0 & (t . n) <= (c * (( max (f,g)) . n)) by A28;

          n >= N1 by A56, A57, XXREAL_0: 2;

          then (f . n) >= 0 by A29;

          then

           A59: ( 0 * (f . n)) <= (c * (f . n)) by A27;

          per cases ;

            suppose

             A60: (f . n) >= (g . n);

            then ( max ((f . n),(g . n))) = (f . n) by XXREAL_0:def 10;

            then (( max (f,g)) . n) = (f . n) by Def7;

            hence (f9 . n) <= (c * (f . n)) & (f9 . n) >= 0 by A34, A58, A60;

          end;

            suppose (f . n) < (g . n);

            hence (f9 . n) <= (c * (f . n)) & (f9 . n) >= 0 by A34, A57, A59;

          end;

        end;

        then f9 in ( Big_Oh f) by A27, A55;

        hence x in ( max (( Big_Oh f),( Big_Oh g))) by A25, A55, A47, A54, A40;

      end;

      hence thesis by TARSKI: 2;

    end;

    definition

      let F,G be FUNCTION_DOMAIN of NAT , REAL ;

      :: ASYMPT_0:def20

      func F to_power G -> FUNCTION_DOMAIN of NAT , REAL equals { t where t be Element of ( Funcs ( NAT , REAL )) : ex f,g be Element of ( Funcs ( NAT , REAL )), N be Element of NAT st f in F & g in G & for n be Element of NAT st n >= N holds (t . n) = ((f . n) to_power (g . n)) };

      coherence

      proof

        set IT = { t where t be Element of ( Funcs ( NAT , REAL )) : ex f,g be Element of ( Funcs ( NAT , REAL )), N be Element of NAT st f in F & g in G & for n be Element of NAT st n >= N holds (t . n) = ((f . n) to_power (g . n)) };

         A1:

        now

          consider g be object such that

           A2: g in G by XBOOLE_0:def 1;

          g is sequence of REAL by A2, FUNCT_2:def 12;

          then

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

          consider f be object such that

           A3: f in F by XBOOLE_0:def 1;

          f is sequence of REAL by A3, FUNCT_2:def 12;

          then

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

          defpred P[ Element of NAT , Real] means $2 = ((f . $1) to_power (g . $1));

          

           A4: for x be Element of NAT holds ex y be Element of REAL st P[x, y]

          proof

            let x be Element of NAT ;

            reconsider y = ((f . x) to_power (g . x)) as Element of REAL by XREAL_0:def 1;

            take y;

            thus thesis;

          end;

          consider t be sequence of REAL such that

           A5: for x be Element of NAT holds P[x, (t . x)] from FUNCT_2:sch 3( A4);

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

          for x be Element of NAT st x >= 0 holds (t . x) = ((f . x) to_power (g . x)) by A5;

          then t in IT by A3, A2;

          hence IT is non empty;

        end;

        IT is functional

        proof

          let x be object;

          assume x in IT;

          then ex t be Element of ( Funcs ( NAT , REAL )) st x = t & ex f,g be Element of ( Funcs ( NAT , REAL )), N be Element of NAT st f in F & g in G & for n be Element of NAT st n >= N holds (t . n) = ((f . n) to_power (g . n));

          hence thesis;

        end;

        then

        reconsider IT1 = IT as functional non empty set by A1;

        now

          let x be Element of IT1;

          x in IT;

          then ex t be Element of ( Funcs ( NAT , REAL )) st x = t & ex f,g be Element of ( Funcs ( NAT , REAL )), N be Element of NAT st f in F & g in G & for n be Element of NAT st n >= N holds (t . n) = ((f . n) to_power (g . n));

          hence x is sequence of REAL ;

        end;

        hence thesis by FUNCT_2:def 12;

      end;

    end