let k be Nat; :: thesis: for c being XFinSequence of REAL st len c = k + 1 & seq_p c is eventually-nonnegative holds
seq_p c in Big_Oh (seq_n^ k)
let c be XFinSequence of REAL ; :: thesis: ( len c = k + 1 & seq_p c is eventually-nonnegative implies seq_p c in Big_Oh (seq_n^ k) )
assume AS: ( len c = k + 1 & seq_p c is eventually-nonnegative ) ; :: thesis: seq_p c in Big_Oh (seq_n^ k)
consider d being XFinSequence of REAL such that
P1: ( len d = len c & ( for i being Nat st i in dom d holds
d . i = |.(c . i).| ) ) by LMXFIN15;
T11: for i being Nat st i in dom d holds
0 <= d . i
proof
let i be Nat; :: thesis: ( i in dom d implies 0 <= d . i )
assume i in dom d ; :: thesis: 0 <= d . i
then d . i = |.(c . i).| by P1;
hence 0 <= d . i by COMPLEX1:46; :: thesis: verum
end;
for r being Real st r in rng d holds
0 <= r
proof
let r be Real; :: thesis: ( r in rng d implies 0 <= r )
assume r in rng d ; :: thesis: 0 <= r
then consider x being object such that
RC: ( x in dom d & r = d . x ) by FUNCT_1:def 3;
thus 0 <= r by RC, T11; :: thesis: verum
end;
then d is nonnegative-yielding ;
then seq_p d in Big_Oh (seq_n^ k) by LMXFIN10, P1, AS;
then consider t being Element of Funcs (NAT,REAL) such that
P5: ( seq_p d = t & 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 * ((seq_n^ k) . n) & t . n >= 0 ) ) ) ) ;
consider N1 being Nat such that
P4A: for n being Nat st N1 <= n holds
0 <= (seq_p c) . n by AS;
consider a being Real, N2 being Element of NAT such that
P6: ( a > 0 & ( for n being Element of NAT st n >= N2 holds
( t . n <= a * ((seq_n^ k) . n) & t . n >= 0 ) ) ) by P5;
set N = N1 + N2;
P7: for n being Element of NAT st n >= N1 + N2 holds
( (seq_p c) . n <= a * ((seq_n^ k) . n) & (seq_p c) . n >= 0 )
proof
let n be Element of NAT ; :: thesis: ( n >= N1 + N2 implies ( (seq_p c) . n <= a * ((seq_n^ k) . n) & (seq_p c) . n >= 0 ) )
assume P8: n >= N1 + N2 ; :: thesis: ( (seq_p c) . n <= a * ((seq_n^ k) . n) & (seq_p c) . n >= 0 )
( N1 <= N1 + N2 & N2 <= N1 + N2 ) by NAT_1:11;
then P9: ( N1 <= n & N2 <= n ) by P8, XXREAL_0:2;
then P10: ( (seq_p c) . n <= (seq_p d) . n & 0 <= (seq_p c) . n ) by P4A, P1, LMXFIN17;
( (seq_p d) . n <= a * ((seq_n^ k) . n) & (seq_p d) . n >= 0 ) by P5, P9, P6;
hence (seq_p c) . n <= a * ((seq_n^ k) . n) by P10, XXREAL_0:2; :: thesis: (seq_p c) . n >= 0
thus 0 <= (seq_p c) . n by P4A, P9; :: thesis: verum
end;
seq_p c is Element of Funcs (NAT,REAL) by FUNCT_2:8;
hence seq_p c in Big_Oh (seq_n^ k) by P6, P7; :: thesis: verum