let f, g be eventually-nonnegative Real_Sequence; :: thesis: Big_Omega (f + g) = Big_Omega (max (f,g))
consider N1 being Nat such that
A1: for n being Nat st n >= N1 holds
f . n >= 0 by Def2;
consider N2 being Nat such that
A2: for n being Nat st n >= N2 holds
g . n >= 0 by Def2;
now :: thesis: for x being object holds
( ( x in Big_Omega (f + g) implies x in Big_Omega (max (f,g)) ) & ( x in Big_Omega (max (f,g)) implies x in Big_Omega (f + g) ) )
let x be object ; :: thesis: ( ( x in Big_Omega (f + g) implies x in Big_Omega (max (f,g)) ) & ( x in Big_Omega (max (f,g)) implies x in Big_Omega (f + g) ) )
hereby :: thesis: ( x in Big_Omega (max (f,g)) implies x in Big_Omega (f + g) )
assume x in Big_Omega (f + g) ; :: thesis: x in Big_Omega (max (f,g))
then consider t being Element of Funcs (NAT,REAL) such that
A3: t = x 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
( d * ((f + g) . n) <= t . n & t . n >= 0 ) ) ) ;
consider d being Real, N being Element of NAT such that
A5: d > 0 and
A6: for n being Element of NAT st n >= N holds
( d * ((f + g) . n) <= t . n & t . n >= 0 ) by A4;
reconsider a = max (N,(max (N1,N2))) as Element of NAT by ORDINAL1:def 12;
A7: a >= N by XXREAL_0:25;
A8: a >= max (N1,N2) by XXREAL_0:25;
max (N1,N2) >= N2 by XXREAL_0:25;
then A9: a >= N2 by A8, XXREAL_0:2;
max (N1,N2) >= N1 by XXREAL_0:25;
then A10: a >= N1 by A8, XXREAL_0:2;
now :: thesis: for n being Element of NAT st n >= a holds
( d * ((max (f,g)) . n) <= t . n & t . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= a implies ( d * ((max (f,g)) . n) <= t . n & t . n >= 0 ) )
assume A11: n >= a ; :: thesis: ( d * ((max (f,g)) . n) <= t . n & t . n >= 0 )
then n >= N1 by A10, XXREAL_0:2;
then A12: f . n >= 0 by A1;
n >= N2 by A9, A11, XXREAL_0:2;
then A13: g . n >= 0 by A2;
A14: (max (f,g)) . n = max ((f . n),(g . n)) by Def7;
(max (f,g)) . n <= (f + g) . n
proof
per cases ( (max (f,g)) . n = f . n or (max (f,g)) . n = g . n ) by A14, XXREAL_0:16;
suppose (max (f,g)) . n = f . n ; :: thesis: (max (f,g)) . n <= (f + g) . n
then ((max (f,g)) . n) + 0 <= (f . n) + (g . n) by A13, XREAL_1:7;
hence (max (f,g)) . n <= (f + g) . n by SEQ_1:7; :: thesis: verum
end;
suppose (max (f,g)) . n = g . n ; :: thesis: (max (f,g)) . n <= (f + g) . n
then ((max (f,g)) . n) + 0 <= (g . n) + (f . n) by A12, XREAL_1:7;
hence (max (f,g)) . n <= (f + g) . n by SEQ_1:7; :: thesis: verum
end;
end;
end;
then A15: d * ((max (f,g)) . n) <= d * ((f + g) . n) by A5, XREAL_1:64;
A16: n >= N by A7, A11, XXREAL_0:2;
then d * ((f + g) . n) <= t . n by A6;
hence d * ((max (f,g)) . n) <= t . n by A15, XXREAL_0:2; :: thesis: t . n >= 0
thus t . n >= 0 by A6, A16; :: thesis: verum
end;
hence x in Big_Omega (max (f,g)) by A3, A5; :: thesis: verum
end;
assume x in Big_Omega (max (f,g)) ; :: thesis: x in Big_Omega (f + g)
then consider t being Element of Funcs (NAT,REAL) such that
A17: t = x and
A18: ex d being Real ex N being Element of NAT st
( d > 0 & ( for n being Element of NAT st n >= N holds
( d * ((max (f,g)) . n) <= t . n & t . n >= 0 ) ) ) ;
consider d being Real, N being Element of NAT such that
A19: d > 0 and
A20: for n being Element of NAT st n >= N holds
( d * ((max (f,g)) . n) <= t . n & t . n >= 0 ) by A18;
reconsider a = max (N,(max (N1,N2))) as Element of NAT by ORDINAL1:def 12;
A21: N <= a by XXREAL_0:25;
A22: now :: thesis: for n being Element of NAT st n >= a holds
( (d * (2 ")) * ((f + g) . n) <= t . n & t . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= a implies ( (d * (2 ")) * ((f + g) . n) <= t . n & t . n >= 0 ) )
( f . n <= max ((f . n),(g . n)) & g . n <= max ((f . n),(g . n)) ) by XXREAL_0:25;
then (f . n) + (g . n) <= (1 * (max ((f . n),(g . n)))) + (1 * (max ((f . n),(g . n)))) by XREAL_1:7;
then (2 ") * ((f . n) + (g . n)) <= (2 ") * (2 * (max ((f . n),(g . n)))) by XREAL_1:64;
then (2 ") * ((f + g) . n) <= max ((f . n),(g . n)) by SEQ_1:7;
then d * ((2 ") * ((f + g) . n)) <= d * (max ((f . n),(g . n))) by A19, XREAL_1:64;
then A23: d * ((2 ") * ((f + g) . n)) <= d * ((max (f,g)) . n) by Def7;
assume n >= a ; :: thesis: ( (d * (2 ")) * ((f + g) . n) <= t . n & t . n >= 0 )
then A24: n >= N by A21, XXREAL_0:2;
then d * ((max (f,g)) . n) <= t . n by A20;
hence (d * (2 ")) * ((f + g) . n) <= t . n by A23, XXREAL_0:2; :: thesis: t . n >= 0
thus t . n >= 0 by A20, A24; :: thesis: verum
end;
d * (2 ") > d * 0 by A19, XREAL_1:68;
hence x in Big_Omega (f + g) by A17, A22; :: thesis: verum
end;
hence Big_Omega (f + g) = Big_Omega (max (f,g)) by TARSKI:2; :: thesis: verum