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


begin :: Preliminaries

theorem :: ASYMPT_3:1
  for r be Real holds r < |. r .| + 1;

theorem :: ASYMPT_3:2
   for r be Real ex N be Nat
  st for n be Nat st N <=n holds r < n /log(2,n);

theorem :: ASYMPT_3:3
  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;

theorem :: ASYMPT_3:4
  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);

theorem :: ASYMPT_3:5
  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);

registration
  cluster positive-yielding for XFinSequence of REAL;
end;

registration
  cluster non empty for positive-yielding XFinSequence of REAL;
end;

theorem :: ASYMPT_3:6
  for c be XFinSequence of REAL,
  a be Real
  holds a (#) c is XFinSequence of REAL;

registration
  let c be XFinSequence of REAL,
  a be Real;
  cluster a (#) c -> finite for Sequence of REAL;
end;

theorem :: ASYMPT_3:7
  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;

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

notation
  let c be XFinSequence of REAL;
  synonym polynom(c) for seq_p(c);
end;

theorem :: ASYMPT_3:8
  for c be non empty positive-yielding XFinSequence of REAL,
  x be Nat
  holds 0 < (polynom(c)).x;

theorem :: ASYMPT_3:9
  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);

begin :: Algebra of polynomially bounded functions

definition
  let p be Real_Sequence;
  attr p is polynomially-abs-bounded means
:: ASYMPT_3:def 1

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

registration
  cluster polynomially-bounded -> polynomially-abs-bounded for Real_Sequence;
end;

theorem :: ASYMPT_3:10
  for r be Element of NAT holds
  for s be Real_Sequence
  st s = NAT --> r
  holds s is polynomially-abs-bounded;

registration
  cluster polynomially-abs-bounded for Function of NAT,REAL;
end;

registration
  let f,g be polynomially-abs-bounded Function of NAT,REAL;
  cluster f + g -> polynomially-abs-bounded for Function of NAT,REAL;
  cluster f (#) g -> polynomially-abs-bounded for Function of NAT,REAL;
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;
end;

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

  for x being object holds x in it
  iff x is polynomially-abs-bounded Function of NAT,REAL;
end;

registration
  cluster Big_Oh_poly -> non empty;
end;

definition
  func R_Algebra_of_Big_Oh_poly -> strict AlgebraStr means
:: 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);
end;

registration
  cluster R_Algebra_of_Big_Oh_poly -> non empty;
end;

theorem :: ASYMPT_3:11
  the carrier of R_Algebra_of_Big_Oh_poly c= the carrier of RAlgebra (NAT);

theorem :: ASYMPT_3:12
  for f be object holds
  f in R_Algebra_of_Big_Oh_poly
  iff f is polynomially-abs-bounded Function of NAT,REAL;

theorem :: ASYMPT_3:13
  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;

theorem :: ASYMPT_3:14
  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;

theorem :: ASYMPT_3:15
  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;

theorem :: ASYMPT_3:16
  0.R_Algebra_of_Big_Oh_poly = 0.(RAlgebra NAT);

theorem :: ASYMPT_3:17
  1. (R_Algebra_of_Big_Oh_poly) = 1. (RAlgebra NAT);

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

theorem :: ASYMPT_3:18
  R_Algebra_of_Big_Oh_poly is Algebra;

theorem :: ASYMPT_3:19
  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);

theorem :: ASYMPT_3:20
  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 );

theorem :: ASYMPT_3:21
  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;

begin :: negligible functions

definition
  let f be Function of NAT,REAL;
  attr f is negligible means
:: ASYMPT_3:def 4

  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 :: ASYMPT_3:22
  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;

theorem :: ASYMPT_3:23
  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;

theorem :: ASYMPT_3:24
  for f be Function of NAT,REAL
  st f is negligible
  holds f is convergent & lim f = 0;

registration
  cluster seq_const 0 -> negligible;
end;

registration
  cluster negligible for Function of NAT,REAL;
end;

registration
  let f be negligible Function of NAT,REAL;
  cluster |.f.| -> negligible for Function of NAT,REAL;
end;

registration
  let f be negligible Function of NAT,REAL,
  a be Real;
  cluster a(#)f -> negligible for Function of NAT,REAL;
end;

registration
  let f,g be negligible Function of NAT,REAL;
  cluster f+g -> negligible for Function of NAT,REAL;
end;

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

theorem :: ASYMPT_3:25
  for f be Function of NAT,REAL
  st for x be Nat holds f.x = 1/ (2 to_power x)
  holds f is negligible;

theorem :: ASYMPT_3:26
  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;

registration
  cluster negligible -> polynomially-abs-bounded for Function of NAT,REAL;
end;

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

  for x being object holds x in it
  iff x is negligible Function of NAT,REAL;
end;

registration
  cluster negligibleFuncs -> non empty;
end;

theorem :: ASYMPT_3:27
  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;

theorem :: ASYMPT_3:28
  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;

theorem :: ASYMPT_3:29
  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;

theorem :: ASYMPT_3:30
  for a be Real
  for v be VECTOR of R_Algebra_of_Big_Oh_poly
  st v in negligibleFuncs
  holds a * v in negligibleFuncs;

theorem :: ASYMPT_3:31
  for v,u be VECTOR of R_Algebra_of_Big_Oh_poly
  st v in negligibleFuncs & u in negligibleFuncs
  holds v + u in negligibleFuncs;

theorem :: ASYMPT_3:32
  for v,u be VECTOR of R_Algebra_of_Big_Oh_poly
  st v in negligibleFuncs & u in negligibleFuncs
  holds v * u in negligibleFuncs;

definition
  let f,g be Function of NAT,REAL;
  pred f negligibleEQ g means
:: ASYMPT_3:def 6
  ex h be Function of NAT,REAL
  st h is negligible
  &
  for x be Nat holds |. f.x - g.x .| <= |.h.x.|;
  reflexivity;
  symmetry;
end;

theorem :: ASYMPT_3:33
  for f,g,h be Function of NAT,REAL
  st f negligibleEQ g & g negligibleEQ h
  holds f negligibleEQ h;

theorem :: ASYMPT_3:34
  for f,g be Function of NAT,REAL
  holds f negligibleEQ g iff f-g is negligible;

theorem :: ASYMPT_3:35
  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);

registration
  let a be nonnegative-yielding XFinSequence of REAL,
  b be nonnegative-yielding Real_Sequence;
  cluster a (#) b -> nonnegative-yielding;
end;

registration
  let a,b be nonnegative-yielding XFinSequence of REAL;
  cluster a ^ b -> nonnegative-yielding;
end;

registration
  let a,b,c be non negative Real;
  cluster seq_a^(a,b,c) -> nonnegative-yielding;
end;

theorem :: ASYMPT_3:36
  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;

theorem :: ASYMPT_3:37
  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;

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

theorem :: ASYMPT_3:38
  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;

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

theorem :: ASYMPT_3:39
  for v,w be VECTOR of R_Algebra_of_Big_Oh_poly
  st w in negligibleFuncs
  holds v * w in negligibleFuncs;