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