:: Polynomially Bounded Sequences and Polynomial Sequences :: by Hiroyuki Okazaki and Yuichi Futa :: :: Received June 30, 2015 :: Copyright (c) 2015-2017 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, POWER; 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 {}; 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= 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 by INT_1:3,AC33; 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 = 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 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;then 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 XFinSequence of REAL; 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,P2P,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; rng |. c .| c= REAL; then reconsider absc = |. c .| as XFinSequence of REAL by RELAT_1:def 19; 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,Q2P; 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; len d is Nat; hence 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,MM1; N in NAT by INT_1:3,MM1,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; rng |. d .| c= REAL; then reconsider c = |. d .| as XFinSequence of REAL by RELAT_1:def 19; B3: for i be Nat st i in dom c holds 0 <= c.i proof let i be Nat; assume i in dom c; then c.i = |. d.i .| by VALUED_1:def 11; hence 0 <= c.i by COMPLEX1:46; end; for r be Real st r in rng c holds 0 <=r proof let r be Real; assume r in rng c;then consider x be object such that RC: x in dom c & r = c.x by FUNCT_1:def 3; thus thesis by RC,B3; end; then B3T: c is nonnegative-yielding; 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,B3T,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;