let f, g be eventually-nonnegative Real_Sequence; :: thesis: ( f in Big_Omega g iff g in Big_Oh f )
A1: g is Element of Funcs (NAT,REAL) by FUNCT_2:8;
hereby :: thesis: ( g in Big_Oh f implies f in Big_Omega g )
consider N1 being Nat such that
A2: for n being Nat st n >= N1 holds
g . n >= 0 by Def2;
assume f in Big_Omega g ; :: thesis: g in Big_Oh f
then consider t being Element of Funcs (NAT,REAL) such that
A3: f = t and
A4: 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 * (g . n) & t . n >= 0 ) ) ) ;
consider d being Real, N being Element of NAT such that
A5: d > 0 and
A6: for n being Element of NAT 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 :: thesis: ex a being Element of NAT st
for n being Element of NAT st n >= a holds
( g . n <= (d ") * (f . n) & g . n >= 0 )
take a = a; :: thesis: for n being Element of NAT st n >= a holds
( g . n <= (d ") * (f . n) & g . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= a implies ( g . n <= (d ") * (f . n) & g . n >= 0 ) )
assume A9: n >= a ; :: thesis: ( g . n <= (d ") * (f . n) & g . n >= 0 )
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; :: thesis: g . n >= 0
n >= N1 by A7, A9, XXREAL_0:2;
hence g . n >= 0 by A2; :: thesis: verum
end;
hence g in Big_Oh f by A1, A5; :: thesis: verum
end;
assume g in Big_Oh f ; :: thesis: f in Big_Omega g
then consider t being Element of Funcs (NAT,REAL) such that
A10: g = t and
A11: 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 ) ) ) ;
consider c being Real, N being Element of NAT such that
A12: c > 0 and
A13: for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) by A11;
consider N1 being Nat such that
A14: for n being 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 :: thesis: ex a being Element of NAT st
for n being Element of NAT st n >= a holds
( f . n >= (c ") * (g . n) & f . n >= 0 )
take a = a; :: thesis: for n being Element of NAT st n >= a holds
( f . n >= (c ") * (g . n) & f . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= a implies ( f . n >= (c ") * (g . n) & f . n >= 0 ) )
assume A18: n >= a ; :: thesis: ( f . n >= (c ") * (g . n) & f . n >= 0 )
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; :: thesis: f . n >= 0
n >= N1 by A15, A18, XXREAL_0:2;
hence f . n >= 0 by A14; :: thesis: verum
end;
f is Element of Funcs (NAT,REAL) by FUNCT_2:8;
hence f in Big_Omega g by A12, A17; :: thesis: verum