:: by Richard Krueger , Piotr Rudnicki and Paul Shelley

::

:: Received November 4, 1999

:: Copyright (c) 1999-2021 Association of Mizar Users

:: deftheorem defines logbase ASYMPT_0:def 1 :

for c being Real holds

( c is logbase iff ( c > 0 & c <> 1 ) );

for c being Real holds

( c is logbase iff ( c > 0 & c <> 1 ) );

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

registration

existence

ex b_{1} being Real st b_{1} is positive

ex b_{1} being Real st b_{1} is negative

ex b_{1} being Real st b_{1} is logbase

not for b_{1} being Real holds b_{1} is negative
by XXREAL_0:def 7;

existence

not for b_{1} being Real holds b_{1} is positive
by XXREAL_0:def 6;

existence

not for b_{1} being Real holds b_{1} is logbase

end;
ex b

proof end;

existence ex b

proof end;

existence ex b

proof end;

existence not for b

existence

not for b

existence

not for b

proof end;

definition

let f be Real_Sequence;

end;
attr f is eventually-nonnegative means :Def2: :: ASYMPT_0:def 2

ex N being Nat st

for n being Nat st n >= N holds

f . n >= 0 ;

ex N being Nat st

for n being Nat st n >= N holds

f . n >= 0 ;

attr f is eventually-positive means :Def4: :: ASYMPT_0:def 4

ex N being Nat st

for n being Nat st n >= N holds

f . n > 0 ;

ex N being Nat st

for n being Nat st n >= N holds

f . n > 0 ;

attr f is eventually-nonzero means :Def5: :: ASYMPT_0:def 5

ex N being Nat st

for n being Nat st n >= N holds

f . n <> 0 ;

ex N being Nat st

for n being Nat st n >= N holds

f . n <> 0 ;

attr f is eventually-nondecreasing means :Def6: :: ASYMPT_0:def 6

ex N being Nat st

for n being Nat st n >= N holds

f . n <= f . (n + 1);

ex N being Nat st

for n being Nat st n >= N holds

f . n <= f . (n + 1);

:: deftheorem Def2 defines eventually-nonnegative ASYMPT_0:def 2 :

for f being Real_Sequence holds

( f is eventually-nonnegative iff ex N being Nat st

for n being Nat st n >= N holds

f . n >= 0 );

for f being Real_Sequence holds

( f is eventually-nonnegative iff ex N being Nat st

for n being Nat st n >= N holds

f . n >= 0 );

:: deftheorem Def3 defines positive ASYMPT_0:def 3 :

for f being Real_Sequence holds

( f is positive iff for n being Nat holds f . n > 0 );

for f being Real_Sequence holds

( f is positive iff for n being Nat holds f . n > 0 );

:: deftheorem Def4 defines eventually-positive ASYMPT_0:def 4 :

for f being Real_Sequence holds

( f is eventually-positive iff ex N being Nat st

for n being Nat st n >= N holds

f . n > 0 );

for f being Real_Sequence holds

( f is eventually-positive iff ex N being Nat st

for n being Nat st n >= N holds

f . n > 0 );

:: deftheorem Def5 defines eventually-nonzero ASYMPT_0:def 5 :

for f being Real_Sequence holds

( f is eventually-nonzero iff ex N being Nat st

for n being Nat st n >= N holds

f . n <> 0 );

for f being Real_Sequence holds

( f is eventually-nonzero iff ex N being Nat st

for n being Nat st n >= N holds

f . n <> 0 );

:: deftheorem Def6 defines eventually-nondecreasing ASYMPT_0:def 6 :

for f being Real_Sequence holds

( f is eventually-nondecreasing iff ex N being Nat st

for n being Nat st n >= N holds

f . n <= f . (n + 1) );

for f being Real_Sequence holds

( f is eventually-nondecreasing iff ex N being Nat st

for n being Nat st n >= N holds

f . n <= f . (n + 1) );

registration

ex b_{1} being Real_Sequence st

( b_{1} is eventually-nonnegative & b_{1} is eventually-nonzero & b_{1} is positive & b_{1} is eventually-positive & b_{1} is eventually-nondecreasing )
end;

cluster V1() V4( NAT ) V5( REAL ) non empty Function-like V28( NAT ) quasi_total V39() V40() V41() eventually-nonnegative positive eventually-positive eventually-nonzero eventually-nondecreasing for Element of K16(K17(NAT,REAL));

existence ex b

( b

proof end;

registration

for b_{1} being Real_Sequence st b_{1} is positive holds

b_{1} is eventually-positive

for b_{1} being Real_Sequence st b_{1} is eventually-positive holds

( b_{1} is eventually-nonnegative & b_{1} is eventually-nonzero )

for b_{1} being Real_Sequence st b_{1} is eventually-nonnegative & b_{1} is eventually-nonzero holds

b_{1} is eventually-positive
end;

cluster Function-like quasi_total positive -> eventually-positive for Element of K16(K17(NAT,REAL));

coherence for b

b

proof end;

cluster Function-like quasi_total eventually-positive -> eventually-nonnegative eventually-nonzero for Element of K16(K17(NAT,REAL));

coherence for b

( b

proof end;

cluster Function-like quasi_total eventually-nonnegative eventually-nonzero -> eventually-positive for Element of K16(K17(NAT,REAL));

coherence for b

b

proof end;

definition

let f, g be eventually-nonnegative Real_Sequence;

:: original: +

redefine func f + g -> eventually-nonnegative Real_Sequence;

coherence

f + g is eventually-nonnegative Real_Sequence

end;
:: original: +

redefine func f + g -> eventually-nonnegative Real_Sequence;

coherence

f + g is eventually-nonnegative Real_Sequence

proof end;

definition

let f be eventually-nonnegative Real_Sequence;

let c be positive Real;

:: original: (#)

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

coherence

c (#) f is eventually-nonnegative Real_Sequence

end;
let c be positive Real;

:: original: (#)

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

coherence

c (#) f is eventually-nonnegative Real_Sequence

proof end;

definition

let f be eventually-nonnegative Real_Sequence;

let c be non negative Real;

:: original: +

redefine func c + f -> eventually-nonnegative Real_Sequence;

coherence

c + f is eventually-nonnegative Real_Sequence

end;
let c be non negative Real;

:: original: +

redefine func c + f -> eventually-nonnegative Real_Sequence;

coherence

c + f is eventually-nonnegative Real_Sequence

proof end;

definition

let f be eventually-nonnegative Real_Sequence;

let c be positive Real;

:: original: +

redefine func c + f -> eventually-positive Real_Sequence;

coherence

c + f is eventually-positive Real_Sequence

end;
let c be positive Real;

:: original: +

redefine func c + f -> eventually-positive Real_Sequence;

coherence

c + f is eventually-positive Real_Sequence

proof end;

definition

let f, g be Real_Sequence;

ex b_{1} being Real_Sequence st

for n being Nat holds b_{1} . n = max ((f . n),(g . n))

for b_{1}, b_{2} being Real_Sequence st ( for n being Nat holds b_{1} . n = max ((f . n),(g . n)) ) & ( for n being Nat holds b_{2} . n = max ((f . n),(g . n)) ) holds

b_{1} = b_{2}

for b_{1}, f, g being Real_Sequence st ( for n being Nat holds b_{1} . n = max ((f . n),(g . n)) ) holds

for n being Nat holds b_{1} . n = max ((g . n),(f . n))
;

end;
func max (f,g) -> Real_Sequence means :Def7: :: ASYMPT_0:def 7

for n being Nat holds it . n = max ((f . n),(g . n));

existence for n being Nat holds it . n = max ((f . n),(g . n));

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

commutativity for b

for n being Nat holds b

:: deftheorem Def7 defines max ASYMPT_0:def 7 :

for f, g, b_{3} being Real_Sequence holds

( b_{3} = max (f,g) iff for n being Nat holds b_{3} . n = max ((f . n),(g . n)) );

for f, g, b

( b

registration

let f be Real_Sequence;

let g be eventually-nonnegative Real_Sequence;

coherence

max (f,g) is eventually-nonnegative

end;
let g be eventually-nonnegative Real_Sequence;

coherence

max (f,g) is eventually-nonnegative

proof end;

registration

let f be Real_Sequence;

let g be eventually-positive Real_Sequence;

coherence

max (f,g) is eventually-positive

end;
let g be eventually-positive Real_Sequence;

coherence

max (f,g) is eventually-positive

proof end;

:: deftheorem defines majorizes ASYMPT_0:def 8 :

for f, g being Real_Sequence holds

( g majorizes f iff ex N being Element of NAT st

for n being Element of NAT st n >= N holds

f . n <= g . n );

for f, g being Real_Sequence holds

( g majorizes f iff ex N being Element of NAT st

for n being Element of NAT st n >= N holds

f . n <= g . n );

Lm1: for f, g being Real_Sequence

for n being Nat holds (f /" g) . n = (f . n) / (g . n)

proof end;

theorem Th1: :: ASYMPT_0:1

for f being Real_Sequence

for N being Nat st ( for n being Nat st n >= N holds

f . n <= f . (n + 1) ) holds

for n, m being Nat st N <= n & n <= m holds

f . n <= f . m

for N being Nat st ( for n being Nat st n >= N holds

f . n <= f . (n + 1) ) holds

for n, m being Nat st N <= n & n <= m holds

f . n <= f . m

proof end;

theorem Th2: :: ASYMPT_0:2

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

( g /" f is convergent & lim (g /" f) = (lim (f /" g)) " )

( g /" f is convergent & lim (g /" f) = (lim (f /" g)) " )

proof end;

theorem Th4: :: ASYMPT_0:4

for f, g being Real_Sequence st f is convergent & g is convergent & g majorizes f holds

lim f <= lim g

lim f <= lim g

proof end;

theorem Th5: :: ASYMPT_0:5

for f being Real_Sequence

for g being eventually-nonzero Real_Sequence st f /" g is divergent_to+infty holds

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

for g being eventually-nonzero Real_Sequence st f /" g is divergent_to+infty holds

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

proof end;

definition

let f be eventually-nonnegative Real_Sequence;

{ t where t is Element of Funcs (NAT,REAL) : ex c being Real ex N being Element of NAT st

( c > 0 & ( for n being Element of NAT st n >= N holds

( t . n <= c * (f . n) & t . n >= 0 ) ) ) } is FUNCTION_DOMAIN of NAT , REAL

end;
func Big_Oh f -> FUNCTION_DOMAIN of NAT , REAL equals :: ASYMPT_0:def 9

{ t where t is Element of Funcs (NAT,REAL) : ex c being Real ex N being Element of NAT st

( c > 0 & ( for n being Element of NAT st n >= N holds

( t . n <= c * (f . n) & t . n >= 0 ) ) ) } ;

coherence { t where t is Element of Funcs (NAT,REAL) : ex c being Real ex N being Element of NAT st

( c > 0 & ( for n being Element of NAT st n >= N holds

( t . n <= c * (f . n) & t . n >= 0 ) ) ) } ;

{ t where t is Element of Funcs (NAT,REAL) : ex c being Real ex N being Element of NAT st

( c > 0 & ( for n being Element of NAT st n >= N holds

( t . n <= c * (f . n) & t . n >= 0 ) ) ) } is FUNCTION_DOMAIN of NAT , REAL

proof end;

:: deftheorem defines Big_Oh ASYMPT_0:def 9 :

for f being eventually-nonnegative Real_Sequence holds Big_Oh f = { t where t is Element of Funcs (NAT,REAL) : ex c being Real ex N being Element of NAT st

( c > 0 & ( for n being Element of NAT st n >= N holds

( t . n <= c * (f . n) & t . n >= 0 ) ) ) } ;

for f being eventually-nonnegative Real_Sequence holds Big_Oh f = { t where t is Element of Funcs (NAT,REAL) : ex c being Real ex N being Element of NAT st

( c > 0 & ( for n being Element of NAT st n >= N holds

( t . n <= c * (f . n) & t . n >= 0 ) ) ) } ;

theorem Th6: :: ASYMPT_0:6

for x being set

for f being eventually-nonnegative Real_Sequence st x in Big_Oh f holds

x is eventually-nonnegative Real_Sequence

for f being eventually-nonnegative Real_Sequence st x in Big_Oh f holds

x is eventually-nonnegative Real_Sequence

proof end;

theorem :: ASYMPT_0:7

for f being positive Real_Sequence

for t being eventually-nonnegative Real_Sequence holds

( t in Big_Oh f iff ex c being Real st

( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) ) )

for t being eventually-nonnegative Real_Sequence holds

( t in Big_Oh f iff ex c being Real st

( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) ) )

proof end;

theorem :: ASYMPT_0:8

for f being eventually-positive Real_Sequence

for t being eventually-nonnegative Real_Sequence

for N being Element of NAT st t in Big_Oh f & ( for n being Element of NAT st n >= N holds

f . n > 0 ) holds

ex c being Real st

( c > 0 & ( for n being Element of NAT st n >= N holds

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

for t being eventually-nonnegative Real_Sequence

for N being Element of NAT st t in Big_Oh f & ( for n being Element of NAT st n >= N holds

f . n > 0 ) holds

ex c being Real st

( c > 0 & ( for n being Element of NAT st n >= N holds

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

proof end;

theorem Th12: :: ASYMPT_0:12

for f, g, h being eventually-nonnegative Real_Sequence st f in Big_Oh g & g in Big_Oh h holds

f in Big_Oh h

f in Big_Oh h

proof end;

Lm2: for f, g being eventually-nonnegative Real_Sequence holds

( ( f in Big_Oh g & g in Big_Oh f ) iff Big_Oh f = Big_Oh g )

proof end;

theorem :: ASYMPT_0:13

for f being eventually-nonnegative Real_Sequence

for c being positive Real holds Big_Oh f = Big_Oh (c (#) f)

for c being positive Real holds Big_Oh f = Big_Oh (c (#) f)

proof end;

theorem :: ASYMPT_0:14

for c being non negative Real

for x, f being eventually-nonnegative Real_Sequence st x in Big_Oh f holds

x in Big_Oh (c + f)

for x, f being eventually-nonnegative Real_Sequence st x in Big_Oh f holds

x in Big_Oh (c + f)

proof end;

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

f in Big_Oh g

proof end;

theorem Th15: :: ASYMPT_0:15

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

Big_Oh f = Big_Oh g

Big_Oh f = Big_Oh g

proof end;

theorem Th16: :: ASYMPT_0:16

for f, g being 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 )

( f in Big_Oh g & not g in Big_Oh f )

proof end;

theorem Th17: :: ASYMPT_0:17

for f, g being eventually-positive Real_Sequence st f /" g is divergent_to+infty holds

( not f in Big_Oh g & g in Big_Oh f )

( not f in Big_Oh g & g in Big_Oh f )

proof end;

definition

let f be eventually-nonnegative Real_Sequence;

{ t where t is Element of Funcs (NAT,REAL) : ex d being Real ex N being Element of NAT st

( d > 0 & ( for n being Element of NAT st n >= N holds

( t . n >= d * (f . n) & t . n >= 0 ) ) ) } is FUNCTION_DOMAIN of NAT , REAL

end;
func Big_Omega f -> FUNCTION_DOMAIN of NAT , REAL equals :: ASYMPT_0:def 10

{ t where t is Element of Funcs (NAT,REAL) : ex d being Real ex N being Element of NAT st

( d > 0 & ( for n being Element of NAT st n >= N holds

( t . n >= d * (f . n) & t . n >= 0 ) ) ) } ;

coherence { t where t is Element of Funcs (NAT,REAL) : ex d being Real ex N being Element of NAT st

( d > 0 & ( for n being Element of NAT st n >= N holds

( t . n >= d * (f . n) & t . n >= 0 ) ) ) } ;

{ t where t is Element of Funcs (NAT,REAL) : ex d being Real ex N being Element of NAT st

( d > 0 & ( for n being Element of NAT st n >= N holds

( t . n >= d * (f . n) & t . n >= 0 ) ) ) } is FUNCTION_DOMAIN of NAT , REAL

proof end;

:: deftheorem defines Big_Omega ASYMPT_0:def 10 :

for f being eventually-nonnegative Real_Sequence holds Big_Omega f = { t where t is Element of Funcs (NAT,REAL) : ex d being Real ex N being Element of NAT st

( d > 0 & ( for n being Element of NAT st n >= N holds

( t . n >= d * (f . n) & t . n >= 0 ) ) ) } ;

for f being eventually-nonnegative Real_Sequence holds Big_Omega f = { t where t is Element of Funcs (NAT,REAL) : ex d being Real ex N being Element of NAT st

( d > 0 & ( for n being Element of NAT st n >= N holds

( t . n >= d * (f . n) & t . n >= 0 ) ) ) } ;

theorem :: ASYMPT_0:18

for x being set

for f being eventually-nonnegative Real_Sequence st x in Big_Omega f holds

x is eventually-nonnegative Real_Sequence

for f being eventually-nonnegative Real_Sequence st x in Big_Omega f holds

x is eventually-nonnegative Real_Sequence

proof end;

theorem Th21: :: ASYMPT_0:21

for f, g, h being eventually-nonnegative Real_Sequence st f in Big_Omega g & g in Big_Omega h holds

f in Big_Omega h

f in Big_Omega h

proof end;

theorem :: ASYMPT_0:22

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

Big_Omega f = Big_Omega g

Big_Omega f = Big_Omega g

proof end;

theorem Th23: :: ASYMPT_0:23

for f, g being 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 )

( g in Big_Omega f & not f in Big_Omega g )

proof end;

theorem :: ASYMPT_0:24

for f, g being eventually-positive Real_Sequence st f /" g is divergent_to+infty holds

( not g in Big_Omega f & f in Big_Omega g )

( not g in Big_Omega f & f in Big_Omega g )

proof end;

theorem :: ASYMPT_0:25

for f, t being positive Real_Sequence holds

( t in Big_Omega f iff ex d being Real st

( d > 0 & ( for n being Element of NAT holds d * (f . n) <= t . n ) ) )

( t in Big_Omega f iff ex d being Real st

( d > 0 & ( for n being Element of NAT holds d * (f . n) <= t . n ) ) )

proof end;

definition

let f be eventually-nonnegative Real_Sequence;

(Big_Oh f) /\ (Big_Omega f) is FUNCTION_DOMAIN of NAT , REAL

end;
func Big_Theta f -> FUNCTION_DOMAIN of NAT , REAL equals :: ASYMPT_0:def 11

(Big_Oh f) /\ (Big_Omega f);

coherence (Big_Oh f) /\ (Big_Omega f);

(Big_Oh f) /\ (Big_Omega f) is FUNCTION_DOMAIN of NAT , REAL

proof end;

:: deftheorem defines Big_Theta ASYMPT_0:def 11 :

for f being eventually-nonnegative Real_Sequence holds Big_Theta f = (Big_Oh f) /\ (Big_Omega f);

for f being eventually-nonnegative Real_Sequence holds Big_Theta f = (Big_Oh f) /\ (Big_Omega f);

theorem Th27: :: ASYMPT_0:27

for f being eventually-nonnegative Real_Sequence holds Big_Theta f = { t where t is Element of Funcs (NAT,REAL) : ex c, d being Real ex N being Element of NAT st

( c > 0 & d > 0 & ( for n being Element of NAT st n >= N holds

( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) }

( c > 0 & d > 0 & ( for n being Element of NAT st n >= N holds

( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) }

proof end;

theorem :: ASYMPT_0:30

for f, g, h being eventually-nonnegative Real_Sequence st f in Big_Theta g & g in Big_Theta h holds

f in Big_Theta h

f in Big_Theta h

proof end;

theorem :: ASYMPT_0:31

for f, t being positive Real_Sequence holds

( t in Big_Theta f iff ex c, d being Real st

( c > 0 & d > 0 & ( for n being Element of NAT holds

( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) )

( t in Big_Theta f iff ex c, d being Real st

( c > 0 & d > 0 & ( for n being Element of NAT holds

( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) )

proof end;

theorem :: ASYMPT_0:33

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

f in Big_Theta g

f in Big_Theta g

proof end;

theorem :: ASYMPT_0:34

for f, g being 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 )

( f in Big_Oh g & not f in Big_Theta g )

proof end;

theorem :: ASYMPT_0:35

for f, g being eventually-positive Real_Sequence st f /" g is divergent_to+infty holds

( f in Big_Omega g & not f in Big_Theta g )

( f in Big_Omega g & not f in Big_Theta g )

proof end;

definition

let f be eventually-nonnegative Real_Sequence;

let X be set ;

{ t where t is Element of Funcs (NAT,REAL) : ex c being Real ex N being Element of NAT st

( c > 0 & ( for n being Element of NAT st n >= N & n in X holds

( t . n <= c * (f . n) & t . n >= 0 ) ) ) } is FUNCTION_DOMAIN of NAT , REAL

end;
let X be set ;

func Big_Oh (f,X) -> FUNCTION_DOMAIN of NAT , REAL equals :: ASYMPT_0:def 12

{ t where t is Element of Funcs (NAT,REAL) : ex c being Real ex N being Element of NAT st

( c > 0 & ( for n being Element of NAT st n >= N & n in X holds

( t . n <= c * (f . n) & t . n >= 0 ) ) ) } ;

coherence { t where t is Element of Funcs (NAT,REAL) : ex c being Real ex N being Element of NAT st

( c > 0 & ( for n being Element of NAT st n >= N & n in X holds

( t . n <= c * (f . n) & t . n >= 0 ) ) ) } ;

{ t where t is Element of Funcs (NAT,REAL) : ex c being Real ex N being Element of NAT st

( c > 0 & ( for n being Element of NAT st n >= N & n in X holds

( t . n <= c * (f . n) & t . n >= 0 ) ) ) } is FUNCTION_DOMAIN of NAT , REAL

proof end;

:: deftheorem defines Big_Oh ASYMPT_0:def 12 :

for f being eventually-nonnegative Real_Sequence

for X being set holds Big_Oh (f,X) = { t where t is Element of Funcs (NAT,REAL) : ex c being Real ex N being Element of NAT st

( c > 0 & ( for n being Element of NAT st n >= N & n in X holds

( t . n <= c * (f . n) & t . n >= 0 ) ) ) } ;

for f being eventually-nonnegative Real_Sequence

for X being set holds Big_Oh (f,X) = { t where t is Element of Funcs (NAT,REAL) : ex c being Real ex N being Element of NAT st

( c > 0 & ( for n being Element of NAT st n >= N & n in X holds

( t . n <= c * (f . n) & t . n >= 0 ) ) ) } ;

definition

let f be eventually-nonnegative Real_Sequence;

let X be set ;

{ t where t is Element of Funcs (NAT,REAL) : ex d being Real ex N being Element of NAT st

( d > 0 & ( for n being Element of NAT st n >= N & n in X holds

( t . n >= d * (f . n) & t . n >= 0 ) ) ) } is FUNCTION_DOMAIN of NAT , REAL

end;
let X be set ;

func Big_Omega (f,X) -> FUNCTION_DOMAIN of NAT , REAL equals :: ASYMPT_0:def 13

{ t where t is Element of Funcs (NAT,REAL) : ex d being Real ex N being Element of NAT st

( d > 0 & ( for n being Element of NAT st n >= N & n in X holds

( t . n >= d * (f . n) & t . n >= 0 ) ) ) } ;

coherence { t where t is Element of Funcs (NAT,REAL) : ex d being Real ex N being Element of NAT st

( d > 0 & ( for n being Element of NAT st n >= N & n in X holds

( t . n >= d * (f . n) & t . n >= 0 ) ) ) } ;

{ t where t is Element of Funcs (NAT,REAL) : ex d being Real ex N being Element of NAT st

( d > 0 & ( for n being Element of NAT st n >= N & n in X holds

( t . n >= d * (f . n) & t . n >= 0 ) ) ) } is FUNCTION_DOMAIN of NAT , REAL

proof end;

:: deftheorem defines Big_Omega ASYMPT_0:def 13 :

for f being eventually-nonnegative Real_Sequence

for X being set holds Big_Omega (f,X) = { t where t is Element of Funcs (NAT,REAL) : ex d being Real ex N being Element of NAT st

( d > 0 & ( for n being Element of NAT st n >= N & n in X holds

( t . n >= d * (f . n) & t . n >= 0 ) ) ) } ;

for f being eventually-nonnegative Real_Sequence

for X being set holds Big_Omega (f,X) = { t where t is Element of Funcs (NAT,REAL) : ex d being Real ex N being Element of NAT st

( d > 0 & ( for n being Element of NAT st n >= N & n in X holds

( t . n >= d * (f . n) & t . n >= 0 ) ) ) } ;

definition

let f be eventually-nonnegative Real_Sequence;

let X be set ;

{ t where t is Element of Funcs (NAT,REAL) : ex c, d being Real ex N being Element of NAT st

( c > 0 & d > 0 & ( for n being Element of NAT st n >= N & n in X holds

( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) } is FUNCTION_DOMAIN of NAT , REAL

end;
let X be set ;

func Big_Theta (f,X) -> FUNCTION_DOMAIN of NAT , REAL equals :: ASYMPT_0:def 14

{ t where t is Element of Funcs (NAT,REAL) : ex c, d being Real ex N being Element of NAT st

( c > 0 & d > 0 & ( for n being Element of NAT st n >= N & n in X holds

( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) } ;

coherence { t where t is Element of Funcs (NAT,REAL) : ex c, d being Real ex N being Element of NAT st

( c > 0 & d > 0 & ( for n being Element of NAT st n >= N & n in X holds

( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) } ;

{ t where t is Element of Funcs (NAT,REAL) : ex c, d being Real ex N being Element of NAT st

( c > 0 & d > 0 & ( for n being Element of NAT st n >= N & n in X holds

( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) } is FUNCTION_DOMAIN of NAT , REAL

proof end;

:: deftheorem defines Big_Theta ASYMPT_0:def 14 :

for f being eventually-nonnegative Real_Sequence

for X being set holds Big_Theta (f,X) = { t where t is Element of Funcs (NAT,REAL) : ex c, d being Real ex N being Element of NAT st

( c > 0 & d > 0 & ( for n being Element of NAT st n >= N & n in X holds

( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) } ;

for f being eventually-nonnegative Real_Sequence

for X being set holds Big_Theta (f,X) = { t where t is Element of Funcs (NAT,REAL) : ex c, d being Real ex N being Element of NAT st

( c > 0 & d > 0 & ( for n being Element of NAT st n >= N & n in X holds

( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) } ;

theorem Th36: :: ASYMPT_0:36

for f being eventually-nonnegative Real_Sequence

for X being set holds Big_Theta (f,X) = (Big_Oh (f,X)) /\ (Big_Omega (f,X))

for X being set holds Big_Theta (f,X) = (Big_Oh (f,X)) /\ (Big_Omega (f,X))

proof end;

definition

let f be Real_Sequence;

let b be Nat;

ex b_{1} being Real_Sequence st

for n being Element of NAT holds b_{1} . n = f . (b * n)

for b_{1}, b_{2} being Real_Sequence st ( for n being Element of NAT holds b_{1} . n = f . (b * n) ) & ( for n being Element of NAT holds b_{2} . n = f . (b * n) ) holds

b_{1} = b_{2}

end;
let b be Nat;

func f taken_every b -> Real_Sequence means :Def15: :: ASYMPT_0:def 15

for n being Element of NAT holds it . n = f . (b * n);

existence for n being Element of NAT holds it . n = f . (b * n);

ex b

for n being Element of NAT holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def15 defines taken_every ASYMPT_0:def 15 :

for f being Real_Sequence

for b being Nat

for b_{3} being Real_Sequence holds

( b_{3} = f taken_every b iff for n being Element of NAT holds b_{3} . n = f . (b * n) );

for f being Real_Sequence

for b being Nat

for b

( b

definition

let f be eventually-nonnegative Real_Sequence;

let b be Nat;

end;
let b be Nat;

pred f is_smooth_wrt b means :: ASYMPT_0:def 16

( f is eventually-nondecreasing & f taken_every b in Big_Oh f );

( f is eventually-nondecreasing & f taken_every b in Big_Oh f );

:: deftheorem defines is_smooth_wrt ASYMPT_0:def 16 :

for f being eventually-nonnegative Real_Sequence

for b being Nat holds

( f is_smooth_wrt b iff ( f is eventually-nondecreasing & f taken_every b in Big_Oh f ) );

for f being eventually-nonnegative Real_Sequence

for b being Nat holds

( f is_smooth_wrt b iff ( f is eventually-nondecreasing & f taken_every b in Big_Oh f ) );

definition

let f be eventually-nonnegative Real_Sequence;

end;
attr f is smooth means :: ASYMPT_0:def 17

for b being Element of NAT st b >= 2 holds

f is_smooth_wrt b;

for b being Element of NAT st b >= 2 holds

f is_smooth_wrt b;

:: deftheorem defines smooth ASYMPT_0:def 17 :

for f being eventually-nonnegative Real_Sequence holds

( f is smooth iff for b being Element of NAT st b >= 2 holds

f is_smooth_wrt b );

for f being eventually-nonnegative Real_Sequence holds

( f is smooth iff for b being Element of NAT st b >= 2 holds

f is_smooth_wrt b );

theorem :: ASYMPT_0:37

for f being eventually-nonnegative Real_Sequence st ex b being Element of NAT st

( b >= 2 & f is_smooth_wrt b ) holds

f is smooth

( b >= 2 & f is_smooth_wrt b ) holds

f is smooth

proof end;

theorem Th38: :: ASYMPT_0:38

for f being eventually-nonnegative Real_Sequence

for t being eventually-nonnegative eventually-nondecreasing Real_Sequence

for b being Nat st f is smooth & b >= 2 & t in Big_Oh (f, { (b |^ n) where n is Element of NAT : verum } ) holds

t in Big_Oh f

for t being eventually-nonnegative eventually-nondecreasing Real_Sequence

for b being Nat st f is smooth & b >= 2 & t in Big_Oh (f, { (b |^ n) where n is Element of NAT : verum } ) holds

t in Big_Oh f

proof end;

theorem Th39: :: ASYMPT_0:39

for f being eventually-nonnegative Real_Sequence

for t being eventually-nonnegative eventually-nondecreasing Real_Sequence

for b being Element of NAT st f is smooth & b >= 2 & t in Big_Omega (f, { (b |^ n) where n is Element of NAT : verum } ) holds

t in Big_Omega f

for t being eventually-nonnegative eventually-nondecreasing Real_Sequence

for b being Element of NAT st f is smooth & b >= 2 & t in Big_Omega (f, { (b |^ n) where n is Element of NAT : verum } ) holds

t in Big_Omega f

proof end;

theorem :: ASYMPT_0:40

for f being eventually-nonnegative Real_Sequence

for t being eventually-nonnegative eventually-nondecreasing Real_Sequence

for b being Element of NAT st f is smooth & b >= 2 & t in Big_Theta (f, { (b |^ n) where n is Element of NAT : verum } ) holds

t in Big_Theta f

for t being eventually-nonnegative eventually-nondecreasing Real_Sequence

for b being Element of NAT st f is smooth & b >= 2 & t in Big_Theta (f, { (b |^ n) where n is Element of NAT : verum } ) holds

t in Big_Theta f

proof end;

definition

let X be non empty set ;

let F, G be FUNCTION_DOMAIN of X, REAL ;

{ t where t is Element of Funcs (X,REAL) : ex f, g being Element of Funcs (X,REAL) st

( f in F & g in G & ( for n being Element of X holds t . n = (f . n) + (g . n) ) ) } is FUNCTION_DOMAIN of X, REAL

end;
let F, G be FUNCTION_DOMAIN of X, REAL ;

func F + G -> FUNCTION_DOMAIN of X, REAL equals :: ASYMPT_0:def 18

{ t where t is Element of Funcs (X,REAL) : ex f, g being Element of Funcs (X,REAL) st

( f in F & g in G & ( for n being Element of X holds t . n = (f . n) + (g . n) ) ) } ;

coherence { t where t is Element of Funcs (X,REAL) : ex f, g being Element of Funcs (X,REAL) st

( f in F & g in G & ( for n being Element of X holds t . n = (f . n) + (g . n) ) ) } ;

{ t where t is Element of Funcs (X,REAL) : ex f, g being Element of Funcs (X,REAL) st

( f in F & g in G & ( for n being Element of X holds t . n = (f . n) + (g . n) ) ) } is FUNCTION_DOMAIN of X, REAL

proof end;

:: deftheorem defines + ASYMPT_0:def 18 :

for X being non empty set

for F, G being FUNCTION_DOMAIN of X, REAL holds F + G = { t where t is Element of Funcs (X,REAL) : ex f, g being Element of Funcs (X,REAL) st

( f in F & g in G & ( for n being Element of X holds t . n = (f . n) + (g . n) ) ) } ;

for X being non empty set

for F, G being FUNCTION_DOMAIN of X, REAL holds F + G = { t where t is Element of Funcs (X,REAL) : ex f, g being Element of Funcs (X,REAL) st

( f in F & g in G & ( for n being Element of X holds t . n = (f . n) + (g . n) ) ) } ;

definition

let X be non empty set ;

let F, G be FUNCTION_DOMAIN of X, REAL ;

{ t where t is Element of Funcs (X,REAL) : ex f, g being Element of Funcs (X,REAL) st

( f in F & g in G & ( for n being Element of X holds t . n = max ((f . n),(g . n)) ) ) } is FUNCTION_DOMAIN of X, REAL

end;
let F, G be FUNCTION_DOMAIN of X, REAL ;

func max (F,G) -> FUNCTION_DOMAIN of X, REAL equals :: ASYMPT_0:def 19

{ t where t is Element of Funcs (X,REAL) : ex f, g being Element of Funcs (X,REAL) st

( f in F & g in G & ( for n being Element of X holds t . n = max ((f . n),(g . n)) ) ) } ;

coherence { t where t is Element of Funcs (X,REAL) : ex f, g being Element of Funcs (X,REAL) st

( f in F & g in G & ( for n being Element of X holds t . n = max ((f . n),(g . n)) ) ) } ;

{ t where t is Element of Funcs (X,REAL) : ex f, g being Element of Funcs (X,REAL) st

( f in F & g in G & ( for n being Element of X holds t . n = max ((f . n),(g . n)) ) ) } is FUNCTION_DOMAIN of X, REAL

proof end;

:: deftheorem defines max ASYMPT_0:def 19 :

for X being non empty set

for F, G being FUNCTION_DOMAIN of X, REAL holds max (F,G) = { t where t is Element of Funcs (X,REAL) : ex f, g being Element of Funcs (X,REAL) st

( f in F & g in G & ( for n being Element of X holds t . n = max ((f . n),(g . n)) ) ) } ;

for X being non empty set

for F, G being FUNCTION_DOMAIN of X, REAL holds max (F,G) = { t where t is Element of Funcs (X,REAL) : ex f, g being Element of Funcs (X,REAL) st

( f in F & g in G & ( for n being Element of X holds t . n = max ((f . n),(g . n)) ) ) } ;

theorem :: ASYMPT_0:42

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

proof end;

definition

let F, G be FUNCTION_DOMAIN of NAT , REAL ;

{ t where t is Element of Funcs (NAT,REAL) : ex f, g being Element of Funcs (NAT,REAL) ex N being Element of NAT st

( f in F & g in G & ( for n being Element of NAT st n >= N holds

t . n = (f . n) to_power (g . n) ) ) } is FUNCTION_DOMAIN of NAT , REAL

end;
func F to_power G -> FUNCTION_DOMAIN of NAT , REAL equals :: ASYMPT_0:def 20

{ t where t is Element of Funcs (NAT,REAL) : ex f, g being Element of Funcs (NAT,REAL) ex N being Element of NAT st

( f in F & g in G & ( for n being Element of NAT st n >= N holds

t . n = (f . n) to_power (g . n) ) ) } ;

coherence { t where t is Element of Funcs (NAT,REAL) : ex f, g being Element of Funcs (NAT,REAL) ex N being Element of NAT st

( f in F & g in G & ( for n being Element of NAT st n >= N holds

t . n = (f . n) to_power (g . n) ) ) } ;

{ t where t is Element of Funcs (NAT,REAL) : ex f, g being Element of Funcs (NAT,REAL) ex N being Element of NAT st

( f in F & g in G & ( for n being Element of NAT st n >= N holds

t . n = (f . n) to_power (g . n) ) ) } is FUNCTION_DOMAIN of NAT , REAL

proof end;

:: deftheorem defines to_power ASYMPT_0:def 20 :

for F, G being FUNCTION_DOMAIN of NAT , REAL holds F to_power G = { t where t is Element of Funcs (NAT,REAL) : ex f, g being Element of Funcs (NAT,REAL) ex N being Element of NAT st

( f in F & g in G & ( for n being Element of NAT st n >= N holds

t . n = (f . n) to_power (g . n) ) ) } ;

for F, G being FUNCTION_DOMAIN of NAT , REAL holds F to_power G = { t where t is Element of Funcs (NAT,REAL) : ex f, g being Element of Funcs (NAT,REAL) ex N being Element of NAT st

( f in F & g in G & ( for n being Element of NAT st n >= N holds

t . n = (f . n) to_power (g . n) ) ) } ;