:: Algebra of Polynomially Bounded Sequences and Negligible Functions :: by Hiroyuki Okazaki :: :: Received August 15, 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, XBOOLE_0, SEQ_1, FUNCT_2, TARSKI, REAL_1, BINOP_1, SUBSET_1, FUNCT_1, ARYTM_3, ZFMISC_1, VALUED_1, CARD_1, NAT_1, RLVECT_1, RELAT_1, SUPINF_2, ARYTM_1, STRUCT_0, ALGSTR_0, REALSET1, XXREAL_0, CARD_3, COMPLEX1, SEQ_2, ORDINAL2, RSSPACE, ASYMPT_1, FUNCSDOM, FINSET_1, POWER, ORDINAL4, FUNCOP_1, VECTSP_1, PARTFUN3, PRE_TOPC, FINSEQ_1, MESFUNC1, ASYMPT_2, ASYMPT_3, ASYMPT_0, ORDINAL1, INT_1, AFINSQ_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, FUNCOP_1, REALSET1, FINSET_1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_1, INT_1, COMPLEX1, VALUED_1, SEQ_1, SEQ_2, RVSUM_1, POWER, SERIES_1, ASYMPT_0, ASYMPT_1, AFINSQ_1, PARTFUN3, AFINSQ_2, STRUCT_0, ALGSTR_0, PRE_TOPC, GROUP_1, RLVECT_1, VECTSP_1, FUNCSDOM, RSSPACE, ASYMPT_2; constructors REAL_1, SEQ_2, SERIES_1, REALSET1, RLSUB_1, RELSET_1, COMSEQ_2, SEQ_1, FUNCSDOM, INTEGRA2, XXREAL_2, RECDEF_1, FCONT_1, PREPOWER, ASYMPT_0, ASYMPT_1, PARTFUN3, AFINSQ_2, FUNCT_4, PARTFUN2, RSSPACE4, PROB_1, NEWTON, VALUED_2, ASYMPT_2, GROUP_1, RVSUM_1, RFINSEQ2, METRIC_1, MATRPROB; registrations ORDINAL1, RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, MEMBERED, VALUED_0, FUNCSDOM, RLVECT_1, STRUCT_0, FUNCOP_1, VALUED_1, FUNCT_2, AFINSQ_1, AFINSQ_2, XBOOLE_0, SUBSET_1, RELAT_1, INT_1, ASYMPT_0, POWER, ASYMPT_1, RSSPACE, PARTFUN3, REALSET1, NEWTON, COMPLEX1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions TARSKI, XBOOLE_0, FUNCT_2, ALGSTR_0, RLVECT_1, VECTSP_1; equalities REALSET1, STRUCT_0, ALGSTR_0, FUNCSDOM, BINOP_1, RLVECT_1, ORDINAL1, ASYMPT_0; expansions TARSKI, RLVECT_1, FUNCT_1, PARTFUN3, GROUP_1, FUNCSDOM, STRUCT_0, VECTSP_1, ASYMPT_2; theorems TARSKI, FUNCT_1, FUNCT_2, NAT_1, SEQ_1, SEQ_2, ABSVALUE, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, COMPLEX1, FUNCOP_1, XREAL_1, XXREAL_0, ORDINAL1, VALUED_1, XREAL_0, AFINSQ_1, AFINSQ_2, INT_1, ASYMPT_0, ASYMPT_1, POWER, FUNCSDOM, PRE_FF, TAYLOR_1, RLVECT_1, VECTSP_1, REALSET1, ZFMISC_1, ASYMPT_2, PARTFUN3, GROUP_1; schemes NAT_1, SEQ_1, XBOOLE_0; begin :: Preliminaries theorem TCL001: for r be Real holds r < |. r .| + 1 proof let r be Real; r + 0 < |. r .| +1 by XREAL_1:8,ABSVALUE:4; hence r < |. r .| +1; end; theorem LMC31: for r be Real ex N be 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 r = r0; thus 0 < r & r0 <=r by A1; end; suppose A2:not 0 < r0; set r=1; take r; thus 0 < r & r0 <=r 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; then 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 ASYMPT_2:13,A0; reconsider N as Element of NAT by ORDINAL1:def 12; take N; thus for n be Nat st N <=n holds r0 < n /log(2,n) proof 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; end; theorem L1: for k be Nat ex N be Nat st for x be Nat st N <= x holds x to_power k < 2 to_power x proof let k be Nat; consider N0 be Nat such that P1: for x be Nat st N0 <= x holds k < x /log(2,x) by LMC31; set N=N0+2; take N; now let x be Nat; assume AS2: N<= x; N0 <= N by NAT_1:12; then N0 <= x by XXREAL_0:2,AS2; then E1:k < x /log(2,x) by P1; 2 <= N by NAT_1:11; then 2 <= x by XXREAL_0:2,AS2; then log(2,2) <= log(2,x) by PRE_FF:10; then P3: 0 < log(2,x) by POWER:52; then k*log(2,x) < x /log(2,x) * log(2,x) by XREAL_1:68,E1; then P4: k*log(2,x) < x by P3,XCMPLX_1:87; 2 to_power (log(2,x)*k) = 2 to_power (log(2,x)) to_power k by POWER:33 .= x to_power k by AS2,POWER:def 3; hence x to_power k < 2 to_power x by P4,POWER:39; end; hence thesis; end; theorem L2: for k be Nat ex N be Nat st for x be Nat st N <= x holds 1/ (2 to_power x) < 1/ (x to_power k) proof let k be Nat; consider N0 be Nat such that P1: for x be Nat st N0 <= x holds x to_power k < 2 to_power x by L1; set N=N0+2; take N; now let x be Nat; assume AS: N <=x; N0 <= N by NAT_1:12; then N0 <= x by XXREAL_0:2,AS; then E1:x to_power k < 2 to_power x by P1; 0 < x to_power k by POWER:34,AS; hence 1/ (2 to_power x) < 1/ (x to_power k) by XREAL_1:76,E1; end; hence thesis; end; theorem for z be Nat st 2 <= z holds for k be Nat ex N be Nat st for x be Nat st N <= x holds 1/ (z to_power x) < 1/ (x to_power k) proof let z be Nat; assume P0: 2 <=z; let k be Nat; consider N be Nat such that P1: for x be Nat st N <= x holds 1/ (2 to_power x) < 1/ (x to_power k) by L2; take N; now let x be Nat; assume N <=x; then E1:1/ (2 to_power x) < 1/ (x to_power k) by P1; P3: 0 < 2 to_power x by POWER:34; 2 to_power x <= z to_power x proof now per cases by P0,XXREAL_0:1; case 2 = z; hence thesis; end; case LL1: 2 < z; now per cases; case LL2: x= 0;then 2 to_power x = 1 by POWER:24 .= z to_power x by POWER:24,LL2; hence thesis; end; case 0 < x; hence thesis by POWER:37,LL1; end; end; hence thesis; end; end; hence thesis; end; then 1/ (z to_power x) <= 1/ (2 to_power x) by P3,XREAL_1:118; hence 1/ (z to_power x) < 1/ (x to_power k) by E1,XXREAL_0:2; end; hence thesis; end; registration cluster positive-yielding for XFinSequence of REAL; correctness proof 1 is Element of REAL by XREAL_0:def 1;then reconsider z = <% 1 %> as XFinSequence of REAL; now let r be Real; assume r in rng z; then r in {1} by AFINSQ_1:33; hence 0 < r; end; then z is positive-yielding; hence thesis; end; end; registration cluster non empty for positive-yielding XFinSequence of REAL; correctness proof 1 is Element of REAL by XREAL_0:def 1;then reconsider z = <% 1 %> as XFinSequence of REAL; now let r be Real; assume r in rng z; then r in {1} by AFINSQ_1:33; hence 0 < r; end; then z is positive-yielding; hence thesis; end; end; theorem NLM1: for c be XFinSequence of REAL, a be Real holds a (#) c is XFinSequence of REAL proof let c be XFinSequence of REAL, a be Real; dom (a(#)c) = dom c by VALUED_1:def 5; then a(#)c is Sequence of rng (a(#)c) by ORDINAL1:31; hence thesis by ORDINAL1:32; end; registration let c be XFinSequence of REAL, a be Real; cluster a (#) c -> finite for Sequence of REAL; correctness; end; theorem NLM2: for c be non empty positive-yielding XFinSequence of REAL, a be Real st 0 < a holds a (#) c is non empty positive-yielding XFinSequence of REAL proof let c be non empty positive-yielding XFinSequence of REAL, a be Real; assume AS: 0 < a; P2: dom (a (#) c) = dom c by VALUED_1:def 5; now let r be Real; assume r in rng (a (#) c); then consider x be object such that P4: x in dom (a (#) c) & r = (a (#) c).x by FUNCT_1:def 3; c.x in rng c by FUNCT_1:3,P4,P2; then P5: 0 < c.x by PARTFUN3:def 1; r = a *c.x by P4,VALUED_1:6; hence 0 < r by P5,AS; end; then a (#) c is positive-yielding; hence thesis by NLM1,P2; end; registration let c be non empty positive-yielding XFinSequence of REAL, a be positive Real; cluster a (#) c -> non empty positive-yielding for XFinSequence of REAL; correctness by NLM2; end; notation let c be XFinSequence of REAL; synonym polynom(c) for seq_p(c); end; theorem NLM3: for c be non empty positive-yielding XFinSequence of REAL, x be Nat holds 0 < (polynom(c)).x proof defpred P[Nat] means for c be non empty positive-yielding XFinSequence of REAL st len c = $1 holds for x be Nat holds 0 < (polynom(c)).x; P0: P[0]; P1: for k be Nat st P[k] holds P[k+1] proof let k be Nat; assume A1: P[k]; let d be non empty positive-yielding XFinSequence of REAL; assume A2: len d = k+1; then consider a be Real,d1 be XFinSequence of REAL, y be Real_Sequence such that A3: len d1 = k & d1= d | k & a = d.k & d =d1^<% a %> & polynom(d) = polynom(d1) + y & for i be Nat holds y.i = a* (i to_power k) by ASYMPT_2:28; per cases; suppose X1:k = 0; then consider a be Real such that A4:a = d.0 & for x be Nat holds (polynom(d)).x = a by ASYMPT_2:29,A2; 0 in Segm (0+1) by NAT_1:44; then d.0 in rng d by FUNCT_1:3,X1,A2; then A5:0 < d.0 by PARTFUN3:def 1; let x be Nat; reconsider n =x as Nat; thus 0 < (polynom(d)).x by A5,A4; end; suppose A7:k <> 0; now let r be Real; assume r in rng d1; then consider x be object such that P4: x in dom d1 & r = d1.x by FUNCT_1:def 3; P5: d1.x = d.x by P4,A3,FUNCT_1:47; x in dom d by P4,A3,RELAT_1:60,TARSKI:def 3; then d.x in rng d by FUNCT_1:3; hence 0 < r by PARTFUN3:def 1,P5,P4; end; then A8: d1 is positive-yielding; reconsider d1 as non empty positive-yielding XFinSequence of REAL by A7,A8,A3; let x be Nat; reconsider n=x as Nat; A9: 0 < (polynom(d1)).n by A1,A3; A10: (polynom(d)).n = (polynom(d1)).n + y.n by SEQ_1:7,A3; A11: y.n = a* (n to_power k) by A3; k < k+1 by NAT_1:13; then k in Segm (k+1) by NAT_1:44;then d.k in rng d by FUNCT_1:3,A2; then 0 < d.k by PARTFUN3:def 1; hence 0 < (polynom(d)).x by A10,A9,A11,A3; end; end; P2: for k be Nat holds P[k] from NAT_1:sch 2(P0,P1); let c be non empty positive-yielding XFinSequence of REAL, x be Nat; len c is Nat; hence 0 < (polynom(c)).x by P2; end; theorem NLM4: for c,c1 be non empty positive-yielding XFinSequence of REAL, a be Real st c1=a(#)c holds for x be Nat holds (polynom(c1)).x = a* ( (polynom(c)).x) proof let c,c1 be non empty positive-yielding XFinSequence of REAL, a be Real; assume AS: c1=a(#)c; let x be Nat; D1: dom (c1 (#) seq_a^(x,1,0)) = dom c1 by ASYMPT_2:26 .= dom c by VALUED_1:def 5,AS; D2: dom (a (#) ( c (#) seq_a^(x,1,0) )) =dom ( c (#) seq_a^(x,1,0) ) by VALUED_1:def 5 .= dom c by ASYMPT_2:26; for i be object st i in dom (c1 (#) seq_a^(x,1,0)) holds (c1 (#) seq_a^(x,1,0)).i = (a (#) ( c (#) seq_a^(x,1,0) )).i proof let i be object; assume D3: i in dom (c1 (#) seq_a^(x,1,0)); then D4: i in dom c1 by ASYMPT_2:26; thus (c1 (#) seq_a^(x,1,0)).i = c1.i * (seq_a^(x,1,0)).i by D4,ASYMPT_2:26 .= a*c.i * (seq_a^(x,1,0)).i by AS,VALUED_1:6 .= a* ( c.i * (seq_a^(x,1,0)).i ) .= a* ( c (#) seq_a^(x,1,0) ).i by D3,D1,ASYMPT_2:26 .= (a (#) ( c (#) seq_a^(x,1,0) )).i by VALUED_1:6; end; then P2: c1 (#) seq_a^(x,1,0) = a (#) ( c (#) seq_a^(x,1,0) ) by D1,D2; thus (polynom(c1)).x = Sum( c1 (#) seq_a^(x,1,0)) by ASYMPT_2:def 2 .= a* Sum( c (#) seq_a^(x,1,0)) by AFINSQ_2:64,P2 .= a* (polynom(c)).x by ASYMPT_2:def 2; end; begin :: Algebra of polynomially bounded functions definition let p be Real_Sequence; attr p is polynomially-abs-bounded means :defabs: ex k be Nat st |.p.| in Big_Oh(seq_n^(k)); end; registration cluster polynomially-bounded -> polynomially-abs-bounded for Real_Sequence; coherence proof let p be Real_Sequence; assume p is polynomially-bounded; then consider k be Nat such that L1: p in Big_Oh(seq_n^(k)); consider t be Element of Funcs(NAT, REAL) such that L2: p = t & ex c be Real, N be Element of NAT st c > 0 & for n be Element of NAT st n >= N holds t.n <= c*((seq_n^(k)).n) & t.n >= 0 by L1; consider c be Real, N be Element of NAT such that L3: c > 0 & for n be Element of NAT st n >= N holds t.n <= c*((seq_n^(k)).n) & t.n >= 0 by L2; reconsider abst = |. t .| as Element of Funcs(NAT, REAL) by FUNCT_2:8; for n be Element of NAT st n >= N holds abst.n <= c*((seq_n^(k)).n) & abst.n >= 0 proof let n be Element of NAT; assume LL2:n >= N;then t.n = |. t.n .| by ABSVALUE:def 1,L3 .= |. t.|.n by VALUED_1:18; hence thesis by LL2,L3; end;then |. p .| in Big_Oh(seq_n^(k)) by L2,L3; hence thesis; end; end; theorem LM1: for r be Element of NAT holds for s be Real_Sequence st s = NAT --> r holds s is polynomially-abs-bounded proof let r be Element of NAT; let s1 be Real_Sequence; assume AS: s1 = NAT --> r; set s=|.s1.|; P1: s in Funcs(NAT, REAL) by FUNCT_2:8; now let n be Element of NAT; assume A2: n >= r; n = 0 or n > 0; then A4: (seq_n^ 1) . n = n to_power 1 by ASYMPT_1:def 3 .=n; A5: s.n = |. s1.n .| by VALUED_1:18 .= |. r .| by AS .= r by ABSVALUE:def 1; hence s.n <= 1*(seq_n^ 1).n by A2,A4; thus s.n >= 0 by A5; end; then s in Big_Oh(seq_n^ 1) by P1; hence thesis; end; reconsider rr = 0 as Element of REAL by XREAL_0:def 1; registration cluster polynomially-abs-bounded for Function of NAT,REAL; existence proof take NAT --> rr; thus thesis by LM1; end; end; registration let f,g be polynomially-abs-bounded Function of NAT,REAL; cluster f + g -> polynomially-abs-bounded for Function of NAT,REAL; coherence proof set h = f + g; A3: for n be Nat holds |.h.| .n <= |.f.|.n + |.g.|.n proof let n be Nat; S1: n in NAT by ORDINAL1:def 12; A30: |.h.| .n =|. h.n .| by VALUED_1:18 .= |. f.n + g.n.| by S1,VALUED_1:1; |. f.n .| + |.g.n.| = |. f .|.n + |.g.n.| by VALUED_1:18 .= |.f.|.n + |.g.|.n by VALUED_1:18; hence thesis by COMPLEX1:56,A30; end; consider k1 be Nat such that A4: |.f.| in Big_Oh(seq_n^(k1)) by defabs; consider k2 be Nat such that A5: |.g.| in Big_Oh(seq_n^(k2)) by defabs; consider t1 be Element of Funcs(NAT, REAL) such that A6: |.f.|=t1 & ex c1 be Real,N1 be Element of NAT st c1 > 0 & for n be Element of NAT st n >= N1 holds t1.n <= c1*(seq_n^(k1)).n & t1.n >= 0 by A4; consider t2 be Element of Funcs(NAT, REAL) such that A7: |.g.|=t2 & ex c2 be Real,N2 be Element of NAT st c2 > 0 & for n be Element of NAT st n >= N2 holds t2.n <= c2*(seq_n^(k2)).n & t2.n >= 0 by A5; consider c1 be Real,N1 be Element of NAT such that A8: c1 > 0 & for n be Element of NAT st n >= N1 holds t1.n <= c1*(seq_n^(k1)).n & t1.n >= 0 by A6; consider c2 be Real,N2 be Element of NAT such that A9: c2 > 0 & for n be Element of NAT st n >= N2 holds t2.n <= c2*(seq_n^(k2)).n & t2.n >= 0 by A7; set c = c1+c2; set N = N1+N2; set k = k1+k2; reconsider t = |.h.| as Element of Funcs(NAT, REAL) by FUNCT_2:8; now let n be Element of NAT; assume B11: n >= N+2; N<=N+2 & 2 <= N+2 by NAT_1:12; then A11: N <= n & 2 <= n by B11,XXREAL_0:2; N1 <= N & N2<= N by NAT_1:12; then A12: N1<=n & N2<=n by A11,XXREAL_0:2; then A13: t1.n <= c1*(seq_n^(k1)).n & t1.n >= 0 by A8; A14: t2.n <= c2*(seq_n^(k2)).n & t2.n >= 0 by A12,A9; B15: 1 < n by A11,XXREAL_0:2; B14: k1 <= k & k2 <= k by NAT_1:12; S1: (seq_n^(k1)).n = n to_power k1 by B11,ASYMPT_1:def 3; S2: (seq_n^(k2)).n = n to_power k2 by B11,ASYMPT_1:def 3; S3: (seq_n^(k)).n = n to_power k by B11,ASYMPT_1:def 3; k1 < k or k1=k by XXREAL_0:1,B14; then (seq_n^(k1)).n <= (seq_n^(k)).n by S1,S3,B15,POWER:39; then S4:c1*(seq_n^(k1)).n <= c1*((seq_n^(k)).n) by XREAL_1:64,A8; k2 < k or k2=k by XXREAL_0:1,B14; then (seq_n^(k2)).n <= (seq_n^(k)).n by S2,S3,B15,POWER:39; then c2*(seq_n^(k2)).n <= c2*((seq_n^(k)).n) by XREAL_1:64,A9; then S6: (c1*(seq_n^(k1)).n) + (c2*(seq_n^(k2)).n) <= c1*(seq_n^(k)).n + c2*(seq_n^(k)).n by S4,XREAL_1:7; t1.n + t2.n <= (c1*(seq_n^(k1)).n) + (c2*(seq_n^(k2)).n) by XREAL_1:7,A13,A14; then A15:t1.n + t2.n <= c *(seq_n^(k)).n by S6,XXREAL_0:2; t.n <= t1.n + t2.n by A3,A6,A7; hence t.n <= c *(seq_n^(k)).n by A15,XXREAL_0:2; |.h.| .n =|. h.n .| by VALUED_1:18; hence 0 <=t.n; end; then |.h.| in Big_Oh(seq_n^(k)) by A8,A9; hence thesis; end; cluster f (#) g -> polynomially-abs-bounded for Function of NAT,REAL; coherence proof set h = f(#)g; A3: for n be Nat holds |.h.| .n = |.f.|.n * |.g.|.n proof let n be Nat; thus |.h.| .n =|. h.n .| by VALUED_1:18 .= |. f.n * g.n.| by VALUED_1:5 .= |. f.n .| * |.g.n.| by COMPLEX1:65 .= |. f .|.n * |.g.n.| by VALUED_1:18 .= |.f.|.n * |.g.|.n by VALUED_1:18; end; consider k1 be Nat such that A4: |.f.| in Big_Oh(seq_n^(k1)) by defabs; consider k2 be Nat such that A5: |.g.| in Big_Oh(seq_n^(k2)) by defabs; consider t1 be Element of Funcs(NAT, REAL) such that A6: |.f.|=t1 & ex c1 be Real,N1 be Element of NAT st c1 > 0 & for n be Element of NAT st n >= N1 holds t1.n <= c1*(seq_n^(k1)).n & t1.n >= 0 by A4; consider t2 be Element of Funcs(NAT, REAL) such that A7: |.g.|=t2 & ex c2 be Real,N2 be Element of NAT st c2 > 0 & for n be Element of NAT st n >= N2 holds t2.n <= c2*(seq_n^(k2)).n & t2.n >= 0 by A5; consider c1 be Real,N1 be Element of NAT such that A8: c1 > 0 & for n be Element of NAT st n >= N1 holds t1.n <= c1*(seq_n^(k1)).n & t1.n >= 0 by A6; consider c2 be Real,N2 be Element of NAT such that A9: c2 > 0 & for n be Element of NAT st n >= N2 holds t2.n <= c2*(seq_n^(k2)).n & t2.n >= 0 by A7; set c = c1*c2; set N = N1+N2; set k = k1+k2; reconsider t = |.h.| as Element of Funcs(NAT, REAL) by FUNCT_2:8; now let n be Element of NAT; assume B11: n >= N+2; N<=N+2 & 2 <= N+2 by NAT_1:12; then A11n: N <= n & 2 <= n by B11,XXREAL_0:2; N1 <= N & N2<= N by NAT_1:12; then A12: N1<=n & N2<=n by A11n,XXREAL_0:2; then A13: t1.n <= c1*(seq_n^(k1)).n & t1.n >= 0 by A8; A14: t2.n <= c2*(seq_n^(k2)).n & t2.n >= 0 by A12,A9; A15: t1.n * t2.n <= (c1*(seq_n^(k1)).n) * (c2*(seq_n^(k2)).n) by XREAL_1:66,A13,A14; (c1*(seq_n^(k1)).n) * (c2*(seq_n^(k2)).n) =c1*c2* ( (seq_n^(k1)).n * (seq_n^(k2)).n) .=c1*c2*( (n to_power k1) * (seq_n^(k2)).n) by B11,ASYMPT_1:def 3 .=c1*c2*( (n to_power k1) * (n to_power k2)) by B11,ASYMPT_1:def 3 .=c1*c2*( n to_power (k1+k2) ) by B11,POWER:27 .=c*(seq_n^(k)).n by B11,ASYMPT_1:def 3; hence t.n <= c*(seq_n^(k)).n by A15,A3,A6,A7; 0 <= t1.n * t2.n by A13,A14; hence 0 <=t.n by A3,A6,A7; end; then |.h.| in Big_Oh(seq_n^(k)) by A8,A9; hence thesis; end; end; registration let f be polynomially-abs-bounded Function of NAT,REAL; let a be Element of REAL; cluster a (#) f -> polynomially-abs-bounded for Function of NAT,REAL; coherence proof set h = a (#) f; per cases; suppose CS1: a= 0; X0: dom h = NAT by FUNCT_2:def 1; now let z be object; assume z in dom h; then reconsider n=z as Element of NAT; thus h.z = 0 * f.n by CS1,VALUED_1:6 .= 0; end; then h = NAT --> 0 by FUNCOP_1:11,X0; hence thesis by LM1; end; suppose A0: a <> 0; A3: for n be Nat holds |.h.| .n = |.a.| * |.f.|.n proof let n be Nat; thus |.h.| .n =|. h.n .| by VALUED_1:18 .= |. a*f.n .| by VALUED_1:6 .= |.a.| * |. f.n .| by COMPLEX1:65 .= |.a.| *|. f .|.n by VALUED_1:18; end; consider k1 be Nat such that A4: |.f.| in Big_Oh(seq_n^(k1)) by defabs; consider t1 be Element of Funcs(NAT, REAL) such that A6: |.f.|=t1 & ex c1 be Real,N1 be Element of NAT st c1 > 0 & for n be Element of NAT st n >= N1 holds t1.n <= c1*(seq_n^(k1)).n & t1.n >= 0 by A4; consider c1 be Real,N1 be Element of NAT such that A8: c1 > 0 & for n be Element of NAT st n >= N1 holds t1.n <= c1*(seq_n^(k1)).n & t1.n >= 0 by A6; set c = |.a.| *c1; reconsider t = |.h.| as Element of Funcs(NAT, REAL) by FUNCT_2:8; now let n be Element of NAT; assume B11: n >= N1+2; N1<=N1+2 & 2 <= N1+2 by NAT_1:12; then N1 <= n & 2 <= n by B11,XXREAL_0:2; then A13: t1.n <= c1*(seq_n^(k1)).n & t1.n >= 0 by A8; then A15: |.a.|*t1.n <= |.a.|*(c1*(seq_n^(k1)).n) by XREAL_1:66; thus t.n <= c*(seq_n^(k1)).n by A15,A3,A6; 0 <= |.a.|*t1.n by A13; hence 0 <=t.n by A3,A6; end; then |.h.| in Big_Oh(seq_n^(k1)) by A8,A0; hence thesis; end; end; end; definition func Big_Oh_poly -> Subset of RAlgebra (NAT) means :DefX1: for x being object holds x in it iff x is polynomially-abs-bounded Function of NAT,REAL; existence proof defpred P[object] means $1 is polynomially-abs-bounded Function of NAT,REAL; consider IT being set such that A01: for x being object holds x in IT iff x in Funcs(NAT,REAL) & P[x] from XBOOLE_0:sch 1; A1: for x being object holds x in IT iff x is polynomially-abs-bounded Function of NAT,REAL proof let x being object; x is polynomially-abs-bounded Function of NAT,REAL implies x in Funcs(NAT,REAL) by FUNCT_2:8; hence thesis by A01; end; for x be object st x in IT holds x in Funcs(NAT,REAL) proof let x be object; assume x in IT; then x is polynomially-abs-bounded Function of NAT,REAL by A1; hence x in Funcs(NAT,REAL) by FUNCT_2:8; end; then IT is Subset of RAlgebra(NAT) by TARSKI:def 3; hence thesis by A1; end; uniqueness proof let X1,X2 be Subset of RAlgebra(NAT); assume that A2: for x being object holds x in X1 iff x is polynomially-abs-bounded Function of NAT,REAL and A3: for x being object holds x in X2 iff x is polynomially-abs-bounded Function of NAT,REAL; thus X1 c= X2 proof let x be object; assume x in X1; then x is polynomially-abs-bounded Function of NAT,REAL by A2; hence thesis by A3; end; let x be object; assume x in X2; then x is polynomially-abs-bounded Function of NAT,REAL by A3; hence thesis by A2; end; end; registration cluster Big_Oh_poly -> non empty; coherence proof the polynomially-abs-bounded Function of NAT,REAL in Big_Oh_poly by DefX1; hence thesis; end; end; definition func R_Algebra_of_Big_Oh_poly -> strict AlgebraStr means :defAlgebra: the carrier of it = Big_Oh_poly & the multF of it = (RealFuncMult(NAT)) || Big_Oh_poly & the addF of it = (RealFuncAdd(NAT)) || Big_Oh_poly & the Mult of it = (RealFuncExtMult(NAT)) | [:REAL,Big_Oh_poly:] & the OneF of it = RealFuncUnit(NAT) & the ZeroF of it = RealFuncZero(NAT); correctness proof set X = Big_Oh_poly; set m = (RealFuncMult(NAT)) || X; set a = (RealFuncAdd(NAT)) || X; set E = (RealFuncExtMult(NAT)) | [:REAL,X:]; set O = RealFuncUnit(NAT); set Z = RealFuncZero(NAT); for x being set holds x in [: X,X:] implies (RealFuncMult(NAT)).x in X proof let x be set; assume x in [: X,X:]; then consider f,g be object such that B2: f in X & g in X & x =[f,g] by ZFMISC_1:def 2; reconsider f,g as polynomially-abs-bounded Function of NAT,REAL by DefX1,B2; set h = (RealFuncMult(NAT)).x; reconsider f1=f,g1=g as Element of Funcs(NAT,REAL) by FUNCT_2:8; B5: h= (RealFuncMult(NAT)).(f1,g1) by B2; reconsider h as Function of NAT,REAL by B5; h = f(#)g proof let n be Element of NAT; thus h.n = f.n*g.n by B5,FUNCSDOM:2 .= (f(#)g).n by VALUED_1:5; end; hence thesis by DefX1; end; then X is Preserv of (RealFuncMult(NAT)) by REALSET1:def 1; then reconsider m as BinOp of X by REALSET1:2; for x being set holds x in [: X,X:] implies (RealFuncAdd(NAT)).x in X proof let x be set; assume x in [: X,X:]; then consider f,g be object such that B2: f in X & g in X & x =[f,g] by ZFMISC_1:def 2; reconsider f,g as polynomially-abs-bounded Function of NAT,REAL by DefX1,B2; set h = (RealFuncAdd(NAT)).x; reconsider f1=f,g1=g as Element of Funcs(NAT,REAL) by FUNCT_2:8; B5: h= (RealFuncAdd(NAT)).(f1,g1) by B2; then reconsider h as Function of NAT,REAL; h = f+g proof let n be Element of NAT; thus h.n = f.n+g.n by B5,FUNCSDOM:1 .= (f+g).n by VALUED_1:1; end; hence thesis by DefX1; end; then X is Preserv of (RealFuncAdd(NAT)) by REALSET1:def 1; then reconsider a as BinOp of X by REALSET1:2; Q0: [:REAL,X:] c= [:REAL,Funcs(NAT,REAL):] by ZFMISC_1:95; [:REAL,Funcs(NAT,REAL):] = dom (RealFuncExtMult(NAT)) by FUNCT_2:def 1; then Q1: dom E = [:REAL,X:] by RELAT_1:62,Q0; for h being object st h in rng E holds h in X proof let h be object; assume h in rng E; then consider x be object such that Q2: x in dom E & h = E.x by FUNCT_1:def 3; consider s,f be object such that B2: s in REAL & f in X and B3: x =[s,f] by Q1,Q2,ZFMISC_1:def 2; reconsider f as polynomially-abs-bounded Function of NAT,REAL by DefX1,B2; reconsider s as Element of REAL by B2; H1: h = (RealFuncExtMult(NAT)).x by Q1,Q2,FUNCT_1:49; reconsider f1=f as Element of Funcs(NAT,REAL) by FUNCT_2:8; reconsider h1=h as Element of Funcs(NAT,REAL) by H1,FUNCT_2:5,Q2; reconsider h1 as Function of NAT,REAL; h1 = s(#)f proof let n be Element of NAT; thus h1.n = s*f1.n by B3,H1,FUNCSDOM:4 .= (s(#)f).n by VALUED_1:6; end; hence h in X by DefX1; end; then rng E c= X; then reconsider E as Function of [:REAL,X:],X by Q1,FUNCT_2:2; reconsider O as Real_Sequence; O in Funcs(NAT,REAL) & seq_id O is polynomially-abs-bounded by LM1; then reconsider O as Element of X by DefX1; reconsider Z as Real_Sequence; Z in Funcs(NAT,REAL) & seq_id Z is polynomially-abs-bounded by LM1; then reconsider Z as Element of X by DefX1; set S = AlgebraStr(#X,m,a,E,O,Z#); S is strict AlgebraStr; hence thesis; end; end; registration cluster R_Algebra_of_Big_Oh_poly -> non empty; correctness by defAlgebra; end; theorem LM12: the carrier of R_Algebra_of_Big_Oh_poly c= the carrier of RAlgebra (NAT) proof the carrier of R_Algebra_of_Big_Oh_poly = Big_Oh_poly by defAlgebra; hence thesis; end; theorem LM14: for f be object holds f in R_Algebra_of_Big_Oh_poly iff f is polynomially-abs-bounded Function of NAT,REAL proof let f be object; the carrier of R_Algebra_of_Big_Oh_poly = Big_Oh_poly by defAlgebra; hence f in R_Algebra_of_Big_Oh_poly iff f is polynomially-abs-bounded Function of NAT,REAL by DefX1; end; theorem LM15: for f,g be Point of R_Algebra_of_Big_Oh_poly, f1,g1 be Point of RAlgebra NAT st f=f1 & g=g1 holds f*g = f1*g1 proof let f,g be Point of R_Algebra_of_Big_Oh_poly, f1,g1 be Point of RAlgebra NAT; assume A1: f=f1 & g=g1; set X = Big_Oh_poly; set S = R_Algebra_of_Big_Oh_poly; A3a: the carrier of R_Algebra_of_Big_Oh_poly = X by defAlgebra; thus f*g = ((RealFuncMult(NAT)) || X). ( [f,g] ) by defAlgebra .=f1*g1 by A1,A3a,FUNCT_1:49; end; theorem LM16: for f,g be Point of R_Algebra_of_Big_Oh_poly, f1,g1 be Point of RAlgebra NAT st f=f1 & g=g1 holds f+g = f1+g1 proof let f,g be Point of R_Algebra_of_Big_Oh_poly, f1,g1 be Point of RAlgebra NAT; assume A1: f=f1 & g=g1; set X = Big_Oh_poly; set S = R_Algebra_of_Big_Oh_poly; A3: the carrier of R_Algebra_of_Big_Oh_poly = X by defAlgebra; thus f+g = ((RealFuncAdd(NAT)) || X). ( [f,g] ) by defAlgebra .=f1+g1 by A1,A3,FUNCT_1:49; end; theorem LM17: for f be Point of R_Algebra_of_Big_Oh_poly, f1 be Point of RAlgebra NAT, a be Element of REAL st f=f1 holds a*f = a*f1 proof let f be Point of R_Algebra_of_Big_Oh_poly, f1 be Point of RAlgebra NAT, a be Element of REAL; assume A1: f=f1; set X = Big_Oh_poly; set S = R_Algebra_of_Big_Oh_poly; A3: the carrier of R_Algebra_of_Big_Oh_poly = X by defAlgebra; thus a*f = ((RealFuncExtMult(NAT)) | [:REAL,X:]). ( [a,f] ) by defAlgebra .=a*f1 by A1,A3, FUNCT_1:49; end; theorem LM18: 0.R_Algebra_of_Big_Oh_poly = 0.(RAlgebra NAT) by defAlgebra; theorem LM19: 1. (R_Algebra_of_Big_Oh_poly) = 1. (RAlgebra NAT) by defAlgebra; registration cluster R_Algebra_of_Big_Oh_poly -> strict Abelian add-associative right_zeroed right_complementable commutative associative right_unital right-distributive vector-associative scalar-associative vector-distributive scalar-distributive; correctness proof set S = R_Algebra_of_Big_Oh_poly; thus S is strict; thus S is Abelian proof let x,y be Element of S; reconsider x1=x,y1=y as Element of RAlgebra NAT by LM12; thus x+y = x1+y1 by LM16 .=y + x by LM16; end; thus S is add-associative proof let x,y,z be Element of S; reconsider x1=x,y1=y,z1=z as Element of RAlgebra NAT by LM12; D1: x+y = x1+y1 by LM16; D2: y+z = y1+z1 by LM16; thus (x+y)+z= (x1+y1)+z1 by D1,LM16 .=x1+(y1+z1) by RLVECT_1:def 3 .=x+ (y + z) by D2,LM16; end; thus S is right_zeroed proof let x be Element of S; reconsider x1=x as Element of RAlgebra NAT by LM12; thus x+0.S = x1+ 0.(RAlgebra NAT) by LM18,LM16 .= x; end; thus S is right_complementable proof let x be Element of S; reconsider x1=x as Element of RAlgebra NAT by LM12; set t1=(-1)*x; take t1; -1 is Element of REAL by XREAL_0:def 1; then D1: (-1)*x = (-1)*x1 by LM17; thus x+t1 = x1+ (-1)*x1 by D1,LM16 .= 0.(RAlgebra NAT) by FUNCSDOM:11 .= 0.S by defAlgebra; end; for x,y be Element of S holds x*y = y*x proof let x,y be Element of S; reconsider x1=x,y1=y as Element of RAlgebra NAT by LM12; thus x*y = x1*y1 by LM15 .=y * x by LM15; end; hence S is commutative; for x,y,z be Element of S holds x*y*z = x*(y*z) proof let x,y,z be Element of S; reconsider x1=x,y1=y,z1=z as Element of RAlgebra NAT by LM12; D1: x*y = x1*y1 by LM15; D2: y*z = y1*z1 by LM15; thus (x*y)*z= (x1*y1)*z1 by D1,LM15 .=x1*(y1*z1) by GROUP_1:def 3 .=x* (y * z) by D2,LM15; end; hence S is associative; thus S is right_unital proof let x be Element of S; reconsider x1=x as Element of RAlgebra NAT by LM12; thus x*(1.S) = x1*1.(RAlgebra NAT) by LM19,LM15 .=x by VECTSP_1:def 4; end; for x,y,z be Element of S holds x*(y+z) =x*y+x*z proof let x,y,z be Element of S; reconsider x1=x,y1=y,z1=z as Element of RAlgebra NAT by LM12; D1: x*y = x1*y1 by LM15; D2: x*z = x1*z1 by LM15; D3: y+z = y1+z1 by LM16; thus x*(y+z) = x1*(y1+z1) by D3,LM15 .=x1*y1+x1*z1 by VECTSP_1:def 2 .=x*y + x*z by D1,D2,LM16; end; hence S is right-distributive; for x, y being Element of S for s being Real holds s * (x * y) = (s * x) * y proof let x,y be Element of S; let s be Real; reconsider x1=x,y1=y as Element of RAlgebra NAT by LM12; D1: x*y = x1*y1 by LM15; D3: s is Element of REAL by XREAL_0:def 1; then D2: s*x = s*x1 by LM17; thus s * (x * y) = s * (x1 * y1) by LM17,D1,D3 .=(s*x1)*y1 by FUNCSDOM:def 9 .= (s*x)*y by LM15,D2; end; hence S is vector-associative; for s,t be Real,x be Element of S holds (s*t)*x = s*(t*x) proof let s,t be Real; let x be Element of S; reconsider x1=x as Element of RAlgebra NAT by LM12; D0: s is Element of REAL & t is Element of REAL by XREAL_0:def 1; D2: s*t is Element of REAL by XREAL_0:def 1; D1: t*x = t*x1 by D0,LM17; thus (s*t)*x =(s*t)*x1 by D2,LM17 .=s*(t*x1) by RLVECT_1:def 7 .=s*(t*x) by D0,D1,LM17; end; hence S is scalar-associative; for s being Real for x, y being Element of S holds s * (x + y) = s * x + s * y proof let s be Real; let x,y be Element of S; reconsider x1=x,y1=y as Element of RAlgebra NAT by LM12; D1: x+y = x1+y1 by LM16; D3: s is Element of REAL by XREAL_0:def 1; then D2: s*x = s*x1 by LM17; D4: s*y = s*y1 by LM17,D3; thus s * (x + y) = s * (x1 + y1) by LM17,D1,D3 .=s*x1+ s*y1 by RLVECT_1:def 5 .= s*x + s*y by LM16,D2,D4; end; hence S is vector-distributive; let s,t be Real, v being Element of S; reconsider s,t as Element of REAL by XREAL_0:def 1; reconsider v1=v as Element of RAlgebra NAT by LM12; D2: s*v = s*v1 by LM17; D4: t*v = t*v1 by LM17; (s + t) * v = (s + t) * v1 by LM17 .= s*v1 +t*v1 by RLVECT_1:def 6 .= s*v +t*v by D2,D4,LM16; hence thesis; end; end; theorem R_Algebra_of_Big_Oh_poly is Algebra; theorem TH11: for f,g,h be VECTOR of R_Algebra_of_Big_Oh_poly for f9,g9,h9 be Function of NAT,REAL st f9=f & g9=g & h9=h holds (h = f+g iff for x be Nat holds h9.x = f9.x + g9.x) proof let f,g,h be VECTOR of R_Algebra_of_Big_Oh_poly; reconsider f1=f,g1=g,h1=h as VECTOR of RAlgebra NAT by LM12; let f9,g9,h9 be Function of NAT,REAL such that A2: f9=f & g9=g & h9=h; A3: now assume A4: h = f+g; let x be Nat; LXN:x in NAT by ORDINAL1:def 12; h1=f1+g1 by A4,LM16; hence h9.x=f9.x+g9.x by A2,FUNCSDOM:1,LXN; end; now assume LAS:for x be Nat holds h9.x=f9.x+g9.x; for x be Element of NAT holds h9.x=f9.x+g9.x by LAS; then h1=f1+g1 by A2,FUNCSDOM:1; hence h =f+g by LM16; end; hence thesis by A3; end; theorem TH11A: for f,g,h be VECTOR of R_Algebra_of_Big_Oh_poly for f9,g9,h9 be Function of NAT,REAL st f9=f & g9=g & h9=h holds (h = f*g iff for x be Nat holds h9.x = f9.x * g9.x ) proof let f,g,h be VECTOR of R_Algebra_of_Big_Oh_poly; reconsider f1=f,g1=g,h1=h as VECTOR of RAlgebra NAT by LM12; let f9,g9,h9 be Function of NAT,REAL such that A2: f9=f & g9=g & h9=h; A3: now assume A4: h = f*g; let x be Nat; LXN:x in NAT by ORDINAL1:def 12; h1=f1*g1 by A4,LM15; hence h9.x=f9.x*g9.x by A2,FUNCSDOM:2,LXN; end; now assume for x be Element of NAT holds h9.x=f9.x*g9.x; then h1=f1*g1 by A2,FUNCSDOM:2; hence h =f*g by LM15; end; hence thesis by A3; end; theorem TH12: for f,h be VECTOR of R_Algebra_of_Big_Oh_poly for f9,h9 be Function of NAT,REAL st f9=f & h9=h for a be Real holds h = a*f iff for x be Nat holds h9.x = a*f9.x proof let f,h be VECTOR of R_Algebra_of_Big_Oh_poly; let f9,h9 be Function of NAT,REAL such that A1: f9=f & h9=h; let a be Real; A0:a is Element of REAL by XREAL_0:def 1; reconsider f1=f, h1=h as VECTOR of RAlgebra NAT by LM12; A3: now assume A4: h = a*f; let x be Nat; LXN:x in NAT by ORDINAL1:def 12; h1=a*f1 by A4,LM17,A0; hence h9.x=a*f9.x by A1,FUNCSDOM:4,LXN; end; now assume for x be Element of NAT holds h9.x=a*f9.x; then h1=a*f1 by A1,FUNCSDOM:4; hence h =a*f by A0,LM17; end; hence thesis by A3; end; begin :: negligible functions definition let f be Function of NAT,REAL; attr f is negligible means :defneg: for c be non empty positive-yielding XFinSequence of REAL holds ex N be Nat st for x be Nat st N <=x holds |. f.x .| < 1/((polynom(c)).x); end; theorem PXR1: for r be Real st 0 < r holds ex c be non empty positive-yielding XFinSequence of REAL st for x be Nat holds (polynom(c)).x = r proof let r be Real; assume AS: 0 < r; r is Element of REAL by XREAL_0:def 1;then reconsider z= <% r %> as XFinSequence of REAL; now let x be Real; assume x in rng z; then x in {r} by AFINSQ_1:33; hence 0 < x by AS,TARSKI:def 1; end; then A1: z is positive-yielding; reconsider z as non empty positive-yielding XFinSequence of REAL by A1; take z; len z = 1 by AFINSQ_1:34; then consider a be Real such that A2: a = z.0 & for x be Nat holds (seq_p(z)).x = a by ASYMPT_2:29; thus thesis by A2; end; theorem PXR2: for f be Function of NAT,REAL st f is negligible holds for r be Real st 0 < r holds ex N be Nat st for x be Nat st N <=x holds |. f.x .| < r proof let f be Function of NAT,REAL; assume AS: f is negligible; let r be Real; assume 0 < r;then consider c be non empty positive-yielding XFinSequence of REAL such that P1: for x be Nat holds (polynom(c)).x = 1/r by PXR1; consider N be Nat such that P2: for x be Nat st N <=x holds |. f.x .| < 1/((polynom(c)).x) by AS; take N; thus for x be Nat st N <=x holds |. f.x .| < r proof let x be Nat; assume N <=x; then |. f.x .| < 1/((polynom(c)).x) by P2; then |. f.x .| < 1/(1/r) by P1; hence |. f.x .| < r by XCMPLX_1:52; end; end; theorem for f be Function of NAT,REAL st f is negligible holds f is convergent & lim f = 0 proof let f be Function of NAT,REAL; assume AS: f is negligible; A1:for p be Real st 0
negligible; coherence proof set f = seq_const 0; let c be non empty positive-yielding XFinSequence of REAL; take N = 0; let x be Nat; D2: |. f.x .| = |. 0 .| by SEQ_1:57 .= 0; 0 < (polynom(c)).x by NLM3; hence thesis by D2; end; end; registration cluster negligible for Function of NAT,REAL; correctness proof seq_const 0 is negligible; hence thesis; end; end; registration let f be negligible Function of NAT,REAL; cluster |.f.| -> negligible for Function of NAT,REAL; coherence proof let g be Function of NAT,REAL such that A1: g = |.f.|; let c be non empty positive-yielding XFinSequence of REAL; consider N be Nat such that D3: for x be Nat st N <=x holds |. f.x .| < 1/((polynom(c)).x) by defneg; take N; let x be Nat; assume B1: N <=x; |. |.f.|.x .| = |. |.f.x.| .| by SEQ_1:12 .= |. f.x .|; hence thesis by A1,D3,B1; end; end; registration let f be negligible Function of NAT,REAL, a be Real; cluster a(#)f -> negligible for Function of NAT,REAL; coherence proof let g be Function of NAT,REAL such that A1: g = a(#)f; let c be non empty positive-yielding XFinSequence of REAL; per cases; suppose D1: a=0; take N = 0; let x be Nat; assume N <=x; D2: |. (a(#)f).x .| = |. a*f.x .| by VALUED_1:6 .= 0 by D1; 0 < (polynom(c)).x by NLM3; hence thesis by A1,D2; end; suppose F1: a<>0; reconsider c1 = |.a .| (#) c as non empty positive-yielding XFinSequence of REAL by NLM2,F1; consider N be Nat such that F3: for x be Nat st N <=x holds |. f.x .| < 1/((polynom(c1)).x) by defneg; take N; let x be Nat; assume F4: N <=x; K2: 0 < (polynom(c)).x by NLM3; F6: (polynom(c1)).x = |. a .| * ((polynom(c)).x) by NLM4; K4: 0 < (polynom(c1)).x by NLM3; |. f.x .| < 1/((polynom(c1)).x) by F3,F4; then |. f.x .| * ((polynom(c1)).x)< 1/((polynom(c1)).x) * ((polynom(c1)).x) by K4,XREAL_1:68; then (|. f.x .|* |. a .|) * (polynom(c)).x < 1 by F6,K4,XCMPLX_1:87; then |. a*f.x .|* ((polynom(c)).x) < 1 by COMPLEX1:65; then |. (a(#)f).x .|* ((polynom(c)).x) < 1 by VALUED_1:6; then |. (a(#)f).x .|* ((polynom(c)).x)/((polynom(c)).x) < 1/((polynom(c)).x) by K2,XREAL_1:74; hence thesis by A1,K2,XCMPLX_1:89; end; end; end; registration let f,g be negligible Function of NAT,REAL; cluster f+g -> negligible for Function of NAT,REAL; coherence proof let h be Function of NAT,REAL such that A0: h = f+g; let c be non empty positive-yielding XFinSequence of REAL; reconsider c1 = 2 (#) c as non empty positive-yielding XFinSequence of REAL by NLM2; consider N1 be Nat such that D1: for x be Nat st N1 <=x holds |. f.x .| < 1/((polynom(c1)).x) by defneg; consider N2 be Nat such that D2: for x be Nat st N2 <=x holds |. g.x .| < 1/((polynom(c1)).x) by defneg; take N=N1+N2; let x be Nat; assume D3: N <=x; N1 <= N by NAT_1:12; then N1<= x by D3,XXREAL_0:2; then D4: |. f.x .| < 1/((polynom(c1)).x) by D1; N2 <= N by NAT_1:12; then N2<= x by D3,XXREAL_0:2; then D5: |. g.x .| < 1/((polynom(c1)).x) by D2; F6: (polynom(c1)).x = 2 * ((polynom(c)).x) by NLM4; |. (f+g).x .| = |. f.x + g.x .| proof x in NAT by ORDINAL1:def 12; hence thesis by VALUED_1:1; end; then D6: |. (f+g).x .| <= |. f.x .| + |. g.x .| by COMPLEX1:56; |. f.x .| + |. g.x .| < (1/((polynom(c1)).x)) + (1/((polynom(c1)).x)) by D4,D5,XREAL_1:8; then |. (f+g).x .| < 2* (1/((polynom(c1)).x)) by XXREAL_0:2,D6; hence thesis by A0,XCMPLX_1:92,F6; end; end; registration let f,g be negligible Function of NAT,REAL; cluster f(#)g -> negligible for Function of NAT,REAL; coherence proof let h be Function of NAT,REAL such that A0: h = f(#)g; let c1 be non empty positive-yielding XFinSequence of REAL; consider N1 be Nat such that D1: for x be Nat st N1 <=x holds |. f.x .| < 1/2 by PXR2; consider N2 be Nat such that D2: for x be Nat st N2 <=x holds |. g.x .| < 1/((polynom(c1)).x) by defneg; take N=N1+N2; let x be Nat; assume D3: N <=x; N1 <= N by NAT_1:12; then N1<= x by D3,XXREAL_0:2; then D4: |. f.x .| < 1/2 by D1; N2 <= N by NAT_1:12; then N2<= x by D3,XXREAL_0:2; then D5: |. g.x .| < 1/((polynom(c1)).x) by D2; then F6: (1/2) * (1/((polynom(c1)).x)) < 1* (1/((polynom(c1)).x)) by XREAL_1:97; |. (f(#)g).x .| = |. f.x * g.x .| by VALUED_1:5; then D6: |. (f(#)g).x .| = |. f.x .| * |. g.x .| by COMPLEX1:65; |. f.x .| * |. g.x .| <= (1/2) * (1/((polynom(c1)).x)) by D4,D5,XREAL_1:66; hence thesis by A0,F6,XXREAL_0:2,D6; end; end; theorem TH3: for f be Function of NAT,REAL st for x be Nat holds f.x = 1/ (2 to_power x) holds f is negligible proof let f be Function of NAT,REAL; assume AS: for x be Nat holds f.x = 1/ (2 to_power x); let c be non empty positive-yielding XFinSequence of REAL; set k = len c; deffunc F(Nat) = 1*($1 to_power k); consider y be Real_Sequence such that P1: for x be Nat holds y.x = F(x) from SEQ_1:sch 1; consider N1 be Nat such that P2: for x be Nat st N1 <=x holds |.(seq_p(c)).x .| <= y.x by ASYMPT_2:43,P1; consider N2 be Nat such that P3: for x be Nat st N2 <= x holds 1/ (2 to_power x) < 1/ (x to_power k) by L2; set N=N1+N2; reconsider N as Element of NAT by ORDINAL1:def 12; take N; thus for x be Nat st N <=x holds |. f.x .| < 1/((polynom(c)).x) proof let x be Nat; assume D3:N <=x; K1: f.x = 1/ (2 to_power x) by AS; N2 <= N by NAT_1:12; then N2<= x by D3,XXREAL_0:2; then 1/ (2 to_power x) < 1/ (x to_power k) by P3; then P4: |.f.x .| < 1/ (x to_power k) by K1,ABSVALUE:def 1; N1 <= N by NAT_1:12; then N1<= x by D3,XXREAL_0:2; then |.(polynom(c)).x .| <= y.x by P2; then (polynom(c)).x <= y.x by ABSVALUE:def 1; then (polynom(c)).x <= 1*(x to_power k) by P1; then 1/ x to_power k <= 1/ ((polynom(c)).x) by XREAL_1:118,NLM3; hence |.f.x .| < 1/ ((polynom(c)).x) by P4,XXREAL_0:2; end; end; theorem TH4: for f,g be Function of NAT,REAL st f is negligible & for x be Nat holds |. g.x .| <= |. f.x .| holds g is negligible proof let f,g be Function of NAT,REAL; assume AS: f is negligible & for x be Nat holds |. g.x .| <= |.f.x.|; thus g is negligible proof let c be non empty positive-yielding XFinSequence of REAL; consider N be Nat such that D3: for x be Nat st N <=x holds |. f.x .| < 1/((polynom(c)).x) by AS; take N; let x be Nat; assume N <=x; then D2: |. f.x .| < 1/((polynom(c)).x) by D3; |. g.x .| <= |. f.x .| by AS; hence thesis by D2,XXREAL_0:2; end; end; registration cluster negligible -> polynomially-abs-bounded for Function of NAT,REAL; coherence proof let f be Function of NAT,REAL; assume A0: f is negligible; consider c be non empty positive-yielding XFinSequence of REAL such that P1: for x be Nat holds (polynom(c)).x = 1 by PXR1; consider N be Nat such that P2: for x be Nat st N <=x holds |. f.x .| < 1/((polynom(c)).x) by A0; set s =|. f .|; ZP1: s in Funcs(NAT, REAL) by FUNCT_2:8; now let n be Element of NAT; assume A2: n >= N+2; 2<=N+2 by NAT_1:12; then 2 <= n by A2,XXREAL_0:2; then A3: n > 1 by XXREAL_0:2; A4: (seq_n^ 1) . n = n to_power 1 by A2, ASYMPT_1:def 3 .=n; A5: s.n = |. f.n .| by VALUED_1:18; N <= N+2 by NAT_1:12; then N <= n by A2,XXREAL_0:2; then s.n < 1/((polynom(c)).n) by A5,P2; then s.n < 1/1 by P1; hence s.n <= 1*(seq_n^ 1).n by XXREAL_0:2,A3,A4; thus s.n >= 0 by A5; end; then s in Big_Oh(seq_n^ 1) by ZP1; hence thesis; end; end; definition func negligibleFuncs -> Subset of Big_Oh_poly means :Def1: for x being object holds x in it iff x is negligible Function of NAT,REAL; existence proof defpred P[object] means $1 is negligible Function of NAT,REAL; consider IT being set such that A01: for x being object holds x in IT iff x in Funcs(NAT,REAL) & P[x] from XBOOLE_0:sch 1; A1: for x being object holds x in IT iff x is negligible Function of NAT,REAL proof let x be object; x is negligible Function of NAT,REAL implies x in Funcs(NAT,REAL) by FUNCT_2:8; hence thesis by A01; end; for x be object st x in IT holds x in Big_Oh_poly proof let x be object; assume x in IT; then x is negligible Function of NAT,REAL by A1; hence x in Big_Oh_poly by DefX1; end; then IT is Subset of Big_Oh_poly by TARSKI:def 3; hence thesis by A1; end; uniqueness proof let X1,X2 be Subset of Big_Oh_poly; assume that A2: for x being object holds x in X1 iff x is negligible Function of NAT,REAL and A3: for x being object holds x in X2 iff x is negligible Function of NAT,REAL; thus X1 c= X2 proof let x be object; assume x in X1; then x is negligible Function of NAT,REAL by A2; hence thesis by A3; end; let x be object; assume x in X2; then x is negligible Function of NAT,REAL by A3; hence thesis by A2; end; end; registration cluster negligibleFuncs -> non empty; coherence proof the negligible Function of NAT,REAL in negligibleFuncs by Def1; hence thesis; end; end; theorem RSSPAC2: for v, w being VECTOR of R_Algebra_of_Big_Oh_poly, v1,w1 being Function of NAT,REAL st v=v1 & w1=w holds v + w = v1 + w1 proof let v, w be VECTOR of R_Algebra_of_Big_Oh_poly, v1,w1 being Function of NAT,REAL; assume A0: v=v1 & w1=w; v+w in the carrier of R_Algebra_of_Big_Oh_poly; then v+w in Big_Oh_poly by defAlgebra;then reconsider h=v+w as Function of NAT,REAL by DefX1; h = v1 + w1 proof let n be Element of NAT; thus h. n = (v1 . n) + (w1 . n) by A0,TH11 .= (v1 + w1) . n by VALUED_1:1; end; hence v + w = v1 + w1; end; theorem RSSPAC2A: for v, w being VECTOR of R_Algebra_of_Big_Oh_poly, v1,w1 being Function of NAT,REAL st v=v1 & w1=w holds v * w = v1 (#) w1 proof let v, w be VECTOR of R_Algebra_of_Big_Oh_poly, v1,w1 be Function of NAT,REAL; assume A0: v=v1 & w1=w; v*w in the carrier of R_Algebra_of_Big_Oh_poly; then v*w in Big_Oh_poly by defAlgebra;then reconsider h=v*w as Function of NAT,REAL by DefX1; h = v1 (#) w1 proof let n be Element of NAT; thus h. n = (v1 . n) * (w1 . n) by TH11A,A0 .= (v1 (#) w1) . n by VALUED_1:5; end; hence v * w = v1 (#) w1; end; theorem RSSPAC3: for a be Real,v being VECTOR of R_Algebra_of_Big_Oh_poly, v1 be Function of NAT,REAL st v=v1 holds a*v= a (#) v1 proof let a be Real; let v be VECTOR of R_Algebra_of_Big_Oh_poly, v1 be Function of NAT,REAL; assume A0: v=v1; a*v in the carrier of R_Algebra_of_Big_Oh_poly; then a*v in Big_Oh_poly by defAlgebra;then reconsider h=a*v as Function of NAT,REAL by DefX1; h = a (#) v1 proof let n be Element of NAT; thus h. n = a* (v1 . n) by TH12,A0 .= (a (#) v1) . n by VALUED_1:6; end; hence a*v = a (#) v1; end; theorem for a be Real for v be VECTOR of R_Algebra_of_Big_Oh_poly st v in negligibleFuncs holds a * v in negligibleFuncs proof let a be Real; let v be VECTOR of R_Algebra_of_Big_Oh_poly; assume v in negligibleFuncs; then reconsider v1=v as negligible Function of NAT,REAL by Def1; a(#)v1 is negligible; then a*v is negligible Function of NAT,REAL by RSSPAC3; hence thesis by Def1; end; theorem for v,u be VECTOR of R_Algebra_of_Big_Oh_poly st v in negligibleFuncs & u in negligibleFuncs holds v + u in negligibleFuncs proof let v,u be VECTOR of R_Algebra_of_Big_Oh_poly; assume v in negligibleFuncs & u in negligibleFuncs; then reconsider v1=v,u1=u as negligible Function of NAT,REAL by Def1; v1+u1 is negligible; then v+u is negligible Function of NAT,REAL by RSSPAC2; hence thesis by Def1; end; theorem for v,u be VECTOR of R_Algebra_of_Big_Oh_poly st v in negligibleFuncs & u in negligibleFuncs holds v * u in negligibleFuncs proof let v,u be VECTOR of R_Algebra_of_Big_Oh_poly; assume v in negligibleFuncs & u in negligibleFuncs; then reconsider v1=v,u1=u as negligible Function of NAT,REAL by Def1; v1(#)u1 is negligible; then v*u is negligible Function of NAT,REAL by RSSPAC2A; hence thesis by Def1; end; definition let f,g be Function of NAT,REAL; pred f negligibleEQ g means ex h be Function of NAT,REAL st h is negligible & for x be Nat holds |. f.x - g.x .| <= |.h.x.|; reflexivity proof let f be Function of NAT,REAL; deffunc F(Nat) = 1/ (2 to_power $1); consider h be Real_Sequence such that P1: for x be Nat holds h.x = F(x) from SEQ_1:sch 1; take h; thus h is negligible by TH3,P1; let x be Nat; |. f.x - f.x .| = 0; hence |. f.x - f.x .| <=|.h.x.|; end; symmetry proof let f,g be Function of NAT,REAL; given h be Function of NAT,REAL such that P1: h is negligible & for x be Nat holds |. f.x - g.x .| <= |.h.x.|; take h; thus h is negligible by P1; let x be Nat; |. f.x - g.x .| <= |.h.x.| by P1; hence |. g.x - f.x .| <= |.h.x.| by COMPLEX1:60; end; end; theorem for f,g,h be Function of NAT,REAL st f negligibleEQ g & g negligibleEQ h holds f negligibleEQ h proof let f,g,h be Function of NAT,REAL; given v be Function of NAT,REAL such that B1: v is negligible & for x be Nat holds |. f.x - g.x .| <= |.v.x.|; given w be Function of NAT,REAL such that B2: w is negligible & for x be Nat holds |. g.x - h.x .| <= |.w.x.|; take u = |.v.| + |.w.|; thus u is negligible by B1,B2; let x be Nat; B4: |. f.x - g.x .| <= |.v.x.| by B1; B5: |. g.x - h.x .| <= |.w.x.| by B2; |. f.x - h.x .| = |. (f.x -g.x) + (g.x - h.x) .|; then B6: |. f.x - h.x .| <= |. (f.x -g.x) .| + |. (g.x -h.x) .| by COMPLEX1:56; |. (f.x -g.x) .| + |. g.x - h.x .| <= |.v.x.| + |.w.x.| by B4,B5,XREAL_1:7; then B7: |. f.x - h.x .| <= |.v.x.| + |.w.x.| by B6,XXREAL_0:2; x in NAT by ORDINAL1:def 12;then consider y be Element of NAT such that LXY: x=y; |.v.x.| + |.w.x.| = (|. v .|).x + |.w.x.| by SEQ_1:12 .= (|. v .|).x + (|. w .|).x by SEQ_1:12 .= (|. v .|+|. w .|).x by LXY,VALUED_1:1; hence |. f.x - h.x .| <= |. u.x .| by B7,ABSVALUE:def 1; end; theorem for f,g be Function of NAT,REAL holds f negligibleEQ g iff f-g is negligible proof let f,g be Function of NAT,REAL; hereby assume A1: f negligibleEQ g; consider v be Function of NAT,REAL such that B1: v is negligible & for x be Nat holds |. f.x - g.x .| <= |.v.x.| by A1; for x be Nat holds |. (f-g).x .| <= |.v.x.| proof let x be Nat; x in NAT by ORDINAL1:def 12;then consider y be Element of NAT such that LXY: x=y; |. (f-g).y .| = |. f.y-g.y .| by VALUED_1:15; hence thesis by B1,LXY; end; hence (f-g) is negligible by B1,TH4; end; set v = f-g; for x be Nat holds |. f.x-g.x .| <= |.v.x.| proof let x be Nat; x in NAT by ORDINAL1:def 12; hence thesis by VALUED_1:15; end; hence thesis; end; theorem LRNG1: for c be non empty positive-yielding XFinSequence of REAL ex a be Real, k,N be Nat st 0 < a & 0 < k & for x be Nat st N<= x holds (polynom(c)).x <=a* (x to_power k) proof let c be non empty positive-yielding XFinSequence of REAL; 1 - 1 <= (len c) -1 by XREAL_1:9,NAT_1:14;then (len c) -1 in NAT by INT_1:3;then reconsider k = (len c) -1 as Nat; C1:len c = k+1; k+1 -1 < len c - 0 by XREAL_1:15; then k in Segm(len c) by NAT_1:44; then C2: c.k in rng c by FUNCT_1:3; for n being Nat st 0 <= n holds 0 <= (seq_p(c)).n by NLM3; then reconsider f = seq_p(c) as eventually-nonnegative Real_Sequence by ASYMPT_0:def 2; f in Big_Oh( seq_n^(k) ) by ASYMPT_2:45,C1,C2,PARTFUN3:def 1; then consider N be Nat such that C5: for x be Nat st N <= x holds f.x <= (seq_n^(k+1)).x by ASYMPT_2:39; reconsider m = k+1 as Nat; reconsider M = N+1 as Nat; take 1,m,M; for x be Nat st M <= x holds f.x <= 1* (x to_power m) proof let x be Nat; assume C8:M <= x; CX: x is Element of NAT by ORDINAL1:def 12; N+1 -1 < M -0 by XREAL_1:15; then N < x by C8,XXREAL_0:2; then f.x <= (seq_n^(m)).x by C5; hence thesis by C8,ASYMPT_1:def 3,CX; end; hence thesis; end; registration let a be nonnegative-yielding XFinSequence of REAL, b be nonnegative-yielding Real_Sequence; cluster a (#) b -> nonnegative-yielding; coherence proof for r being Real st r in rng (a (#) b) holds 0 <= r proof let r be Real; assume r in rng (a (#) b); then consider x being object such that AS1: x in dom (a (#) b) & r = (a (#) b).x by FUNCT_1:def 3; x in dom a /\ dom b by AS1,VALUED_1:def 4;then x in dom a & x in dom b by XBOOLE_0:def 4;then a.x in rng a & b.x in rng b by FUNCT_1:3;then L1:0 <= a.x & 0 <= b.x by PARTFUN3:def 4; (a (#) b).x = a.x * b.x by AS1,VALUED_1:def 4; hence thesis by L1, AS1; end; hence thesis; end; end; registration let a,b be nonnegative-yielding XFinSequence of REAL; cluster a ^ b -> nonnegative-yielding; coherence proof for r being Real st r in rng (a^b) holds 0 <= r proof let r be Real; assume r in rng (a^b);then r in (rng a \/ rng b) by AFINSQ_1:26; then r in rng a or r in rng b by XBOOLE_0:def 3; hence thesis by PARTFUN3:def 4; end; hence thesis; end; end; registration let a,b,c be non negative Real; cluster seq_a^(a,b,c) -> nonnegative-yielding; coherence proof set f = seq_a^(a,b,c); for r be Real st r in rng f holds r >= 0 proof let r be Real; assume r in rng f; then consider n being object such that A2: n in dom f & r = f.n by FUNCT_1:def 3; reconsider n as Element of NAT by A2; LL1:r = a to_power (b*n+c) by ASYMPT_1:def 1,A2; now per cases; case CA0: a = 0; now per cases; case b*n+c <>0; hence thesis by CA0,LL1,POWER:def 2; end; case b*n+c = 0; hence thesis by POWER:24,LL1; end; end; hence thesis; end; case 0 < a; hence thesis by LL1,POWER:34; end; end; hence thesis; end; hence thesis; end; end; theorem LRNG2: for a be Real, k be Nat holds ex c be non empty positive-yielding XFinSequence of REAL st for x be Nat holds a* (x to_power k) <= (polynom(c)).x proof let a be Real,k be Nat; reconsider c = Segm (k+1) --> (|. a .| +1 ) as XFinSequence of REAL by AFINSQ_1:63,XREAL_0:def 1; reconsider c as non empty positive-yielding XFinSequence of REAL; take c; for x be Nat holds a* (x to_power k) <=(polynom(c)).x proof let x be Nat; set c2 = c (#) seq_a^(x,1,0); T0: (polynom(c)).x = Sum(c2) by ASYMPT_2:def 2; LN2:k +0 < k+1 by XREAL_1:8; T1:dom c2 = dom c /\ dom seq_a^(x,1,0) by VALUED_1:def 4 .= dom c /\ NAT by SEQ_1:1 .= (Segm (k+1)) /\ NAT; T3:c2.k=(c.k)*((seq_a^(x,1,0)).k) by VALUED_1:5 .=(c.k)*(x to_power (1*k+0)) by ASYMPT_1:def 1 .= (|. a .| +1)*(x to_power k) by FUNCOP_1:7,NAT_1:44,LN2; a < (|. a .| +1) by TCL001; then T4:a*(x to_power k) <= (|. a .| +1)*(x to_power k) by XREAL_1:64; len c2 = k+1 by T1,XBOOLE_1:28;then Sum c2 >= (|. a .| +1)*(x to_power k) by T3,AFINSQ_2:61,NAT_1:44,LN2; hence thesis by T4,XXREAL_0:2,T0; end; hence thesis; end; theorem RNG0: for c,s be non empty positive-yielding XFinSequence of REAL ex d be non empty positive-yielding XFinSequence of REAL, N be Nat st for x be Nat st N<= x holds (polynom(c)).x * (polynom(s)).x <= (polynom(d)).x proof let c,s be non empty positive-yielding XFinSequence of REAL; consider a1 be Real, k1,N1 be Nat such that P1: 0 < a1 & 0 < k1 & for x be Nat st N1<= x holds (polynom(c)).x <=a1* (x to_power k1) by LRNG1; consider a2 be Real, k2,N2 be Nat such that P2: 0 < a2 & 0 < k2 & for x be Nat st N2<= x holds (polynom(s)).x <=a2* (x to_power k2) by LRNG1; consider d be non empty positive-yielding XFinSequence of REAL such that P3: for x be Nat holds (a1*a2)*(x to_power (k1+k2)) <=(polynom(d)).x by LRNG2; set N = N1+N2; take d,N; let x be Nat; assume P4:N <=x; N1<=N by NAT_1:12; then N1<=x by XXREAL_0:2,P4; then P5: (polynom(c)).x <=a1* (x to_power k1) by P1; N2<=N by NAT_1:12; then N2<=x by XXREAL_0:2,P4; then P6: (polynom(s)).x <=a2* (x to_power k2) by P2; P7: 0 < (polynom(c)).x by NLM3; P8: 0 < (polynom(s)).x by NLM3; P9: (polynom(c)).x * (polynom(s)).x <= (a1* (x to_power k1))*(a2* (x to_power k2)) by XREAL_1:66,P5,P6,P7,P8; P10: (a1* (x to_power k1))*(a2* (x to_power k2)) =(a1*a2)*(x to_power (k1+k2)) proof per cases; suppose P11: x=0; P12: x to_power k1 = 0 by P1,P11,POWER:def 2; x to_power (k1+k2) =0 by P2,P11,POWER:def 2; hence thesis by P12; end; suppose x<>0; then (x to_power k1) * (x to_power k2) = x to_power (k1+k2) by POWER:27; hence thesis; end; end; (a1*a2)*(x to_power (k1+k2)) <= (polynom(d)).x by P3; hence (polynom(c)).x * (polynom(s)).x <=(polynom(d)).x by P9,P10,XXREAL_0:2; end; registration let f be negligible Function of NAT,REAL, c be non empty positive-yielding XFinSequence of REAL; cluster (polynom(c)) (#) f -> negligible for Function of NAT,REAL; coherence proof let g be Function of NAT,REAL such that A0: g = (polynom(c)) (#) f; let s be non empty positive-yielding XFinSequence of REAL; consider d be non empty positive-yielding XFinSequence of REAL, N0 be Nat such that P1: for x be Nat st N0 <= x holds (polynom(c)).x * (polynom(s)).x <= (polynom(d)).x by RNG0; consider N1 be Nat such that P2: for x be Nat st N1 <=x holds |. f.x .| < 1/((polynom(d)).x) by defneg; take N=N0+N1; let x be Nat; assume P3:N <=x; P4: 0 < (polynom(c)).x by NLM3; Q4: 0 < (polynom(d)).x by NLM3; N1 <= N by NAT_1:12; then N1<=x by P3,XXREAL_0:2; then P7: |. f.x .| < 1/((polynom(d)).x) by P2; P6: |. f.x .|*(polynom(c)).x < 1/((polynom(d)).x) * (polynom(c)).x by P7,P4,XREAL_1:97; Q6: 0 < (polynom(s)).x by NLM3; N0 <= N by NAT_1:12; then N0<=x by P3,XXREAL_0:2; then (polynom(c)).x * (polynom(s)).x <= (polynom(d)).x by P1; then 1/(polynom(d)).x <= 1/((polynom(c)).x * (polynom(s)).x) by P4,Q6,XREAL_1:118; then P8: 1/(polynom(d)).x * (polynom(c)).x <= 1/((polynom(c)).x * (polynom(s)).x) * (polynom(c)).x by Q4,P4,XREAL_1:66; P5: 1/((polynom(c)).x * (polynom(s)).x ) * (polynom(c)).x = 1/((polynom(s)).x) by P4,XCMPLX_1:92; |. f.x .|*(polynom(c)).x = |. f.x .|*|.(polynom(c)).x .| by P4,ABSVALUE:def 1 .= |. ((polynom(c)).x)*(f.x) .| by COMPLEX1:65 .= |. ((polynom(c))(#)f).x .| by VALUED_1:5; hence thesis by A0,P5,XXREAL_0:2,P6,P8; end; end; theorem RNG2: for g be polynomially-abs-bounded Function of NAT,REAL ex d be non empty positive-yielding XFinSequence of REAL, N be Nat st for x be Nat st N<= x holds |. g.x .| <= (polynom(d)).x proof let g be polynomially-abs-bounded Function of NAT,REAL; consider k1 be Nat such that A4: |.g.| in Big_Oh(seq_n^(k1)) by defabs; consider t1 be Element of Funcs(NAT, REAL) such that A6: |.g.|=t1 & ex c1 be Real,N1 be Element of NAT st c1 > 0 & for n be Element of NAT st n >= N1 holds t1.n <= c1*(seq_n^(k1)).n & t1.n >= 0 by A4; consider c1 be Real,N1 be Element of NAT such that A7: c1 > 0 & for n be Element of NAT st n >= N1 holds t1.n <= c1*(seq_n^(k1)).n & t1.n >= 0 by A6; consider d be non empty positive-yielding XFinSequence of REAL such that A8: for x be Nat holds c1* (x to_power k1) <=(polynom(d)).x by LRNG2; reconsider N=N1+1 as Nat; take d,N; let x be Nat; assume B1: N<=x; LXN: x is Element of NAT by ORDINAL1:def 12; N1<=N by NAT_1:12; then N1<=x by XXREAL_0:2,B1; then A9:t1.x <= c1*(seq_n^(k1)).x & t1.x >= 0 by A7,LXN; A10:(seq_n^(k1)).x = x to_power k1 by ASYMPT_1:def 3,LXN,B1; c1* (x to_power k1) <=(polynom(d)).x by A8; then t1.x <= (polynom(d)).x by A10,A9,XXREAL_0:2; hence |.g.x.| <= (polynom(d)).x by A6,VALUED_1:18; end; registration let f be negligible Function of NAT,REAL, g be polynomially-abs-bounded Function of NAT,REAL; cluster g(#)f -> negligible for Function of NAT,REAL; coherence proof let h be Function of NAT,REAL such that A0: h = g(#)f; consider s be non empty positive-yielding XFinSequence of REAL, N0 be Nat such that P1: for x be Nat st N0 <= x holds |. g.x .| <= (polynom(s)).x by RNG2; let d be non empty positive-yielding XFinSequence of REAL; (polynom(s))(#)f is negligible; then consider N1 be Nat such that P2: for x be Nat st N1 <=x holds |. ((polynom(s))(#)f).x .| < 1/((polynom(d)).x); take N=N1+N0; let x be Nat; assume P3: N <=x; P4: |. ( g(#)f ).x .| = |.g.x * f.x .| by VALUED_1:5 .=|.g.x.| *|.f.x.| by COMPLEX1:65; N0 <= N by NAT_1:12; then N0 <= x by XXREAL_0:2,P3; then P6: |. g.x .| <= (polynom(s)).x by P1; Q7: 0 < (polynom(s)).x by NLM3; (polynom(s)).x * |.f.x.| = |.(polynom(s)).x .| * |.f.x.| by Q7,ABSVALUE:def 1 .= |. ((polynom(s)).x)*(f.x) .| by COMPLEX1:65 .= |. ((polynom(s))(#)f).x .| by VALUED_1:5; then P8: |. ( g(#)f ).x .| <= |. ((polynom(s))(#)f).x .| by P4,XREAL_1:66,P6; N1<=N by NAT_1:12; then N1 <= x by P3,XXREAL_0:2; then |. ((polynom(s))(#)f).x .| < 1/((polynom(d)).x) by P2; hence thesis by A0,P8,XXREAL_0:2; end; end; theorem for v,w be VECTOR of R_Algebra_of_Big_Oh_poly st w in negligibleFuncs holds v * w in negligibleFuncs proof let v,w be VECTOR of R_Algebra_of_Big_Oh_poly; assume w in negligibleFuncs; then reconsider w1=w as negligible Function of NAT,REAL by Def1; v in R_Algebra_of_Big_Oh_poly; then reconsider v1=v as polynomially-abs-bounded Function of NAT,REAL by LM14; v1(#)w1 is negligible; then v*w is negligible Function of NAT,REAL by RSSPAC2A; hence thesis by Def1; end;