begin
:: deftheorem ASYMPT_0:def 1 :
canceled;
:: deftheorem ASYMPT_0:def 2 :
canceled;
:: deftheorem Def3 defines logbase ASYMPT_0:def 3 :
for c being real number holds
( c is logbase iff ( c > 0 & c <> 1 ) );
:: deftheorem Def4 defines eventually-nonnegative ASYMPT_0:def 4 :
for f being Real_Sequence holds
( f is eventually-nonnegative iff ex N being Element of NAT st
for n being Element of NAT st n >= N holds
f . n >= 0 );
:: deftheorem Def5 defines positive ASYMPT_0:def 5 :
for f being Real_Sequence holds
( f is positive iff for n being Element of NAT holds f . n > 0 );
:: deftheorem Def6 defines eventually-positive ASYMPT_0:def 6 :
for f being Real_Sequence holds
( f is eventually-positive iff ex N being Element of NAT st
for n being Element of NAT st n >= N holds
f . n > 0 );
:: deftheorem Def7 defines eventually-nonzero ASYMPT_0:def 7 :
for f being Real_Sequence holds
( f is eventually-nonzero iff ex N being Element of NAT st
for n being Element of NAT st n >= N holds
f . n <> 0 );
:: deftheorem Def8 defines eventually-nondecreasing ASYMPT_0:def 8 :
for f being Real_Sequence holds
( f is eventually-nondecreasing iff ex N being Element of NAT st
for n being Element of NAT st n >= N holds
f . n <= f . (n + 1) );
:: deftheorem ASYMPT_0:def 9 :
canceled;
definition
let f,
g be
Real_Sequence;
func max (
f,
g)
-> Real_Sequence means :
Def10:
for
n being
Element of
NAT holds
it . n = max (
(f . n),
(g . n));
existence
ex b1 being Real_Sequence st
for n being Element of NAT holds b1 . n = max ((f . n),(g . n))
uniqueness
for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = max ((f . n),(g . n)) ) & ( for n being Element of NAT holds b2 . n = max ((f . n),(g . n)) ) holds
b1 = b2
commutativity
for b1, f, g being Real_Sequence st ( for n being Element of NAT holds b1 . n = max ((f . n),(g . n)) ) holds
for n being Element of NAT holds b1 . n = max ((g . n),(f . n))
;
end;
:: deftheorem Def10 defines max ASYMPT_0:def 10 :
for f, g, b3 being Real_Sequence holds
( b3 = max (f,g) iff for n being Element of NAT holds b3 . n = max ((f . n),(g . n)) );
:: deftheorem Def11 defines majorizes ASYMPT_0:def 11 :
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 Element of NAT holds (f /" g) . n = (f . n) / (g . n)
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
begin
:: deftheorem defines Big_Oh ASYMPT_0:def 12 :
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:
theorem
theorem
theorem
theorem Th10:
theorem Th11:
theorem Th12:
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 )
theorem
theorem
Lm3:
for f, g being eventually-positive Real_Sequence st f /" g is convergent & lim (f /" g) > 0 holds
f in Big_Oh g
theorem Th15:
theorem Th16:
theorem Th17:
begin
:: deftheorem defines Big_Omega ASYMPT_0:def 13 :
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
theorem Th19:
theorem Th20:
theorem Th21:
theorem
theorem Th23:
theorem
theorem
theorem
:: deftheorem defines Big_Theta ASYMPT_0:def 14 :
for f being eventually-nonnegative Real_Sequence holds Big_Theta f = (Big_Oh f) /\ (Big_Omega f);
theorem Th27:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
begin
:: deftheorem defines Big_Oh ASYMPT_0:def 15 :
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 ) ) ) } ;
:: deftheorem defines Big_Omega ASYMPT_0:def 16 :
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 ) ) ) } ;
:: deftheorem defines Big_Theta ASYMPT_0:def 17 :
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:
:: deftheorem Def18 defines taken_every ASYMPT_0:def 18 :
for f being Real_Sequence
for b being Element of NAT
for b3 being Real_Sequence holds
( b3 = f taken_every b iff for n being Element of NAT holds b3 . n = f . (b * n) );
:: deftheorem Def19 defines is_smooth_wrt ASYMPT_0:def 19 :
for f being eventually-nonnegative Real_Sequence
for b being Element of NAT holds
( f is_smooth_wrt b iff ( f is eventually-nondecreasing & f taken_every b in Big_Oh f ) );
:: deftheorem Def20 defines smooth ASYMPT_0:def 20 :
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
theorem Th38:
theorem Th39:
theorem
begin
definition
let X be non
empty set ;
let F,
G be
FUNCTION_DOMAIN of
X,
REAL ;
func F + G -> FUNCTION_DOMAIN of
X,
REAL equals
{ 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) ) ) } is FUNCTION_DOMAIN of X, REAL
end;
:: deftheorem defines + ASYMPT_0:def 21 :
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 ;
func max (
F,
G)
-> FUNCTION_DOMAIN of
X,
REAL equals
{ 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)) ) ) } is FUNCTION_DOMAIN of X, REAL
end;
:: deftheorem defines max ASYMPT_0:def 22 :
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
theorem
definition
let F,
G be
FUNCTION_DOMAIN of
NAT ,
REAL ;
func F to_power G -> FUNCTION_DOMAIN of
NAT ,
REAL equals
{ 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) ) ) } is FUNCTION_DOMAIN of NAT , REAL
end;
:: deftheorem defines to_power ASYMPT_0:def 23 :
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) ) ) } ;