:: ASYMPT_0 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

scheme :: ASYMPT_0:sch 1
FinSegRng1{ F1() -> Nat, F2() -> Nat, F3() -> non empty set , F4( set ) -> Element of F3() } :
{ F4(i) where i is Nat : ( F1() <= i & i <= F2() ) } is non empty finite Subset of F3()
provided
A1: F1() <= F2()
proof end;

scheme :: ASYMPT_0:sch 2
FinImInit1{ F1() -> Nat, F2() -> non empty set , F3( set ) -> Element of F2() } :
{ F3(n) where n is Nat : n <= F1() } is non empty finite Subset of F2()
proof end;

scheme :: ASYMPT_0:sch 3
FinImInit2{ F1() -> Nat, F2() -> non empty set , F3( set ) -> Element of F2() } :
{ F3(n) where n is Nat : n < F1() } is non empty finite Subset of F2()
provided
A1: F1() > 0
proof end;

definition
let c be real number ;
canceled;
canceled;
attr c is logbase means :Def3: :: ASYMPT_0:def 3
( c > 0 & c <> 1 );
end;

:: 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 ) );

registration
cluster positive Element of REAL ;
existence
ex b1 being Real st b1 is positive
proof end;
cluster negative Element of REAL ;
existence
ex b1 being Real st b1 is negative
proof end;
cluster logbase Element of REAL ;
existence
ex b1 being Real st b1 is logbase
proof end;
cluster non negative Element of REAL ;
existence
not for b1 being Real holds b1 is negative
by XREAL_0:def 4;
cluster non positive Element of REAL ;
existence
not for b1 being Real holds b1 is positive
by XREAL_0:def 3;
cluster non logbase Element of REAL ;
existence
not for b1 being Real holds b1 is logbase
proof end;
end;

definition
let f be Real_Sequence;
attr f is eventually-nonnegative means :Def4: :: ASYMPT_0:def 4
ex N being Nat st
for n being Nat st n >= N holds
f . n >= 0;
attr f is positive means :Def5: :: ASYMPT_0:def 5
for n being Nat holds f . n > 0;
attr f is eventually-positive means :Def6: :: ASYMPT_0:def 6
ex N being Nat st
for n being Nat st n >= N holds
f . n > 0;
attr f is eventually-nonzero means :Def7: :: ASYMPT_0:def 7
ex N being Nat st
for n being Nat st n >= N holds
f . n <> 0;
attr f is eventually-nondecreasing means :Def8: :: ASYMPT_0:def 8
ex N being Nat st
for n being Nat st n >= N holds
f . n <= f . (n + 1);
end;

:: deftheorem Def4 defines eventually-nonnegative ASYMPT_0:def 4 :
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 Def5 defines positive ASYMPT_0:def 5 :
for f being Real_Sequence holds
( f is positive iff for n being 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 Nat st
for n being 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 Nat st
for n being 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 Nat st
for n being Nat st n >= N holds
f . n <= f . (n + 1) );

registration
cluster eventually-nonnegative positive eventually-positive eventually-nonzero eventually-nondecreasing M5( NAT , REAL );
existence
ex b1 being Real_Sequence st
( b1 is eventually-nonnegative & b1 is eventually-nonzero & b1 is positive & b1 is eventually-positive & b1 is eventually-nondecreasing )
proof end;
end;

registration
cluster positive -> eventually-positive M5( NAT , REAL );
coherence
for b1 being Real_Sequence st b1 is positive holds
b1 is eventually-positive
proof end;
cluster eventually-positive -> eventually-nonnegative eventually-nonzero M5( NAT , REAL );
coherence
for b1 being Real_Sequence st b1 is eventually-positive holds
( b1 is eventually-nonnegative & b1 is eventually-nonzero )
proof end;
cluster eventually-nonnegative eventually-nonzero -> eventually-positive M5( NAT , REAL );
coherence
for b1 being Real_Sequence st b1 is eventually-nonnegative & b1 is eventually-nonzero holds
b1 is eventually-positive
proof end;
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
proof end;
end;

definition
let f be Real_Sequence;
let c be real number ;
func c + f -> Real_Sequence means :Def9: :: ASYMPT_0:def 9
for n being Nat holds it . n = c + (f . n);
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = c + (f . n)
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = c + (f . n) ) & ( for n being Nat holds b2 . n = c + (f . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines + ASYMPT_0:def 9 :
for f being Real_Sequence
for c being real number
for b3 being Real_Sequence holds
( b3 = c + f iff for n being Nat holds b3 . n = c + (f . n) );

notation
let f be Real_Sequence;
let c be real number ;
synonym f + c for c + f;
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
proof end;
end;

registration
let f be eventually-nonnegative Real_Sequence;
let c be non negative Real;
cluster c + f -> eventually-nonnegative ;
coherence
c + f is eventually-nonnegative
proof end;
end;

registration
let f be eventually-nonnegative Real_Sequence;
let c be positive Real;
cluster c + f -> eventually-nonnegative eventually-positive eventually-nonzero ;
coherence
c + f is eventually-positive
proof end;
end;

definition
let f, g be Real_Sequence;
func max f,g -> Real_Sequence means :Def10: :: ASYMPT_0:def 10
for n being Nat holds it . n = max (f . n),(g . n);
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = max (f . n),(g . n)
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = max (f . n),(g . n) ) & ( for n being Nat holds b2 . n = max (f . n),(g . n) ) holds
b1 = b2
proof end;
commutativity
for b1, f, g being Real_Sequence st ( for n being Nat holds b1 . n = max (f . n),(g . n) ) holds
for n being 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 Nat holds b3 . n = max (f . n),(g . n) );

registration
let f be Real_Sequence;
let g be eventually-nonnegative Real_Sequence;
cluster max f,g -> eventually-nonnegative ;
coherence
max f,g is eventually-nonnegative
proof end;
end;

registration
let f be Real_Sequence;
let g be eventually-positive Real_Sequence;
cluster max f,g -> eventually-nonnegative eventually-positive eventually-nonzero ;
coherence
max f,g is eventually-positive
proof end;
end;

definition
let f, g be Real_Sequence;
pred g majorizes f means :Def11: :: ASYMPT_0:def 11
ex N being Nat st
for n being Nat st n >= N holds
f . n <= g . n;
end;

:: deftheorem Def11 defines majorizes ASYMPT_0:def 11 :
for f, g being Real_Sequence holds
( g majorizes f iff ex N being Nat st
for n being 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th2: :: ASYMPT_0:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)) " )
proof end;

theorem Th3: :: ASYMPT_0:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being eventually-nonnegative Real_Sequence st f is convergent holds
0 <= lim f
proof end;

theorem Th4: :: ASYMPT_0:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being Real_Sequence st f is convergent & g is convergent & g majorizes f holds
lim f <= lim g
proof end;

theorem Th5: :: ASYMPT_0:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

definition
let f be eventually-nonnegative Real_Sequence;
func Big_Oh f -> 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 Nat st
( c > 0 & ( for n being 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 Nat st
( c > 0 & ( for n being Nat st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) ) )
}
is FUNCTION_DOMAIN of NAT , REAL
proof end;
end;

:: 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 Nat st
( c > 0 & ( for n being Nat st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) ) )
}
;

theorem Th6: :: ASYMPT_0:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Nat holds t . n <= c * (f . n) ) ) )
proof end;

theorem :: ASYMPT_0:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being eventually-positive Real_Sequence
for t being eventually-nonnegative Real_Sequence
for N being Nat st t in Big_Oh f & ( for n being Nat st n >= N holds
f . n > 0 ) holds
ex c being Real st
( c > 0 & ( for n being Nat st n >= N holds
t . n <= c * (f . n) ) )
proof end;

theorem :: ASYMPT_0:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being eventually-nonnegative Real_Sequence holds Big_Oh (f + g) = Big_Oh (max f,g)
proof end;

theorem Th10: :: ASYMPT_0:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being eventually-nonnegative Real_Sequence holds f in Big_Oh f
proof end;

theorem Th11: :: ASYMPT_0:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being eventually-nonnegative Real_Sequence st f in Big_Oh g holds
Big_Oh f c= Big_Oh g
proof end;

theorem Th12: :: ASYMPT_0:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being eventually-nonnegative Real_Sequence
for c being positive Real holds Big_Oh f = Big_Oh (c (#) f)
proof end;

theorem :: ASYMPT_0:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being eventually-positive Real_Sequence st f /" g is convergent & lim (f /" g) > 0 holds
Big_Oh f = Big_Oh g
proof end;

theorem Th16: :: ASYMPT_0:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th17: :: ASYMPT_0:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

definition
let f be eventually-nonnegative Real_Sequence;
func Big_Omega f -> 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 Nat st
( d > 0 & ( for n being 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 Nat st
( d > 0 & ( for n being Nat st n >= N holds
( t . n >= d * (f . n) & t . n >= 0 ) ) )
}
is FUNCTION_DOMAIN of NAT , REAL
proof end;
end;

:: 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 Nat st
( d > 0 & ( for n being Nat st n >= N holds
( t . n >= d * (f . n) & t . n >= 0 ) ) )
}
;

theorem :: ASYMPT_0:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for f being eventually-nonnegative Real_Sequence st x in Big_Omega f holds
x is eventually-nonnegative Real_Sequence
proof end;

theorem Th19: :: ASYMPT_0:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being eventually-nonnegative Real_Sequence holds
( f in Big_Omega g iff g in Big_Oh f )
proof end;

theorem Th20: :: ASYMPT_0:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being eventually-nonnegative Real_Sequence holds f in Big_Omega f
proof end;

theorem Th21: :: ASYMPT_0:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: ASYMPT_0:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being eventually-positive Real_Sequence st f /" g is convergent & lim (f /" g) > 0 holds
Big_Omega f = Big_Omega g
proof end;

theorem Th23: :: ASYMPT_0:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: ASYMPT_0:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: ASYMPT_0:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, t being positive Real_Sequence holds
( t in Big_Omega f iff ex d being Real st
( d > 0 & ( for n being Nat holds d * (f . n) <= t . n ) ) )
proof end;

theorem :: ASYMPT_0:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being eventually-nonnegative Real_Sequence holds Big_Omega (f + g) = Big_Omega (max f,g)
proof end;

definition
let f be eventually-nonnegative Real_Sequence;
func Big_Theta f -> FUNCTION_DOMAIN of NAT , REAL equals :: ASYMPT_0:def 14
(Big_Oh f) /\ (Big_Omega f);
coherence
(Big_Oh f) /\ (Big_Omega f) is FUNCTION_DOMAIN of NAT , REAL
proof end;
end;

:: 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: :: ASYMPT_0:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Nat st
( c > 0 & d > 0 & ( for n being Nat st n >= N holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) )
}
proof end;

theorem :: ASYMPT_0:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being eventually-nonnegative Real_Sequence holds f in Big_Theta f
proof end;

theorem :: ASYMPT_0:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being eventually-nonnegative Real_Sequence st f in Big_Theta g holds
g in Big_Theta f
proof end;

theorem :: ASYMPT_0:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: ASYMPT_0:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Nat holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) )
proof end;

theorem :: ASYMPT_0:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being eventually-nonnegative Real_Sequence holds Big_Theta (f + g) = Big_Theta (max f,g)
proof end;

theorem :: ASYMPT_0:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being eventually-positive Real_Sequence st f /" g is convergent & lim (f /" g) > 0 holds
f in Big_Theta g
proof end;

theorem :: ASYMPT_0:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: ASYMPT_0:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

definition
let f be eventually-nonnegative Real_Sequence;
let X be set ;
func Big_Oh f,X -> FUNCTION_DOMAIN of NAT , REAL equals :: ASYMPT_0:def 15
{ t where t is Element of Funcs NAT ,REAL : ex c being Real ex N being Nat st
( c > 0 & ( for n being 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 Nat st
( c > 0 & ( for n being Nat st n >= N & n in X holds
( t . n <= c * (f . n) & t . n >= 0 ) ) )
}
is FUNCTION_DOMAIN of NAT , REAL
proof end;
end;

:: 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 Nat st
( c > 0 & ( for n being 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 ;
func Big_Omega f,X -> FUNCTION_DOMAIN of NAT , REAL equals :: ASYMPT_0:def 16
{ t where t is Element of Funcs NAT ,REAL : ex d being Real ex N being Nat st
( d > 0 & ( for n being 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 Nat st
( d > 0 & ( for n being Nat st n >= N & n in X holds
( t . n >= d * (f . n) & t . n >= 0 ) ) )
}
is FUNCTION_DOMAIN of NAT , REAL
proof end;
end;

:: 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 Nat st
( d > 0 & ( for n being 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 ;
func Big_Theta f,X -> FUNCTION_DOMAIN of NAT , REAL equals :: ASYMPT_0:def 17
{ t where t is Element of Funcs NAT ,REAL : ex c, d being Real ex N being Nat st
( c > 0 & d > 0 & ( for n being 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 Nat st
( c > 0 & d > 0 & ( for n being 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;
end;

:: 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 Nat st
( c > 0 & d > 0 & ( for n being Nat st n >= N & n in X holds
( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) )
}
;

theorem Th36: :: ASYMPT_0:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being eventually-nonnegative Real_Sequence
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;
func f taken_every b -> Real_Sequence means :Def18: :: ASYMPT_0:def 18
for n being Nat holds it . n = f . (b * n);
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = f . (b * n)
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = f . (b * n) ) & ( for n being Nat holds b2 . n = f . (b * n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines taken_every ASYMPT_0:def 18 :
for f being Real_Sequence
for b being Nat
for b3 being Real_Sequence holds
( b3 = f taken_every b iff for n being Nat holds b3 . n = f . (b * n) );

definition
let f be eventually-nonnegative Real_Sequence;
let b be Nat;
pred f is_smooth_wrt b means :Def19: :: ASYMPT_0:def 19
( f is eventually-nondecreasing & f taken_every b in Big_Oh f );
end;

:: deftheorem Def19 defines is_smooth_wrt ASYMPT_0:def 19 :
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;
attr f is smooth means :Def20: :: ASYMPT_0:def 20
for b being Nat st b >= 2 holds
f is_smooth_wrt b;
end;

:: deftheorem Def20 defines smooth ASYMPT_0:def 20 :
for f being eventually-nonnegative Real_Sequence holds
( f is smooth iff for b being Nat st b >= 2 holds
f is_smooth_wrt b );

theorem :: ASYMPT_0:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being eventually-nonnegative Real_Sequence st ex b being Nat st
( b >= 2 & f is_smooth_wrt b ) holds
f is smooth
proof end;

theorem Th38: :: ASYMPT_0:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Nat : verum } holds
t in Big_Oh f
proof end;

theorem Th39: :: ASYMPT_0:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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_Omega f,{ (b |^ n) where n is Nat : verum } holds
t in Big_Omega f
proof end;

theorem :: ASYMPT_0:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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_Theta f,{ (b |^ n) where n is 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 ;
func F + G -> FUNCTION_DOMAIN of X, REAL equals :: ASYMPT_0:def 21
{ 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
proof end;
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 :: ASYMPT_0:def 22
{ 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
proof end;
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 :: ASYMPT_0:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being eventually-nonnegative Real_Sequence holds (Big_Oh f) + (Big_Oh g) = Big_Oh (f + g)
proof end;

theorem :: ASYMPT_0:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ;
func F to_power G -> FUNCTION_DOMAIN of NAT , REAL equals :: ASYMPT_0:def 23
{ 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
proof end;
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) ) )
}
;