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