let f, g be eventually-positive Real_Sequence; :: thesis: ( f /" g is convergent & lim (f /" g) = 0 implies ( f in Big_Oh g & not g in Big_Oh f ) )
assume that
A1: f /" g is convergent and
A2: lim (f /" g) = 0 ; :: thesis: ( f in Big_Oh g & not g in Big_Oh f )
A3: f is Element of Funcs NAT ,REAL by FUNCT_2:11;
consider N being Element of NAT such that
A4: for n being Element of NAT st N <= n holds
abs (((f /" g) . n) - 0 ) < 1 by A1, A2, SEQ_2:def 7;
consider N1 being Element of NAT such that
A5: for n being Element of NAT st n >= N1 holds
f . n >= 0 by Def4;
consider N2 being Element of NAT such that
A6: for n being Element of NAT st n >= N2 holds
g . n > 0 by Def6;
set b = max N,N1;
set a = max (max N,N1),N2;

A7: now

let n be Element of NAT ; :: thesis: ( n >= max (max N,N1),N2 implies ( f . n <= 1 * (g . n) & f . n >= 0 ) )
assume A8: n >= max (max N,N1),N2 ; :: thesis: ( f . n <= 1 * (g . n) & f . n >= 0 )
A9: ( max (max N,N1),N2 >= max N,N1 & max (max N,N1),N2 >= N2 ) by XXREAL_0:25;
then A10: n >= N2 by A8, XXREAL_0:2;
A11: ( max N,N1 >= N & max N,N1 >= N1 ) by XXREAL_0:25;
n >= max N,N1 by A8, A9, XXREAL_0:2;
then A12: ( n >= N & n >= N1 ) by A11, XXREAL_0:2;
then abs (((f /" g) . n) - 0 ) < 1 by A4;
then (f /" g) . n <= 1 by ABSVALUE:12;
then (f . n) * ((g " ) . n) <= 1 by SEQ_1:12;
then A13: (f . n) * ((g . n) " ) <= 1 by VALUED_1:10;
g . n > 0 by A6, A10;
then ((f . n) * ((g . n) " )) * (g . n) <= 1 * (g . n) by A13, XREAL_1:66;
then A14: (f . n) * (((g . n) " ) * (g . n)) <= 1 * (g . n) ;
g . n <> 0 by A6, A10;
then (f . n) * 1 <= 1 * (g . n) by A14, XCMPLX_0:def 7;
hence f . n <= 1 * (g . n) ; :: thesis: f . n >= 0
thus f . n >= 0 by A5, A12; :: thesis: verum

end;

not g in Big_Oh f

proof

assume g in Big_Oh f ; :: thesis: contradiction
then consider t being Element of Funcs NAT ,REAL such that
A15: t = g and
A16: 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
A17: c > 0 and
A18: for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) by A16;
set a = max N,N2;
A19: ( max N,N2 >= N & max N,N2 >= N2 ) by XXREAL_0:25;
reconsider q = NAT --> (1 / c) as Real_Sequence ;

now

take a = max N,N2; :: thesis: for n being Element of NAT st n >= a holds
q . n <= (f /" g) . n
let n be Element of NAT ; :: thesis: ( n >= a implies q . n <= (f /" g) . n )
assume n >= a ; :: thesis: q . n <= (f /" g) . n
then A20: ( n >= N & n >= N2 ) by A19, XXREAL_0:2;
then A21: ( g . n <= c * (f . n) & g . n >= 0 ) by A15, A18;
A22: g . n > 0 by A6, A20;
A24: c " > 0 by A17;
(g . n) * ((g . n) " ) <= (c * (f . n)) * ((g . n) " ) by A21, XREAL_1:66;
then 1 <= (c * (f . n)) * ((g . n) " ) by A22, XCMPLX_0:def 7;
then (c " ) * 1 <= (c " ) * (c * ((f . n) * ((g . n) " ))) by A24, XREAL_1:66;
then (c " ) * 1 <= ((c " ) * c) * ((f . n) * ((g . n) " )) ;
then (c " ) * 1 <= 1 * ((f . n) * ((g . n) " )) by A17, XCMPLX_0:def 7;
then 1 / c <= (1 * (f . n)) * ((g . n) " ) by XCMPLX_0:def 9;
then 1 / c <= (1 * (f . n)) / (g . n) by XCMPLX_0:def 9;
then 1 / c <= (f /" g) . n by Lm1;
hence q . n <= (f /" g) . n by FUNCOP_1:13; :: thesis: verum

end;

then A25: f /" g majorizes q by Def11;

now

take p = 1 / c; :: thesis: for p1 being real number st p1 > 0 holds
ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs ((q . n) - p) < p1
let p1 be real number ; :: thesis: ( p1 > 0 implies ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs ((q . n) - p) < p1 )
assume A26: p1 > 0 ; :: thesis: ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs ((q . n) - p) < p1
take N = N; :: thesis: for n being Element of NAT st n >= N holds
abs ((q . n) - p) < p1
let n be Element of NAT ; :: thesis: ( n >= N implies abs ((q . n) - p) < p1 )
assume n >= N ; :: thesis: abs ((q . n) - p) < p1
abs ((q . n) - p) = abs ((1 / c) - (1 / c)) by FUNCOP_1:13
.= abs 0 ;
hence abs ((q . n) - p) < p1 by A26, ABSVALUE:7; :: thesis: verum

end;

then A27: q is convergent by SEQ_2:def 6;

now

let p1 be real number ; :: thesis: ( p1 > 0 implies ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs ((q . n) - (1 / c)) < p1 )
assume A28: p1 > 0 ; :: thesis: ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs ((q . n) - (1 / c)) < p1
take N = N; :: thesis: for n being Element of NAT st n >= N holds
abs ((q . n) - (1 / c)) < p1
let n be Element of NAT ; :: thesis: ( n >= N implies abs ((q . n) - (1 / c)) < p1 )
assume n >= N ; :: thesis: abs ((q . n) - (1 / c)) < p1
abs ((q . n) - (1 / c)) = abs ((1 / c) - (1 / c)) by FUNCOP_1:13
.= abs 0 ;
hence abs ((q . n) - (1 / c)) < p1 by A28, ABSVALUE:7; :: thesis: verum

end;

then lim q = 1 / c by A27, SEQ_2:def 7;
then 1 / c <= 0 by A1, A2, A25, A27, Th4;
then (1 / c) * c <= 0 * c by A17;
hence contradiction by A17, XCMPLX_1:107; :: thesis: verum

end;

hence ( f in Big_Oh g & not g in Big_Oh f ) by A3, A7; :: thesis: verum