let f, g be eventually-nonnegative Real_Sequence; Big_Theta (f + g) = Big_Theta (max (f,g))
A1:
Big_Theta (max (f,g)) = { s where s is Element of Funcs (NAT,REAL) : ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N holds
( d * ((max (f,g)) . n) <= s . n & s . n <= c * ((max (f,g)) . n) ) ) ) }
by Th27;
consider N2 being Nat such that
A2:
for n being Nat st n >= N2 holds
g . n >= 0
by Def2;
consider N1 being Nat such that
A3:
for n being Nat st n >= N1 holds
f . n >= 0
by Def2;
A4:
Big_Theta (f + g) = { s where s is Element of Funcs (NAT,REAL) : ex c, d being Real ex N being Element of NAT st
( c > 0 & d > 0 & ( for n being Element of NAT st n >= N holds
( d * ((f + g) . n) <= s . n & s . n <= c * ((f + g) . n) ) ) ) }
by Th27;
now for x being object holds
( ( x in Big_Theta (f + g) implies x in Big_Theta (max (f,g)) ) & ( x in Big_Theta (max (f,g)) implies x in Big_Theta (f + g) ) )let x be
object ;
( ( x in Big_Theta (f + g) implies x in Big_Theta (max (f,g)) ) & ( x in Big_Theta (max (f,g)) implies x in Big_Theta (f + g) ) )hereby ( x in Big_Theta (max (f,g)) implies x in Big_Theta (f + g) )
assume
x in Big_Theta (f + g)
;
x in Big_Theta (max (f,g))then consider t being
Element of
Funcs (
NAT,
REAL)
such that A5:
t = x
and A6:
ex
c,
d being
Real ex
N being
Element of
NAT st
(
c > 0 &
d > 0 & ( for
n being
Element of
NAT st
n >= N holds
(
d * ((f + g) . n) <= t . n &
t . n <= c * ((f + g) . n) ) ) )
by A4;
consider c,
d being
Real,
N being
Element of
NAT such that A7:
c > 0
and A8:
d > 0
and A9:
for
n being
Element of
NAT st
n >= N holds
(
d * ((f + g) . n) <= t . n &
t . n <= c * ((f + g) . n) )
by A6;
reconsider a =
max (
N,
(max (N1,N2))) as
Element of
NAT by ORDINAL1:def 12;
A10:
a >= N
by XXREAL_0:25;
A11:
a >= max (
N1,
N2)
by XXREAL_0:25;
max (
N1,
N2)
>= N2
by XXREAL_0:25;
then A12:
a >= N2
by A11, XXREAL_0:2;
max (
N1,
N2)
>= N1
by XXREAL_0:25;
then A13:
a >= N1
by A11, XXREAL_0:2;
A14:
now for n being Element of NAT st n >= a holds
( d * ((max (f,g)) . n) <= t . n & t . n <= (2 * c) * ((max (f,g)) . n) )let n be
Element of
NAT ;
( n >= a implies ( d * ((max (f,g)) . n) <= t . n & t . n <= (2 * c) * ((max (f,g)) . n) ) )A15:
(
g . n <= max (
(f . n),
(g . n)) &
(1 * ((max (f,g)) . n)) + (1 * ((max (f,g)) . n)) = (1 + 1) * ((max (f,g)) . n) )
by XXREAL_0:25;
A16:
(max (f,g)) . n = max (
(f . n),
(g . n))
by Def7;
(
(f + g) . n = (f . n) + (g . n) &
f . n <= max (
(f . n),
(g . n)) )
by SEQ_1:7, XXREAL_0:25;
then
(f + g) . n <= 2
* ((max (f,g)) . n)
by A16, A15, XREAL_1:7;
then A17:
c * ((f + g) . n) <= c * (2 * ((max (f,g)) . n))
by A7, XREAL_1:64;
assume A18:
n >= a
;
( d * ((max (f,g)) . n) <= t . n & t . n <= (2 * c) * ((max (f,g)) . n) )then
n >= N2
by A12, XXREAL_0:2;
then A19:
g . n >= 0
by A2;
n >= N1
by A13, A18, XXREAL_0:2;
then A20:
f . n >= 0
by A3;
(max (f,g)) . n <= (f + g) . n
then A21:
d * ((max (f,g)) . n) <= d * ((f + g) . n)
by A8, XREAL_1:64;
n >= N
by A10, A18, XXREAL_0:2;
then
(
t . n <= c * ((f + g) . n) &
d * ((f + g) . n) <= t . n )
by A9;
hence
(
d * ((max (f,g)) . n) <= t . n &
t . n <= (2 * c) * ((max (f,g)) . n) )
by A17, A21, XXREAL_0:2;
verum end;
2
* c > 2
* 0
by A7, XREAL_1:68;
hence
x in Big_Theta (max (f,g))
by A1, A5, A8, A14;
verum
end; consider N1 being
Nat such that A22:
for
n being
Nat st
n >= N1 holds
f . n >= 0
by Def2;
consider N2 being
Nat such that A23:
for
n being
Nat st
n >= N2 holds
g . n >= 0
by Def2;
assume
x in Big_Theta (max (f,g))
;
x in Big_Theta (f + g)then consider t being
Element of
Funcs (
NAT,
REAL)
such that A24:
t = x
and A25:
ex
c,
d being
Real ex
N being
Element of
NAT st
(
c > 0 &
d > 0 & ( for
n being
Element of
NAT st
n >= N holds
(
d * ((max (f,g)) . n) <= t . n &
t . n <= c * ((max (f,g)) . n) ) ) )
by A1;
consider c,
d being
Real,
N being
Element of
NAT such that A26:
c > 0
and A27:
d > 0
and A28:
for
n being
Element of
NAT st
n >= N holds
(
d * ((max (f,g)) . n) <= t . n &
t . n <= c * ((max (f,g)) . n) )
by A25;
reconsider a =
max (
N,
(max (N1,N2))) as
Element of
NAT by ORDINAL1:def 12;
A29:
max (
N1,
N2)
<= a
by XXREAL_0:25;
N2 <= max (
N1,
N2)
by XXREAL_0:25;
then A30:
N2 <= a
by A29, XXREAL_0:2;
A31:
N <= a
by XXREAL_0:25;
N1 <= max (
N1,
N2)
by XXREAL_0:25;
then A32:
N1 <= a
by A29, XXREAL_0:2;
A33:
now for n being Element of NAT st n >= a holds
( (d * (2 ")) * ((f + g) . n) <= t . n & t . n <= c * ((f + g) . n) )let n be
Element of
NAT ;
( n >= a implies ( (d * (2 ")) * ((f + g) . n) <= t . n & t . n <= c * ((f + g) . n) ) )assume A34:
n >= a
;
( (d * (2 ")) * ((f + g) . n) <= t . n & t . n <= c * ((f + g) . n) )then
n >= N1
by A32, XXREAL_0:2;
then
f . n >= 0
by A22;
then A35:
(f . n) + (g . n) >= 0 + (g . n)
by XREAL_1:7;
(
f . n <= max (
(f . n),
(g . n)) &
g . n <= max (
(f . n),
(g . n)) )
by XXREAL_0:25;
then
(f . n) + (g . n) <= (1 * (max ((f . n),(g . n)))) + (1 * (max ((f . n),(g . n))))
by XREAL_1:7;
then
(2 ") * ((f . n) + (g . n)) <= (2 ") * (2 * (max ((f . n),(g . n))))
by XREAL_1:64;
then
(2 ") * ((f + g) . n) <= max (
(f . n),
(g . n))
by SEQ_1:7;
then
d * ((2 ") * ((f + g) . n)) <= d * (max ((f . n),(g . n)))
by A27, XREAL_1:64;
then A36:
d * ((2 ") * ((f + g) . n)) <= d * ((max (f,g)) . n)
by Def7;
n >= N2
by A30, A34, XXREAL_0:2;
then
g . n >= 0
by A23;
then A37:
(f . n) + (g . n) >= (f . n) + 0
by XREAL_1:7;
(
(max (f,g)) . n = max (
(f . n),
(g . n)) &
(f + g) . n = (f . n) + (g . n) )
by Def7, SEQ_1:7;
then
(max (f,g)) . n <= (f + g) . n
by A37, A35, XXREAL_0:16;
then A38:
c * ((max (f,g)) . n) <= c * ((f + g) . n)
by A26, XREAL_1:64;
n >= N
by A31, A34, XXREAL_0:2;
then
(
t . n <= c * ((max (f,g)) . n) &
d * ((max (f,g)) . n) <= t . n )
by A28;
hence
(
(d * (2 ")) * ((f + g) . n) <= t . n &
t . n <= c * ((f + g) . n) )
by A38, A36, XXREAL_0:2;
verum end;
d * (2 ") > d * 0
by A27, XREAL_1:68;
hence
x in Big_Theta (f + g)
by A4, A24, A26, A33;
verum end;
hence
Big_Theta (f + g) = Big_Theta (max (f,g))
by TARSKI:2; verum