let f, g be eventually-nonnegative Real_Sequence; :: thesis: Big_Oh (f + g) = Big_Oh (max (f,g))

now :: thesis: for x being object holds
( ( x in Big_Oh (f + g) implies x in Big_Oh (max (f,g)) ) & ( x in Big_Oh (max (f,g)) implies x in Big_Oh (f + g) ) )

let x be object ; :: thesis: ( ( x in Big_Oh (f + g) implies x in Big_Oh (max (f,g)) ) & ( x in Big_Oh (max (f,g)) implies x in Big_Oh (f + g) ) )

hereby :: thesis: ( x in Big_Oh (max (f,g)) implies x in Big_Oh (f + g) )

assume x in Big_Oh (f + g) ; :: thesis: x in Big_Oh (max (f,g))
then consider t being Element of Funcs (NAT,REAL) such that
A1: t = x 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 * ((f + g) . n) & t . n >= 0 ) ) ) ;
consider c being Real, N being Element of NAT such that
A3: c > 0 and
A4: for n being Element of NAT st n >= N holds
( t . n <= c * ((f + g) . n) & t . n >= 0 ) by A2;

A5: now :: thesis: for n being Element of NAT st n >= N holds
( t . n <= (2 * c) * ((max (f,g)) . n) & t . n >= 0 )

let n be Element of NAT ; :: thesis: ( n >= N implies ( t . n <= (2 * c) * ((max (f,g)) . n) & t . n >= 0 ) )
A6: ( f . n <= max ((f . n),(g . n)) & g . n <= max ((f . n),(g . n)) ) by XXREAL_0:25;
A7: (1 * ((max (f,g)) . n)) + (1 * ((max (f,g)) . n)) = (1 + 1) * ((max (f,g)) . n) ;
( (f + g) . n = (f . n) + (g . n) & (max (f,g)) . n = max ((f . n),(g . n)) ) by Def7, SEQ_1:7;
then (f + g) . n <= 2 * ((max (f,g)) . n) by A6, A7, XREAL_1:7;
then A8: c * ((f + g) . n) <= c * (2 * ((max (f,g)) . n)) by A3, XREAL_1:64;
assume A9: n >= N ; :: thesis: ( t . n <= (2 * c) * ((max (f,g)) . n) & t . n >= 0 )
then t . n <= c * ((f + g) . n) by A4;
hence t . n <= (2 * c) * ((max (f,g)) . n) by A8, XXREAL_0:2; :: thesis: t . n >= 0
thus t . n >= 0 by A4, A9; :: thesis: verum

end;

2 * c > 2 * 0 by A3, XREAL_1:68;
hence x in Big_Oh (max (f,g)) by A1, A5; :: thesis: verum

end;

assume x in Big_Oh (max (f,g)) ; :: thesis: x in Big_Oh (f + g)
then consider t being Element of Funcs (NAT,REAL) such that
A10: t = x 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 * ((max (f,g)) . n) & t . n >= 0 ) ) ) ;
consider c being Real, N1 being Element of NAT such that
A12: c > 0 and
A13: for n being Element of NAT st n >= N1 holds
( t . n <= c * ((max (f,g)) . n) & t . n >= 0 ) by A11;
consider M1 being Nat such that
A14: for n being Nat st n >= M1 holds
f . n >= 0 by Def2;
consider M2 being Nat such that
A15: for n being Nat st n >= M2 holds
g . n >= 0 by Def2;
set N = max (N1,(max (M1,M2)));
A16: max (M1,M2) <= max (N1,(max (M1,M2))) by XXREAL_0:25;
M2 <= max (M1,M2) by XXREAL_0:25;
then A17: M2 <= max (N1,(max (M1,M2))) by A16, XXREAL_0:2;
A18: N1 <= max (N1,(max (M1,M2))) by XXREAL_0:25;
M1 <= max (M1,M2) by XXREAL_0:25;
then A19: M1 <= max (N1,(max (M1,M2))) by A16, XXREAL_0:2;
reconsider N = max (N1,(max (M1,M2))) as Element of NAT by ORDINAL1:def 12;
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 + g) . n) & t . n >= 0 ) ) )

proof

take c ; :: thesis: ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * ((f + g) . n) & t . n >= 0 ) ) )
take N ; :: thesis: ( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * ((f + g) . n) & t . n >= 0 ) ) )
thus c > 0 by A12; :: thesis: for n being Element of NAT st n >= N holds
( t . n <= c * ((f + g) . n) & t . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= N implies ( t . n <= c * ((f + g) . n) & t . n >= 0 ) )
A20: ( max ((f . n),(g . n)) = f . n or max ((f . n),(g . n)) = g . n ) by XXREAL_0:16;
assume A21: n >= N ; :: thesis: ( t . n <= c * ((f + g) . n) & t . n >= 0 )
then n >= M1 by A19, XXREAL_0:2;
then f . n >= 0 by A14;
then A22: (f . n) + (g . n) >= 0 + (g . n) by XREAL_1:7;
n >= M2 by A17, A21, XXREAL_0:2;
then g . n >= 0 by A15;
then A23: (f . n) + (g . n) >= (f . n) + 0 by XREAL_1:7;
( (max (f,g)) . n = max ((f . n),(g . n)) & (f + g) . n = (f . n) + (g . n) ) by Def7, SEQ_1:7;
then A24: c * ((max (f,g)) . n) <= c * ((f + g) . n) by A12, A23, A22, A20, XREAL_1:64;
A25: n >= N1 by A18, A21, XXREAL_0:2;
then t . n <= c * ((max (f,g)) . n) by A13;
hence t . n <= c * ((f + g) . n) by A24, XXREAL_0:2; :: thesis: t . n >= 0
thus t . n >= 0 by A13, A25; :: thesis: verum

end;

hence x in Big_Oh (f + g) by A10; :: thesis: verum

end;

hence Big_Oh (f + g) = Big_Oh (max (f,g)) by TARSKI:2; :: thesis: verum