:: Algebra of Polynomially Bounded Sequences and Negligible Functions
:: by Hiroyuki Okazaki
::
:: 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
correctness
existence
ex b1 being XFinSequence of REAL st b1 is positive-yielding
;
proof end;
end;

registration
correctness
existence
not for b1 being positive-yielding XFinSequence of REAL holds b1 is empty
;
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
coherence
for b1 being Sequence of REAL st b1 = a (#) c holds
b1 is finite
;
;
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
coherence
for b1 being XFinSequence of REAL st b1 = a (#) c holds
( not b1 is empty & b1 is positive-yielding )
;
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 < () . 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 * (() . 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 ();
end;

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

registration
coherence
for b1 being Real_Sequence st b1 is polynomially-bounded holds
b1 is polynomially-abs-bounded
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
existence
ex b1 being Function of NAT,REAL st b1 is polynomially-abs-bounded
proof end;
end;

registration
let f, g be polynomially-abs-bounded Function of NAT,REAL;
coherence
for b1 being Function of NAT,REAL st b1 = f + g holds
b1 is polynomially-abs-bounded
proof end;
coherence
for b1 being Function of NAT,REAL st b1 = f (#) g holds
b1 is polynomially-abs-bounded
proof end;
end;

registration
let f be polynomially-abs-bounded Function of NAT,REAL;
let a be Element of REAL ;
coherence
for b1 being Function of NAT,REAL st b1 = a (#) f holds
b1 is polynomially-abs-bounded
proof end;
end;

definition
func Big_Oh_poly -> Subset of () 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
ex b1 being Subset of () st
for x being object holds
( x in b1 iff x is polynomially-abs-bounded Function of NAT,REAL )
proof end;
uniqueness
for b1, b2 being Subset of () st ( for x being object holds
( x in b1 iff x is polynomially-abs-bounded Function of NAT,REAL ) ) & ( for x being object holds
( x in b2 iff x is polynomially-abs-bounded Function of NAT,REAL ) ) holds
b1 = b2
proof end;
end;

:: deftheorem DefX1 defines Big_Oh_poly ASYMPT_3:def 2 :
for b1 being Subset of () holds
( b1 = Big_Oh_poly iff for x being object holds
( x in b1 iff x is polynomially-abs-bounded Function of NAT,REAL ) );

registration
cluster Big_Oh_poly -> non empty ;
coherence
not Big_Oh_poly is empty
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 = || Big_Oh_poly & the addF of it = || Big_Oh_poly & the Mult of it = | & the OneF of it = RealFuncUnit NAT & the ZeroF of it = RealFuncZero NAT );
correctness
existence
ex b1 being strict AlgebraStr st
( the carrier of b1 = Big_Oh_poly & the multF of b1 = || Big_Oh_poly & the addF of b1 = || Big_Oh_poly & the Mult of b1 = | & the OneF of b1 = RealFuncUnit NAT & the ZeroF of b1 = RealFuncZero NAT )
;
uniqueness
for b1, b2 being strict AlgebraStr st the carrier of b1 = Big_Oh_poly & the multF of b1 = || Big_Oh_poly & the addF of b1 = || Big_Oh_poly & the Mult of b1 = | & the OneF of b1 = RealFuncUnit NAT & the ZeroF of b1 = RealFuncZero NAT & the carrier of b2 = Big_Oh_poly & the multF of b2 = || Big_Oh_poly & the addF of b2 = || Big_Oh_poly & the Mult of b2 = | & the OneF of b2 = RealFuncUnit NAT & the ZeroF of b2 = RealFuncZero NAT holds
b1 = b2
;
proof end;
end;

:: deftheorem defAlgebra defines R_Algebra_of_Big_Oh_poly ASYMPT_3:def 3 :
for b1 being strict AlgebraStr holds
( b1 = R_Algebra_of_Big_Oh_poly iff ( the carrier of b1 = Big_Oh_poly & the multF of b1 = || Big_Oh_poly & the addF of b1 = || Big_Oh_poly & the Mult of b1 = | & the OneF of b1 = RealFuncUnit NAT & the ZeroF of b1 = RealFuncZero NAT ) );

registration
correctness
coherence ;
by defAlgebra;
end;

theorem LM12: :: ASYMPT_3:11
the carrier of R_Algebra_of_Big_Oh_poly c= the carrier of ()
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 () 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 () 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 ()
for a being Element of REAL st f = f1 holds
a * f = a * f1
proof end;

theorem LM18: :: ASYMPT_3:16

theorem LM19: :: ASYMPT_3:17

registration
correctness
coherence ;
proof end;
end;

theorem :: ASYMPT_3:18

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 / (() . x);
end;

:: 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 / (() . 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 () . 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
coherence
proof end;
end;

registration
correctness
existence
ex b1 being Function of NAT,REAL st b1 is negligible
;
proof end;
end;

registration
let f be negligible Function of NAT,REAL;
cluster |.f.| -> negligible for Function of NAT,REAL;
coherence
for b1 being Function of NAT,REAL st b1 = |.f.| holds
b1 is negligible
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
for b1 being Function of NAT,REAL st b1 = a (#) f holds
b1 is negligible
proof end;
end;

registration
let f, g be negligible Function of NAT,REAL;
cluster f + g -> negligible for Function of NAT,REAL;
coherence
for b1 being Function of NAT,REAL st b1 = f + g holds
b1 is negligible
proof end;
end;

registration
let f, g be negligible Function of NAT,REAL;
cluster f (#) g -> negligible for Function of NAT,REAL;
coherence
for b1 being Function of NAT,REAL st b1 = f (#) g holds
b1 is negligible
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
coherence
for b1 being Function of NAT,REAL st b1 is negligible holds
b1 is polynomially-abs-bounded
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
ex b1 being Subset of Big_Oh_poly st
for x being object holds
( x in b1 iff x is negligible Function of NAT,REAL )
proof end;
uniqueness
for b1, b2 being Subset of Big_Oh_poly st ( for x being object holds
( x in b1 iff x is negligible Function of NAT,REAL ) ) & ( for x being object holds
( x in b2 iff x is negligible Function of NAT,REAL ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines negligibleFuncs ASYMPT_3:def 5 :
for b1 being Subset of Big_Oh_poly holds
( b1 = negligibleFuncs iff for x being object holds
( x in b1 iff x is negligible Function of NAT,REAL ) );

registration
coherence
not negligibleFuncs is empty
proof end;
end;

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;

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;

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

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
() . 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
proof end;
end;

registration
let a, b be nonnegative-yielding XFinSequence of REAL ;
coherence
proof end;
end;

registration
let a, b, c be non negative Real;
cluster seq_a^ (a,b,c) -> nonnegative-yielding ;
coherence
seq_a^ (a,b,c) is nonnegative-yielding
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) <= () . 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
(() . x) * (() . x) <= () . x
proof end;

registration
let f be negligible Function of NAT,REAL;
let c be non empty positive-yielding XFinSequence of REAL ;
cluster () (#) f -> negligible for Function of NAT,REAL;
coherence
for b1 being Function of NAT,REAL st b1 = () (#) f holds
b1 is negligible
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).| <= () . 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
for b1 being Function of NAT,REAL st b1 = g (#) f holds
b1 is negligible
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;