let f, g be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds f . n = n mod 2 ) & ( for n being Element of NAT holds g . n = (n + 1) mod 2 ) implies ex s, s1 being eventually-nonnegative Real_Sequence st
( s = f & s1 = g & not s in Big_Oh s1 & not s1 in Big_Oh s ) )
assume that
A1: for n being Element of NAT holds f . n = n mod 2 and
A2: for n being Element of NAT holds g . n = (n + 1) mod 2 ; :: thesis: ex s, s1 being eventually-nonnegative Real_Sequence st
( s = f & s1 = g & not s in Big_Oh s1 & not s1 in Big_Oh s )
g is eventually-nonnegative
proof
take 0 ; :: according to ASYMPT_0:def 2 :: thesis: for b1 being set holds
( not 0 <= b1 or 0 <= g . b1 )
let n be Nat; :: thesis: ( not 0 <= n or 0 <= g . n )
A3: n in NAT by ORDINAL1:def 12;
assume n >= 0 ; :: thesis: 0 <= g . n
A4: g . n = (n + 1) mod 2 by A2, A3;
per cases ( g . n = 0 or g . n = 1 ) by A4, NAT_D:12;
suppose g . n = 0 ; :: thesis: 0 <= g . n
hence 0 <= g . n ; :: thesis: verum
end;
suppose g . n = 1 ; :: thesis: 0 <= g . n
hence 0 <= g . n ; :: thesis: verum
end;
end;
end;
then reconsider g = g as eventually-nonnegative Real_Sequence ;
f is eventually-nonnegative
proof
take 0 ; :: according to ASYMPT_0:def 2 :: thesis: for b1 being set holds
( not 0 <= b1 or 0 <= f . b1 )
let n be Nat; :: thesis: ( not 0 <= n or 0 <= f . n )
A5: n in NAT by ORDINAL1:def 12;
assume n >= 0 ; :: thesis: 0 <= f . n
A6: f . n = n mod 2 by A1, A5;
per cases ( f . n = 0 or f . n = 1 ) by A6, NAT_D:12;
suppose f . n = 0 ; :: thesis: 0 <= f . n
hence 0 <= f . n ; :: thesis: verum
end;
suppose f . n = 1 ; :: thesis: 0 <= f . n
hence 0 <= f . n ; :: thesis: verum
end;
end;
end;
then reconsider f = f as eventually-nonnegative Real_Sequence ;
A7: now :: thesis: not g in Big_Oh f
assume g in Big_Oh f ; :: thesis: contradiction
then consider t being Element of Funcs (NAT,REAL) such that
A8: t = g and
A9: 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
c > 0 and
A10: for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) by A9;
ex n being Element of NAT st
( n >= N & t . n > c * (f . n) )
proof
per cases ( N mod 2 = 0 or N mod 2 = 1 ) by NAT_D:12;
suppose A11: N mod 2 = 0 ; :: thesis: ex n being Element of NAT st
( n >= N & t . n > c * (f . n) )
then f . N = 0 by A1;
then A12: c * (f . N) = 0 ;
t . N = (N + 1) mod 2 by A2, A8
.= (0 + (1 mod 2)) mod 2 by A11, EULER_2:6
.= (0 + 1) mod 2 by NAT_D:14
.= 1 by NAT_D:14 ;
hence ex n being Element of NAT st
( n >= N & t . n > c * (f . n) ) by A12; :: thesis: verum
end;
suppose A13: N mod 2 = 1 ; :: thesis: ex n being Element of NAT st
( n >= N & t . n > c * (f . n) )
f . (N + 1) = (N + 1) mod 2 by A1
.= (1 + (1 mod 2)) mod 2 by A13, EULER_2:6
.= (1 + 1) mod 2 by NAT_D:14
.= 0 by NAT_D:25 ;
then A14: c * (f . (N + 1)) = 0 ;
A15: N + 1 >= N by NAT_1:13;
t . (N + 1) = ((N + 1) + 1) mod 2 by A2, A8
.= (N + (1 + 1)) mod 2
.= (1 + (2 mod 2)) mod 2 by A13, EULER_2:6
.= (1 + 0) mod 2 by NAT_D:25
.= 1 by NAT_D:14 ;
hence ex n being Element of NAT st
( n >= N & t . n > c * (f . n) ) by A15, A14; :: thesis: verum
end;
end;
end;
hence contradiction by A10; :: thesis: verum
end;
take f ; :: thesis: ex s1 being eventually-nonnegative Real_Sequence st
( f = f & s1 = g & not f in Big_Oh s1 & not s1 in Big_Oh f )
take g ; :: thesis: ( f = f & g = g & not f in Big_Oh g & not g in Big_Oh f )
now :: thesis: not f in Big_Oh g
assume f in Big_Oh g ; :: thesis: contradiction
then consider t being Element of Funcs (NAT,REAL) such that
A16: t = f and
A17: 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 * (g . n) & t . n >= 0 ) ) ) ;
consider c being Real, N being Element of NAT such that
c > 0 and
A18: for n being Element of NAT st n >= N holds
( t . n <= c * (g . n) & t . n >= 0 ) by A17;
ex n being Element of NAT st
( n >= N & t . n > c * (g . n) )
proof
per cases ( N mod 2 = 0 or N mod 2 = 1 ) by NAT_D:12;
suppose A19: N mod 2 = 0 ; :: thesis: ex n being Element of NAT st
( n >= N & t . n > c * (g . n) )
g . (N + 1) = ((N + 1) + 1) mod 2 by A2
.= (N + (1 + 1)) mod 2
.= (0 + (2 mod 2)) mod 2 by A19, EULER_2:6
.= (0 + 0) mod 2 by NAT_D:25
.= 0 by NAT_D:26 ;
then A20: c * (g . (N + 1)) = 0 ;
A21: N + 1 >= N by NAT_1:13;
t . (N + 1) = (N + 1) mod 2 by A1, A16
.= (0 + (1 mod 2)) mod 2 by A19, EULER_2:6
.= (0 + 1) mod 2 by NAT_D:14
.= 1 by NAT_D:14 ;
hence ex n being Element of NAT st
( n >= N & t . n > c * (g . n) ) by A21, A20; :: thesis: verum
end;
suppose A22: N mod 2 = 1 ; :: thesis: ex n being Element of NAT st
( n >= N & t . n > c * (g . n) )
g . N = (N + 1) mod 2 by A2
.= (1 + (1 mod 2)) mod 2 by A22, EULER_2:6
.= (1 + 1) mod 2 by NAT_D:14
.= 0 by NAT_D:25 ;
then A23: c * (g . N) = 0 ;
t . N = 1 by A1, A16, A22;
hence ex n being Element of NAT st
( n >= N & t . n > c * (g . n) ) by A23; :: thesis: verum
end;
end;
end;
hence contradiction by A18; :: thesis: verum
end;
hence ( f = f & g = g & not f in Big_Oh g & not g in Big_Oh f ) by A7; :: thesis: verum