let f, g be eventually-nonnegative Real_Sequence; max ((Big_Oh f),(Big_Oh g)) = Big_Oh (max (f,g))
now 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 ;
( ( 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 ( 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))
;
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 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 ;
( n >= N implies ( t . n <= (max (c,d)) * ((max (f,g)) . n) & t . n >= 0 ) )assume A17:
n >= N
;
( 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;
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;
verum end; hence
x in Big_Oh (max (f,g))
by A1, A14;
verum
end; assume
x in Big_Oh (max (f,g))
;
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]
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]
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;
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;
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;
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;
verum end;
hence
max ((Big_Oh f),(Big_Oh g)) = Big_Oh (max (f,g))
by TARSKI:2; verum