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;