set f = seq_a^ 2,1,0 ;
set g = seq_a^ 2,1,1;
set h = (seq_a^ 2,1,0 ) /" (seq_a^ 2,1,1);
reconsider f = seq_a^ 2,1,0 as eventually-positive Real_Sequence ;
reconsider g = seq_a^ 2,1,1 as eventually-positive Real_Sequence ;
take
f
; :: thesis: ex s1 being eventually-positive Real_Sequence st
( f = seq_a^ 2,1,0 & s1 = seq_a^ 2,1,1 & Big_Oh f = Big_Oh s1 )
take
g
; :: thesis: ( f = seq_a^ 2,1,0 & g = seq_a^ 2,1,1 & Big_Oh f = Big_Oh g )
thus
( f = seq_a^ 2,1,0 & g = seq_a^ 2,1,1 )
; :: thesis: Big_Oh f = Big_Oh g
A2:
for n being Element of NAT holds ((seq_a^ 2,1,0 ) /" (seq_a^ 2,1,1)) . n = 2 "
proof
now let n be
Element of
NAT ;
:: thesis: ((seq_a^ 2,1,0 ) /" (seq_a^ 2,1,1)) . n = 2 " A3:
f . n = 2
to_power ((1 * n) + 0 )
by Def1;
A4:
g . n = 2
to_power ((1 * n) + 1)
by Def1;
((seq_a^ 2,1,0 ) /" (seq_a^ 2,1,1)) . n =
(2 to_power n) / (g . n)
by A3, Lm4
.=
2
to_power (n - (n + 1))
by A4, POWER:34
.=
2
to_power (0 + (- 1))
.=
1
/ (2 to_power 1)
by POWER:33
.=
1
/ 2
by POWER:30
.=
2
"
;
hence
((seq_a^ 2,1,0 ) /" (seq_a^ 2,1,1)) . n = 2
"
;
:: thesis: verum end;
hence
for
n being
Element of
NAT holds
((seq_a^ 2,1,0 ) /" (seq_a^ 2,1,1)) . n = 2
"
;
:: thesis: verum
end;
A5:
now let p be
real number ;
:: thesis: ( p > 0 implies ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs ((((seq_a^ 2,1,0 ) /" (seq_a^ 2,1,1)) . n) - (2 " )) < p )assume A6:
p > 0
;
:: thesis: ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs ((((seq_a^ 2,1,0 ) /" (seq_a^ 2,1,1)) . n) - (2 " )) < ptake N =
0 ;
:: thesis: for n being Element of NAT st n >= N holds
abs ((((seq_a^ 2,1,0 ) /" (seq_a^ 2,1,1)) . n) - (2 " )) < plet n be
Element of
NAT ;
:: thesis: ( n >= N implies abs ((((seq_a^ 2,1,0 ) /" (seq_a^ 2,1,1)) . n) - (2 " )) < p )assume
n >= N
;
:: thesis: abs ((((seq_a^ 2,1,0 ) /" (seq_a^ 2,1,1)) . n) - (2 " )) < p abs ((((seq_a^ 2,1,0 ) /" (seq_a^ 2,1,1)) . n) - (2 " )) =
abs ((2 " ) - (2 " ))
by A2
.=
0
by ABSVALUE:7
;
hence
abs ((((seq_a^ 2,1,0 ) /" (seq_a^ 2,1,1)) . n) - (2 " )) < p
by A6;
:: thesis: verum end;
then A7:
(seq_a^ 2,1,0 ) /" (seq_a^ 2,1,1) is convergent
by SEQ_2:def 6;
then
lim ((seq_a^ 2,1,0 ) /" (seq_a^ 2,1,1)) > 0
by A5, SEQ_2:def 7;
hence
Big_Oh f = Big_Oh g
by A7, ASYMPT_0:15; :: thesis: verum