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

now

let x be set ; :: 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

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 Def10, SEQ_1:11;
then (f + g) . n <= 2 * ((max f,g) . n) by A6, A7, XREAL_1:9;
then A8: c * ((f + g) . n) <= c * (2 * ((max f,g) . n)) by A3, XREAL_1:66;
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:70;
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 Element of NAT such that
A14: for n being Element of NAT st n >= M1 holds
f . n >= 0 by Def4;
consider M2 being Element of NAT such that
A15: for n being Element of NAT st n >= M2 holds
g . n >= 0 by Def4;
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;

now

let n be Element of NAT ; :: thesis: ( n >= max N1,(max M1,M2) 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 >= max N1,(max M1,M2) ; :: 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:9;
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:9;
( (max f,g) . n = max (f . n),(g . n) & (f + g) . n = (f . n) + (g . n) ) by Def10, SEQ_1:11;
then A24: c * ((max f,g) . n) <= c * ((f + g) . n) by A12, A23, A22, A20, XREAL_1:66;
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, A12; :: thesis: verum

end;

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