let f be eventually-nonnegative Real_Sequence; :: thesis: for k being Nat st f in Big_Oh (seq_n^ k) holds

ex N being Nat st

for n being Nat st N <= n holds

f . n <= (seq_n^ (k + 1)) . n

let k be Nat; :: thesis: ( f in Big_Oh (seq_n^ k) implies ex N being Nat st

for n being Nat st N <= n holds

f . n <= (seq_n^ (k + 1)) . n )

assume f in Big_Oh (seq_n^ k) ; :: thesis: ex N being Nat st

for n being Nat st N <= n holds

f . n <= (seq_n^ (k + 1)) . n

then consider t being Element of Funcs (NAT,REAL) such that

L1: ( f = 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 c being Real, N being Element of NAT such that

L2: ( c > 0 & ( for n being Element of NAT st n >= N holds

( f . n <= c * ((seq_n^ k) . n) & f . n >= 0 ) ) ) by L1;

set n = [/(max (N,c))\];

P1: ( N <= max (N,c) & c <= max (N,c) ) by XXREAL_0:25;

P2P: max (N,c) <= [/(max (N,c))\] by INT_1:def 7;

then P2: ( N <= [/(max (N,c))\] & c <= [/(max (N,c))\] ) by P1, XXREAL_0:2;

reconsider n = [/(max (N,c))\] as Element of NAT by INT_1:3, P2P, P1;

take n ; :: thesis: for n being Nat st n <= n holds

f . n <= (seq_n^ (k + 1)) . n

let x be Nat; :: thesis: ( n <= x implies f . x <= (seq_n^ (k + 1)) . x )

A: x in NAT by ORDINAL1:def 12;

assume P4: n <= x ; :: thesis: f . x <= (seq_n^ (k + 1)) . x

then P4r: ( 0 < x & N <= x & c <= x ) by P2, L2, XXREAL_0:2;

P5: (seq_n^ (k + 1)) . x = x * ((seq_n^ k) . x) by TPOWSUCC, P2P, L2, P4, P1;

P6: ( f . x <= c * ((seq_n^ k) . x) & f . x >= 0 ) by A, P4r, L2;

(seq_n^ k) . x = x to_power k by P4, P2P, L2, A, ASYMPT_1:def 3, P1;

then c * ((seq_n^ k) . x) <= x * ((seq_n^ k) . x) by P4r, XREAL_1:64;

hence f . x <= (seq_n^ (k + 1)) . x by P5, XXREAL_0:2, P6; :: thesis: verum

ex N being Nat st

for n being Nat st N <= n holds

f . n <= (seq_n^ (k + 1)) . n

let k be Nat; :: thesis: ( f in Big_Oh (seq_n^ k) implies ex N being Nat st

for n being Nat st N <= n holds

f . n <= (seq_n^ (k + 1)) . n )

assume f in Big_Oh (seq_n^ k) ; :: thesis: ex N being Nat st

for n being Nat st N <= n holds

f . n <= (seq_n^ (k + 1)) . n

then consider t being Element of Funcs (NAT,REAL) such that

L1: ( f = 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 c being Real, N being Element of NAT such that

L2: ( c > 0 & ( for n being Element of NAT st n >= N holds

( f . n <= c * ((seq_n^ k) . n) & f . n >= 0 ) ) ) by L1;

set n = [/(max (N,c))\];

P1: ( N <= max (N,c) & c <= max (N,c) ) by XXREAL_0:25;

P2P: max (N,c) <= [/(max (N,c))\] by INT_1:def 7;

then P2: ( N <= [/(max (N,c))\] & c <= [/(max (N,c))\] ) by P1, XXREAL_0:2;

reconsider n = [/(max (N,c))\] as Element of NAT by INT_1:3, P2P, P1;

take n ; :: thesis: for n being Nat st n <= n holds

f . n <= (seq_n^ (k + 1)) . n

let x be Nat; :: thesis: ( n <= x implies f . x <= (seq_n^ (k + 1)) . x )

A: x in NAT by ORDINAL1:def 12;

assume P4: n <= x ; :: thesis: f . x <= (seq_n^ (k + 1)) . x

then P4r: ( 0 < x & N <= x & c <= x ) by P2, L2, XXREAL_0:2;

P5: (seq_n^ (k + 1)) . x = x * ((seq_n^ k) . x) by TPOWSUCC, P2P, L2, P4, P1;

P6: ( f . x <= c * ((seq_n^ k) . x) & f . x >= 0 ) by A, P4r, L2;

(seq_n^ k) . x = x to_power k by P4, P2P, L2, A, ASYMPT_1:def 3, P1;

then c * ((seq_n^ k) . x) <= x * ((seq_n^ k) . x) by P4r, XREAL_1:64;

hence f . x <= (seq_n^ (k + 1)) . x by P5, XXREAL_0:2, P6; :: thesis: verum