let c be non negative Real; :: thesis: for x, f being eventually-nonnegative Real_Sequence st ex e being Real ex N being Element of NAT st
( e > 0 & ( for n being Element of NAT st n >= N holds
f . n >= e ) ) & x in Big_Oh (c + f) holds
x in Big_Oh f
let x, f be eventually-nonnegative Real_Sequence; :: thesis: ( ex e being Real ex N being Element of NAT st
( e > 0 & ( for n being Element of NAT st n >= N holds
f . n >= e ) ) & x in Big_Oh (c + f) implies x in Big_Oh f )
given e being Real, N0 being Element of NAT such that A1: e > 0 and
A2: for n being Element of NAT st n >= N0 holds
f . n >= e ; :: thesis: ( not x in Big_Oh (c + f) or x in Big_Oh f )
assume x in Big_Oh (c + f) ; :: thesis: x in Big_Oh f
then consider t being Element of Funcs (NAT,REAL) such that
A3: x = 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 * ((c + f) . n) & t . n >= 0 ) ) ) ;
consider d being Real, N1 being Element of NAT such that
A5: d > 0 and
A6: for n being Element of NAT st n >= N1 holds
( t . n <= d * ((c + f) . n) & t . n >= 0 ) by A4;
set b = max ((2 * d),(((2 * d) * c) / e));
2 * d > 2 * 0 by A5, XREAL_1:68;
then A7: max ((2 * d),(((2 * d) * c) / e)) > 0 by XXREAL_0:25;
set N = max (N0,N1);
A8: max (N0,N1) >= N1 by XXREAL_0:25;
A9: max (N0,N1) >= N0 by XXREAL_0:25;
now :: thesis: for n being Element of NAT st n >= max (N0,N1) holds
( t . n <= (max ((2 * d),(((2 * d) * c) / e))) * (f . n) & t . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= max (N0,N1) implies ( t . n <= (max ((2 * d),(((2 * d) * c) / e))) * (f . n) & t . n >= 0 ) )
assume A10: n >= max (N0,N1) ; :: thesis: ( t . n <= (max ((2 * d),(((2 * d) * c) / e))) * (f . n) & t . n >= 0 )
then A11: n >= N1 by A8, XXREAL_0:2;
then t . n <= d * ((c + f) . n) by A6;
then A12: t . n <= d * (c + (f . n)) by VALUED_1:2;
A13: n >= N0 by A9, A10, XXREAL_0:2;
thus t . n <= (max ((2 * d),(((2 * d) * c) / e))) * (f . n) :: thesis: t . n >= 0
proof
per cases ( c >= f . n or c < f . n ) ;
suppose c >= f . n ; :: thesis: t . n <= (max ((2 * d),(((2 * d) * c) / e))) * (f . n)
then d * c >= d * (f . n) by A5, XREAL_1:64;
then (d * c) + (d * c) >= (d * c) + (d * (f . n)) by XREAL_1:6;
then t . n <= (2 * (d * c)) * 1 by A12, XXREAL_0:2;
then A14: t . n <= (2 * (d * c)) * ((1 / e) * e) by A1, XCMPLX_1:106;
(max ((2 * d),(((2 * d) * c) / e))) * e >= (((2 * d) * c) / e) * e by A1, XREAL_1:64, XXREAL_0:25;
then A15: t . n <= (max ((2 * d),(((2 * d) * c) / e))) * e by A14, XXREAL_0:2;
(max ((2 * d),(((2 * d) * c) / e))) * (f . n) >= (max ((2 * d),(((2 * d) * c) / e))) * e by A2, A7, A13, XREAL_1:64;
hence t . n <= (max ((2 * d),(((2 * d) * c) / e))) * (f . n) by A15, XXREAL_0:2; :: thesis: verum
end;
suppose c < f . n ; :: thesis: t . n <= (max ((2 * d),(((2 * d) * c) / e))) * (f . n)
then d * c < d * (f . n) by A5, XREAL_1:68;
then (d * c) + (d * (f . n)) < (d * (f . n)) + (d * (f . n)) by XREAL_1:6;
then A16: t . n < 2 * (d * (f . n)) by A12, XXREAL_0:2;
f . n > 0 by A1, A2, A13;
then (max ((2 * d),(((2 * d) * c) / e))) * (f . n) >= (2 * d) * (f . n) by XREAL_1:64, XXREAL_0:25;
hence t . n <= (max ((2 * d),(((2 * d) * c) / e))) * (f . n) by A16, XXREAL_0:2; :: thesis: verum
end;
end;
end;
thus t . n >= 0 by A6, A11; :: thesis: verum
end;
hence x in Big_Oh f by A3, A7; :: thesis: verum