let f, g be eventually-nonnegative Real_Sequence; ( f in Big_Oh g implies Big_Oh f c= Big_Oh g )
assume
f in Big_Oh g
; Big_Oh f c= Big_Oh g
then consider t being Element of Funcs (NAT,REAL) such that
A1:
t = f
and
A2:
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 ct being Real, Nt being Element of NAT such that
ct > 0
and
A3:
for n being Element of NAT st n >= Nt holds
( t . n <= ct * (g . n) & t . n >= 0 )
by A2;
consider Ng being Nat such that
A4:
for n being Nat st n >= Ng holds
g . n >= 0
by Def2;
let x be object ; TARSKI:def 3 ( not x in Big_Oh f or x in Big_Oh g )
assume
x in Big_Oh f
; x in Big_Oh g
then consider s being Element of Funcs (NAT,REAL) such that
A5:
s = x
and
A6:
ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( s . n <= c * (f . n) & s . n >= 0 ) ) )
;
consider cs being Real, Ns being Element of NAT such that
A7:
cs > 0
and
A8:
for n being Element of NAT st n >= Ns holds
( s . n <= cs * (f . n) & s . n >= 0 )
by A6;
now ex c being object st
( c > 0 & ex N being Element of NAT st
for n being Element of NAT st n >= N holds
( s . n <= c * (g . n) & s . n >= 0 ) )take c =
max (
(cs * ct),
(max (cs,ct)));
( c > 0 & ex N being Element of NAT st
for n being Element of NAT st n >= N holds
( s . n <= c * (g . n) & s . n >= 0 ) )
c >= max (
cs,
ct)
by XXREAL_0:25;
hence
c > 0
by A7, XXREAL_0:25;
ex N being Element of NAT st
for n being Element of NAT st n >= N holds
( s . n <= c * (g . n) & s . n >= 0 )reconsider N =
max (
(max (Ns,Nt)),
Ng) as
Element of
NAT by ORDINAL1:def 12;
take N =
N;
for n being Element of NAT st n >= N holds
( s . n <= c * (g . n) & s . n >= 0 )let n be
Element of
NAT ;
( n >= N implies ( s . n <= c * (g . n) & s . n >= 0 ) )assume A9:
n >= N
;
( s . n <= c * (g . n) & s . n >= 0 )A10:
N >= max (
Ns,
Nt)
by XXREAL_0:25;
max (
Ns,
Nt)
>= Nt
by XXREAL_0:25;
then
N >= Nt
by A10, XXREAL_0:2;
then
n >= Nt
by A9, XXREAL_0:2;
then
t . n <= ct * (g . n)
by A3;
then A11:
cs * (t . n) <= cs * (ct * (g . n))
by A7, XREAL_1:64;
N >= Ng
by XXREAL_0:25;
then
n >= Ng
by A9, XXREAL_0:2;
then
g . n >= 0
by A4;
then
(cs * ct) * (g . n) <= c * (g . n)
by XREAL_1:64, XXREAL_0:25;
then A12:
cs * (t . n) <= c * (g . n)
by A11, XXREAL_0:2;
max (
Ns,
Nt)
>= Ns
by XXREAL_0:25;
then
N >= Ns
by A10, XXREAL_0:2;
then A13:
n >= Ns
by A9, XXREAL_0:2;
then
s . n <= cs * (f . n)
by A8;
hence
s . n <= c * (g . n)
by A1, A12, XXREAL_0:2;
s . n >= 0 thus
s . n >= 0
by A8, A13;
verum end;
hence
x in Big_Oh g
by A5; verum