:: Polynomially Bounded Sequences and Polynomial Sequences :: by Hiroyuki Okazaki and Yuichi Futa :: :: Received June 30, 2015 :: Copyright (c) 2015-2021 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; begin :: Preliminaries theorem :: ASYMPT_2:1 for m,k be Nat st 1 <= m holds 1 <= m to_power k; theorem :: ASYMPT_2:2 for m,n be Nat holds m <= m to_power (n+1); theorem :: ASYMPT_2:3 for m,n be Nat st 2 <= m holds n+1 <= m to_power n; theorem :: ASYMPT_2:4 for k be Nat holds 2*k <= 2 to_power k; theorem :: ASYMPT_2:5 for k,n be Nat st k <= n holds n+k <= 2 to_power n; theorem :: ASYMPT_2:6 for k,m be Nat st 2*k + 1 <= m holds 2 to_power k <= (2 to_power m) / m; theorem :: ASYMPT_2:7 for a,b,c be Real st 1 < a & 0 < b & b <= c holds log(a,b) <= log(a,c); theorem :: ASYMPT_2:8 for n be Nat, a be Real st 1 < a holds a to_power n < a to_power (n+1); theorem :: ASYMPT_2:9 for n be Nat, a be Real st 1 <= a holds a to_power n <= a to_power (n+1); theorem :: ASYMPT_2:10 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); theorem :: ASYMPT_2:11 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; theorem :: ASYMPT_2:12 for x,y be Real st number_e < x & x <= y holds x/log(2,x) <= y/log(2,y); theorem :: ASYMPT_2:13 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); theorem :: ASYMPT_2:14 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); theorem :: ASYMPT_2:15 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); theorem :: ASYMPT_2:16 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); theorem :: ASYMPT_2:17 for a,b be Nat st a <= b holds seq_n^ a in Big_Oh (seq_n^ b); theorem :: ASYMPT_2:18 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); theorem :: ASYMPT_2:19 for a be non negative Real, n be Nat st 1 <= n holds 0 < (seq_n^(a)).n; begin :: Polynomially Bounded Sequences definition let p be Real_Sequence; attr p is polynomially-bounded means :: ASYMPT_2:def 1 ex k be Nat st p in Big_Oh(seq_n^(k)); end; theorem :: ASYMPT_2:20 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 :: ASYMPT_2:21 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 :: ASYMPT_2:22 for a be positive Real holds seq_a^(a,1,0) is positive; theorem :: ASYMPT_2:23 for a be Real st 1 <= a holds seq_a^(a,1,0) is non-decreasing; theorem :: ASYMPT_2:24 for a be Real st 1 < a holds seq_a^(a,1,0) is increasing; theorem :: ASYMPT_2:25 for a be Nat st 1 < a holds seq_a^(a,1,0) is non polynomially-bounded; begin :: Polynomial Sequences theorem :: ASYMPT_2:26 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); definition let x be XFinSequence of REAL, y be Real_Sequence; redefine func x(#)y -> XFinSequence of REAL; end; theorem :: ASYMPT_2:27 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); definition let c be XFinSequence of REAL; func seq_p(c) -> Real_Sequence means :: ASYMPT_2:def 2 for x be Nat holds it.x = Sum(c (#) seq_a^(x,1,0)); end; theorem :: ASYMPT_2:28 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); theorem :: ASYMPT_2:29 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; theorem :: ASYMPT_2:30 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) ); theorem :: ASYMPT_2:31 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 ); theorem :: ASYMPT_2:32 for k,n be Nat st k <= n holds Big_Oh( seq_n^k ) c= Big_Oh( seq_n^(n) ); theorem :: ASYMPT_2:33 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) ); theorem :: ASYMPT_2:34 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 .|; theorem :: ASYMPT_2:35 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; theorem :: ASYMPT_2:36 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) ); theorem :: ASYMPT_2:37 for k,n be Nat st 0 < n holds n*(seq_n^(k)).n = ((seq_n^(k+1)).n); theorem :: ASYMPT_2:38 for c be XFinSequence of REAL st len c = 0 holds for x be Nat holds (seq_p(c)).x = 0; theorem :: ASYMPT_2:39 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; theorem :: ASYMPT_2:40 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; theorem :: ASYMPT_2:41 for c,absc be XFinSequence of REAL st absc = |. c .| holds for n be Nat holds |.(seq_p(c)).n .| <= (seq_p(absc)).n; theorem :: ASYMPT_2:42 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); theorem :: ASYMPT_2:43 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; theorem :: ASYMPT_2:44 for k be Nat, d be XFinSequence of REAL st len d = k+1 & 0 < d.k holds seq_p(d) is eventually-nonnegative; theorem :: ASYMPT_2:45 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)); theorem :: ASYMPT_2:46 for k be Nat, c be XFinSequence of REAL st len c = k+1 & 0 < c.k holds seq_p(c) is polynomially-bounded;