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