let f, g be eventually-nonnegative Real_Sequence; :: thesis: ( f in Big_Theta g iff Big_Theta f = Big_Theta g )
A1: Big_Theta g = { s where s 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 * (g . n) <= s . n & s . n <= c * (g . n) ) ) ) } by ASYMPT_0:27;
consider N2 being Nat such that
A2: for n being Nat st n >= N2 holds
g . n >= 0 by ASYMPT_0:def 2;
consider N1 being Nat such that
A3: for n being Nat st n >= N1 holds
f . n >= 0 by ASYMPT_0:def 2;
A4: Big_Theta f = { s where s 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) <= s . n & s . n <= c * (f . n) ) ) ) } by ASYMPT_0:27;
hereby :: thesis: ( Big_Theta f = Big_Theta g implies f in Big_Theta g )
assume A5: f in Big_Theta g ; :: thesis: Big_Theta f = Big_Theta g
now :: thesis: for x being object holds
( ( x in Big_Theta f implies x in Big_Theta g ) & ( x in Big_Theta g implies x in Big_Theta f ) )
let x be object ; :: thesis: ( ( x in Big_Theta f implies x in Big_Theta g ) & ( x in Big_Theta g implies x in Big_Theta f ) )
A6: g in Big_Theta f by A5, ASYMPT_0:29;
hereby :: thesis: ( x in Big_Theta g implies x in Big_Theta f )
assume x in Big_Theta f ; :: thesis: x in Big_Theta g
then consider s being Element of Funcs (NAT,REAL) such that
A7: s = x and
A8: 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) <= s . n & s . n <= c * (f . n) ) ) ) by A4;
consider c, d being Real, N3 being Element of NAT such that
c > 0 and
A9: d > 0 and
A10: for n being Element of NAT st n >= N3 holds
( d * (f . n) <= s . n & s . n <= c * (f . n) ) by A8;
reconsider N = max (N1,N3) as Nat by TARSKI:1;
A11: N >= N3 by XXREAL_0:25;
A12: N >= N1 by XXREAL_0:25;
now :: thesis: ex N being Nat st
for n being Nat st n >= N holds
s . n >= 0
take N = N; :: thesis: for n being Nat st n >= N holds
s . n >= 0
let n be Nat; :: thesis: ( n >= N implies s . n >= 0 )
A13: n in NAT by ORDINAL1:def 12;
assume A14: n >= N ; :: thesis: s . n >= 0
then n >= N1 by A12, XXREAL_0:2;
then f . n >= 0 by A3;
then A15: d * (f . n) >= d * 0 by A9;
n >= N3 by A11, A14, XXREAL_0:2;
hence s . n >= 0 by A10, A15, A13; :: thesis: verum
end;
then A16: s is eventually-nonnegative ;
s in Big_Theta f by A4, A8;
hence x in Big_Theta g by A5, A7, A16, ASYMPT_0:30; :: thesis: verum
end;
assume x in Big_Theta g ; :: thesis: x in Big_Theta f
then consider s being Element of Funcs (NAT,REAL) such that
A17: s = x and
A18: 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 * (g . n) <= s . n & s . n <= c * (g . n) ) ) ) by A1;
consider c, d being Real, N3 being Element of NAT such that
c > 0 and
A19: d > 0 and
A20: for n being Element of NAT st n >= N3 holds
( d * (g . n) <= s . n & s . n <= c * (g . n) ) by A18;
reconsider N = max (N2,N3) as Nat by TARSKI:1;
A21: N >= N3 by XXREAL_0:25;
A22: N >= N2 by XXREAL_0:25;
now :: thesis: ex N being Nat st
for n being Nat st n >= N holds
s . n >= 0
take N = N; :: thesis: for n being Nat st n >= N holds
s . n >= 0
let n be Nat; :: thesis: ( n >= N implies s . n >= 0 )
A23: n in NAT by ORDINAL1:def 12;
assume A24: n >= N ; :: thesis: s . n >= 0
then n >= N2 by A22, XXREAL_0:2;
then g . n >= 0 by A2;
then A25: d * (g . n) >= d * 0 by A19;
n >= N3 by A21, A24, XXREAL_0:2;
hence s . n >= 0 by A20, A25, A23; :: thesis: verum
end;
then A26: s is eventually-nonnegative ;
s in Big_Theta g by A1, A18;
hence x in Big_Theta f by A17, A26, A6, ASYMPT_0:30; :: thesis: verum
end;
hence Big_Theta f = Big_Theta g by TARSKI:2; :: thesis: verum
end;
assume Big_Theta f = Big_Theta g ; :: thesis: f in Big_Theta g
hence f in Big_Theta g by ASYMPT_0:28; :: thesis: verum