ASYMPT_3: Algebra of Polynomially Bounded Sequences and Negligible Functions

:: Algebra of Polynomially Bounded Sequences and Negligible Functions
:: by Hiroyuki Okazaki
::
:: Received August 15, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users

theorem TCL001: :: ASYMPT_3:1

for r being Real holds r < |.r.| + 1

proof end;

theorem LMC31: :: ASYMPT_3:2

for r being Real ex N being Nat st
for n being Nat st N <= n holds
r < n / (log (2,n))

proof end;

theorem L1: :: ASYMPT_3:3

for k being Nat ex N being Nat st
for x being Nat st N <= x holds
x to_power k < 2 to_power x

proof end;

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)

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)

proof end;

registration

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

correctness

proof end;

end;

registration

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

correctness

proof end;

end;

theorem NLM1: :: ASYMPT_3:6

for c being XFinSequence of REAL
for a being Real holds a (#) c is XFinSequence of REAL

proof end;

registration

let c be XFinSequence of REAL ;
let a be Real;

cluster a (#) c -> finite for Sequence of REAL ;

correctness ;

end;

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

proof end;

registration

let c be non empty positive-yielding XFinSequence of REAL ;
let 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: :: ASYMPT_3:8

for c being non empty positive-yielding XFinSequence of REAL
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)

proof end;

definition

let p be Real_Sequence;

attr p is polynomially-abs-bounded means :defabs: :: ASYMPT_3:def 1
ex k being Nat st |.p.| in Big_Oh (seq_n^ k);

end;

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

registration

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

coherence

proof end;

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

proof end;

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

registration

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

proof 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 end;

cluster f (#) g -> polynomially-abs-bounded for Function of NAT,REAL;

coherence

proof 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 end;

end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem DefX1 defines Big_Oh_poly ASYMPT_3:def 2 :

registration

cluster Big_Oh_poly -> non empty ;

coherence

proof end;

end;

definition

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

proof end;

end;

:: deftheorem defAlgebra defines R_Algebra_of_Big_Oh_poly ASYMPT_3:def 3 :

registration

cluster R_Algebra_of_Big_Oh_poly -> non empty strict ;

correctness by defAlgebra;

end;

theorem LM12: :: ASYMPT_3:11

the carrier of R_Algebra_of_Big_Oh_poly c= the carrier of (RAlgebra NAT)

proof end;

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 )

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

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

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

proof end;

theorem LM18: :: ASYMPT_3:16

0. R_Algebra_of_Big_Oh_poly = 0. (RAlgebra NAT) by defAlgebra;

theorem LM19: :: ASYMPT_3:17

1. R_Algebra_of_Big_Oh_poly = 1. (RAlgebra NAT) by defAlgebra;

registration

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

proof end;

end;

theorem :: ASYMPT_3:18

R_Algebra_of_Big_Oh_poly is Algebra ;

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

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

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

proof end;

definition

let f be Function of NAT,REAL;

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

end;

:: deftheorem defneg defines negligible ASYMPT_3:def 4 :

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

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

proof end;

theorem :: ASYMPT_3:24

for f being Function of NAT,REAL st f is negligible holds
( f is convergent & lim f = 0 )

proof end;

registration

cluster seq_const 0 -> negligible ;

coherence

proof end;

end;

registration

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

proof end;

end;

registration

let f be negligible Function of NAT,REAL;

cluster |.f.| -> negligible for Function of NAT,REAL;

coherence

proof end;

end;

registration

let f be negligible Function of NAT,REAL;
let a be Real;

cluster a (#) f -> negligible for Function of NAT,REAL;

coherence

proof end;

end;

registration

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

cluster f + g -> negligible for Function of NAT,REAL;

coherence

proof end;

end;

registration

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

cluster f (#) g -> negligible for Function of NAT,REAL;

coherence

proof end;

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

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

proof end;

registration

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

coherence

proof end;

end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines negligibleFuncs ASYMPT_3:def 5 :

registration

cluster negligibleFuncs -> non empty ;

coherence

proof end;

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

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

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

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

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

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

proof end;

definition

let f, g be Function of NAT,REAL;

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

proof end;

symmetry

proof end;

end;

:: deftheorem defines negligibleEQ ASYMPT_3:def 6 :

theorem :: ASYMPT_3:33

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

proof end;

theorem :: ASYMPT_3:34

for f, g being Function of NAT,REAL holds
( f negligibleEQ g iff f - g is negligible )

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

proof end;

registration

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

cluster a (#) b -> nonnegative-yielding ;

coherence

proof end;

end;

registration

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

cluster a ^ b -> nonnegative-yielding ;

coherence

proof end;

end;

registration

let a, b, c be non negative Real;

cluster seq_a^ (a,b,c) -> nonnegative-yielding ;

coherence

proof end;

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

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

proof end;

registration

let f be negligible Function of NAT,REAL;
let c be non empty positive-yielding XFinSequence of REAL ;

cluster (polynom c) (#) f -> negligible for Function of NAT,REAL;

coherence

proof end;

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

proof end;

registration

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

cluster g (#) f -> negligible for Function of NAT,REAL;

coherence

proof end;

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

proof end;