:: Polynomially Bounded Sequences and Polynomial Sequences
:: by Hiroyuki Okazaki and Yuichi Futa
::
:: Received June 30, 2015
:: Copyright (c) 2015-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, REAL_1, SUBSET_1, SEQ_1, FDIFF_1, FUNCT_1, PARTFUN1,
PARTFUN3, ARYTM_1, VALUED_0, ORDINAL2, CARD_1, RELAT_1, ARYTM_3,
XXREAL_0, COMPLEX1, NAT_1, TARSKI, VALUED_1, FUNCT_2, SQUARE_1, XBOOLE_0,
ORDINAL4, LIMFUNC1, FUNCT_7, ASYMPT_1, POWER, ASYMPT_0, FINSET_1,
ORDINAL1, INT_1, CARD_3, AFINSQ_1, FINSEQ_1, TAYLOR_1, ASYMPT_2;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1,
PARTFUN1, FUNCT_2, FINSET_1, PARTFUN2, PARTFUN3, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, SQUARE_1, NAT_1, INT_1, VALUED_0, COMPLEX1, VALUED_1,
SEQ_1, RFUNCT_1, RVSUM_1, FDIFF_1, POWER, SERIES_1, LIMFUNC1, ASYMPT_0,
ASYMPT_1, AFINSQ_1, TAYLOR_1, AFINSQ_2;
constructors REAL_1, SQUARE_1, RCOMP_1, PARTFUN2, PARTFUN3, LIMFUNC1, FDIFF_1,
RELSET_1, RVSUM_1, NEWTON, PREPOWER, SERIES_1, ASYMPT_0, AFINSQ_2,
ASYMPT_1, TAYLOR_1, SIN_COS;
registrations ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, MEMBERED,
POWER, FCONT_3, VALUED_0, VALUED_1, SQUARE_1, AFINSQ_1, AFINSQ_2,
XBOOLE_0, RELAT_1, INT_1, ASYMPT_0, ASYMPT_1, FUNCT_1, PARTFUN3;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities SQUARE_1, SUBSET_1, LIMFUNC1, AFINSQ_1, ORDINAL1, TAYLOR_1,
ASYMPT_0;
expansions TARSKI, FUNCT_1, FUNCT_2, FDIFF_1, ASYMPT_0, PARTFUN3;
theorems TARSKI, FUNCT_1, FUNCT_2, NAT_1, SEQ_1, SEQM_3, ABSVALUE, PARTFUN3,
RFUNCT_1, FDIFF_1, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, COMPLEX1,
XREAL_1, XXREAL_0, ORDINAL1, VALUED_1, XXREAL_1, VALUED_0, XREAL_0,
AFINSQ_1, AFINSQ_2, INT_1, ASYMPT_0, ASYMPT_1, POWER, PRE_FF, FDIFF_2,
TAYLOR_1, FIB_NUM2, ENTROPY1, PREPOWER, NEWTON;
schemes NAT_1, SEQ_1, AFINSQ_2;
begin :: Preliminaries
theorem
for m,k be Nat st 1 <= m holds 1 <= m to_power k
proof
let m,n be Nat;
per cases;
suppose n = 0;
hence thesis by POWER:24;
end;
suppose
A1: n <> 0;
assume 1 <= m;
then 1 < m or 1 = m by XXREAL_0:1;
hence thesis by A1,POWER:26,35;
end;
end;
LMC31X:
for m,n be Nat st 2 <= m holds n < m to_power n by NEWTON:86;
theorem LMC31B:
for m,n be Nat holds m <= m to_power (n+1)
proof
let m,n be Nat;
per cases by NAT_1:14;
suppose m = 0;
hence thesis;
end;
suppose
A1: 1 <= m;
1 <= n+1 by NAT_1:11; then
m to_power 1 <= m to_power (n+1) by A1,PRE_FF:8;
hence thesis by NEWTON:5;
end;
end;
theorem
for m,n be Nat st 2 <= m holds n+1 <= m to_power n by NEWTON:85;
theorem LMC31D:
for k be Nat holds 2*k <= 2 to_power k
proof
defpred P[Nat] means 2*$1 <= 2 to_power $1;
P1:P[0];
P2: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A1: P[n];
per cases;
suppose n=0;
hence 2*(n+1) <= 2 to_power (n+1) by POWER:25;
end;
suppose n <> 0; then
n-1 in NAT by INT_1:5,NAT_1:14;
then reconsider m=n-1 as Nat;
A3: 2 <= 2 to_power (m+1) by LMC31B;
A2: 2 to_power (n+1) = 2 to_power n * 2 to_power 1 by POWER:27
.= 2 to_power n * 2 by POWER:25
.= 2 to_power n + 2 to_power n;
2*n + 2 <= 2 to_power n + 2 to_power n by A3,XREAL_1:7,A1;
hence 2*(n+1) <= 2 to_power (n+1) by A2;
end;
end;
for n be Nat holds P[n] from NAT_1:sch 2(P1,P2);
hence thesis;
end;
theorem LMC31E:
for k,n be Nat st k <= n holds n+k <= 2 to_power n
proof
let k be Nat;
defpred P[Nat] means
$1 + k + k <= 2 to_power ($1 + k);
2*k <= 2 to_power k by LMC31D; then
P1:P[0];
P2: for n be Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume A1: P[n];
A2: 2 to_power (k+(n+1)) = 2 to_power ((k+n)+1)
.= 2 to_power (k+n) * 2 to_power 1 by POWER:27
.= 2 to_power (k+n) * 2 by POWER:25
.= 2 to_power (k+n) + 2 to_power (k+n);
1 <= 2 to_power (k+n)
proof
per cases;
suppose k+n = 0;
hence 1 <= 2 to_power (k+n) by POWER:24;
end;
suppose k+n <> 0;
hence 1 <= 2 to_power (k+n) by POWER:35;
end;
end; then
n+k+k+1 <= 2 to_power (k+n) + 2 to_power (k+n) by XREAL_1:7,A1;
hence (n+1) +k +k <= 2 to_power ((n+1)+k) by A2;
end;
X1: for n be Nat holds P[n] from NAT_1:sch 2(P1,P2);
let n be Nat;
assume k <= n; then
n-k in NAT by INT_1:5;
then reconsider m=n-k as Nat;
m + k + k <= 2 to_power (m + k) by X1;
hence n+k <= 2 to_power n;
end;
theorem LMC31G:
for k,m be Nat st 2*k + 1 <= m holds
2 to_power k <= (2 to_power m) / m
proof
let k,m be Nat;
assume A1: 2*k +1 <= m;
2*k <= 2*k +1 by NAT_1:11; then
k+k <= m by A1,XXREAL_0:2; then
X1: k+k-k <= m -k by XREAL_1:9;
then m -k in NAT by INT_1:3; then
reconsider n=m-k as Nat;
A2: n+k <= 2 to_power n by LMC31E,X1;
2 to_power (n+k) /2 to_power n
<= 2 to_power (n+k) / (n+k) by A1,A2,XREAL_1:118; then
2 to_power (n+k-n) <= 2 to_power (n+k) / (n+k) by POWER:29;
hence 2 to_power k <= 2 to_power m /m;
end;
Lm5: dom(id [#]REAL)=[#]REAL &
(for x be Real holds (id [#]REAL).x=x) &
for x be Real holds (id [#]REAL)
is_differentiable_in x & diff((id [#]REAL),x)=1
proof
set g = id [#]REAL;
thus dom g = [#]REAL;
thus for d be Real holds g.d = d by FUNCT_1:17,XREAL_0:def 1;
A6: for d be Real st d in REAL holds g.d = 1*d + 0
by FUNCT_1:17; then
A7: g is_differentiable_on dom(g) by FDIFF_1:23;
for x be Real holds g is_differentiable_in x & diff(g,x)=1
proof
let dd be Real;
reconsider d=dd as Element of REAL by XREAL_0:def 1;
g is_differentiable_in d by A7;
hence g is_differentiable_in dd;
thus diff(g,dd)=(g`|dom(g)).d by A7,FDIFF_1:def 7
.= 1 by A6,FDIFF_1:23;
end;
hence thesis;
end;
theorem CPOWER57:
for a,b,c be Real st 1 < a & 0 < b & b <= c holds
log(a,b) <= log(a,c)
proof
let a,b,c be Real;
assume AS: 1 < a & 0 < b & b <= c;
now per cases by AS,XXREAL_0:1;
case b < c;
hence log(a,b) < log(a,c) by POWER:57,AS;
end;
case b = c;
hence log(a,b) =log(a,c);
end;
end;
hence thesis;
end;
LEMC01:
for x,n,a be Nat st 0 < a & a <= x holds
a to_power n <= x to_power n by PREPOWER:9;
theorem LC5aa:
for n be Nat, a be Real st 1 < a holds
a to_power n < a to_power (n+1)
proof
let n be Nat, a be Real;
assume AS: 1 < a;
LP3:a to_power (n+1) = (a to_power n)*(a to_power 1) by FIB_NUM2:5
.=(a to_power n)*a by POWER:25;
a to_power n > 0 by POWER:34,AS;then
1*(a to_power n) < (a to_power n)*a by XREAL_1:68,AS;
hence thesis by LP3;
end;
theorem LC5a:
for n be Nat, a be Real st 1 <= a holds
a to_power n <= a to_power (n+1)
proof
let n be Nat, a be Real;
assume AS: 1 <= a;
LP3:a to_power (n+1) = (a to_power n)*(a to_power 1) by FIB_NUM2:5
.=(a to_power n)*a by POWER:25;
a to_power n > 0 by POWER:34,AS;then
1*(a to_power n) <= (a to_power n)*a by XREAL_1:64,AS;
hence thesis by LP3;
end;
theorem Lm6:
ex g be PartFunc of REAL,REAL st
dom(g)=right_open_halfline(0) &
(for x be Real st x in right_open_halfline(0) holds g.x=log(2,x))
&
g is_differentiable_on right_open_halfline(0) &
for x be Real st x in right_open_halfline(0)
holds g is_differentiable_in x
& diff(g,x)=(log(2,number_e))/x
& 0 < diff(g,x)
proof
set g = (log(2,number_e)) (#)ln;
take g;
thus
A3: dom g = dom ln by VALUED_1:def 5
.= right_open_halfline(0) by TAYLOR_1:def 2;
E1: number_e > 1 by XXREAL_0:2,TAYLOR_1:11;
thus for d be Real st d in right_open_halfline(0) holds g.d = log(2,d)
proof
let d be Real;
assume A51:d in right_open_halfline(0); then
reconsider d0 = d as Element of right_open_halfline(0);
d in {y where y is Real: 0<y} by XXREAL_1:230,A51; then
E3: ex y be Real st d=y & 0 < y;
thus g.d = (log(2,number_e)) *ln.d by A3,A51,VALUED_1:def 5
.= (log(2,number_e))*log(number_e,d0) by TAYLOR_1:def 2
.= log(2,d) by E1,E3,POWER:56;
end;
thus g is_differentiable_on right_open_halfline(0)
by FDIFF_1:20,A3,TAYLOR_1:18;
thus for x be Real
st x in right_open_halfline(0) holds g is_differentiable_in x
& diff(g,x)=(log(2,number_e))/x
& 0 < diff(g,x)
proof
let x be Real;
assume A1:x in right_open_halfline(0);
A2:ln is_differentiable_in x by A1,TAYLOR_1:18;
hence g is_differentiable_in x by FDIFF_1:15;
A3: diff(ln,x)=1/x by A1,TAYLOR_1:18;
A4: diff(g,x) = (log(2,number_e)) * diff(ln,x) by FDIFF_1:15,A2;
thus diff(g,x) = (1*log(2,number_e))/x by XCMPLX_1:74,A4,A3
.= log(2,number_e)/x;
A5: 0 < diff(ln,x) by A1,TAYLOR_1:18;
log(2,2) < log(2,number_e) by POWER:57,TAYLOR_1:11;
then 0 < log(2,number_e) by POWER:52;
hence 0 < diff(g,x) by A4,A5;
end;
end;
theorem LMC31H2:
ex f be PartFunc of REAL,REAL st
right_open_halfline (number_e) = dom f &
(for x be Real st x in dom f holds f.x = x/log(2,x) ) &
f is_differentiable_on right_open_halfline (number_e) &
(for x0 being Real st x0 in right_open_halfline (number_e) holds
0 <= diff (f,x0) )
& f is non-decreasing
proof
consider g be PartFunc of REAL,REAL such that
A2:dom(g)=right_open_halfline(0) and
A3:(for x be Real st x in right_open_halfline(0)
holds g.x=log(2,x)) and
A4: g is_differentiable_on right_open_halfline(0) and
A5: for x be Real st x in right_open_halfline(0)
holds g is_differentiable_in x
& diff(g,x)=(log(2,number_e))/x
& 0 < diff(g,x) by Lm6;
set g0 = g | right_open_halfline (number_e);
AA6:
for x be object st x in right_open_halfline (number_e) holds
x in right_open_halfline(0)
proof
let x be object;
assume x in right_open_halfline (number_e); then
x in {y where y is Real: number_e<y} by XXREAL_1:230;
then consider y be Real such that
AA2: x=y & number_e < y;
x in {z where z is Real: 0 <z} by TAYLOR_1:11,AA2;
hence thesis by XXREAL_1:230;
end;
then A6: right_open_halfline (number_e) c= right_open_halfline(0);
then
A7: dom g0 = right_open_halfline (number_e) by RELAT_1:62,A2;
set f = (id [#]REAL ) / g0;
G0: g0 " {0} = {}
proof
assume g0 " {0} <> {}; then
consider x be object such that
P01: x in g0 " {0} by XBOOLE_0:def 1;
P02: x in dom g0 & g0.x in {0}
by P01,FUNCT_1:def 7;
P04: g0.x = 0 by TARSKI:def 1,P02;
reconsider x0=x as Real by P01;
x0 in {y where y is Real: number_e<y} by XXREAL_1:230,P02,A7;
then
ex y be Real st x=y & number_e < y;
then
E5: 2 < x0 by XXREAL_0:2,TAYLOR_1:11;
F3: g0.x = g.x by FUNCT_1:49,P02,A7
.=log(2,x0) by A3,AA6,P02,A7;
log(2,2) <= log(2,x0) by E5,PRE_FF:10;
hence contradiction by POWER:52,P04,F3;
end;
take f;
thus
P1: dom f = dom (id [#]REAL )
/\ ((dom g0) \ (g0 " {0})) by RFUNCT_1:def 1
.= right_open_halfline(number_e) by XBOOLE_1:28,A7,G0;
thus for x be Real st x in dom f holds f.x = x/log(2,x)
proof
let x be Real;
assume F1: x in dom f;
thus f.x = (id [#]REAL ).x * (g0 . x) " by F1,RFUNCT_1:def 1
.= x * (g0.x) " by Lm5
.= x * (g.x) " by P1,F1,FUNCT_1:49
.= x * (log(2,x)) " by A3,P1,AA6,F1
.= x * (1/log(2,x)) by XCMPLX_1:215
.= (1*x) / log(2,x) by XCMPLX_1:74
.= x / log(2,x);
end;
P3:g is_differentiable_on right_open_halfline (number_e)
by FDIFF_1:26,A4,A6; then
XP:
g0 is_differentiable_on right_open_halfline (number_e) &
g `| right_open_halfline (number_e)
= g0 `| right_open_halfline (number_e) by FDIFF_2:16;
F12: for x be Real
st x in (right_open_halfline (number_e))
holds f is_differentiable_in x
& diff(f,x) = (log(2,x) - log(2,number_e))/(log(2,x))^2
proof
let x be Real;
assume F1: x in (right_open_halfline (number_e));
then FA: x in right_open_halfline(0) by AA6;
FB:diff(g,x) = (g `| right_open_halfline (number_e)).x
by P3,F1,FDIFF_1:def 7
.=diff(g0,x) by XP,F1,FDIFF_1:def 7;
x in {y where y is Real: number_e<y} by XXREAL_1:230,F1; then
EE5: ex y be Real st x=y & number_e < y;
then
E5: 2 < x by XXREAL_0:2,TAYLOR_1:11;
F3: g0.x = g.x by F1,FUNCT_1:49
.=log(2,x) by F1,AA6,A3;
log(2,2) <= log(2,x) by E5,PRE_FF:10; then
F2: 0 < g0.x by F3,POWER:52;
F3: id [#]REAL is_differentiable_in x by Lm5;
F6:g0 is_differentiable_in x by P3,F1;
diff(f,x) = (diff(id [#]REAL,x) * g0.x
- diff(g0,x) * (id [#]REAL).x)/(g0.x)^2 by FDIFF_2:14,F2,F3,F6
.=(1 * g0.x - diff(g0,x) * (id [#]REAL).x)/(g0.x)^2 by Lm5
.=(1 * g0.x - diff(g0,x) * x) /(g0.x)^2 by Lm5
.=(1 * g.x - diff(g,x) * x) /(g0.x)^2 by F1,FUNCT_1:49,FB
.=(1 * g.x - diff(g,x) * x) /(g.x)^2 by F1,FUNCT_1:49
.=(1 * log(2,x) - diff(g,x) * x) /(g.x)^2 by A3,F1,AA6
.=(1 * log(2,x) - diff(g,x) * x) /(log(2,x))^2 by A3,AA6,F1
.=(1 * log(2,x) - ((log(2,number_e))/x)* x) /(log(2,x))^2 by A5,FA
.=(log(2,x) - log(2,number_e))
/(log(2,x))^2 by XCMPLX_1:87,EE5,TAYLOR_1:11;
hence thesis by FDIFF_2:14,F2,F3,F6;
end;
hence
P3: f is_differentiable_on right_open_halfline (number_e) by P1;
thus for x be Real st x
in right_open_halfline(number_e) holds 0 <= diff(f,x)
proof
let x be Real;
assume F1: x in right_open_halfline(number_e); then
P41: diff(f,x) = (log(2,x) - log(2,number_e)) /(log(2,x))^2 by F12;
x in {y where y is Real: number_e<y} by XXREAL_1:230,F1; then
ex y be Real st x=y & number_e < y; then
log(2,number_e) < log(2,x) by POWER:57,TAYLOR_1:11; then
0 < log(2,x) - log(2,number_e) by XREAL_1:50;
hence thesis by P41;
end;
hence thesis by P1,P3,FDIFF_2:35;
end;
theorem LMC31H1:
for x,y be Real st number_e < x & x <= y holds
x/log(2,x) <= y/log(2,y)
proof
let x,y be Real;
assume AS: number_e < x & x <= y;
consider f be PartFunc of REAL,REAL such that
A11: right_open_halfline number_e = dom f and
A12:(for x be Real st x in dom f holds f.x = x/log(2,x) ) and
f is_differentiable_on right_open_halfline number_e and
(for x0 being Real st
x0 in right_open_halfline number_e holds 0 <= diff (f,x0) ) and
A15: f is non-decreasing by LMC31H2;
number_e < y by AS,XXREAL_0:2; then
x in {g where g is Real : number_e<g} &
y in {g where g is Real : number_e<g} by AS; then
A3: x in dom f & y in dom f by A11,XXREAL_1:230; then
A4: f .x <= f .y by AS,A15,VALUED_0:def 15;
f.x =x/log(2,x) by A12,A3;
hence thesis by A4,A12,A3;
end;
theorem LMC31H:
for k be Nat st number_e < k holds
ex N be Nat st for n be Nat st N<=n holds 2 to_power k <= n/log(2,n)
proof let k be Nat;
assume
K1: number_e < k;
set N = 2 to_power (2*k + 1);
k*1 <= 2*k by XREAL_1:64; then
X1: k+ 0 < 2*k + 1 by XREAL_1:8;
2*k + 1 <= 2 to_power (2*k + 1) by LMC31X; then
k < 2 to_power (2*k + 1) by X1,XXREAL_0:2; then
DD: number_e < N by K1,XXREAL_0:2;
take N;
let n be Nat;
assume N<=n; then
B0: N/log(2,N) <=n/log(2,n) by LMC31H1,DD;
X0: 0 < 2 to_power (2*k + 1) by POWER:34; then
X1: 2*k + 1 = log(2,N) by POWER:def 3;
reconsider m= log(2,N) as Nat by X0,POWER:def 3;
X3: 2 to_power k <= (2 to_power m) / m by LMC31G,X1;
(2 to_power m) = N by POWER:def 3,X0;
hence thesis by B0,XXREAL_0:2,X3;
end;
LMC31: for r be Real ex N be Element of NAT
st for n be Nat st N <= n holds r < n /log(2,n)
proof
let r0 be Real;
ex r be Real st 0 < r & r0 <= r
proof
per cases;
suppose A1:0 < r0;
take r0;
thus 0 < r0 & r0 <= r0 by A1;
end;
suppose A2:not 0 < r0;
take 1;
thus 0 < 1 & r0 <= 1 by A2;
end;
end;
then consider r be Real such that
AS: 0 < r & r0 <=r;
set a0 = max(log(2,r),number_e);
A01: log(2,r) <= a0 & number_e <= a0 by XXREAL_0:25;
set k = [/a0\] + 1;
a0 < k by INT_1:32;
k in NAT by INT_1:3,TAYLOR_1:11,A01;
then reconsider k as Nat;
A0: log(2,r) < k & number_e < k by A01,XXREAL_0:2,INT_1:32;
2 to_power log(2,r) < 2 to_power k by A0,POWER:39; then
A1:r < 2 to_power k by AS,POWER:def 3;
consider N be Nat such that
A2: for n be Nat st N<=n
holds 2 to_power k <= n/log(2,n) by LMC31H,A0;
reconsider N as Element of NAT by ORDINAL1:def 12;
take N;
let n be Nat;
assume N<=n; then
2 to_power k <= n/log(2,n) by A2;
then r < n /log(2,n) by A1,XXREAL_0:2;
hence r0 < n /log(2,n) by AS,XXREAL_0:2;
end;
LMC31HC:
ex N be Element of NAT
st for n be Nat st N<=n holds 4 < n/log(2,n)
proof
reconsider k = [/ number_e \] +1 as Integer;
LLC2: number_e <= [/ number_e \] by INT_1:def 7; then
LC2:number_e < k by XREAL_1:145; then
LC3: 2 < k by XXREAL_0:2,TAYLOR_1:11;
k in NAT by INT_1:3,TAYLOR_1:11;
then reconsider k as Nat;
consider N be Nat such that LC4:
for n be Nat st N <=n holds 2 to_power k <= n/log(2,n) by LMC31H,LC2;
reconsider N as Element of NAT by ORDINAL1:def 12;
take N;
let n be Nat;
assume N <=n;then
LC5: 2 to_power k <= n/log(2,n) by LC4;
4 < 2 to_power k by POWER:60,POWER:39,LC3;
hence thesis by LC5,XXREAL_0:2;
end;
theorem
for x be Nat st 1 < x holds
ex N be Nat st for n be Nat st N<=n holds 4 < n/log(x,n)
proof
let x be Nat;
assume AS: 1 < x;
log(2,x) >= log(2,2) by PRE_FF:10,AS,NAT_1:23; then
AS2: 1 <= log(2,x) by POWER:52;
consider N be Nat such that LL1: for n be Nat st N<=n
holds 4 < n/log(2,n) by LMC31HC;
take N;
let n be Nat;
assume N <= n;then
CL1: 4 < n/log(2,n) by LL1;
then 0 <> n;then
log(2,n) = log(2,x)*log(x,n) by POWER:56,AS;then
4*log(2,x) < n/(log(x,n)*log(2,x)) *log(2,x) by AS2,XREAL_1:68,CL1;
then
4*log(2,x) < ( n/log(x,n)) *(1/log(2,x)) *log(2,x) by XCMPLX_1:103;
then
4*log(2,x) < ( n/log(x,n)) * (log(2,x)* (1/log(2,x)));then
TT11:4*log(2,x) < ( n/log(x,n))*1 by XCMPLX_1:106,AS2;
4*1 <= 4*log(2,x) by XREAL_1:64,AS2;
hence thesis by TT11,XXREAL_0:2;
end;
theorem
for x be Nat st 1 < x holds
ex N,c be Nat st
for n be Nat st N <= n holds n to_power x <= c * (x to_power n)
proof
let x be Nat;
assume AS1:1 < x;
consider N0 be Element of NAT
such that
P1: for n be Nat
st N0 <=n holds x/log(2,x) < n /log(2,n) by LMC31;
set N=N0+2;
reconsider N as Nat;
reconsider c = 1 as Element of NAT;
take N,c;
let n be Nat;
assume AS2: N<= n;
N0 <= N by NAT_1:12;
then N0 <= n by XXREAL_0:2,AS2; then
E1: x/log(2,x) < n /log(2,n) by P1;
1+1 <= x by AS1,NAT_1:13;
then log(2,2) <= log(2,x) by PRE_FF:10; then
P2: 0 < log(2,x) by POWER:52;
2 <= N by NAT_1:11; then
2 <= n by XXREAL_0:2,AS2; then
log(2,2) <= log(2,n) by PRE_FF:10; then
P3: 0 < log(2,n) by POWER:52; then
x/log(2,x) * log(2,n) < n /log(2,n) * log(2,n) by XREAL_1:68,E1;
then
x/log(2,x) * log(2,n) < n by P3,XCMPLX_1:87; then
log(2,n)*(x/log(2,x))*log(2,x) < n *log(2,x) by XREAL_1:68,P2;
then log(2,n)*((x/log(2,x))*log(2,x)) < n *log(2,x); then
PP4:log(2,n)*x < n *log(2,x) by P2,XCMPLX_1:87;
P5: 2 to_power (log(2,n)*x)
= 2 to_power (log(2,n)) to_power x by POWER:33
.= n to_power x by POWER:def 3,AS2;
2 to_power (n *log(2,x)) = 2 to_power (log(2,x)) to_power n by POWER:33
.= x to_power n by AS1,POWER:def 3;
hence thesis by PP4,P5,POWER:39;
end;
theorem N2POWINPOLY:
for x be Nat st 1 < x holds
not ex N,c be Nat st
for n be Nat st N <= n holds 2 to_power n <= c * (n to_power x)
proof
let x be Nat;
assume AS1:1 < x;
assume ASC:ex N,c be Nat st
for n be Nat st N <= n holds
2 to_power n <= c * (n to_power x);
consider N be Nat such that
ASC1: ex c be Nat st
for n be Nat st N <= n holds
2 to_power n <= c * (n to_power x) by ASC;
N <> 0
proof
assume N=0;then
consider c be Nat such that LNT:
for n be Nat st 0 <= n holds
2 to_power n <= c * ( n to_power x) by ASC1;
2 to_power 0 <= c * ( 0 to_power x) by LNT;then
2 to_power 0 <= c * 0 by POWER:42,AS1;
hence contradiction by POWER:24;
end;
then
LPNN2:0 < N;
consider c be Nat such that
ASC2: for n be Nat st N <= n holds
2 to_power n <= c * (n to_power x) by ASC1;
ex n be Element of NAT st N <= n & 0 < n - x/4
proof
now per cases;
case AC1: x/4 < N;
reconsider n = N+1 as Element of NAT;
take n;
thus N <= n by INT_1:6;then
x/4 < n by AC1,XXREAL_0:2;
hence 0 < n- x/4 by XREAL_1:50;
end;
case AC2: N <= x/4;
reconsider n = [/x/4 \] + 1 as Integer;
AC33: x/4 <= [/ x/4 \] by INT_1:def 7;then
AC3:x/4 +0 < [/ x/4 \] +1 by XREAL_1:8;
reconsider n as Element of NAT;
take n;
thus 0 < n -x/4 by AC3,XREAL_1:50;
thus N <= n by AC3,AC2,XXREAL_0:2;
end;
end;
hence thesis;
end;then
consider n be Element of NAT such that
ASC3: N <= n & 0 < n - x/4;
XC1: 2 to_power n <= c * ( n to_power x) by ASC2,ASC3;
ZZ1:0 <n & 1 <x by AS1,ASC3;
TEZ1: 0 <c
proof
assume not 0 < c; then
2 to_power n <= 0 * (n to_power x) by XC1;
hence contradiction by POWER:34;
end;
ASC22: for k be Nat st 1 <= k holds
2 to_power (k*n) <= c * ((k*n) to_power x)
proof
let k be Nat;
assume 1 <= k;then
1*N <= k*n by ASC3,XREAL_1:66;
hence thesis by ASC2;
end;
HCL1:
for k be Nat st 1 <= k holds
k*n <= log(2, c) + x*log(2, k) + x*log(2,n)
proof
let k be Nat;
assume ASK: 1 <= k; then
L1: 2 to_power (k*n) <= c * ( (k*n) to_power x) by ASC22;
L3:0 < (k*n) to_power x by POWER:34,LPNN2,ASC3,ASK;
0 < 2 to_power(k*n) by POWER:34;then
log (2,2 to_power (k*n)) <= log(2, c * ( (k*n) to_power x))
by L1,CPOWER57;then
(k*n)* log (2,2) <= log(2, c * ( (k*n) to_power x))
by POWER:55;then
(k*n)* 1 <= log(2, c * ( (k*n) to_power x)) by POWER:52;then
k*n <= log(2, c ) + log(2, (k*n) to_power x)
by POWER:53,TEZ1,L3;then
k*n <= log(2, c ) + x*log(2, k*n) by POWER:55,LPNN2,ASC3,ASK; then
k*n <= log(2, c ) + x*(log(2, k) + log(2,n)) by POWER:53,ASK,ZZ1;
hence k*n <= log(2, c ) + x*log(2, k) + x*log(2,n);
end;
consider Z be Element of NAT such that
HCL2: for k be Nat st Z <= k holds 4 < k/log(2,k) by LMC31HC;
HEXK:
ex k be Nat st Z <= k &
(log(2, c) + x*log(2,n))/ (n - x/4) <= k
proof
now per cases;
case AC1: (log(2, c ) + x*log(2,n))/ (n - x/4) < Z;
reconsider k = Z+1 as Element of NAT;
take k;
thus Z <= k by INT_1:6;
hence (log(2, c ) + x*log(2,n))/ (n - x/4) < k by AC1,XXREAL_0:2;
end;
case AC2: Z <= (log(2, c ) + x*log(2,n))/ (n - x/4);
reconsider
k = [/ (log(2, c) + x*log(2,n))/ (n - x/4) \] + 1 as Integer;
AC3P:(log(2, c) + x*log(2,n))/ (n - x/4)
<= [/ (log(2, c) + x*log(2,n))/ (n - x/4) \] by INT_1:def 7;then
AC3:(log(2, c) + x*log(2,n))/ (n - x/4) +0
<= [/ (log(2, c) + x*log(2,n))/ (n - x/4) \] +1 by XREAL_1:8;
reconsider k as Element of NAT by INT_1:3,AC2;
take k;
thus (log(2, c) + x*log(2,n))/ (n - x/4) <= k by AC3;
thus Z <= k by AC3,AC2,XXREAL_0:2;
end;
end;
hence thesis;
end;
ex k be Nat st Z <= k &
(log(2, c ) + x*log(2,n))/ (n - x/4) <= k & 1 < k
proof
consider k be Nat such that HEXK2: Z <= k &
(log(2, c ) + x*log(2,n))/ (n - x/4) <= k by HEXK;
reconsider a = k+2 as Nat;
take a;
CC1:0 + 2 <= k+2 by XREAL_1:6;
k <= a by NAT_1:11;
hence thesis by CC1,XXREAL_0:2,HEXK2;
end; then
consider k be Nat such that
HCL3: Z <= k & 1 <k &
(log(2, c ) + x*log(2,n))/ (n - x/4) <= k;
FF0:(log(2, c ) + x*log(2,n))/ (n - x/4)
* (n - x/4) <= k *(n - x/4) by HCL3,ASC3,XREAL_1:64;
HCL4: 4 < k/log(2,k) by HCL2,HCL3;
HCL7:
k*n <= log(2, c ) + x*log(2, k) + x*log(2,n) by HCL1,HCL3;
HCL8: 0 < log(2,k) by ENTROPY1:4,HCL3; then
4*log(2,k) < k/log(2,k) *log(2,k) by HCL4,XREAL_1:68;then
4*log(2,k) < k*log(2,k) /log(2,k) by XCMPLX_1:74;then
4*log(2,k) < k*(log(2,k) /log(2,k)) by XCMPLX_1:74;then
4*log(2,k) < k*(1) by XCMPLX_1:60,HCL8;then
log(2,k)*4*x < k*x by XREAL_1:68,AS1; then
log(2,k)*x*4/4 < k*x/4 by XREAL_1:74; then
k*n - k*x/4 < log(2, c) + x*log(2, k) + x*log(2,n) -x*log(2,k)
by HCL7,XREAL_1:15;
hence contradiction by FF0,XCMPLX_1:87,ASC3;
end;
FROMASYMPT1t11:
for a,b be Nat st a < b holds
seq_n^ a in Big_Oh (seq_n^ b)
proof
let a,b be Nat;
assume AS:a< b;
set g = seq_n^ b;
set f = seq_n^ a;
LL11: now
let n be Element of NAT;
assume A2: n >= 2;
then A3: n > 1 by XXREAL_0:2;
A4: (seq_n^ a) . n = n to_power a by A2, ASYMPT_1:def 3;
(seq_n^ b) . n = n to_power b by A2,ASYMPT_1:def 3;
hence (seq_n^ a) . n <= 1 * ((seq_n^ b) . n) by AS,A3, A4, POWER:39;
thus (seq_n^ a) . n >= 0 by A4;
end;
reconsider f as Element of Funcs (NAT,REAL) by FUNCT_2:8;
reconsider g as eventually-nonnegative Real_Sequence;
f in Big_Oh (g) by LL11;
hence thesis;
end;
theorem
for a,b be Nat st a <= b holds
seq_n^ a in Big_Oh (seq_n^ b)
proof
let a,b be Nat;
assume AS: a <= b;
per cases by AS,XXREAL_0:1;
suppose a = b;
hence thesis by ASYMPT_0:10;
end;
suppose a <b;
hence thesis by FROMASYMPT1t11;
end;
end;
theorem
for x be Nat st 1 < x holds
not ex N,c be Nat st
for n be Nat st N <= n holds x to_power n <= c * (n to_power x)
proof
let x be Nat;
assume AS: 1 < x;
assume CNT: ex N,c be Nat st
for n be Nat st N <= n holds
x to_power n <= c * (n to_power x);
ex N,c be Nat st for n be Nat st N <= n holds
2 to_power n <= c * (n to_power x)
proof
consider N,c be Nat such that CNT2:
for n be Nat st N <= n holds
x to_power n <= c * (n to_power x) by CNT;
take N,c;
let n be Nat;
assume N <= n;then
LCX1: x to_power n <= c * ( n to_power x) by CNT2;
1+1 <= x by AS,INT_1:7;then
2 to_power n <= x to_power n by LEMC01;
hence thesis by LCX1,XXREAL_0:2;
end;
hence contradiction by AS,N2POWINPOLY;
end;
theorem LC4:
for a be non negative Real, n be Nat st 1 <= n
holds 0 < (seq_n^(a)).n
proof
let a be non negative Real, n be Nat;
AA: n in NAT by ORDINAL1:def 12;
assume AS:1 <= n;then
(seq_n^(a)).n = n to_power a by AA,ASYMPT_1:def 3;
hence thesis by AS,POWER:34;
end;
begin :: Polynomially Bounded Sequences
definition
let p be Real_Sequence;
attr p is polynomially-bounded means
ex k be Nat st p in Big_Oh(seq_n^(k));
end;
theorem
for f be Real_Sequence st f is non polynomially-bounded holds
for k be Nat holds not f in Big_Oh(seq_n^(k));
theorem
for f be Real_Sequence st
for k be Nat holds not f in Big_Oh(seq_n^(k))
holds f is non polynomially-bounded;
theorem
for a be positive Real holds seq_a^(a,1,0) is positive
proof
let a be positive Real;
now let n be Nat;
seq_a^(a,1,0).n = a to_power (1*n+0) by ASYMPT_1:def 1
.= a to_power n;
hence 0 < seq_a^(a,1,0).n by POWER:34;
end;
hence thesis;
end;
theorem
for a be Real st 1 <= a holds seq_a^(a,1,0) is non-decreasing
proof
let a be Real;
assume AS: 1 <= a;
for n be Nat holds seq_a^(a,1,0).n <= seq_a^(a,1,0).(n+1)
proof
let n be Nat;
L2:(seq_a^(a,1,0)).n =a to_power (1*n+0) by ASYMPT_1:def 1
.= a to_power n;
(seq_a^(a,1,0)).(n+1) =a to_power (1*(n+1)+0) by ASYMPT_1:def 1
.= a to_power (n+1);
hence thesis by L2, LC5a,AS;
end;
hence thesis by SEQM_3:def 8;
end;
theorem
for a be Real st 1 < a holds seq_a^(a,1,0) is increasing
proof
let a be Real;
assume AS: 1 < a;
C1:for n be Element of NAT holds
seq_a^(a,1,0).n < seq_a^(a,1,0).(n+1)
proof
let n be Element of NAT;
L2:(seq_a^(a,1,0)).n =a to_power (1*n+0) by ASYMPT_1:def 1
.= a to_power n;
(seq_a^(a,1,0)).(n+1) =a to_power (1*(n+1)+0) by ASYMPT_1:def 1
.= a to_power (n+1);
hence thesis by L2,LC5aa,AS;
end;
reconsider S = seq_a^(a,1,0) as Real_Sequence;
for n be Nat holds S.n < S.(n+1)
proof
let n be Nat;
reconsider n as Element of NAT by ORDINAL1:def 12;
seq_a^(a,1,0).n < seq_a^(a,1,0).(n+1) by C1;
hence thesis;
end;
hence thesis by SEQM_3:def 6;
end;
theorem
for a be Nat st 1 < a holds
seq_a^(a,1,0) is non polynomially-bounded
proof
let a be Nat;
assume AS1: 1 < a;
assume seq_a^(a,1,0) is polynomially-bounded; then
consider k be Nat such that CL1:
seq_a^(a,1,0) in Big_Oh(seq_n^(k));
reconsider f = seq_n^(k) as eventually-positive Real_Sequence;
reconsider t = seq_a^(a,1,0)
as eventually-nonnegative Real_Sequence by AS1;
t in Big_Oh(f) &
for n be Element of NAT st 1 <= n holds 0< (f).n by LC4,CL1;
then consider c be Real such that
LL1: c > 0 & for n be Element of NAT st n >= 1 holds
seq_a^(a,1,0).n <= c*(seq_n^(k)).n by ASYMPT_0:8;
TLCPP:for n be Nat st n >= 1 holds
2 to_power n <= c*(n to_power k)
proof
let n be Nat;
ZZ: n in NAT by ORDINAL1:def 12;
assume AT1:n >= 1;then
seq_a^(a,1,0).n <= c*((seq_n^(k)).n) by ZZ,LL1;then
a to_power (1*n +0) <= c*((seq_n^(k)).n) by ASYMPT_1:def 1; then
TZ1:a to_power (n) <= c*(n to_power k) by ASYMPT_1:def 3,AT1;
1+1 <= a by AS1,INT_1:7;then
2 to_power n <= a to_power n by LEMC01;
hence thesis by XXREAL_0:2,TZ1;
end;
TLCPP2:ex N,b be Nat st
for n be Nat st N <= n holds
2 to_power n <= b*(n to_power k)
proof
consider N be Nat such that TLCPP3:
for n be Nat st N <= n holds
2 to_power n <= c*(n to_power k) by TLCPP;
set b = [/ c \];
TLCPP4: c <= b by INT_1:def 7;
reconsider b as Element of NAT by INT_1:3, LL1;
take N,b;
for n be Nat st N <= n holds
2 to_power n <= b*(n to_power k)
proof
let n be Nat;
assume N <= n;then
TLCPP5: 2 to_power n <= c*(n to_power k) by TLCPP3;
c*(n to_power k) <= b*(n to_power k) by XREAL_1:64,TLCPP4;
hence thesis by TLCPP5, XXREAL_0:2;
end;
hence thesis;
end;
per cases;
suppose 1 < k;
hence contradiction by TLCPP2,N2POWINPOLY;
end;
suppose k <= 1;
then TLCPPAA: k < 2 by XXREAL_0:2;
ex N,b be Nat st
for n be Nat st N <= n holds 2 to_power n <= b*(n to_power 2)
proof
consider N,b be Nat such that TLCPPA3:
for n be Nat st N <= n holds
2 to_power n <= b*(n to_power k) by TLCPP2;
reconsider M = N+2 as Element of NAT;
TLCPPAA1: N <= M by NAT_1:11;
take M, b;
let n be Nat;
assume TLCPPAS: M <= n;then
N <= n by XXREAL_0:2,TLCPPAA1;then
TLCPPA4: 2 to_power n <= b*(n to_power k) by TLCPPA3;
2 <= N +2 by NAT_1:11;then
1 +1 <=n by TLCPPAS,XXREAL_0:2;then
1 <n by NAT_1:13;then
(n to_power k) <= (n to_power 2) by POWER:39,TLCPPAA;then
b*(n to_power k) <= b*(n to_power 2) by XREAL_1:64;
hence thesis by TLCPPA4, XXREAL_0:2;
end;
hence contradiction by N2POWINPOLY;
end;
end;
begin :: Polynomial Sequences
theorem LMXFIN1:
for x be XFinSequence of REAL,
y be Real_Sequence
holds x(#)y is finite Sequence of REAL
& dom (x(#)y) = dom x
& for i be object st i in dom x
holds (x(#)y).i = (x.i) * (y.i)
proof
let x be XFinSequence of REAL, y be Real_Sequence;
P1:dom y = NAT by FUNCT_2:def 1;
P2: dom (x(#)y) = (dom x) /\ (dom y) by VALUED_1:def 4
.= (dom x) by XBOOLE_1:28,P1; then
x(#)y is Sequence of rng (x(#)y) by ORDINAL1:31;
hence thesis by P2,VALUED_1:def 4;
end;
definition
let x be XFinSequence of REAL,
y be Real_Sequence;
redefine func x(#)y -> XFinSequence of REAL; :: redefines (#) (VALUED_1, definition)
correctness by LMXFIN1;
end;
theorem LMXFIN2:
for d be XFinSequence of REAL
holds for x,i be Nat st i in dom d holds
(d (#) seq_a^(x,1,0)).i = (d.i) * x to_power (i)
proof
let d be XFinSequence of REAL;
let x,i be Nat;
assume i in dom d;
hence (d (#) seq_a^(x,1,0)).i = (d.i) * (seq_a^(x,1,0)).i by LMXFIN1
.= (d.i) * x to_power ((1 * i) + 0) by ASYMPT_1:def 1
.= (d.i) * x to_power (i);
end;
definition
let c be XFinSequence of REAL;
func seq_p(c) -> Real_Sequence means
:defseqp:
for x be Nat holds it.x = Sum(c (#) seq_a^(x,1,0));
existence
proof
deffunc F(Nat) = Sum(c (#) seq_a^($1,1,0));
consider h being Real_Sequence such that
A1: for x being Nat holds h.x = F(x) from SEQ_1:sch 1;
take h;
thus thesis by A1;
end;
uniqueness
proof
let s1,s2 be Real_Sequence such that
A1: for x be Nat holds s1.x = Sum(c (#) seq_a^(x,1,0) ) and
A2: for x be Nat holds s2.x = Sum(c (#) seq_a^(x,1,0) );
now let x be Element of NAT;
thus s1.x=Sum(c (#) seq_a^(x,1,0) ) by A1
.= s2.x by A2;
end;
hence s1=s2;
end;
end;
LMXFIN3:
for d be XFinSequence of REAL,k be Nat st len d = k+1
holds ex a be Real,d1 be XFinSequence of REAL st len d1 = k
& d1= d | k & a = d.k & d =d1^<% a %>
proof
let d be XFinSequence of REAL,k be Nat;
assume AS: len d = k+1;
set d1= d | k;
set a = d.k;
reconsider d1 as XFinSequence of REAL;
reconsider a as Real;
take a,d1;
thus thesis by AFINSQ_1:56,AS,AFINSQ_1:54,NAT_1:11;
end;
theorem LMXFIN4:
for d be XFinSequence of REAL,k be Nat st len d = k+1 holds
ex a be Real,d1 be XFinSequence of REAL,
y be Real_Sequence st len d1 = k & d1= d | k & a = d.k & d =d1^<% a %> &
seq_p(d) = seq_p(d1) + y &
for i be Nat holds y.i = a* (i to_power k)
proof
let d be XFinSequence of REAL,k be Nat;
assume AS: len d = k+1; then
consider a be Real,d1 be XFinSequence of REAL such that
P1: len d1 = k & d1= d | k & a = d.k & d =d1^<% a %> by LMXFIN3;
deffunc F(Nat) = a* ($1 to_power k);
consider y be Real_Sequence such that
P3: for x be Nat holds y.x = F(x) from SEQ_1:sch 1;
for x be Element of NAT holds (seq_p(d)).x = (seq_p(d1) + y).x
proof
let x be Element of NAT;
Q1: (seq_p(d)).x = Sum(d (#) seq_a^(x,1,0)) by defseqp;
Q2: (seq_p(d1)).x = Sum(d1 (#) seq_a^(x,1,0)) by defseqp;
Q3: len (d (#) seq_a^(x,1,0)) = k+1 by AS,LMXFIN1;
K1: k < k+1 by NAT_1:13; then
k in Segm (k+1) by NAT_1:44;then
Q6:(d (#) seq_a^(x,1,0)).k = a* (x to_power k) by AS,P1,LMXFIN2;
Q5: (d (#) seq_a^(x,1,0))
= (d (#) seq_a^(x,1,0)) |k ^<% a* (x to_power k) %>
by Q6,Q3,AFINSQ_1:56;
Q7:len ( (d (#) seq_a^(x,1,0)) |k ) = k by AFINSQ_1:54,Q3,K1;
for i be object
st i in dom ((d (#) seq_a^(x,1,0)) |k) holds
((d (#) seq_a^(x,1,0)) |k).i = (d1 (#) seq_a^(x,1,0)).i
proof
let i be object;
assume A1: i in dom ((d (#) seq_a^(x,1,0)) |k); then
i in dom (d (#) seq_a^(x,1,0)) by RELAT_1:57; then
A2: i in dom d by LMXFIN1;
reconsider i0=i as Nat by A1;
thus ((d (#) seq_a^(x,1,0)) |k).i
= (d (#) seq_a^(x,1,0)).i by A1,FUNCT_1:47
.= (d.i) * x to_power i0 by A2,LMXFIN2
.= (d1.i) * x to_power i0 by FUNCT_1:47,A1,P1,Q7
.= (d1 (#) seq_a^(x,1,0)).i by LMXFIN2,A1,P1,Q7;
end; then
(d (#) seq_a^(x,1,0)) |k = d1 (#) seq_a^(x,1,0) by P1,LMXFIN1,Q7;
hence (seq_p(d)).x = Sum(d1 (#) seq_a^(x,1,0))
+ Sum( <% a* (x to_power k) %> ) by Q1,Q5,AFINSQ_2:55
.= (seq_p(d1)).x + a* (x to_power k) by AFINSQ_2:53,Q2
.= (seq_p(d1)).x + y.x by P3
.= ((seq_p(d1)) + y).x by SEQ_1:7;
end; then
seq_p(d) = seq_p(d1) + y;
hence thesis by P1,P3;
end;
theorem LMXFIN5:
for d be XFinSequence of REAL,k be Nat st len d = 1 holds
ex a be Real st a = d.0 &
for x be Nat holds (seq_p(d)).x = a
proof
let d be XFinSequence of REAL,k be Nat;
assume AS: len d = 1;
reconsider a=d.0 as Real;
take a;
thus a=d.0;
let x be Nat;
Q1: (seq_p(d)).x = Sum(d (#) seq_a^(x,1,0)) by defseqp;
Q3:0 in Segm 1 by NAT_1:44;
Q4:(d (#) seq_a^(x,1,0)).0 = (d.0) * ((seq_a^(x,1,0)).0) by AS,Q3,LMXFIN1
.= a* x to_power ((1 * 0) + 0) by ASYMPT_1:def 1
.= a*1 by POWER:24
.= a;
len (d (#) seq_a^(x,1,0)) = 1 by AS,LMXFIN1;
then (d (#) seq_a^(x,1,0)) = <% a %> by AFINSQ_1:34,Q4;
hence (seq_p(d)).x = a by Q1,AFINSQ_2:53;
end;
theorem LMXFIN6:
for d be XFinSequence of REAL,k be Nat
st len d = 1 & d is nonnegative-yielding holds
seq_p(d) in Big_Oh( seq_n^(k) )
proof
let d be XFinSequence of REAL,k be Nat;
assume AS: len d = 1 & d is nonnegative-yielding;
then consider a be Real such that
P1: a = d.0 & for x be Nat holds (seq_p(d)).x = a by LMXFIN5;
set y = seq_p(d);
set c = a + 1;
XA1:a + 0 < a + 1 by XREAL_1:8;
0 in Segm 1 by NAT_1:44;then
ASX: 0 <= d.0 by AS,FUNCT_1:3;
A1: now
let n be Element of NAT;
assume A2: n >= 2;
then A3: n > 1 by XXREAL_0:2;
A4: (seq_n^ k) . n = n to_power k by A2,ASYMPT_1:def 3;
1 <= ((seq_n^ k) . n)
proof
per cases;
suppose k= 0;
hence 1 <= ((seq_n^ k) . n) by A4,POWER:24;
end;
suppose 0 < k;
hence 1 <= ((seq_n^ k) . n) by A4,A3,POWER:35;
end;
end; then
1*a <= ((seq_n^ k) . n) * c by XA1,XREAL_1:66,P1,ASX;
hence y.n <= c * ((seq_n^ k) . n) by P1;
thus y.n >= 0 by P1,ASX;
end;
y is Element of Funcs (NAT,REAL) by FUNCT_2:8;
hence y in Big_Oh (seq_n^ k) by A1,P1,ASX;
end;
LMXFIN7:
for k be Nat,x,y be Real_Sequence
st x in Big_Oh( seq_n^k) & y in Big_Oh( seq_n^k)
holds x+y in Big_Oh( seq_n^k )
proof
let k be Nat,x,y be Real_Sequence;
assume AS: x in Big_Oh( seq_n^k)
& y in Big_Oh( seq_n^k);
consider t be Element of Funcs (NAT,REAL) such that
P1: x=t & ex c being Real,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 ) by AS;
consider w be Element of Funcs (NAT,REAL) such that
P2: y=w & ex c being Real,N being Element of NAT st c > 0 &
for n being Element of NAT st n >= N holds
( w . n <= c * ((seq_n^k).n) & w . n >= 0 ) by AS;
consider c1 being Real,N1 being Element of NAT such that
P11: c1 > 0 &
for n being Element of NAT st n >= N1 holds
( x . n <= c1 * ((seq_n^k).n) & x . n >= 0 ) by P1;
consider c2 being Real,N2 being Element of NAT such that
P21:
c2 > 0 & for n being Element of NAT st n >= N2 holds
( y . n <= c2 * ((seq_n^k).n) & y . n >= 0) by P2;
set c = c1+c2;
set N = N1+N2;
X2: for n being Element of NAT st n >= N holds
(x+y) . n <= c * ((seq_n^k).n) & (x+y) . n >= 0
proof
let n be Element of NAT;
assume X3: n >= N;
N1 <= N1 + N2 & N2 <= N1 + N2 by NAT_1:11; then
X4: N1 <= n & N2 <= n by X3,XXREAL_0:2; then
X5: x . n <= c1 * ((seq_n^k).n) & x . n >= 0 by P11;
X6: y . n <= c2 * ((seq_n^k).n) & y . n >= 0 by P21,X4;
x . n + y.n <= c1 * ((seq_n^k).n)
+ c2 * ((seq_n^k).n) by X5,X6,XREAL_1:7;
hence thesis by SEQ_1:7,X5,X6;
end;
x+y is Element of Funcs (NAT,REAL) by FUNCT_2:8;
hence x+y in Big_Oh( seq_n^k ) by P11,P21,X2;
end;
theorem LMXFIN8:
for k be Nat,a be Real,y be Real_Sequence
st 0<=a &
for i be Nat holds
y.i = a* (i to_power k) holds y in Big_Oh( seq_n^k )
proof
let k be Nat,a be Real,y be Real_Sequence;
assume AS: 0 <= a &
for n be Nat holds y.n = a* (n to_power k);
set c = a + 1;
XA1:a + 0 < a + 1 by XREAL_1:8;
A1: now
let n be Element of NAT;
assume A2: n >= 2;
A4: (seq_n^ k) . n = n to_power k by A2,ASYMPT_1:def 3; then
A5: y.n = a* ((seq_n^ k) . n ) by AS;
hence y.n <= c * ((seq_n^ k) . n) by XA1,A4,XREAL_1:64;
thus y.n >= 0 by A4,A5,AS;
end;
y is Element of Funcs (NAT,REAL) by FUNCT_2:8;
hence y in Big_Oh (seq_n^ k) by AS,A1;
end;
LMXFIN9:
for k be Nat
holds Big_Oh( seq_n^k ) c= Big_Oh( seq_n^(k+1) )
proof
let k be Nat;
set g = seq_n^ (k+1);
set f = seq_n^ k;
A0: k < k+1 by NAT_1:13;
A1: now
let n be Element of NAT;
assume A2: n >= 2;
then A3: n > 1 by XXREAL_0:2;
A4: (seq_n^ k) . n = n to_power k by A2,ASYMPT_1:def 3;
(seq_n^ (k+1)) . n = n to_power (k+1) by A2, ASYMPT_1:def 3;
hence (seq_n^ k) . n <= 1 * ((seq_n^ (k+1)) . n) by A3, A4, A0,POWER:39;
thus (seq_n^ k) . n >= 0 by A4;
end;
seq_n^ k is Element of Funcs (NAT,REAL) by FUNCT_2:8;
then seq_n^ k in Big_Oh (seq_n^ (k+1)) by A1;
hence Big_Oh( seq_n^k ) c=Big_Oh( seq_n^(k+1) ) by ASYMPT_0:11;
end;
theorem
for k,n be Nat st k <= n
holds Big_Oh( seq_n^k ) c= Big_Oh( seq_n^(n) )
proof
let k,n be Nat;
assume k <= n;then
consider i be Nat such that LA: n = k + i by NAT_1:10;
defpred P[Nat] means
Big_Oh( seq_n^k ) c= Big_Oh( seq_n^(k+ $1) );
P0:P[0];
P1:for x be Nat st P[x] holds P[x+1]
proof
let x be Nat;
assume P1L1:P[x];
Big_Oh( seq_n^(k+x) ) c= Big_Oh( seq_n^(k+ x +1) ) by LMXFIN9;
hence thesis by XBOOLE_1:1,P1L1;
end;
for x be Nat holds P[x] from NAT_1:sch 2(P0,P1);
hence thesis by LA;
end;
theorem LMXFIN10:
for k be Nat,
c be nonnegative-yielding XFinSequence of REAL
st len c = k+1
holds seq_p(c) in Big_Oh( seq_n^(k) )
proof
defpred P[Nat] means
for c be nonnegative-yielding XFinSequence of REAL
st len c = $1+1
holds seq_p(c) in Big_Oh( seq_n^($1) );
P0:P[0] by LMXFIN6;
P1:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P11: P[k];
let d be nonnegative-yielding XFinSequence of REAL;
assume P12: len d = (k+1)+1;then
consider a be Real,d1 be XFinSequence of REAL,
y be Real_Sequence such that
P13: len d1 = k + 1 & d1= d | (k+1) &
a = d.(k+1) & d =d1^<% a %> & seq_p(d) = seq_p(d1) + y &
for i be Nat holds
y.i = a* (i to_power (k+1)) by LMXFIN4;
T11: for i be Nat st i in dom d1 holds 0 <=d1.i
proof
let i be Nat;
assume AA1: i in dom d1; then
AA2: d1.i = d.i by P13,FUNCT_1:47;
k+1 <= (k+1)+1 by NAT_1:13; then
Segm (k+1) c= Segm ((k+1)+1) by NAT_1:39;
hence 0 <=d1.i by PARTFUN3:def 4,AA2,FUNCT_1:3,AA1,P12,P13;
end;
for r be Real st r in rng d1 holds 0 <=r
proof
let r be Real;
assume r in rng d1;then
consider x be object such that RC:
x in dom d1 & r = d1.x by FUNCT_1:def 3;
thus thesis by RC,T11;
end; then
d1 is nonnegative-yielding;then
seq_p(d1) in Big_Oh( seq_n^k ) by P11,P13; then
P14: seq_p(d1) in Big_Oh( seq_n^(k+1)) by LMXFIN9,TARSKI:def 3;
k+1 < (k+1)+1 by NAT_1:13; then
k+1 in Segm ((k+1)+1) by NAT_1:44;then
d.(k+1) in rng d by FUNCT_1:3,P12;then
y in Big_Oh( seq_n^(k+1) ) by P13,LMXFIN8,PARTFUN3:def 4;
hence seq_p(d) in Big_Oh( seq_n^(k+1) ) by P14,P13,LMXFIN7;
end;
for k be Nat holds P[k] from NAT_1:sch 2(P0,P1);
hence thesis;
end;
theorem LMXFIN15:
for k be Nat,
c be XFinSequence of REAL holds
ex d be XFinSequence of REAL st len d = len c &
for i be Nat st i in dom d holds d.i = |. c.i .|
proof
let k be Nat,
c be XFinSequence of REAL;
deffunc F(Nat) = In(|. c.$1 .|,REAL);
consider d being XFinSequence of REAL such that
A1: len d = len c &
for j be Nat st j in len c holds d.j = F(j) from AFINSQ_2:sch 1;
take d;
thus len d = len c by A1;
let i be Nat;
assume i in dom d;
then d.i = In(|. c.i .|,REAL) by A1;
hence d.i = |. c.i .|;
end;
theorem LMXFIN17:
for c be XFinSequence of REAL,
d be XFinSequence of REAL
st len d = len c &
for i be Nat st i in dom d holds d.i = |. c.i .| holds
for n be Nat holds ( seq_p(c) ).n <= ( seq_p(d) ).n
proof
let c be XFinSequence of REAL,
d be XFinSequence of REAL;
assume AS:len d = len c &
for i be Nat st i in dom d holds d.i = |. c.i .|;
let x be Nat;
P1: (seq_p(c)).x = Sum(c (#) seq_a^(x,1,0)) by defseqp;
P2: (seq_p(d)).x = Sum(d (#) seq_a^(x,1,0)) by defseqp;
dom (d (#) seq_a^(x,1,0)) = dom d by LMXFIN1
.= dom (c (#) seq_a^(x,1,0)) by LMXFIN1,AS; then
D1: len (d (#) seq_a^(x,1,0)) = len (c (#) seq_a^(x,1,0));
for i be Nat st i in dom (c (#) seq_a^(x,1,0)) holds
(c (#) seq_a^(x,1,0)).i <= (d (#) seq_a^(x,1,0)).i
proof
let i be Nat;
assume i in dom (c (#) seq_a^(x,1,0)); then
P6:i in dom c by LMXFIN1; then
P7: (c (#) seq_a^(x,1,0)).i = (c.i) * x to_power (i) by LMXFIN2;
P8: (d (#) seq_a^(x,1,0)).i = (d.i) * x to_power (i) by P6,AS,LMXFIN2;
d.i = |. c.i .| by AS,P6;
hence thesis by XREAL_1:64,P7,P8,ABSVALUE:4;
end;
hence ( seq_p(c) ).x <= ( seq_p(d) ).x by D1,AFINSQ_2:57,P1,P2;
end;
theorem LMXFIN20A:
for k be Nat,
c be XFinSequence of REAL
st len c = k+1 & seq_p(c) is eventually-nonnegative
holds seq_p(c) in Big_Oh( seq_n^(k) )
proof
let k be Nat,
c be XFinSequence of REAL;
assume AS: len c = k+1 & seq_p(c) is eventually-nonnegative;
consider d be XFinSequence of REAL such that
P1: len d = len c &
for i be Nat st i in dom d holds d.i = |. c.i .| by LMXFIN15;
T11: for i be Nat st i in dom d holds 0 <= d.i
proof
let i be Nat;
assume i in dom d;
then d.i = |. c.i .| by P1;
hence 0 <= d.i by COMPLEX1:46;
end;
for r be Real st r in rng d holds 0 <=r
proof
let r be Real;
assume r in rng d;then
consider x be object such that RC:
x in dom d & r = d.x by FUNCT_1:def 3;
thus thesis by RC,T11;
end;
then
d is nonnegative-yielding;
then
seq_p(d) in Big_Oh( seq_n^(k) ) by LMXFIN10,P1,AS; then
consider t be Element of Funcs (NAT,REAL) such that
P5: seq_p(d)=t &
ex c being Real,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 be Nat such that
P4A: for n be 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 >= N holds
((seq_p(c)).n <= a * ((seq_n^k).n) & (seq_p(c)).n >= 0)
proof
let n be Element of NAT;
assume P8: n >= N;
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;
thus 0 <= ( seq_p(c) ).n by P4A,P9;
end;
seq_p(c) is Element of Funcs (NAT,REAL) by FUNCT_2:8;
hence seq_p(c) in Big_Oh( seq_n^k ) by P6,P7;
end;
theorem TPOWSUCC:
for k,n be Nat st 0 < n holds
n*(seq_n^(k)).n = ((seq_n^(k+1)).n)
proof
let k,n be Nat;
ZZ: k in NAT & n in NAT by ORDINAL1:def 12;
assume AS: 0 < n;
(seq_n^(k+1)).n = n to_power (k+1) by ZZ,ASYMPT_1:def 3,AS
.= (n to_power k)*(n to_power 1) by POWER:27,AS
.= (n to_power k)* n by POWER:25;
hence thesis by AS,ZZ,ASYMPT_1:def 3;
end;
theorem TLNEG1:
for c be XFinSequence of REAL st len c = 0 holds
for x be Nat holds (seq_p(c)).x = 0
proof
let c be XFinSequence of REAL;
assume AS:len c = 0;
let x be Nat;
L1:(seq_p(c)).x = Sum(c (#) seq_a^(x,1,0)) by defseqp;
reconsider f =c (#) seq_a^(x,1,0) as Sequence;
dom f = (dom c) /\ (dom seq_a^(x,1,0)) by VALUED_1:def 4;
then L2: f = {} by AS;
reconsider f as XFinSequence of REAL;
thus thesis by L2,L1;
end;
theorem
for f be eventually-nonnegative Real_Sequence,
k be Nat st
f in Big_Oh(seq_n^(k)) holds
ex N be Nat st
for n be Nat st N <= n holds f.n <= (seq_n^(k+1)).n
proof
let f be eventually-nonnegative Real_Sequence,
k be Nat;
assume f in Big_Oh(seq_n^(k));
then consider t be Element of Funcs (NAT,REAL) such that
L1: f=t &
ex c being Real,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) <= n by INT_1:def 7;then
P2:N <= n & c <= n by P1, XXREAL_0:2;
reconsider n as Element of NAT by INT_1:3,P1;
take n;
let x be Nat;
A: x in NAT by ORDINAL1:def 12;
assume P4:n <= 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 thesis by P5,XXREAL_0:2,P6;
end;
theorem
for c be XFinSequence of REAL holds
ex absc be XFinSequence of REAL st
absc = |. c .| &
for n be Nat holds (seq_p(c)).n <= (seq_p(absc)).n
proof
let c be XFinSequence of REAL;
reconsider absc = |. c .| as XFinSequence of REAL;
take absc;
thus absc = |.c.|;
let n be Nat;
CL1: (seq_p(c)).n = Sum(c (#) seq_a^(n,1,0)) by defseqp;
CL2: (seq_p(absc)).n = Sum(absc (#) seq_a^(n,1,0)) by defseqp;
set mc = c (#) seq_a^(n,1,0);
set mac = absc (#) seq_a^(n,1,0);
px0:dom c =dom absc by VALUED_1:def 11;
dom mc = dom c /\ dom (seq_a^(n,1,0)) by VALUED_1:def 4; then
px: len mc = len mac by px0,VALUED_1:def 4;
for x be Nat st x in dom mc holds mc.x <= mac.x
proof
let x be Nat;
CCL1: mc.x =c.x * (seq_a^(n,1,0)).x by VALUED_1:5;
CCL2: mac.x =absc.x * (seq_a^(n,1,0)).x by VALUED_1:5;
PX2:(seq_a^(n,1,0)).x = n to_power (1*x+0) by ASYMPT_1:def 1
.= n to_power x;
absc.x = |. c.x .| by VALUED_1:18;
hence thesis by XREAL_1:64,CCL1,CCL2,ABSVALUE:4,PX2;
end;
hence thesis by CL1,CL2,AFINSQ_2:57,px;
end;
theorem TLNEG41:
for c,absc be XFinSequence of REAL st absc = |. c .|
holds for n be Nat holds |.(seq_p(c)).n .| <= (seq_p(absc)).n
proof
defpred P[Nat] means for c,absc be XFinSequence of REAL
st len c = $1 & absc = |. c .|
holds for x be Nat holds |.(seq_p(c)).x .| <= (seq_p(absc)).x;
P0:P[0]
proof
let c,absc be XFinSequence of REAL;
assume A0: len c = 0 & absc = |. c .|;
D2: dom absc = {} by A0,VALUED_1:def 11;
let x be Nat;
c (#) seq_a^(x,1,0) = {} by A0,LMXFIN1; then
Q2: Sum(c (#) seq_a^(x,1,0)) = 0;
absc (#) seq_a^(x,1,0) = {} by D2,LMXFIN1; then
Q3: Sum(absc (#) seq_a^(x,1,0)) = 0;
|. (seq_p(c)).x .| = 0 by COMPLEX1:44,Q2,defseqp;
hence |.(seq_p(c)).x .| <= (seq_p(absc)).x by Q3,defseqp;
end;
P1:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A0: P[k];
let c,absc be XFinSequence of REAL;
assume A1: len c = k+1 & absc = |. c .|;
consider a1 be Real,c1 be XFinSequence of REAL,
y1 be Real_Sequence such that
A2: len c1 = k & c1= c | k & a1 = c.k & c =c1^<% a1 %> &
seq_p(c) = seq_p(c1) + y1 &
for i be Nat holds
y1.i = a1* (i to_power k) by A1,LMXFIN4;
len absc = k+1 by A1,VALUED_1:def 11; then
consider a2 be Real,c2 be XFinSequence of REAL,
y2 be Real_Sequence such that
A4: len c2 = k & c2= absc | k & a2 = absc.k & absc =c2^<% a2 %> &
seq_p(absc) = seq_p(c2) + y2 &
for i be Nat holds y2.i = a2* (i to_power k) by LMXFIN4;
A5: |. a1 .| = a2 by A1,A2,A4,VALUED_1:18;
for i being object st i in dom c2 holds c2.i = |. c1.i .|
proof
let i be object;
assume B1: i in dom c2;
c2.i = absc.i by A4,B1,FUNCT_1:47
.= |. c.i .| by A1,VALUED_1:18
.= |. c1.i .| by A2,B1,FUNCT_1:47,A4;
hence thesis;
end; then
AA7:c2= |. c1 .| by VALUED_1:def 11,A2,A4;
let x be Nat;
A8: (seq_p(c)).x = (seq_p(c1)).x + y1.x by SEQ_1:7,A2;
A9: (seq_p(absc)).x = (seq_p(c2)).x + y2.x by SEQ_1:7,A4;
A10: |.(seq_p(c)).x .| <= |.(seq_p(c1)).x .| + |.y1.x .|
by A8,COMPLEX1:56;
A11: |.(seq_p(c1)).x .| <= (seq_p(c2)).x by AA7,A2,A0;
y1.x = a1* (x to_power k) by A2; then
|.y1.x .| = |. a1 .| * |. x to_power k .| by COMPLEX1:65
.=|. a1 .| * (x to_power k) by ABSVALUE:def 1
.= y2.x by A4,A5; then
|.(seq_p(c1)).x .| + |.y1.x .| <= (seq_p(c2)).x + y2.x
by XREAL_1:7,A11;
hence |.(seq_p(c)).x .| <= (seq_p(absc)).x by A9,XXREAL_0:2,A10;
end;
X1: for n be Nat holds P[n] from NAT_1:sch 2(P0,P1);
let c,absc be XFinSequence of REAL;
assume X2: absc = |. c .|;
len c is Nat;
hence for n be Nat holds |.(seq_p(c)).n .| <= (seq_p(absc)).n by X1,X2;
end;
TLNEG42:
for d be XFinSequence of REAL
st (for i be Nat st i in dom d holds 0 <=d.i)
holds ex M be Real st 0 <= M &
for i be Nat st i in dom d holds d.i <= M
proof
defpred P[Nat] means
for d be XFinSequence of REAL st len d = $1 &
(for i be Nat st i in dom d holds 0 <=d.i)
holds ex M be Real st 0 <= M &
for i be Nat st i in dom d holds d.i <= M;
P0:P[0]
proof
let d be XFinSequence of REAL;
assume A1: len d = 0 &
(for i be Nat st i in dom d holds 0 <=d.i );
set M = 0;
take M;
thus 0 <= M;
thus for i be Nat st i in dom d holds d.i <= M by A1;
end;
P1:for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A0: P[k];
let d be XFinSequence of REAL;
assume A1: len d = k+1 &
(for i be Nat st i in dom d holds 0 <=d.i );
consider a be Real,d1 be XFinSequence of REAL such that
A2:len d1 = k & d1= d | k & a = d.k &
d =d1^<% a %> by A1,LMXFIN3;
for i be Nat st i in dom d1 holds 0 <=d1.i
proof
let i be Nat;
assume AA1: i in dom d1; then
AA2: d1.i = d.i by A2,FUNCT_1:47;
k <= k+1 by NAT_1:13; then
Segm k c= Segm (k+1) by NAT_1:39;
hence 0 <=d1.i by A1,AA2,AA1,A2;
end;
then consider M0 be Real such that
A3: 0 <= M0 &
for i be Nat st i in dom d1 holds d1.i <= M0 by A0,A2;
set M = [/ max(M0,a) \];
Q1: M0 <= max(M0,a) & a <= max(M0,a) by XXREAL_0:25;
Q2P: max(M0,a) <= M by INT_1:def 7; then
Q2:M0 <= M & a <= M by Q1, XXREAL_0:2;
M in NAT by INT_1:3,A3,Q1; then
reconsider M as Nat;
take M;
thus 0 <=M;
let i be Nat;
assume i in dom d; then
i in Segm (k+1) by A1; then
i < k+1 by NAT_1:44; then
Q6: i <=k by NAT_1:13;
per cases;
suppose i <> k; then
i < k by XXREAL_0:1,Q6; then
Q8P:i in Segm k by NAT_1:44; then
Q9: d1.i =d.i by A2,FUNCT_1:47;
d1.i <= M0 by A3,Q8P,A2;
hence d.i <= M by Q9,Q2,XXREAL_0:2;
end;
suppose i = k;
hence d.i <= M by Q2P,A2,Q1, XXREAL_0:2;
end;
end;
X1:for k be Nat holds P[k] from NAT_1:sch 2(P0,P1);
let d be XFinSequence of REAL;
assume X2: for i be Nat st i in dom d holds 0 <=d.i;
thus ex M be Real st 0 <= M &
for i be Nat st i in dom d holds d.i <= M by X1,X2;
end;
theorem TLNEG36:
for a be Real st 0 < a holds
for k be Nat, d be nonnegative-yielding XFinSequence of REAL
st len d = k holds
ex N be Nat st
for x be Nat st N <=x holds
for i be Nat st i in dom d
holds (d.i) * (x to_power i)*k <= a* (x to_power k)
proof
let a be Real;
assume AS: 0 < a;
let k be Nat, d be nonnegative-yielding XFinSequence of REAL;
assume
A1: len d = k;
A2: for i be Nat st i in dom d holds 0 <=d.i
proof
let i be Nat;
assume i in dom d;then
d.i in rng d by FUNCT_1:3;
hence thesis by PARTFUN3:def 4;
end;
per cases;
suppose P0:k= 0;
set N = 0;
take N;
let x be Nat;
assume N <=x;
thus for i be Nat st i in dom d holds (d.i) * (x to_power i)*k
<= a* (x to_power k) by P0,A1;
end;
suppose K1P:k <> 0; then
0 <= k-1 by XREAL_1:48,NAT_1:14; then
reconsider k1=k-1 as Nat by INT_1:3,ORDINAL1:def 12;
consider M be Real such that
Q1: 0 <= M & for i be Nat st i in dom d holds d.i <= M by TLNEG42,A2;
set N = [/ M*k/a \] + 2;
MM1:M*k/a <= [/ M*k/a \] by INT_1:def 7;
Q20P:0 <= M*k/a by AS,Q1; then
Q20: 1 + 0 < 2 + [/ M*k/a \] by XREAL_1:8;
N in NAT by INT_1:3,Q20P; then
reconsider N as Nat;
[/ M*k/a \] + 1 + 0 < [/ M*k/a \] + 1 + 1 by XREAL_1:8; then
M*k/a < N by XXREAL_0:2,INT_1:32; then
M*k/a *a <= N *a by AS,XREAL_1:64; then
Q2: M*k <= a*N & 1 < N by XCMPLX_1:87,AS,Q20;
take N;
thus for x be Nat st N <= x holds for i be Nat st i in dom d
holds (d.i) * (x to_power i)*k <= a* (x to_power k)
proof
let x be Nat;
assume Q3: N <=x;
let i be Nat;
assume Q4: i in dom d; then
(d.i)*k <= M*k by XREAL_1:64,Q1; then
Q5: (d.i)*k*(x to_power i) <= M*k *(x to_power i) by XREAL_1:64;
i in Segm k by Q4,A1; then
i < k1+1 by NAT_1:44; then
Y1: i <= k1 by NAT_1:13;
Y2: 1 < x by Q3,XXREAL_0:2,Q20;
X1: x to_power i <= x to_power k1
proof
per cases;
suppose i = k1;
hence x to_power i <= x to_power k1;
end;
suppose i <> k1; then
i < k1 by Y1,XXREAL_0:1;
hence x to_power i <= x to_power k1 by Y2,POWER:39;
end;
end;
N1:x*(x to_power k1) = x to_power k
proof
per cases;
suppose x = 0;
hence x*(x to_power k1) = x to_power k by K1P,POWER:def 2;
end;
suppose XX1: x <> 0;
x = x to_power 1 by POWER:25;
hence x*(x to_power k1) = x to_power (1 +k1) by XX1,POWER:27
.= x to_power k;
end;
end;
(M*k) *(x to_power i) <=(M*k) * (x to_power k1) by X1,XREAL_1:64,Q1;
then
Q7: (d.i)*k*(x to_power i)
<=M*k * (x to_power k1) by XXREAL_0:2,Q5;
M*k * (x to_power k1) <= a*N* (x to_power k1) by Q2,XREAL_1:64;
then
Q8: (d.i)*k*(x to_power i)
<= a*N* (x to_power k1) by XXREAL_0:2,Q7;
a*N <= a*x by XREAL_1:64,AS,Q3; then
a*N* (x to_power k1) <= a*x*(x to_power k1) by XREAL_1:64;
hence (d.i)*(x to_power i)*k <= a*(x to_power k) by XXREAL_0:2,Q8,N1;
end;
end;
end;
theorem TLNEG35:
for k be Nat,
d be XFinSequence of REAL,
a be Real,
y be Real_Sequence
st 0 < a
& len d = k
& for x be Nat holds y.x = a * (x to_power k)
holds
ex N be Nat st
for x be Nat st N <= x holds |.(seq_p(d)).x .| <= y.x
proof
let k be Nat, d be XFinSequence of REAL,
a be Real, y be Real_Sequence;
assume that
A1: 0 < a and
A2:len d = k and
A3:for x be Nat holds y.x = a* (x to_power k);
per cases;
suppose K1: k = 0;
set N = 0;
take N;
thus for x be Nat st N <=x holds |.(seq_p(d)).x .| <= y.x
proof
let x be Nat;
assume N <=x;
D2: |.(seq_p(d)).x .| = 0 by COMPLEX1:44,A2,K1,TLNEG1;
y.x = a* (x to_power k) by A3;
hence thesis by D2,A1;
end;
end;
suppose B4: k <> 0;
reconsider c = |. d .| as XFinSequence of REAL;
len c = k by A2,VALUED_1:def 11;
then consider N be Nat such that
A4: for x be Nat st N <=x holds
for i be Nat st i in dom c holds ( (c.i) * x to_power i ) *k
<= a* (x to_power k) by A1,TLNEG36;
take N;
thus for x be Nat st N <=x holds |.(seq_p(d)).x .| <= y.x
proof
let x be Nat;
assume A0:N <=x;
NN0:dom (c (#) seq_a^(x,1,0)) = dom c by LMXFIN1
.= dom d by VALUED_1:def 11;
P1: (seq_p(c)).x = Sum(c (#) seq_a^(x,1,0)) by defseqp;
for i be Nat st i in dom (c (#) seq_a^(x,1,0)) holds
(c (#) seq_a^(x,1,0)).i <= (y.x) / k
proof
let i be Nat;
assume i in dom (c (#) seq_a^(x,1,0)); then
X5: i in dom c by LMXFIN1; then
(c.i) * (x to_power i)*k/k <= a* (x to_power k)/k
by XREAL_1:72,A0,A4; then
(c.i) * x to_power i <= a* (x to_power k)/k by B4,XCMPLX_1:89;
then
(c.i) * x to_power i <= (y.x) / k by A3;
hence (c (#) seq_a^(x,1,0)).i <= (y.x) / k by X5,LMXFIN2;
end; then
Sum (c (#) seq_a^(x,1,0)) <= ((y.x)/k ) *len (c (#) seq_a^(x,1,0))
by AFINSQ_2:59; then
P6: ( seq_p(c) ).x <= y.x by P1,NN0,A2,B4,XCMPLX_1:87;
|.(seq_p(d)).x .| <= ( seq_p(c) ).x by TLNEG41;
hence |.(seq_p(d)).x .| <= y.x by XXREAL_0:2,P6;
end;
end;
end;
theorem TLNEG3:
for k be Nat, d be XFinSequence of REAL
st len d = k+1 & 0 < d.k holds
seq_p(d) is eventually-nonnegative
proof
let k be Nat, d be XFinSequence of REAL;
assume
AS: len d = k+1 & 0 < d.k; then
consider a be Real,d1 be XFinSequence of REAL,
y be Real_Sequence such that
P1: len d1 = k & d1= d | k & a = d.k & d = d1^<% a %> &
seq_p(d) = seq_p(d1) + y &
for i be Nat holds y.i = a* (i to_power k) by LMXFIN4;
consider N be Nat such that
P20: for i be Nat st N <= i holds |. (seq_p(d1)).i .| <= y.i
by P1,TLNEG35,AS;
for i be Nat st N <= i holds 0 <= (seq_p(d)).i
proof
let i be Nat;
assume N <= i; then
P32: 0 <= y.i - |. (seq_p(d1)).i .| by XREAL_1:48,P20;
-(seq_p(d1)).i <= -(-|. (seq_p(d1)).i .|) by XREAL_1:24,ABSVALUE:4;
then y.i - |. (seq_p(d1)).i .| <= y.i -(-(seq_p(d1)).i) by XREAL_1:13;
then y.i - |. (seq_p(d1)).i .| <= (seq_p(d1)).i + y.i;
hence thesis by P1,SEQ_1:7,P32;
end;
hence thesis;
end;
theorem
for k be Nat,
c be XFinSequence of REAL
st len c = k+1 & 0 < c.k
holds seq_p(c) in Big_Oh (seq_n^(k)) by LMXFIN20A,TLNEG3;
theorem
for k be Nat,
c be XFinSequence of REAL
st len c = k+1 & 0 < c.k holds seq_p(c) is polynomially-bounded
proof
let k be Nat,
c be XFinSequence of REAL;
assume AS: len c = k+1 & 0 < c.k;
take k;
thus thesis by LMXFIN20A,TLNEG3,AS;
end;