reconsider g = seq_a^ (2,1,1) as eventually-positive Real_Sequence ;
set f = seq_a^ (2,1,0);
take
g
; ( g = seq_a^ (2,1,1) & seq_a^ (2,1,0) in Big_Theta g )
thus
g = seq_a^ (2,1,1)
; seq_a^ (2,1,0) in Big_Theta g
A1:
seq_a^ (2,1,0) is Element of Funcs (NAT,REAL)
by FUNCT_2:8;
A2:
now for n being Element of NAT st n >= 2 holds
( (2 to_power (- 1)) * (g . n) <= (seq_a^ (2,1,0)) . n & (seq_a^ (2,1,0)) . n <= 1 * (g . n) )let n be
Element of
NAT ;
( n >= 2 implies ( (2 to_power (- 1)) * (g . n) <= (seq_a^ (2,1,0)) . n & (seq_a^ (2,1,0)) . n <= 1 * (g . n) ) )assume
n >= 2
;
( (2 to_power (- 1)) * (g . n) <= (seq_a^ (2,1,0)) . n & (seq_a^ (2,1,0)) . n <= 1 * (g . n) )A3:
(seq_a^ (2,1,0)) . n = 2
to_power ((1 * n) + 0)
by Def1;
A4:
g . n = 2
to_power ((1 * n) + 1)
by Def1;
then (2 to_power (- 1)) * (g . n) =
2
to_power ((- 1) + (n + 1))
by POWER:27
.=
(seq_a^ (2,1,0)) . n
by A3
;
hence
(2 to_power (- 1)) * (g . n) <= (seq_a^ (2,1,0)) . n
;
(seq_a^ (2,1,0)) . n <= 1 * (g . n)
n + 0 <= n + 1
by XREAL_1:7;
hence
(seq_a^ (2,1,0)) . n <= 1
* (g . n)
by A3, A4, PRE_FF:8;
verum end;
A5:
2 to_power (- 1) > 0
by POWER:34;
Big_Theta 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 * (g . n) <= s . n & s . n <= c * (g . n) ) ) ) }
by ASYMPT_0:27;
hence
seq_a^ (2,1,0) in Big_Theta g
by A1, A5, A2; verum