let f be Real_Sequence; :: thesis: for k being Element of NAT st ( for n being Element of NAT holds f . n = Sum (seq_n^ k),n ) holds
f in Big_Theta (seq_n^ (k + 1))
let k be Element of NAT ; :: thesis: ( ( for n being Element of NAT holds f . n = Sum (seq_n^ k),n ) implies f in Big_Theta (seq_n^ (k + 1)) )
assume A1: for n being Element of NAT holds f . n = Sum (seq_n^ k),n ; :: thesis: f in Big_Theta (seq_n^ (k + 1))
set g = seq_n^ (k + 1);
A2: f is Element of Funcs NAT ,REAL by FUNCT_2:11;
A3: now
set p = seq_n^ k;
let n be Element of NAT ; :: thesis: ( n >= 1 implies ( ((2 to_power (k + 1)) " ) * ((seq_n^ (k + 1)) . n) <= f . n & f . n >= 0 ) )
set n1 = [/(n / 2)\];
ex s being Real_Sequence st
( s . 0 = 0 & ( for m being Element of NAT st m > 0 holds
s . m = (n / 2) to_power k ) )
proof
defpred S1[ Element of NAT , Real] means ( ( $1 = 0 implies $2 = 0 ) & ( $1 > 0 implies $2 = (n / 2) to_power k ) );
A4: for x being Element of NAT ex y being Element of REAL st S1[x,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of REAL st S1[n,y]
per cases ( n = 0 or n > 0 ) ;
suppose n = 0 ; :: thesis: ex y being Element of REAL st S1[n,y]
hence ex y being Element of REAL st S1[n,y] ; :: thesis: verum
end;
suppose n > 0 ; :: thesis: ex y being Element of REAL st S1[n,y]
hence ex y being Element of REAL st S1[n,y] ; :: thesis: verum
end;
end;
end;
consider h being Function of NAT ,REAL such that
A5: for x being Element of NAT holds S1[x,h . x] from FUNCT_2:sch 3(A4);
 take h ; :: thesis: ( h . 0 = 0 & ( for m being Element of NAT st m > 0 holds
h . m = (n / 2) to_power k ) )
thus h . 0 = 0 by A5; :: thesis: for m being Element of NAT st m > 0 holds
h . m = (n / 2) to_power k
let n be Element of NAT ; :: thesis: ( n > 0 implies h . n = (n / 2) to_power k )
thus ( n > 0 implies h . n = (n / 2) to_power k ) by A5; :: thesis: verum
end;
then consider q being Real_Sequence such that
A6: q . 0 = 0 and
A7: for m being Element of NAT st m > 0 holds
q . m = (n / 2) to_power k ;
A8: [/(n / 2)\] >= n / 2 by INT_1:def 5;
then reconsider n1 = [/(n / 2)\] as Element of NAT by INT_1:16;
set n2 = n1 - 1;
assume A9: n >= 1 ; :: thesis: ( ((2 to_power (k + 1)) " ) * ((seq_n^ (k + 1)) . n) <= f . n & f . n >= 0 )
then A10: n * (2 " ) > 0 * (2 " ) by XREAL_1:70;
then A11: (n / 2) to_power k > 0 by POWER:39;
now
assume n1 - 1 < 0 ; :: thesis: contradiction
then n1 - 1 <= - 1 by INT_1:21;
then (n1 - 1) + 1 <= (- 1) + 1 by XREAL_1:8;
hence contradiction by A10, INT_1:def 5; :: thesis: verum
end;
then reconsider n2 = n1 - 1 as Element of NAT by INT_1:16;
A12: now
[/(n / 2)\] < (n / 2) + 1 by INT_1:def 5;
then n2 < n / 2 by XREAL_1:21;
then A13: (n / 2) + n2 < (n / 2) + (n / 2) by XREAL_1:8;
assume n - n2 < n / 2 ; :: thesis: contradiction
hence contradiction by A13, XREAL_1:21; :: thesis: verum
end;
Sum q,n,n2 = (n - n2) * ((n / 2) to_power k) by A6, A7, Lm18;
then Sum q,n,n2 >= (n / 2) * ((n / 2) to_power k) by A12, A11, XREAL_1:66;
then Sum q,n,n2 >= ((n / 2) to_power 1) * ((n / 2) to_power k) by POWER:30;
then Sum q,n,n2 >= (n / 2) to_power (k + 1) by A10, POWER:32;
then A14: Sum q,n,n2 >= (n to_power (k + 1)) / (2 to_power (k + 1)) by A9, POWER:36;
A15: f . n = Sum (seq_n^ k),n by A1;
A16: now
let m be Element of NAT ; :: thesis: ( m <= n implies (seq_n^ k) . b1 >= 0 )
assume m <= n ; :: thesis: (seq_n^ k) . b1 >= 0
per cases ( m = 0 or m > 0 ) ;
suppose m = 0 ; :: thesis: (seq_n^ k) . b1 >= 0
hence (seq_n^ k) . m >= 0 by Def3; :: thesis: verum
end;
suppose m > 0 ; :: thesis: (seq_n^ k) . b1 >= 0
then (seq_n^ k) . m = m to_power k by Def3;
hence (seq_n^ k) . m >= 0 ; :: thesis: verum
end;
end;
end;
now
let m be Element of NAT ; :: thesis: ( m <= n2 implies (seq_n^ k) . m >= 0 )
n1 <= n1 + 1 by NAT_1:11;
then A17: n2 <= n1 by XREAL_1:22;
A18: n1 <= n by Lm17;
assume m <= n2 ; :: thesis: (seq_n^ k) . m >= 0
then m <= n1 by A17, XXREAL_0:2;
then m <= n by A18, XXREAL_0:2;
hence (seq_n^ k) . m >= 0 by A16; :: thesis: verum
end;
then Sum (seq_n^ k),n2 >= 0 by Lm12;
then A19: (Sum (seq_n^ k),n) + (Sum (seq_n^ k),n2) >= (Sum (seq_n^ k),n) + 0 by XREAL_1:9;
A20: for N0 being Element of NAT st n1 <= N0 & N0 <= n holds
q . N0 <= (seq_n^ k) . N0
proof
let N0 be Element of NAT ; :: thesis: ( n1 <= N0 & N0 <= n implies q . N0 <= (seq_n^ k) . N0 )
assume that
A21: n1 <= N0 and
N0 <= n ; :: thesis: q . N0 <= (seq_n^ k) . N0
A22: N0 >= n / 2 by A8, A21, XXREAL_0:2;
A23: (seq_n^ k) . N0 = N0 to_power k by A10, A8, A21, Def3;
q . N0 = (n / 2) to_power k by A7, A10, A8, A21;
hence q . N0 <= (seq_n^ k) . N0 by A10, A23, A22, Lm6; :: thesis: verum
end;
n >= n2 + 1 by Lm17;
then Sum (seq_n^ k),n,n2 >= Sum q,n,n2 by A20, Lm16;
then A24: Sum (seq_n^ k),n,n2 >= (n to_power (k + 1)) * ((2 to_power (k + 1)) " ) by A14, XXREAL_0:2;
Sum (seq_n^ k),n,n2 = (Sum (seq_n^ k),n) - (Sum (seq_n^ k),n2) by SERIES_1:def 7;
then A25: Sum (seq_n^ k),n >= Sum (seq_n^ k),n,n2 by A19, XREAL_1:22;
(seq_n^ (k + 1)) . n = n to_power (k + 1) by A9, Def3;
hence ((2 to_power (k + 1)) " ) * ((seq_n^ (k + 1)) . n) <= f . n by A15, A25, A24, XXREAL_0:2; :: thesis: f . n >= 0
Sum (seq_n^ k),n >= 0 by A16, Lm12;
hence f . n >= 0 by A1; :: thesis: verum
end;
now
set p = seq_n^ k;
let n be Element of NAT ; :: thesis: ( n >= 1 implies ( f . n <= 1 * ((seq_n^ (k + 1)) . n) & f . n >= 0 ) )
assume A26: n >= 1 ; :: thesis: ( f . n <= 1 * ((seq_n^ (k + 1)) . n) & f . n >= 0 )
ex s being Real_Sequence st
( s . 0 = 0 & ( for m being Element of NAT st m > 0 holds
s . m = n to_power k ) )
proof
defpred S1[ Element of NAT , Real] means ( ( $1 = 0 implies $2 = 0 ) & ( $1 > 0 implies $2 = n to_power k ) );
A27: for x being Element of NAT ex y being Element of REAL st S1[x,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of REAL st S1[n,y]
per cases ( n = 0 or n > 0 ) ;
suppose n = 0 ; :: thesis: ex y being Element of REAL st S1[n,y]
hence ex y being Element of REAL st S1[n,y] ; :: thesis: verum
end;
suppose n > 0 ; :: thesis: ex y being Element of REAL st S1[n,y]
hence ex y being Element of REAL st S1[n,y] ; :: thesis: verum
end;
end;
end;
consider h being Function of NAT ,REAL such that
A28: for x being Element of NAT holds S1[x,h . x] from FUNCT_2:sch 3(A27);
 take h ; :: thesis: ( h . 0 = 0 & ( for m being Element of NAT st m > 0 holds
h . m = n to_power k ) )
thus h . 0 = 0 by A28; :: thesis: for m being Element of NAT st m > 0 holds
h . m = n to_power k
let n be Element of NAT ; :: thesis: ( n > 0 implies h . n = n to_power k )
thus ( n > 0 implies h . n = n to_power k ) by A28; :: thesis: verum
end;
then consider q being Real_Sequence such that
A29: q . 0 = 0 and
A30: for m being Element of NAT st m > 0 holds
q . m = n to_power k ;
now
let m be Element of NAT ; :: thesis: ( m <= n implies (seq_n^ k) . b1 <= q . b1 )
assume A31: m <= n ; :: thesis: (seq_n^ k) . b1 <= q . b1
per cases ( m = 0 or m > 0 ) ;
suppose m = 0 ; :: thesis: (seq_n^ k) . b1 <= q . b1
hence (seq_n^ k) . m <= q . m by A29, Def3; :: thesis: verum
end;
suppose A32: m > 0 ; :: thesis: (seq_n^ k) . b1 <= q . b1
then A33: q . m = n to_power k by A30;
(seq_n^ k) . m = m to_power k by A32, Def3;
hence (seq_n^ k) . m <= q . m by A31, A32, A33, Lm6; :: thesis: verum
end;
end;
end;
then A34: Sum (seq_n^ k),n <= Sum q,n by Lm13;
Sum q,n = (n to_power k) * n by A29, A30, Lm14
.= (n to_power k) * (n to_power 1) by POWER:30
.= n to_power (k + 1) by A26, POWER:32
.= (seq_n^ (k + 1)) . n by A26, Def3 ;
hence f . n <= 1 * ((seq_n^ (k + 1)) . n) by A1, A34; :: thesis: f . n >= 0
A35: now
let m be Element of NAT ; :: thesis: ( m <= n implies (seq_n^ k) . b1 >= 0 )
assume m <= n ; :: thesis: (seq_n^ k) . b1 >= 0
per cases ( m = 0 or m > 0 ) ;
suppose m = 0 ; :: thesis: (seq_n^ k) . b1 >= 0
hence (seq_n^ k) . m >= 0 by Def3; :: thesis: verum
end;
suppose m > 0 ; :: thesis: (seq_n^ k) . b1 >= 0
then (seq_n^ k) . m = m to_power k by Def3;
hence (seq_n^ k) . m >= 0 ; :: thesis: verum
end;
end;
end;
f . n = Sum (seq_n^ k),n by A1;
hence f . n >= 0 by A35, Lm12; :: thesis: verum
end;
then A36: f in Big_Oh (seq_n^ (k + 1)) by A2;
2 to_power (k + 1) > 0 by POWER:39;
then f in Big_Omega (seq_n^ (k + 1)) by A2, A3;
hence f in Big_Theta (seq_n^ (k + 1)) by A36, XBOOLE_0:def 4; :: thesis: verum