:: by Hiroyuki Okazaki

::

:: Received August 15, 2015

:: Copyright (c) 2015-2016 Association of Mizar Users

theorem L2: :: ASYMPT_3:4

for k being Nat ex N being Nat st

for x being Nat st N <= x holds

1 / (2 to_power x) < 1 / (x to_power k)

for x being Nat st N <= x holds

1 / (2 to_power x) < 1 / (x to_power k)

proof end;

theorem :: ASYMPT_3:5

for z being Nat st 2 <= z holds

for k being Nat ex N being Nat st

for x being Nat st N <= x holds

1 / (z to_power x) < 1 / (x to_power k)

for k being Nat ex N being Nat st

for x being Nat st N <= x holds

1 / (z to_power x) < 1 / (x to_power k)

proof end;

registration

existence

ex b_{1} being XFinSequence of REAL st b_{1} is positive-yielding ;

end;

cluster Relation-like omega -defined REAL -valued Sequence-like Function-like V39() V40() V41() finite positive-yielding V181() for set ;

correctness existence

ex b

proof end;

registration

existence

not for b_{1} being positive-yielding XFinSequence of REAL holds b_{1} is empty ;

end;

cluster Relation-like non-empty omega -defined REAL -valued non empty Sequence-like Function-like V39() V40() V41() finite positive-yielding nonnegative-yielding V181() for set ;

correctness existence

not for b

proof end;

registration

let c be XFinSequence of REAL ;

let a be Real;

correctness

coherence

for b_{1} being Sequence of REAL st b_{1} = a (#) c holds

b_{1} is finite ;

;

end;
let a be Real;

correctness

coherence

for b

b

;

theorem NLM2: :: ASYMPT_3:7

for c being non empty positive-yielding XFinSequence of REAL

for a being Real st 0 < a holds

a (#) c is non empty positive-yielding XFinSequence of REAL

for a being Real st 0 < a holds

a (#) c is non empty positive-yielding XFinSequence of REAL

proof end;

registration

let c be non empty positive-yielding XFinSequence of REAL ;

let a be positive Real;

correctness

coherence

for b_{1} being XFinSequence of REAL st b_{1} = a (#) c holds

( not b_{1} is empty & b_{1} is positive-yielding );

by NLM2;

end;
let a be positive Real;

correctness

coherence

for b

( not b

by NLM2;

theorem NLM3: :: ASYMPT_3:8

for c being non empty positive-yielding XFinSequence of REAL

for x being Nat holds 0 < (polynom c) . x

for x being Nat holds 0 < (polynom c) . x

proof end;

theorem NLM4: :: ASYMPT_3:9

for c, c1 being non empty positive-yielding XFinSequence of REAL

for a being Real st c1 = a (#) c holds

for x being Nat holds (polynom c1) . x = a * ((polynom c) . x)

for a being Real st c1 = a (#) c holds

for x being Nat holds (polynom c1) . x = a * ((polynom c) . x)

proof end;

definition

let p be Real_Sequence;

end;
attr p is polynomially-abs-bounded means :defabs: :: ASYMPT_3:def 1

ex k being Nat st |.p.| in Big_Oh (seq_n^ k);

ex k being Nat st |.p.| in Big_Oh (seq_n^ k);

:: deftheorem defabs defines polynomially-abs-bounded ASYMPT_3:def 1 :

for p being Real_Sequence holds

( p is polynomially-abs-bounded iff ex k being Nat st |.p.| in Big_Oh (seq_n^ k) );

for p being Real_Sequence holds

( p is polynomially-abs-bounded iff ex k being Nat st |.p.| in Big_Oh (seq_n^ k) );

registration

for b_{1} being Real_Sequence st b_{1} is polynomially-bounded holds

b_{1} is polynomially-abs-bounded
end;

cluster Function-like quasi_total polynomially-bounded -> polynomially-abs-bounded for Element of bool [:omega,REAL:];

coherence for b

b

proof end;

theorem LM1: :: ASYMPT_3:10

for r being Element of NAT

for s being Real_Sequence st s = NAT --> r holds

s is polynomially-abs-bounded

for s being Real_Sequence st s = NAT --> r holds

s is polynomially-abs-bounded

proof end;

reconsider rr = 0 as Element of REAL by XREAL_0:def 1;

registration

ex b_{1} being Function of NAT,REAL st b_{1} is polynomially-abs-bounded
end;

cluster Relation-like NAT -defined REAL -valued non empty Function-like V28( NAT ) quasi_total V39() V40() V41() polynomially-abs-bounded for Element of bool [:NAT,REAL:];

existence ex b

proof end;

registration

let f, g be polynomially-abs-bounded Function of NAT,REAL;

coherence

for b_{1} being Function of NAT,REAL st b_{1} = f + g holds

b_{1} is polynomially-abs-bounded

for b_{1} being Function of NAT,REAL st b_{1} = f (#) g holds

b_{1} is polynomially-abs-bounded

end;
coherence

for b

b

proof end;

coherence for b

b

proof end;

registration

let f be polynomially-abs-bounded Function of NAT,REAL;

let a be Element of REAL ;

coherence

for b_{1} being Function of NAT,REAL st b_{1} = a (#) f holds

b_{1} is polynomially-abs-bounded

end;
let a be Element of REAL ;

coherence

for b

b

proof end;

definition

ex b_{1} being Subset of (RAlgebra NAT) st

for x being object holds

( x in b_{1} iff x is polynomially-abs-bounded Function of NAT,REAL )

for b_{1}, b_{2} being Subset of (RAlgebra NAT) st ( for x being object holds

( x in b_{1} iff x is polynomially-abs-bounded Function of NAT,REAL ) ) & ( for x being object holds

( x in b_{2} iff x is polynomially-abs-bounded Function of NAT,REAL ) ) holds

b_{1} = b_{2}
end;

func Big_Oh_poly -> Subset of (RAlgebra NAT) means :DefX1: :: ASYMPT_3:def 2

for x being object holds

( x in it iff x is polynomially-abs-bounded Function of NAT,REAL );

existence for x being object holds

( x in it iff x is polynomially-abs-bounded Function of NAT,REAL );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem DefX1 defines Big_Oh_poly ASYMPT_3:def 2 :

for b_{1} being Subset of (RAlgebra NAT) holds

( b_{1} = Big_Oh_poly iff for x being object holds

( x in b_{1} iff x is polynomially-abs-bounded Function of NAT,REAL ) );

for b

( b

( x in b

definition

existence

ex b_{1} being strict AlgebraStr st

( the carrier of b_{1} = Big_Oh_poly & the multF of b_{1} = (RealFuncMult NAT) || Big_Oh_poly & the addF of b_{1} = (RealFuncAdd NAT) || Big_Oh_poly & the Mult of b_{1} = (RealFuncExtMult NAT) | [:REAL,Big_Oh_poly:] & the OneF of b_{1} = RealFuncUnit NAT & the ZeroF of b_{1} = RealFuncZero NAT );

uniqueness

for b_{1}, b_{2} being strict AlgebraStr st the carrier of b_{1} = Big_Oh_poly & the multF of b_{1} = (RealFuncMult NAT) || Big_Oh_poly & the addF of b_{1} = (RealFuncAdd NAT) || Big_Oh_poly & the Mult of b_{1} = (RealFuncExtMult NAT) | [:REAL,Big_Oh_poly:] & the OneF of b_{1} = RealFuncUnit NAT & the ZeroF of b_{1} = RealFuncZero NAT & the carrier of b_{2} = Big_Oh_poly & the multF of b_{2} = (RealFuncMult NAT) || Big_Oh_poly & the addF of b_{2} = (RealFuncAdd NAT) || Big_Oh_poly & the Mult of b_{2} = (RealFuncExtMult NAT) | [:REAL,Big_Oh_poly:] & the OneF of b_{2} = RealFuncUnit NAT & the ZeroF of b_{2} = RealFuncZero NAT holds

b_{1} = b_{2};

end;

func R_Algebra_of_Big_Oh_poly -> strict AlgebraStr means :defAlgebra: :: ASYMPT_3:def 3

( 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 ( 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 );

existence

ex b

( the carrier of b

uniqueness

for b

b

proof end;

:: deftheorem defAlgebra defines R_Algebra_of_Big_Oh_poly ASYMPT_3:def 3 :

for b_{1} being strict AlgebraStr holds

( b_{1} = R_Algebra_of_Big_Oh_poly iff ( the carrier of b_{1} = Big_Oh_poly & the multF of b_{1} = (RealFuncMult NAT) || Big_Oh_poly & the addF of b_{1} = (RealFuncAdd NAT) || Big_Oh_poly & the Mult of b_{1} = (RealFuncExtMult NAT) | [:REAL,Big_Oh_poly:] & the OneF of b_{1} = RealFuncUnit NAT & the ZeroF of b_{1} = RealFuncZero NAT ) );

for b

( b

theorem LM14: :: ASYMPT_3:12

for f being object holds

( f in R_Algebra_of_Big_Oh_poly iff f is polynomially-abs-bounded Function of NAT,REAL )

( f in R_Algebra_of_Big_Oh_poly iff f is polynomially-abs-bounded Function of NAT,REAL )

proof end;

theorem LM15: :: ASYMPT_3:13

for f, g being Point of R_Algebra_of_Big_Oh_poly

for f1, g1 being Point of (RAlgebra NAT) st f = f1 & g = g1 holds

f * g = f1 * g1

for f1, g1 being Point of (RAlgebra NAT) st f = f1 & g = g1 holds

f * g = f1 * g1

proof end;

theorem LM16: :: ASYMPT_3:14

for f, g being Point of R_Algebra_of_Big_Oh_poly

for f1, g1 being Point of (RAlgebra NAT) st f = f1 & g = g1 holds

f + g = f1 + g1

for f1, g1 being Point of (RAlgebra NAT) st f = f1 & g = g1 holds

f + g = f1 + g1

proof end;

theorem LM17: :: ASYMPT_3:15

for f being Point of R_Algebra_of_Big_Oh_poly

for f1 being Point of (RAlgebra NAT)

for a being Element of REAL st f = f1 holds

a * f = a * f1

for f1 being Point of (RAlgebra NAT)

for a being Element of REAL st f = f1 holds

a * f = a * f1

proof end;

registration

coherence

( R_Algebra_of_Big_Oh_poly is strict & R_Algebra_of_Big_Oh_poly is Abelian & R_Algebra_of_Big_Oh_poly is add-associative & R_Algebra_of_Big_Oh_poly is right_zeroed & R_Algebra_of_Big_Oh_poly is right_complementable & R_Algebra_of_Big_Oh_poly is commutative & R_Algebra_of_Big_Oh_poly is associative & R_Algebra_of_Big_Oh_poly is right_unital & R_Algebra_of_Big_Oh_poly is right-distributive & R_Algebra_of_Big_Oh_poly is vector-associative & R_Algebra_of_Big_Oh_poly is scalar-associative & R_Algebra_of_Big_Oh_poly is vector-distributive & R_Algebra_of_Big_Oh_poly is scalar-distributive );

end;

cluster R_Algebra_of_Big_Oh_poly -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative strict vector-associative right-distributive right_unital associative commutative ;

correctness coherence

( R_Algebra_of_Big_Oh_poly is strict & R_Algebra_of_Big_Oh_poly is Abelian & R_Algebra_of_Big_Oh_poly is add-associative & R_Algebra_of_Big_Oh_poly is right_zeroed & R_Algebra_of_Big_Oh_poly is right_complementable & R_Algebra_of_Big_Oh_poly is commutative & R_Algebra_of_Big_Oh_poly is associative & R_Algebra_of_Big_Oh_poly is right_unital & R_Algebra_of_Big_Oh_poly is right-distributive & R_Algebra_of_Big_Oh_poly is vector-associative & R_Algebra_of_Big_Oh_poly is scalar-associative & R_Algebra_of_Big_Oh_poly is vector-distributive & R_Algebra_of_Big_Oh_poly is scalar-distributive );

proof end;

theorem TH11: :: ASYMPT_3:19

for f, g, h being VECTOR of R_Algebra_of_Big_Oh_poly

for f9, g9, h9 being Function of NAT,REAL st f9 = f & g9 = g & h9 = h holds

( h = f + g iff for x being Nat holds h9 . x = (f9 . x) + (g9 . x) )

for f9, g9, h9 being Function of NAT,REAL st f9 = f & g9 = g & h9 = h holds

( h = f + g iff for x being Nat holds h9 . x = (f9 . x) + (g9 . x) )

proof end;

theorem TH11A: :: ASYMPT_3:20

for f, g, h being VECTOR of R_Algebra_of_Big_Oh_poly

for f9, g9, h9 being Function of NAT,REAL st f9 = f & g9 = g & h9 = h holds

( h = f * g iff for x being Nat holds h9 . x = (f9 . x) * (g9 . x) )

for f9, g9, h9 being Function of NAT,REAL st f9 = f & g9 = g & h9 = h holds

( h = f * g iff for x being Nat holds h9 . x = (f9 . x) * (g9 . x) )

proof end;

theorem TH12: :: ASYMPT_3:21

for f, h being VECTOR of R_Algebra_of_Big_Oh_poly

for f9, h9 being Function of NAT,REAL st f9 = f & h9 = h holds

for a being Real holds

( h = a * f iff for x being Nat holds h9 . x = a * (f9 . x) )

for f9, h9 being Function of NAT,REAL st f9 = f & h9 = h holds

for a being Real holds

( h = a * f iff for x being Nat holds h9 . x = a * (f9 . x) )

proof end;

definition

let f be Function of NAT,REAL;

end;
attr f is negligible means :defneg: :: ASYMPT_3:def 4

for c being non empty positive-yielding XFinSequence of REAL ex N being Nat st

for x being Nat st N <= x holds

|.(f . x).| < 1 / ((polynom c) . x);

for c being non empty positive-yielding XFinSequence of REAL ex N being Nat st

for x being Nat st N <= x holds

|.(f . x).| < 1 / ((polynom c) . x);

:: deftheorem defneg defines negligible ASYMPT_3:def 4 :

for f being Function of NAT,REAL holds

( f is negligible iff for c being non empty positive-yielding XFinSequence of REAL ex N being Nat st

for x being Nat st N <= x holds

|.(f . x).| < 1 / ((polynom c) . x) );

for f being Function of NAT,REAL holds

( f is negligible iff for c being non empty positive-yielding XFinSequence of REAL ex N being Nat st

for x being Nat st N <= x holds

|.(f . x).| < 1 / ((polynom c) . x) );

theorem PXR1: :: ASYMPT_3:22

for r being Real st 0 < r holds

ex c being non empty positive-yielding XFinSequence of REAL st

for x being Nat holds (polynom c) . x = r

ex c being non empty positive-yielding XFinSequence of REAL st

for x being Nat holds (polynom c) . x = r

proof end;

theorem PXR2: :: ASYMPT_3:23

for f being Function of NAT,REAL st f is negligible holds

for r being Real st 0 < r holds

ex N being Nat st

for x being Nat st N <= x holds

|.(f . x).| < r

for r being Real st 0 < r holds

ex N being Nat st

for x being Nat st N <= x holds

|.(f . x).| < r

proof end;

registration
end;

registration

existence

ex b_{1} being Function of NAT,REAL st b_{1} is negligible ;

end;

cluster Relation-like NAT -defined REAL -valued non empty Function-like V28( NAT ) quasi_total V39() V40() V41() negligible for Element of bool [:NAT,REAL:];

correctness existence

ex b

proof end;

registration

let f be negligible Function of NAT,REAL;

coherence

for b_{1} being Function of NAT,REAL st b_{1} = |.f.| holds

b_{1} is negligible

end;
coherence

for b

b

proof end;

registration

let f be negligible Function of NAT,REAL;

let a be Real;

coherence

for b_{1} being Function of NAT,REAL st b_{1} = a (#) f holds

b_{1} is negligible

end;
let a be Real;

coherence

for b

b

proof end;

registration

let f, g be negligible Function of NAT,REAL;

coherence

for b_{1} being Function of NAT,REAL st b_{1} = f + g holds

b_{1} is negligible

end;
coherence

for b

b

proof end;

registration

let f, g be negligible Function of NAT,REAL;

coherence

for b_{1} being Function of NAT,REAL st b_{1} = f (#) g holds

b_{1} is negligible

end;
coherence

for b

b

proof end;

theorem TH3: :: ASYMPT_3:25

for f being Function of NAT,REAL st ( for x being Nat holds f . x = 1 / (2 to_power x) ) holds

f is negligible

f is negligible

proof end;

theorem TH4: :: ASYMPT_3:26

for f, g being Function of NAT,REAL st f is negligible & ( for x being Nat holds |.(g . x).| <= |.(f . x).| ) holds

g is negligible

g is negligible

proof end;

registration

for b_{1} being Function of NAT,REAL st b_{1} is negligible holds

b_{1} is polynomially-abs-bounded
end;

cluster Function-like quasi_total negligible -> polynomially-abs-bounded for Element of bool [:NAT,REAL:];

coherence for b

b

proof end;

definition

ex b_{1} being Subset of Big_Oh_poly st

for x being object holds

( x in b_{1} iff x is negligible Function of NAT,REAL )

for b_{1}, b_{2} being Subset of Big_Oh_poly st ( for x being object holds

( x in b_{1} iff x is negligible Function of NAT,REAL ) ) & ( for x being object holds

( x in b_{2} iff x is negligible Function of NAT,REAL ) ) holds

b_{1} = b_{2}
end;

func negligibleFuncs -> Subset of Big_Oh_poly means :Def1: :: ASYMPT_3:def 5

for x being object holds

( x in it iff x is negligible Function of NAT,REAL );

existence for x being object holds

( x in it iff x is negligible Function of NAT,REAL );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def1 defines negligibleFuncs ASYMPT_3:def 5 :

for b_{1} being Subset of Big_Oh_poly holds

( b_{1} = negligibleFuncs iff for x being object holds

( x in b_{1} iff x is negligible Function of NAT,REAL ) );

for b

( b

( x in b

registration
end;

theorem RSSPAC2: :: ASYMPT_3:27

for v, w being VECTOR of R_Algebra_of_Big_Oh_poly

for v1, w1 being Function of NAT,REAL st v = v1 & w1 = w holds

v + w = v1 + w1

for v1, w1 being Function of NAT,REAL st v = v1 & w1 = w holds

v + w = v1 + w1

proof end;

theorem RSSPAC2A: :: ASYMPT_3:28

for v, w being VECTOR of R_Algebra_of_Big_Oh_poly

for v1, w1 being Function of NAT,REAL st v = v1 & w1 = w holds

v * w = v1 (#) w1

for v1, w1 being Function of NAT,REAL st v = v1 & w1 = w holds

v * w = v1 (#) w1

proof end;

theorem RSSPAC3: :: ASYMPT_3:29

for a being Real

for v being VECTOR of R_Algebra_of_Big_Oh_poly

for v1 being Function of NAT,REAL st v = v1 holds

a * v = a (#) v1

for v being VECTOR of R_Algebra_of_Big_Oh_poly

for v1 being Function of NAT,REAL st v = v1 holds

a * v = a (#) v1

proof end;

theorem :: ASYMPT_3:30

for a being Real

for v being VECTOR of R_Algebra_of_Big_Oh_poly st v in negligibleFuncs holds

a * v in negligibleFuncs

for v being VECTOR of R_Algebra_of_Big_Oh_poly st v in negligibleFuncs holds

a * v in negligibleFuncs

proof end;

theorem :: ASYMPT_3:31

for v, u being VECTOR of R_Algebra_of_Big_Oh_poly st v in negligibleFuncs & u in negligibleFuncs holds

v + u in negligibleFuncs

v + u in negligibleFuncs

proof end;

theorem :: ASYMPT_3:32

for v, u being VECTOR of R_Algebra_of_Big_Oh_poly st v in negligibleFuncs & u in negligibleFuncs holds

v * u in negligibleFuncs

v * u in negligibleFuncs

proof end;

definition

let f, g be Function of NAT,REAL;

for f being Function of NAT,REAL ex h being Function of NAT,REAL st

( h is negligible & ( for x being Nat holds |.((f . x) - (f . x)).| <= |.(h . x).| ) )

for f, g being Function of NAT,REAL st ex h being Function of NAT,REAL st

( h is negligible & ( for x being Nat holds |.((f . x) - (g . x)).| <= |.(h . x).| ) ) holds

ex h being Function of NAT,REAL st

( h is negligible & ( for x being Nat holds |.((g . x) - (f . x)).| <= |.(h . x).| ) )

end;
pred f negligibleEQ g means :: ASYMPT_3:def 6

ex h being Function of NAT,REAL st

( h is negligible & ( for x being Nat holds |.((f . x) - (g . x)).| <= |.(h . x).| ) );

reflexivity ex h being Function of NAT,REAL st

( h is negligible & ( for x being Nat holds |.((f . x) - (g . x)).| <= |.(h . x).| ) );

for f being Function of NAT,REAL ex h being Function of NAT,REAL st

( h is negligible & ( for x being Nat holds |.((f . x) - (f . x)).| <= |.(h . x).| ) )

proof end;

symmetry for f, g being Function of NAT,REAL st ex h being Function of NAT,REAL st

( h is negligible & ( for x being Nat holds |.((f . x) - (g . x)).| <= |.(h . x).| ) ) holds

ex h being Function of NAT,REAL st

( h is negligible & ( for x being Nat holds |.((g . x) - (f . x)).| <= |.(h . x).| ) )

proof end;

:: deftheorem defines negligibleEQ ASYMPT_3:def 6 :

for f, g being Function of NAT,REAL holds

( f negligibleEQ g iff ex h being Function of NAT,REAL st

( h is negligible & ( for x being Nat holds |.((f . x) - (g . x)).| <= |.(h . x).| ) ) );

for f, g being Function of NAT,REAL holds

( f negligibleEQ g iff ex h being Function of NAT,REAL st

( h is negligible & ( for x being Nat holds |.((f . x) - (g . x)).| <= |.(h . x).| ) ) );

theorem :: ASYMPT_3:33

for f, g, h being Function of NAT,REAL st f negligibleEQ g & g negligibleEQ h holds

f negligibleEQ h

f negligibleEQ h

proof end;

theorem LRNG1: :: ASYMPT_3:35

for c being non empty positive-yielding XFinSequence of REAL ex a being Real ex k, N being Nat st

( 0 < a & 0 < k & ( for x being Nat st N <= x holds

(polynom c) . x <= a * (x to_power k) ) )

( 0 < a & 0 < k & ( for x being Nat st N <= x holds

(polynom c) . x <= a * (x to_power k) ) )

proof end;

registration

let a be nonnegative-yielding XFinSequence of REAL ;

let b be nonnegative-yielding Real_Sequence;

coherence

a (#) b is nonnegative-yielding

end;
let b be nonnegative-yielding Real_Sequence;

coherence

a (#) b is nonnegative-yielding

proof end;

registration

let a, b be nonnegative-yielding XFinSequence of REAL ;

coherence

a ^ b is nonnegative-yielding

end;
coherence

a ^ b is nonnegative-yielding

proof end;

registration
end;

theorem LRNG2: :: ASYMPT_3:36

for a being Real

for k being Nat ex c being non empty positive-yielding XFinSequence of REAL st

for x being Nat holds a * (x to_power k) <= (polynom c) . x

for k being Nat ex c being non empty positive-yielding XFinSequence of REAL st

for x being Nat holds a * (x to_power k) <= (polynom c) . x

proof end;

theorem RNG0: :: ASYMPT_3:37

for c, s being non empty positive-yielding XFinSequence of REAL ex d being non empty positive-yielding XFinSequence of REAL ex N being Nat st

for x being Nat st N <= x holds

((polynom c) . x) * ((polynom s) . x) <= (polynom d) . x

for x being Nat st N <= x holds

((polynom c) . x) * ((polynom s) . x) <= (polynom d) . x

proof end;

registration

let f be negligible Function of NAT,REAL;

let c be non empty positive-yielding XFinSequence of REAL ;

coherence

for b_{1} being Function of NAT,REAL st b_{1} = (polynom c) (#) f holds

b_{1} is negligible

end;
let c be non empty positive-yielding XFinSequence of REAL ;

coherence

for b

b

proof end;

theorem RNG2: :: ASYMPT_3:38

for g being polynomially-abs-bounded Function of NAT,REAL ex d being non empty positive-yielding XFinSequence of REAL ex N being Nat st

for x being Nat st N <= x holds

|.(g . x).| <= (polynom d) . x

for x being Nat st N <= x holds

|.(g . x).| <= (polynom d) . x

proof end;

registration

let f be negligible Function of NAT,REAL;

let g be polynomially-abs-bounded Function of NAT,REAL;

coherence

for b_{1} being Function of NAT,REAL st b_{1} = g (#) f holds

b_{1} is negligible

end;
let g be polynomially-abs-bounded Function of NAT,REAL;

coherence

for b

b

proof end;

theorem :: ASYMPT_3:39

for v, w being VECTOR of R_Algebra_of_Big_Oh_poly st w in negligibleFuncs holds

v * w in negligibleFuncs

v * w in negligibleFuncs

proof end;