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

0 <= r

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 )

hence seq_p c in Big_Oh (seq_n^ k) by P6, P7; :: thesis: verum

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

for r being Real st r in rng d holds
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;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

0 <= r

proof

then
d is nonnegative-yielding
;
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;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

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

seq_p c is Element of Funcs (NAT,REAL)
by FUNCT_2:8;
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;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

hence seq_p c in Big_Oh (seq_n^ k) by P6, P7; :: thesis: verum