let f, g be eventually-nonnegative Real_Sequence; :: thesis: (Big_Oh f) + (Big_Oh g) = Big_Oh (f + g)
now
let x be set ; :: 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 f', g' being Element of Funcs NAT ,REAL st
( f' in Big_Oh f & g' in Big_Oh g & ( for n being Element of NAT holds t . n = (f' . n) + (g' . n) ) ) ;
consider f', g' being Element of Funcs NAT ,REAL such that
A3: ( f' in Big_Oh f & g' in Big_Oh g ) and
A4: for n being Element of NAT holds t . n = (f' . n) + (g' . n) by A2;
consider r being Element of Funcs NAT ,REAL such that
A5: r = f' and
A6: 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 s being Element of Funcs NAT ,REAL such that
A7: s = g' and
A8: 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 A3;
consider c being Real, N1 being Element of NAT such that
A9: c > 0 and
A10: for n being Element of NAT st n >= N1 holds
( r . n <= c * (f . n) & r . n >= 0 ) by A6;
consider d being Real, N2 being Element of NAT such that
A11: d > 0 and
A12: for n being Element of NAT st n >= N2 holds
( s . n <= d * (g . n) & s . n >= 0 ) by A8;
set e = max c,d;
A13: ( max c,d >= c & max c,d >= d ) by XXREAL_0:25;
A14: max c,d > 0 by A9, XXREAL_0:25;
set N = max N1,N2;
A15: ( max N1,N2 >= N1 & max N1,N2 >= N2 ) by XXREAL_0:25;
now
let n be Element of NAT ; :: thesis: ( n >= max N1,N2 implies ( t . n <= (max c,d) * ((f + g) . n) & t . n >= 0 ) )
assume n >= max N1,N2 ; :: thesis: ( t . n <= (max c,d) * ((f + g) . n) & t . n >= 0 )
then A16: ( n >= N1 & n >= N2 ) by A15, XXREAL_0:2;
then ( r . n <= c * (f . n) & r . n >= 0 & s . n <= d * (g . n) & s . n >= 0 ) by A10, A12;
then ( (f . n) * c >= 0 * c & (g . n) * d >= 0 * d ) ;
then ( f . n >= 0 & g . n >= 0 ) by A9, A11, XREAL_1:70;
then ( r . n <= c * (f . n) & s . n <= d * (g . n) & c * (f . n) <= (max c,d) * (f . n) & d * (g . n) <= (max c,d) * (g . n) ) by A10, A12, A13, A16, XREAL_1:66;
then ( r . n <= (max c,d) * (f . n) & s . n <= (max c,d) * (g . n) ) by XXREAL_0:2;
then ( (r . n) + (s . n) <= ((max c,d) * (f . n)) + (s . n) & ((max c,d) * (f . n)) + (s . n) <= ((max c,d) * (f . n)) + ((max c,d) * (g . n)) ) by XREAL_1:8;
then (r . n) + (s . n) <= (max c,d) * ((f . n) + (g . n)) by XXREAL_0:2;
then (r . n) + (s . n) <= (max c,d) * ((f + g) . n) by SEQ_1:11;
hence t . n <= (max c,d) * ((f + g) . n) by A4, A5, A7; :: thesis: t . n >= 0
( f' . n >= 0 & g' . n >= 0 ) by A5, A7, A10, A12, A16;
then ( (f' . n) + (g' . n) >= 0 + (g' . n) & 0 + (g' . n) >= 0 ) by XREAL_1:8;
hence t . n >= 0 by A4; :: thesis: verum
end;
hence x in Big_Oh (f + g) by A1, A14; :: 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
A17: x = t and
A18: 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
A19: c > 0 and
A20: for n being Element of NAT st n >= N3 holds
( t . n <= c * ((f + g) . n) & t . n >= 0 ) by A18;
consider N1 being Element of NAT such that
A21: for n being Element of NAT st n >= N1 holds
f . n >= 0 by Def4;
consider N2 being Element of NAT such that
A22: for n being Element of NAT st n >= N2 holds
g . n >= 0 by Def4;
set N = max N3,(max N1,N2);
( max N3,(max N1,N2) >= N3 & max N3,(max N1,N2) >= max N1,N2 & max N1,N2 >= N1 & max N1,N2 >= N2 ) by XXREAL_0:25;
then A23: ( max N3,(max N1,N2) >= N3 & max N3,(max N1,N2) >= N1 & max N3,(max N1,N2) >= N2 ) by XXREAL_0:2;
defpred S1[ Element of NAT , Real] means ( ( t . $1 <= c * (f . $1) implies $2 = t . $1 ) & ( c * (f . $1) < t . $1 implies $2 = c * (f . $1) ) );
A24: 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 t . n <= c * (f . n) ; :: thesis: ex y being Element of REAL st S1[n,y]
hence ex y being Element of REAL st S1[n,y] ; :: thesis: verum
end;
suppose c * (f . n) < t . n ; :: thesis: ex y being Element of REAL st S1[n,y]
hence ex y being Element of REAL st S1[n,y] ; :: thesis: verum
end;
end;
end;
consider f' being Function of NAT ,REAL such that
A25: for x being Element of NAT holds S1[x,f' . x] from FUNCT_2:sch 3(A24);
defpred S2[ 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)) ) );
A26: 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 c * (f . n) < t . 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;
end;
end;
consider g' being Function of NAT ,REAL such that
A27: for x being Element of NAT holds S2[x,g' . x] from FUNCT_2:sch 3(A26);
A28: ( f' is Element of Funcs NAT ,REAL & g' is Element of Funcs NAT ,REAL ) by FUNCT_2:11;
now
let n be Element of NAT ; :: thesis: ( n >= max N3,(max N1,N2) implies ( f' . b1 <= c * (f . b1) & f' . b1 >= 0 ) )
assume n >= max N3,(max N1,N2) ; :: thesis: ( f' . b1 <= c * (f . b1) & f' . b1 >= 0 )
then ( n >= N3 & n >= N1 ) by A23, XXREAL_0:2;
then A29: ( t . n >= 0 & f . n >= 0 ) by A20, A21;
then A30: 0 * (f . n) <= c * (f . n) by A19;
per cases ( t . n <= c * (f . n) or t . n > c * (f . n) ) ;
suppose t . n <= c * (f . n) ; :: thesis: ( f' . b1 <= c * (f . b1) & f' . b1 >= 0 )
hence ( f' . n <= c * (f . n) & f' . n >= 0 ) by A25, A29; :: thesis: verum
end;
suppose t . n > c * (f . n) ; :: thesis: ( f' . b1 <= c * (f . b1) & f' . b1 >= 0 )
hence ( f' . n <= c * (f . n) & f' . n >= 0 ) by A25, A30; :: thesis: verum
end;
end;
end;
then A31: f' in Big_Oh f by A19, A28;
now
let n be Element of NAT ; :: thesis: ( n >= max N3,(max N1,N2) implies ( g' . b1 <= c * (g . b1) & g' . b1 >= 0 ) )
assume n >= max N3,(max N1,N2) ; :: thesis: ( g' . b1 <= c * (g . b1) & g' . b1 >= 0 )
then ( n >= N3 & n >= N2 ) by A23, XXREAL_0:2;
then A32: ( t . n >= 0 & g . n >= 0 & t . n <= c * ((f + g) . n) ) by A20, A22;
then A33: 0 * (g . n) <= c * (g . n) by A19;
per cases ( t . n <= c * (f . n) or t . n > c * (f . n) ) ;
suppose t . n <= c * (f . n) ; :: thesis: ( g' . b1 <= c * (g . b1) & g' . b1 >= 0 )
hence ( g' . n <= c * (g . n) & g' . n >= 0 ) by A27, A33; :: thesis: verum
end;
suppose t . n > c * (f . n) ; :: thesis: ( g' . b1 <= c * (g . b1) & g' . b1 >= 0 )
then t . n > 0 + (c * (f . n)) ;
then A34: (t . n) - (c * (f . n)) >= 0 by XREAL_1:21;
t . n <= c * ((f . n) + (g . n)) by A32, SEQ_1:11;
then t . n <= (c * (f . n)) + (c * (g . n)) ;
then (t . n) - (c * (f . n)) <= c * (g . n) by XREAL_1:22;
hence ( g' . n <= c * (g . n) & g' . n >= 0 ) by A27, A34; :: thesis: verum
end;
end;
end;
then A35: g' in Big_Oh g by A19, A28;
now
let n be Element of NAT ; :: thesis: t . b1 = (f' . b1) + (g' . b1)
per cases ( t . n <= c * (f . n) or c * (f . n) < t . n ) ;
suppose t . n <= c * (f . n) ; :: thesis: t . b1 = (f' . b1) + (g' . b1)
then ( f' . n = t . n & g' . n = 0 ) by A25, A27;
hence t . n = (f' . n) + (g' . n) ; :: thesis: verum
end;
suppose c * (f . n) < t . n ; :: thesis: (f' . b1) + (g' . b1) = t . b1
then ( f' . n = c * (f . n) & g' . n = (t . n) - (c * (f . n)) ) by A25, A27;
hence (f' . n) + (g' . n) = t . n ; :: thesis: verum
end;
end;
end;
hence x in (Big_Oh f) + (Big_Oh g) by A17, A28, A31, A35; :: thesis: verum
end;
hence (Big_Oh f) + (Big_Oh g) = Big_Oh (f + g) by TARSKI:2; :: thesis: verum