let f, g be eventually-nonnegative Real_Sequence; :: thesis: max (Big_Oh f),(Big_Oh g) = Big_Oh (max f,g)
now
let x be set ; :: 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 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 = max (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 = max (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) * ((max f,g) . n) & t . n >= 0 ) )
assume n >= max N1,N2 ; :: thesis: ( t . n <= (max c,d) * ((max 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 A17: ( r . n <= (max c,d) * (f . n) & s . n <= (max c,d) * (g . n) ) by XXREAL_0:2;
( (max c,d) * (f . n) <= (max c,d) * (max (f . n),(g . n)) & (max c,d) * (g . n) <= (max c,d) * (max (f . n),(g . n)) ) by A14, XREAL_1:66, XXREAL_0:25;
then ( r . n <= (max c,d) * (max (f . n),(g . n)) & s . n <= (max c,d) * (max (f . n),(g . n)) ) by A17, XXREAL_0:2;
then max (r . n),(s . n) <= (max c,d) * (max (f . n),(g . n)) by XXREAL_0:28;
then max (r . n),(s . n) <= (max c,d) * ((max f,g) . n) by Def10;
hence t . n <= (max c,d) * ((max f,g) . n) by A4, A5, A7; :: thesis: t . n >= 0
( max (f' . n),(g' . n) >= f' . n & f' . n >= 0 ) by A5, A10, A16, XXREAL_0:25;
hence t . n >= 0 by A4; :: 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
A18: x = t and
A19: 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
A20: c > 0 and
A21: for n being Element of NAT st n >= N3 holds
( t . n <= c * ((max f,g) . n) & t . n >= 0 ) by A19;
consider N1 being Element of NAT such that
A22: for n being Element of NAT st n >= N1 holds
f . n >= 0 by Def4;
consider N2 being Element of NAT such that
A23: for n being Element of NAT st n >= N2 holds
g . n >= 0 by Def4;
set N = max N3,(max N1,N2);
A24: ( 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 A25: ( 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 ( ( ( f . $1 >= g . $1 or $1 < max N3,(max N1,N2) ) implies $2 = t . $1 ) & ( f . $1 < g . $1 & $1 >= max N3,(max N1,N2) implies $2 = 0 ) );
A26: 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 A27: 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 < max N3,(max N1,N2) or n >= max N3,(max N1,N2) ) ;
suppose n < max N3,(max N1,N2) ; :: 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 n >= max N3,(max N1,N2) ; :: thesis: ex y being Element of REAL st S1[n,y]
hence ex y being Element of REAL st S1[n,y] by A27; :: thesis: verum
end;
end;
end;
end;
end;
end;
consider f' being Function of NAT ,REAL such that
A28: for x being Element of NAT holds S1[x,f' . x] from FUNCT_2:sch 3(A26);
defpred S2[ Element of NAT , Real] means ( ( f . $1 >= g . $1 & $1 >= max N3,(max N1,N2) implies $2 = 0 ) & ( ( f . $1 < g . $1 or $1 < max N3,(max N1,N2) ) implies $2 = t . $1 ) );
A29: 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 A30: 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 < max N3,(max N1,N2) or n >= max N3,(max N1,N2) ) ;
suppose n < max N3,(max N1,N2) ; :: 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 n >= max N3,(max N1,N2) ; :: thesis: ex y being Element of REAL st S2[n,y]
hence ex y being Element of REAL st S2[n,y] by A30; :: 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 g' being Function of NAT ,REAL such that
A31: for x being Element of NAT holds S2[x,g' . x] from FUNCT_2:sch 3(A29);
A32: ( 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 A33: n >= max N3,(max N1,N2) ; :: thesis: ( f' . b1 <= c * (f . b1) & f' . b1 >= 0 )
then ( n >= N3 & n >= N1 ) by A25, XXREAL_0:2;
then A34: ( t . n >= 0 & f . n >= 0 & t . n <= c * ((max f,g) . n) ) by A21, A22;
then A35: 0 * (f . n) <= c * (f . n) by A20;
per cases ( f . n >= g . n or f . n < g . n ) ;
suppose A36: f . n >= g . n ; :: thesis: ( f' . b1 <= c * (f . b1) & f' . b1 >= 0 )
then max (f . n),(g . n) = f . n by XXREAL_0:def 10;
then (max f,g) . n = f . n by Def10;
hence ( f' . n <= c * (f . n) & f' . n >= 0 ) by A28, A34, A36; :: thesis: verum
end;
suppose f . n < g . n ; :: thesis: ( f' . b1 <= c * (f . b1) & f' . b1 >= 0 )
hence ( f' . n <= c * (f . n) & f' . n >= 0 ) by A28, A33, A35; :: thesis: verum
end;
end;
end;
then A37: f' in Big_Oh f by A20, A32;
now
let n be Element of NAT ; :: thesis: ( n >= max N3,(max N1,N2) implies ( g' . b1 <= c * (g . b1) & g' . b1 >= 0 ) )
assume A38: n >= max N3,(max N1,N2) ; :: thesis: ( g' . b1 <= c * (g . b1) & g' . b1 >= 0 )
then ( n >= N3 & n >= N2 ) by A25, XXREAL_0:2;
then A39: ( t . n >= 0 & g . n >= 0 & t . n <= c * ((max f,g) . n) ) by A21, A23;
then A40: 0 * (g . n) <= c * (g . n) by A20;
per cases ( f . n >= g . n or f . n < g . n ) ;
suppose f . n >= g . n ; :: thesis: ( g' . b1 <= c * (g . b1) & g' . b1 >= 0 )
hence ( g' . n <= c * (g . n) & g' . n >= 0 ) by A31, A38, A40; :: thesis: verum
end;
suppose A41: f . n < g . n ; :: thesis: ( g' . b1 <= c * (g . b1) & g' . b1 >= 0 )
then max (f . n),(g . n) = g . n by XXREAL_0:def 10;
then (max f,g) . n = g . n by Def10;
hence ( g' . n <= c * (g . n) & g' . n >= 0 ) by A31, A39, A41; :: thesis: verum
end;
end;
end;
then A42: g' in Big_Oh g by A20, A32;
now
let n be Element of NAT ; :: thesis: t . b1 = max (f' . b1),(g' . b1)
per cases ( n < max N3,(max N1,N2) or n >= max N3,(max N1,N2) ) ;
suppose n < max N3,(max N1,N2) ; :: thesis: t . b1 = max (f' . b1),(g' . b1)
then ( f' . n = t . n & g' . n = t . n ) by A28, A31;
hence t . n = max (f' . n),(g' . n) ; :: thesis: verum
end;
suppose A43: n >= max N3,(max N1,N2) ; :: thesis: t . b1 = max (f' . b1),(g' . b1)
then A44: n >= N3 by A24, XXREAL_0:2;
thus t . n = max (f' . n),(g' . n) :: thesis: verum
proof
per cases ( f . n >= g . n or f . n < g . n ) ;
suppose f . n >= g . n ; :: thesis: t . n = max (f' . n),(g' . n)
then ( f' . n = t . n & g' . n = 0 & t . n >= 0 ) by A21, A28, A31, A43, A44;
hence t . n = max (f' . n),(g' . n) by XXREAL_0:def 10; :: thesis: verum
end;
suppose f . n < g . n ; :: thesis: t . n = max (f' . n),(g' . n)
then ( f' . n = 0 & g' . n = t . n & t . n >= 0 ) by A21, A28, A31, A43, A44;
hence t . n = max (f' . n),(g' . n) by XXREAL_0:def 10; :: thesis: verum
end;
end;
end;
end;
end;
end;
hence x in max (Big_Oh f),(Big_Oh g) by A18, A32, A37, A42; :: thesis: verum
end;
hence max (Big_Oh f),(Big_Oh g) = Big_Oh (max f,g) by TARSKI:2; :: thesis: verum