let f, g be eventually-nonnegative Real_Sequence; :: thesis: (Big_Oh f) + (Big_Oh g) = Big_Oh (f + g)
now :: thesis: for x being object holds
( ( x in (Big_Oh f) + (Big_Oh g) implies x in Big_Oh (f + g) ) & ( x in Big_Oh (f + g) implies x in (Big_Oh f) + (Big_Oh g) ) )
let x be object ; :: thesis: ( ( x in (Big_Oh f) + (Big_Oh g) implies x in Big_Oh (f + g) ) & ( x in Big_Oh (f + g) implies x in (Big_Oh f) + (Big_Oh g) ) )
hereby :: thesis: ( x in Big_Oh (f + g) implies x in (Big_Oh f) + (Big_Oh g) )
assume x in (Big_Oh f) + (Big_Oh g) ; :: thesis: x in Big_Oh (f + g)
then consider t being Element of Funcs (NAT,REAL) such that
A1: x = t and
A2: ex f9, g9 being Element of Funcs (NAT,REAL) st
( f9 in Big_Oh f & g9 in Big_Oh g & ( for n being Element of NAT holds t . n = (f9 . n) + (g9 . n) ) ) ;
consider f9, g9 being Element of Funcs (NAT,REAL) such that
A3: f9 in Big_Oh f and
A4: g9 in Big_Oh g and
A5: for n being Element of NAT holds t . n = (f9 . n) + (g9 . n) by A2;
consider r being Element of Funcs (NAT,REAL) such that
A6: r = f9 and
A7: ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( r . n <= c * (f . n) & r . n >= 0 ) ) ) by A3;
consider c being Real, N1 being Element of NAT such that
A8: c > 0 and
A9: for n being Element of NAT st n >= N1 holds
( r . n <= c * (f . n) & r . n >= 0 ) by A7;
consider s being Element of Funcs (NAT,REAL) such that
A10: s = g9 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
( s . n <= c * (g . n) & s . n >= 0 ) ) ) by A4;
consider d being Real, N2 being Element of NAT such that
A12: d > 0 and
A13: for n being Element of NAT st n >= N2 holds
( s . n <= d * (g . n) & s . n >= 0 ) by A11;
set N = max (N1,N2);
set e = max (c,d);
A14: max (N1,N2) >= N2 by XXREAL_0:25;
A15: max (N1,N2) >= N1 by XXREAL_0:25;
A16: now :: thesis: for n being Element of NAT st n >= max (N1,N2) holds
( t . n <= (max (c,d)) * ((f + g) . n) & t . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= max (N1,N2) implies ( t . n <= (max (c,d)) * ((f + g) . n) & t . n >= 0 ) )
assume A17: n >= max (N1,N2) ; :: thesis: ( t . n <= (max (c,d)) * ((f + g) . n) & t . n >= 0 )
then A18: n >= N1 by A15, XXREAL_0:2;
then f9 . n >= 0 by A6, A9;
then A19: (f9 . n) + (g9 . n) >= 0 + (g9 . n) by XREAL_1:6;
r . n <= c * (f . n) by A9, A18;
then (f . n) * c >= 0 * c by A9, A18;
then f . n >= 0 by A8, XREAL_1:68;
then A20: c * (f . n) <= (max (c,d)) * (f . n) by XREAL_1:64, XXREAL_0:25;
r . n <= c * (f . n) by A9, A18;
then r . n <= (max (c,d)) * (f . n) by A20, XXREAL_0:2;
then A21: (r . n) + (s . n) <= ((max (c,d)) * (f . n)) + (s . n) by XREAL_1:6;
A22: n >= N2 by A14, A17, XXREAL_0:2;
then s . n <= d * (g . n) by A13;
then (g . n) * d >= 0 * d by A13, A22;
then g . n >= 0 by A12, XREAL_1:68;
then A23: d * (g . n) <= (max (c,d)) * (g . n) by XREAL_1:64, XXREAL_0:25;
s . n <= d * (g . n) by A13, A22;
then s . n <= (max (c,d)) * (g . n) by A23, XXREAL_0:2;
then ((max (c,d)) * (f . n)) + (s . n) <= ((max (c,d)) * (f . n)) + ((max (c,d)) * (g . n)) by XREAL_1:6;
then (r . n) + (s . n) <= (max (c,d)) * ((f . n) + (g . n)) by A21, XXREAL_0:2;
then (r . n) + (s . n) <= (max (c,d)) * ((f + g) . n) by SEQ_1:7;
hence t . n <= (max (c,d)) * ((f + g) . n) by A5, A6, A10; :: thesis: t . n >= 0
0 + (g9 . n) >= 0 by A10, A13, A22;
hence t . n >= 0 by A5, A19; :: thesis: verum
end;
max (c,d) > 0 by A8, XXREAL_0:25;
hence x in Big_Oh (f + g) by A1, A16; :: thesis: verum
end;
assume x in Big_Oh (f + g) ; :: thesis: x in (Big_Oh f) + (Big_Oh g)
then consider t being Element of Funcs (NAT,REAL) such that
A24: x = t and
A25: 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, N3 being Element of NAT such that
A26: c > 0 and
A27: for n being Element of NAT st n >= N3 holds
( t . n <= c * ((f + g) . n) & t . n >= 0 ) by A25;
consider N1 being Nat such that
A28: for n being Nat st n >= N1 holds
f . n >= 0 by Def2;
consider N2 being Nat such that
A29: for n being Nat st n >= N2 holds
g . n >= 0 by Def2;
reconsider N = max (N3,(max (N1,N2))) as Element of NAT by ORDINAL1:def 12;
A30: N >= max (N1,N2) by XXREAL_0:25;
defpred S1[ Element of NAT , Real] means ( ( t . $1 <= c * (f . $1) implies $2 = 0 ) & ( c * (f . $1) < t . $1 implies $2 = (t . $1) - (c * (f . $1)) ) );
A31: for x being Element of NAT ex y being Element of REAL st S1[x,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of REAL st S1[n,y]
per cases ( t . n <= c * (f . n) or c * (f . n) < t . n ) ;
suppose A32: t . n <= c * (f . n) ; :: thesis: ex y being Element of REAL st S1[n,y]
0 in REAL by XREAL_0:def 1;
hence ex y being Element of REAL st S1[n,y] by A32; :: thesis: verum
end;
suppose A33: c * (f . n) < t . n ; :: thesis: ex y being Element of REAL st S1[n,y]
reconsider y = (t . n) - (c * (f . n)) as Element of REAL by XREAL_0:def 1;
take y ; :: thesis: S1[n,y]
thus S1[n,y] by A33; :: thesis: verum
end;
end;
end;
consider g9 being sequence of REAL such that
A34: for x being Element of NAT holds S1[x,g9 . x] from FUNCT_2:sch 3(A31);
A35: N >= N3 by XXREAL_0:25;
A36: g9 is Element of Funcs (NAT,REAL) by FUNCT_2:8;
max (N1,N2) >= N2 by XXREAL_0:25;
then A37: N >= N2 by A30, XXREAL_0:2;
now :: thesis: for n being Element of NAT st n >= N holds
( g9 . n <= c * (g . n) & g9 . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= N implies ( g9 . b1 <= c * (g . b1) & g9 . b1 >= 0 ) )
assume A38: n >= N ; :: thesis: ( g9 . b1 <= c * (g . b1) & g9 . b1 >= 0 )
then n >= N3 by A35, XXREAL_0:2;
then A39: t . n <= c * ((f + g) . n) by A27;
n >= N2 by A37, A38, XXREAL_0:2;
then g . n >= 0 by A29;
then A40: 0 * (g . n) <= c * (g . n) by A26;
per cases ( t . n <= c * (f . n) or t . n > c * (f . n) ) ;
suppose t . n <= c * (f . n) ; :: thesis: ( g9 . b1 <= c * (g . b1) & g9 . b1 >= 0 )
hence ( g9 . n <= c * (g . n) & g9 . n >= 0 ) by A34, A40; :: thesis: verum
end;
suppose A41: t . n > c * (f . n) ; :: thesis: ( g9 . b1 <= c * (g . b1) & g9 . b1 >= 0 )
t . n <= c * ((f . n) + (g . n)) by A39, SEQ_1:7;
then t . n <= (c * (f . n)) + (c * (g . n)) ;
then A42: (t . n) - (c * (f . n)) <= c * (g . n) by XREAL_1:20;
t . n > 0 + (c * (f . n)) by A41;
then (t . n) - (c * (f . n)) >= 0 by XREAL_1:19;
hence ( g9 . n <= c * (g . n) & g9 . n >= 0 ) by A34, A42; :: thesis: verum
end;
end;
end;
then A43: g9 in Big_Oh g by A26, A36;
defpred S2[ Element of NAT , Real] means ( ( t . $1 <= c * (f . $1) implies $2 = t . $1 ) & ( c * (f . $1) < t . $1 implies $2 = c * (f . $1) ) );
A44: for x being Element of NAT ex y being Element of REAL st S2[x,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of REAL st S2[n,y]
per cases ( t . n <= c * (f . n) or c * (f . n) < t . n ) ;
suppose t . n <= c * (f . n) ; :: thesis: ex y being Element of REAL st S2[n,y]
hence ex y being Element of REAL st S2[n,y] ; :: thesis: verum
end;
suppose A45: c * (f . n) < t . n ; :: thesis: ex y being Element of REAL st S2[n,y]
reconsider y = c * (f . n) as Element of REAL by XREAL_0:def 1;
take y ; :: thesis: S2[n,y]
thus S2[n,y] by A45; :: thesis: verum
end;
end;
end;
consider f9 being sequence of REAL such that
A46: for x being Element of NAT holds S2[x,f9 . x] from FUNCT_2:sch 3(A44);
A47: now :: thesis: for n being Element of NAT holds t . n = (f9 . n) + (g9 . n)
let n be Element of NAT ; :: thesis: t . b1 = (f9 . b1) + (g9 . b1)
per cases ( t . n <= c * (f . n) or c * (f . n) < t . n ) ;
suppose A48: t . n <= c * (f . n) ; :: thesis: t . b1 = (f9 . b1) + (g9 . b1)
then g9 . n = 0 by A34;
hence t . n = (f9 . n) + (g9 . n) by A46, A48; :: thesis: verum
end;
suppose c * (f . n) < t . n ; :: thesis: (f9 . b1) + (g9 . b1) = t . b1
then ( f9 . n = c * (f . n) & g9 . n = (t . n) - (c * (f . n)) ) by A46, A34;
hence (f9 . n) + (g9 . n) = t . n ; :: thesis: verum
end;
end;
end;
A49: f9 is Element of Funcs (NAT,REAL) by FUNCT_2:8;
max (N1,N2) >= N1 by XXREAL_0:25;
then A50: N >= N1 by A30, XXREAL_0:2;
now :: thesis: for n being Element of NAT st n >= N holds
( f9 . n <= c * (f . n) & f9 . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= N implies ( f9 . b1 <= c * (f . b1) & f9 . b1 >= 0 ) )
assume A51: n >= N ; :: thesis: ( f9 . b1 <= c * (f . b1) & f9 . b1 >= 0 )
then n >= N3 by A35, XXREAL_0:2;
then A52: t . n >= 0 by A27;
n >= N1 by A50, A51, XXREAL_0:2;
then A53: f . n >= 0 by A28;
per cases ( t . n <= c * (f . n) or t . n > c * (f . n) ) ;
suppose t . n <= c * (f . n) ; :: thesis: ( f9 . b1 <= c * (f . b1) & f9 . b1 >= 0 )
hence ( f9 . n <= c * (f . n) & f9 . n >= 0 ) by A46, A52; :: thesis: verum
end;
suppose t . n > c * (f . n) ; :: thesis: ( f9 . b1 <= c * (f . b1) & f9 . b1 >= 0 )
hence ( f9 . n <= c * (f . n) & f9 . n >= 0 ) by A26, A46, A53; :: thesis: verum
end;
end;
end;
then f9 in Big_Oh f by A26, A49;
hence x in (Big_Oh f) + (Big_Oh g) by A24, A49, A36, A43, A47; :: thesis: verum
end;
hence (Big_Oh f) + (Big_Oh g) = Big_Oh (f + g) by TARSKI:2; :: thesis: verum