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 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;
set N = max N1,N2;
A15: max N1,N2 >= N2 by XXREAL_0:25;
A16: max N1,N2 >= N1 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 A17: n >= max N1,N2 ; :: 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:70;
then A19: c * (f . n) <= (max c,d) * (f . n) by XREAL_1:66, 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:70;
then A21: d * (g . n) <= (max c,d) * (g . n) by XREAL_1:66, 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:66, 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:66, 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 Def10;
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 Element of NAT such that
A29: for n being Element of NAT st n >= N1 holds
f . n >= 0 by Def4;
consider N2 being Element of NAT such that
A30: for n being Element of NAT st n >= N2 holds
g . n >= 0 by Def4;
set N = max N3,(max N1,N2);
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 ) );
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 ) );
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 < 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 A32; :: thesis: verum
end;
end;
end;
end;
end;
end;
consider f9 being Function of NAT ,REAL such that
A33: for x being Element of NAT holds S1[x,f9 . x] from FUNCT_2:sch 3(A31);
A34: 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 A35: 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 A35; :: 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 Function of NAT ,REAL such that
A36: for x being Element of NAT holds S2[x,g9 . x] from FUNCT_2:sch 3(A34);
A37: max N3,(max N1,N2) >= N3 by XXREAL_0:25;
A38: now
let n be Element of NAT ; :: thesis: t . b1 = max (f9 . b1),(g9 . 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 (f9 . b1),(g9 . b1)
then ( f9 . n = t . n & g9 . n = t . n ) by A33, A36;
hence t . n = max (f9 . n),(g9 . n) ; :: thesis: verum
end;
suppose A39: n >= max N3,(max N1,N2) ; :: thesis: t . b1 = max (f9 . b1),(g9 . b1)
then A40: n >= N3 by A37, 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 A41: f . n >= g . n ; :: thesis: t . n = max (f9 . n),(g9 . n)
A42: t . n >= 0 by A28, A40;
( f9 . n = t . n & g9 . n = 0 ) by A33, A36, A39, A41;
hence t . n = max (f9 . n),(g9 . n) by A42, XXREAL_0:def 10; :: thesis: verum
end;
suppose A43: f . n < g . n ; :: thesis: t . n = max (f9 . n),(g9 . n)
A44: t . n >= 0 by A28, A40;
( f9 . n = 0 & g9 . n = t . n ) by A33, A36, A39, A43;
hence t . n = max (f9 . n),(g9 . n) by A44, XXREAL_0:def 10; :: thesis: verum
end;
end;
end;
end;
end;
end;
A45: g9 is Element of Funcs NAT ,REAL by FUNCT_2:11;
A46: max N3,(max N1,N2) >= max N1,N2 by XXREAL_0:25;
max N1,N2 >= N2 by XXREAL_0:25;
then A47: max N3,(max N1,N2) >= N2 by A46, XXREAL_0:2;
now
let n be Element of NAT ; :: thesis: ( n >= max N3,(max N1,N2) implies ( g9 . b1 <= c * (g . b1) & g9 . b1 >= 0 ) )
assume A48: n >= max N3,(max N1,N2) ; :: thesis: ( g9 . b1 <= c * (g . b1) & g9 . b1 >= 0 )
then n >= N3 by A37, XXREAL_0:2;
then A49: ( t . n >= 0 & t . n <= c * ((max f,g) . n) ) by A28;
n >= N2 by A47, A48, XXREAL_0:2;
then g . n >= 0 by A30;
then A50: 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 A36, A48, A50; :: thesis: verum
end;
suppose A51: 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 Def10;
hence ( g9 . n <= c * (g . n) & g9 . n >= 0 ) by A36, A49, A51; :: thesis: verum
end;
end;
end;
then A52: g9 in Big_Oh g by A27, A45;
A53: f9 is Element of Funcs NAT ,REAL by FUNCT_2:11;
max N1,N2 >= N1 by XXREAL_0:25;
then A54: max N3,(max N1,N2) >= N1 by A46, XXREAL_0:2;
now
let n be Element of NAT ; :: thesis: ( n >= max N3,(max N1,N2) implies ( f9 . b1 <= c * (f . b1) & f9 . b1 >= 0 ) )
assume A55: n >= max N3,(max N1,N2) ; :: thesis: ( f9 . b1 <= c * (f . b1) & f9 . b1 >= 0 )
then n >= N3 by A37, XXREAL_0:2;
then A56: ( t . n >= 0 & t . n <= c * ((max f,g) . n) ) by A28;
n >= N1 by A54, A55, XXREAL_0:2;
then f . n >= 0 by A29;
then A57: 0 * (f . n) <= c * (f . n) by A27;
per cases ( f . n >= g . n or f . n < g . n ) ;
suppose A58: 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 Def10;
hence ( f9 . n <= c * (f . n) & f9 . n >= 0 ) by A33, A56, A58; :: 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 A33, A55, A57; :: thesis: verum
end;
end;
end;
then f9 in Big_Oh f by A27, A53;
hence x in max (Big_Oh f),(Big_Oh g) by A25, A53, A45, A52, A38; :: thesis: verum
end;
hence max (Big_Oh f),(Big_Oh g) = Big_Oh (max f,g) by TARSKI:2; :: thesis: verum