let f be eventually-nonnegative Real_Sequence; for X being set holds Big_Theta (f,X) = (Big_Oh (f,X)) /\ (Big_Omega (f,X))
let X be set ; Big_Theta (f,X) = (Big_Oh (f,X)) /\ (Big_Omega (f,X))
now for x being object holds
( ( x in Big_Theta (f,X) implies x in (Big_Oh (f,X)) /\ (Big_Omega (f,X)) ) & ( x in (Big_Oh (f,X)) /\ (Big_Omega (f,X)) implies x in Big_Theta (f,X) ) )let x be
object ;
( ( x in Big_Theta (f,X) implies x in (Big_Oh (f,X)) /\ (Big_Omega (f,X)) ) & ( x in (Big_Oh (f,X)) /\ (Big_Omega (f,X)) implies x in Big_Theta (f,X) ) )hereby ( x in (Big_Oh (f,X)) /\ (Big_Omega (f,X)) implies x in Big_Theta (f,X) )
consider N1 being
Nat such that A1:
for
n being
Nat st
n >= N1 holds
f . n >= 0
by Def2;
assume
x in Big_Theta (
f,
X)
;
x in (Big_Oh (f,X)) /\ (Big_Omega (f,X))then consider t being
Element of
Funcs (
NAT,
REAL)
such that A2:
x = t
and A3:
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 &
n in X holds
(
d * (f . n) <= t . n &
t . n <= c * (f . n) ) ) )
;
consider c,
d being
Real,
N being
Element of
NAT such that A4:
c > 0
and A5:
d > 0
and A6:
for
n being
Element of
NAT st
n >= N &
n in X holds
(
d * (f . n) <= t . n &
t . n <= c * (f . n) )
by A3;
reconsider a =
max (
N,
N1) as
Element of
NAT by ORDINAL1:def 12;
A7:
a >= N1
by XXREAL_0:25;
A8:
a >= N
by XXREAL_0:25;
then A12:
x in Big_Omega (
f,
X)
by A2, A5;
then
x in Big_Oh (
f,
X)
by A2, A4;
hence
x in (Big_Oh (f,X)) /\ (Big_Omega (f,X))
by A12, XBOOLE_0:def 4;
verum
end; assume A16:
x in (Big_Oh (f,X)) /\ (Big_Omega (f,X))
;
x in Big_Theta (f,X)then
x in Big_Oh (
f,
X)
by XBOOLE_0:def 4;
then consider t being
Element of
Funcs (
NAT,
REAL)
such that A17:
x = t
and A18:
ex
c being
Real ex
N being
Element of
NAT st
(
c > 0 & ( for
n being
Element of
NAT st
n >= N &
n in X holds
(
t . n <= c * (f . n) &
t . n >= 0 ) ) )
;
x in Big_Omega (
f,
X)
by A16, XBOOLE_0:def 4;
then consider s being
Element of
Funcs (
NAT,
REAL)
such that A19:
x = s
and A20:
ex
d being
Real ex
N being
Element of
NAT st
(
d > 0 & ( for
n being
Element of
NAT st
n >= N &
n in X holds
(
s . n >= d * (f . n) &
s . n >= 0 ) ) )
;
consider c being
Real,
N being
Element of
NAT such that A21:
c > 0
and A22:
for
n being
Element of
NAT st
n >= N &
n in X holds
(
t . n <= c * (f . n) &
t . n >= 0 )
by A18;
consider d being
Real,
N1 being
Element of
NAT such that A23:
d > 0
and A24:
for
n being
Element of
NAT st
n >= N1 &
n in X holds
(
s . n >= d * (f . n) &
s . n >= 0 )
by A20;
set a =
max (
N,
N1);
A25:
(
max (
N,
N1)
>= N &
max (
N,
N1)
>= N1 )
by XXREAL_0:25;
hence
x in Big_Theta (
f,
X)
by A17, A21, A23;
verum end;
hence
Big_Theta (f,X) = (Big_Oh (f,X)) /\ (Big_Omega (f,X))
by TARSKI:2; verum