The Mizar abstract of ASYMPT

Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users
The abstract of the Mizar article:: Asymptotic Notation. Part I: Theory
by
Richard Krueger,
Piotr Rudnicki, and
Paul Shelley
Received November 4, 1999
MML identifier: ASYMPT_0
[ Mizar article, MML identifier index ]
environ

 vocabulary FINSET_1, ARYTM, ZF_LANG, ARYTM_1, SEQ_1, FUNCT_1, SQUARE_1,
      ARYTM_3, RELAT_1, SEQ_2, ORDINAL2, ABSVALUE, LIMFUNC1, FRAENKEL, FUNCT_2,
      BOOLE, INT_1, POWER, GROUP_1, ASYMPT_0;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, FUNCT_1, FUNCT_2, FRAENKEL, INT_1, NAT_1, SEQ_1, SEQ_2, NEWTON,
      POWER, PRE_CIRC, FINSET_1, SQUARE_1, LIMFUNC1, ABSVALUE, SFMASTR3;
 constructors REAL_1, FRAENKEL, SEQ_2, POWER, PRE_CIRC, SFMASTR3, LIMFUNC1,
      CARD_4, PARTFUN1, ABSVALUE, NAT_1, ORDINAL2, NUMBERS;
 clusters XREAL_0, FRAENKEL, GROUP_2, INT_1, SEQ_1, MEMBERED, ORDINAL2,
      NUMBERS;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: Preliminaries

reserve c, c1, d for Real,
        k, n, m, N, n1, N1, N2, N3, N4, N5, M for Nat,
        x for set;

scheme FinSegRng1{m, n() -> Nat, X() -> non empty set,
                  F(set) -> Element of X()} :
 {F(i) where i is Nat: m() <= i & i <= n()} is finite non empty Subset of X()
provided
 m() <= n();

scheme FinImInit1{N() -> Nat, X() -> non empty set, F(set) -> Element of X()} :
 {F(n) where n is Nat: n <= N()} is finite non empty Subset of X();

scheme FinImInit2{N() -> Nat, X() -> non empty set, F(set) -> Element of X()} :
 {F(n) where n is Nat: n < N()} is finite non empty Subset of X()
provided
 N() > 0;

definition let c be real number;
 canceled 2;

 attr c is logbase means
:: ASYMPT_0:def 3
 c > 0 & c <> 1;
end;

definition
 cluster positive Real;
 cluster negative Real;
 cluster logbase Real;
 cluster non negative Real;
 cluster non positive Real;
 cluster non logbase Real;
end;

definition let f be Real_Sequence;
 attr f is eventually-nonnegative means
:: ASYMPT_0:def 4
  ex N st for n st n >= N holds f.n >= 0;
 attr f is positive means
:: ASYMPT_0:def 5
  for n holds f.n > 0;
 attr f is eventually-positive means
:: ASYMPT_0:def 6
  ex N st for n st n >= N holds f.n > 0;
 attr f is eventually-nonzero means
:: ASYMPT_0:def 7
  ex N st for n st n >= N holds f.n <> 0;
 attr f is eventually-nondecreasing means
:: ASYMPT_0:def 8
  ex N st for n st n >= N holds f.n <= f.(n+1);
end;

definition
 cluster eventually-nonnegative eventually-nonzero positive eventually-positive
         eventually-nondecreasing Real_Sequence;
end;

definition
 cluster positive -> eventually-positive Real_Sequence;
 cluster eventually-positive ->
                       eventually-nonnegative eventually-nonzero Real_Sequence;
 cluster eventually-nonnegative eventually-nonzero ->
                                             eventually-positive Real_Sequence;
end;

definition let f,g be eventually-nonnegative Real_Sequence;
 cluster f+g -> eventually-nonnegative;
end;

definition let f be Real_Sequence, c be real number;
 func c+f -> Real_Sequence means
:: ASYMPT_0:def 9
  for n holds it.n = c + f.n;
 synonym f+c;
end;

definition let f be eventually-nonnegative Real_Sequence, c be positive Real;
 cluster c(#)f -> eventually-nonnegative;
end;

definition let f be eventually-nonnegative Real_Sequence,
               c be non negative Real;
 cluster c+f -> eventually-nonnegative;
end;

definition let f be eventually-nonnegative Real_Sequence, c be positive Real;
 cluster c+f -> eventually-positive;
end;

definition let f,g be Real_Sequence;
 func max(f, g) -> Real_Sequence means
:: ASYMPT_0:def 10
  for n holds it.n = max( f.n, g.n );
 commutativity;
end;

definition let f be Real_Sequence, g be eventually-nonnegative Real_Sequence;
 cluster max(f, g) -> eventually-nonnegative;
end;

definition let f be Real_Sequence, g be eventually-positive Real_Sequence;
 cluster max(f, g) -> eventually-positive;
end;

definition let f,g be Real_Sequence;
 pred g majorizes f means
:: ASYMPT_0:def 11
  ex N st for n st n >= N holds f.n <= g.n;
end;

theorem :: ASYMPT_0:1  :: Problem 3.25
 for f being Real_Sequence, N being Nat st for n st n >= N holds f.n <= f.(n+1)
  holds for n,m being Nat st N <= n & n <= m holds f.n <= f.m;

theorem :: ASYMPT_0:2
 for f,g being eventually-positive Real_Sequence
  st f/"g is convergent & lim(f/"g) <> 0
   holds g/"f is convergent & lim(g/"f) = (lim(f/"g))";

theorem :: ASYMPT_0:3
 for f being eventually-nonnegative Real_Sequence
  st f is convergent holds 0 <= lim f;

theorem :: ASYMPT_0:4
 for f,g being Real_Sequence
  st f is convergent & g is convergent & g majorizes f holds lim(f) <= lim(g);

theorem :: ASYMPT_0:5
 for f being Real_Sequence, g being eventually-nonzero Real_Sequence
  st f/"g is divergent_to+infty holds g/"f is convergent & lim(g/"f)=0;

begin :: A Notation for "the order of" (Section 3.2)

definition :: Defining O(f) (page 80)
 let f be eventually-nonnegative Real_Sequence;
 func Big_Oh(f) -> FUNCTION_DOMAIN of NAT, REAL equals
:: ASYMPT_0:def 12
  { t where t is Element of Funcs(NAT, REAL) :
     ex c,N st c > 0 & for n st n >= N holds t.n <= c*f.n & t.n >= 0 };
end;

theorem :: ASYMPT_0:6
 for x being set, f being eventually-nonnegative Real_Sequence
  st x in Big_Oh(f) holds x is eventually-nonnegative Real_Sequence;

theorem :: ASYMPT_0:7 :: Threshold Rule (page 81)
   for f being positive Real_Sequence,
     t being eventually-nonnegative Real_Sequence holds
  t in Big_Oh(f) iff ex c st c > 0 & for n holds t.n <= c*f.n;

theorem :: ASYMPT_0:8 :: Generalized Threshold Rule (page 81)
   for f being eventually-positive Real_Sequence,
     t being eventually-nonnegative Real_Sequence,
     N being Nat
  st t in Big_Oh(f) & for n st n >= N holds f.n > 0
   holds ex c st c > 0 & for n st n >= N holds t.n <= c*f.n;

theorem :: ASYMPT_0:9 :: Maximum Rule (page 81)
   for f,g being eventually-nonnegative Real_Sequence holds
  Big_Oh( f + g ) = Big_Oh( max( f, g ) );

theorem :: ASYMPT_0:10  :: Reflexivity of Big_Oh (page 83; Problem 3.9)
 for f being eventually-nonnegative Real_Sequence holds f in Big_Oh(f);

theorem :: ASYMPT_0:11
 for f,g being eventually-nonnegative Real_Sequence
  st f in Big_Oh(g) holds Big_Oh(f) c= Big_Oh(g);

theorem :: ASYMPT_0:12  :: Transitivity of Big_Oh (page 83; Problem 3.10)
 for f,g,h being eventually-nonnegative Real_Sequence holds
  f in Big_Oh(g) & g in Big_Oh(h) implies f in Big_Oh(h);

theorem :: ASYMPT_0:13
   for f being eventually-nonnegative Real_Sequence, c being positive Real
holds
  Big_Oh(f) = Big_Oh(c(#)f);

theorem :: ASYMPT_0:14
:: NOTE: The reverse implication is not true. Consider the case of
:: f = 1/n, c = 1. Then 1/n in Big_Oh(1+1/n), but 1+1/n is not in Big_Oh(1/n).
   for c being non negative Real, x,f being eventually-nonnegative
Real_Sequence
  holds x in Big_Oh(f) implies x in Big_Oh(c+f);

theorem :: ASYMPT_0:15  :: Limit Rule, Part 1 (page 84)
for f,g being eventually-positive Real_Sequence
 st f/"g is convergent & lim( f/"g ) > 0 holds Big_Oh(f) = Big_Oh(g);

theorem :: ASYMPT_0:16  :: Limit Rule, Part 2 (page 84)
for f,g being eventually-positive Real_Sequence
 st f/"g is convergent & lim( f/"g )=0 holds f in Big_Oh(g) & not g in
 Big_Oh(f);

theorem :: ASYMPT_0:17  :: Limit Rule, Part 3 (page 84)
 for f,g being eventually-positive Real_Sequence
  st f/"g is divergent_to+infty holds not f in Big_Oh(g) & g in Big_Oh(f);

begin :: Other Asymptotic Notation (Section 3.3)

definition :: (page 86)
 let f be eventually-nonnegative Real_Sequence;
 func Big_Omega(f) -> FUNCTION_DOMAIN of NAT, REAL equals
:: ASYMPT_0:def 13
  { t where t is Element of Funcs(NAT, REAL) :
     ex d,N st d > 0 & for n st n >= N holds t.n >= d*f.n & t.n >= 0 };
end;

theorem :: ASYMPT_0:18
   for x being set, f being eventually-nonnegative Real_Sequence
  st x in Big_Omega(f) holds x is eventually-nonnegative Real_Sequence;

theorem :: ASYMPT_0:19  :: Duality Rule (page 86)
 for f,g being eventually-nonnegative Real_Sequence holds
  f in Big_Omega(g) iff g in Big_Oh(f);

theorem :: ASYMPT_0:20  :: Reflexivity of Big_Omega (Problem 3.12)
 for f being eventually-nonnegative Real_Sequence holds f in Big_Omega(f);

theorem :: ASYMPT_0:21  :: Transitivity of Big_Omega (Problem 3.12)
 for f,g,h being eventually-nonnegative Real_Sequence holds
  f in Big_Omega(g) & g in Big_Omega(h) implies f in Big_Omega(h);

theorem :: ASYMPT_0:22 :: Limit Rule for Big_Omega, Part 1 (page 86)
   for f,g being eventually-positive Real_Sequence
  st f/"g is convergent & lim( f/"g ) > 0 holds Big_Omega(f) = Big_Omega(g);

theorem :: ASYMPT_0:23  :: Limit Rule for Big_Omega, Part 2 (page 86)
for f,g being eventually-positive Real_Sequence
 st f/"g is convergent & lim( f/"g ) = 0 holds
  g in Big_Omega(f) & not f in Big_Omega(g);

theorem :: ASYMPT_0:24 :: Limit Rule for Big_Omega, Part 3 (page 86)
   for f,g being eventually-positive Real_Sequence
  st f/"g is divergent_to+infty holds not g in Big_Omega(f) & f in Big_Omega(g)
;

theorem :: ASYMPT_0:25 :: Threshold Rule for Big_Omega (page 86)
   for f,t being positive Real_Sequence holds
  t in Big_Omega(f) iff ex d st d > 0 & for n holds d*f.n <= t.n;

theorem :: ASYMPT_0:26 :: Maximum Rule for Big_Omega (page 86)
   for f,g being eventually-nonnegative Real_Sequence holds
  Big_Omega(f+g) = Big_Omega(max(f,g));

definition :: (page 87)
 let f be eventually-nonnegative Real_Sequence;
 func Big_Theta(f) -> FUNCTION_DOMAIN of NAT, REAL equals
:: ASYMPT_0:def 14

  Big_Oh(f) /\ Big_Omega(f);
end;

theorem :: ASYMPT_0:27  :: Alternate Definition for Big_Theta (page 87)
 for f being eventually-nonnegative Real_Sequence holds
  Big_Theta(f) = { t where t is Element of Funcs(NAT, REAL) :
     ex c,d,N st c > 0 & d > 0 &
      for n st n >= N holds d*f.n <= t.n & t.n <= c*f.n };

theorem :: ASYMPT_0:28 :: Reflexivity of Big_Theta (Problem 3.18 Part 1)
   for f being eventually-nonnegative Real_Sequence holds f in Big_Theta(f);

theorem :: ASYMPT_0:29 :: Symmetry of Big_Theta (Problem 3.18 Part 2)
   for f,g being eventually-nonnegative Real_Sequence
  st f in Big_Theta(g) holds g in Big_Theta(f);

theorem :: ASYMPT_0:30 :: Transitivity of Big_Theta (Problem 3.18 Part 3)
   for f,g,h being eventually-nonnegative Real_Sequence
  st f in Big_Theta(g) & g in Big_Theta(h) holds f in Big_Theta(h);

theorem :: ASYMPT_0:31 :: Threshold Rule for Big_Theta (page 87)
   for f,t being positive Real_Sequence holds
  t in Big_Theta(f) iff
   ex c,d st c > 0 & d > 0 & for n holds d*f.n <= t.n & t.n <= c*f.n;

theorem :: ASYMPT_0:32 :: Maximum Rule for Big_Theta (page 87)
   for f,g being eventually-nonnegative Real_Sequence holds
  Big_Theta(f+g) = Big_Theta(max(f,g));

theorem :: ASYMPT_0:33 :: Limit Rule for Big_Theta, Part 1 (page 88)
  for f,g being eventually-positive Real_Sequence
 st f/"g is convergent & lim( f/"g ) > 0 holds f in Big_Theta(g);

theorem :: ASYMPT_0:34 :: Limit Rule for Big_Theta, Part 2 (page 88)
  for f,g being eventually-positive Real_Sequence
 st f/"g is convergent & lim( f/"g ) = 0
  holds f in Big_Oh(g) & not f in Big_Theta(g);

theorem :: ASYMPT_0:35 :: Limit Rule for Big_Theta, Part 3 (page 88)
   for f,g being eventually-positive Real_Sequence
  st f/"g is divergent_to+infty holds f in Big_Omega(g) & not f in Big_Theta(g)
;

begin :: Conditional Asymptotic Notation (Section 3.4)

definition :: page 89
 let f be eventually-nonnegative Real_Sequence, X be set;
 func Big_Oh(f,X) -> FUNCTION_DOMAIN of NAT, REAL equals
:: ASYMPT_0:def 15
  { t where t is Element of Funcs(NAT, REAL) :
     ex c,N st c > 0 & for n st n >= N & n in X holds t.n <= c*f.n & t.n >=
 0 };
end;

definition :: page 89
 let f be eventually-nonnegative Real_Sequence, X be set;
 func Big_Omega(f,X) -> FUNCTION_DOMAIN of NAT, REAL equals
:: ASYMPT_0:def 16
  { t where t is Element of Funcs(NAT, REAL) :
     ex d,N st d > 0 & for n st n >= N & n in X holds t.n >= d*f.n & t.n >=
 0 };
end;

definition :: page 89
 let f be eventually-nonnegative Real_Sequence, X be set;
 func Big_Theta(f,X) -> FUNCTION_DOMAIN of NAT, REAL equals
:: ASYMPT_0:def 17
  { t where t is Element of Funcs(NAT, REAL) :
     ex c,d,N st c > 0 & d > 0 &
      for n st n >= N & n in X holds d*f.n <= t.n & t.n <= c*f.n };
end;

theorem :: ASYMPT_0:36  :: Alternate definition for Big_Theta_Cond
 for f being eventually-nonnegative Real_Sequence, X being set holds
  Big_Theta(f,X) = Big_Oh(f,X) /\ Big_Omega(f,X);

definition :: Definition of f(bn) (page 89)
 let f be Real_Sequence, b be Nat;
  func f taken_every b -> Real_Sequence means
:: ASYMPT_0:def 18
   for n holds it.n = f.(b*n);
end;

definition :: (page 89)
 let f be eventually-nonnegative Real_Sequence, b be Nat;
 pred f is_smooth_wrt b means
:: ASYMPT_0:def 19
  f is eventually-nondecreasing & f taken_every b in Big_Oh(f);
end;

definition :: (page 89)
 let f be eventually-nonnegative Real_Sequence;
 attr f is smooth means
:: ASYMPT_0:def 20
  for b being Nat st b >= 2 holds f is_smooth_wrt b;
end;

theorem :: ASYMPT_0:37 :: b-smooth implies smooth (page 90)
   for f being eventually-nonnegative Real_Sequence
  st ex b being Nat st b >= 2 & f is_smooth_wrt b holds f is smooth;

theorem :: ASYMPT_0:38  :: First half of smoothness rule proof (page 90)
 for f being eventually-nonnegative Real_Sequence,
     t being eventually-nonnegative eventually-nondecreasing Real_Sequence,
     b being Nat
  st f is smooth & b >= 2 &
     t in Big_Oh(f, { b|^n where n is Nat : not contradiction } )
   holds t in Big_Oh(f);

theorem :: ASYMPT_0:39  :: Second half of smoothness rule proof (page 90),
                    :: also Problem 3.29
 for f being eventually-nonnegative Real_Sequence,
     t being eventually-nonnegative eventually-nondecreasing Real_Sequence,
     b being Nat
  st f is smooth & b >= 2 &
     t in Big_Omega(f, { b|^n where n is Nat : not contradiction } )
   holds t in Big_Omega(f);

theorem :: ASYMPT_0:40 :: Smoothness Rule (page 90)
   for f being eventually-nonnegative Real_Sequence,
     t being eventually-nonnegative eventually-nondecreasing Real_Sequence,
     b being Nat
  st f is smooth & b >= 2 &
     t in Big_Theta(f, { b|^n where n is Nat : not contradiction } )
   holds t in Big_Theta(f);

:: Section 3.5 omitted

begin :: Operations on Asymptotic Notation (Section 3.6)

definition :: Definition of operators on sets (page 91)
 let X be non empty set, F,G be FUNCTION_DOMAIN of X,REAL;
  func F + G -> FUNCTION_DOMAIN of X,REAL equals
:: ASYMPT_0:def 21
   { t where t is Element of Funcs(X,REAL) :
      ex f,g being Element of Funcs(X,REAL) st
       f in F & g in G & for n being Element of X holds t.n = f.n + g.n };
end;

definition :: (page 91)
 let X be non empty set, F,G be FUNCTION_DOMAIN of X,REAL;
  func max(F, G) -> FUNCTION_DOMAIN of X,REAL equals
:: ASYMPT_0:def 22
   { t where t is Element of Funcs(X,REAL) :
      ex f,g being Element of Funcs(X,REAL) st
       f in F & g in G & for n being Element of X holds t.n = max(f.n, g.n) };
end;

theorem :: ASYMPT_0:41 :: Properties, Part 1 (page 91; Problem 3.33)
   for f,g being eventually-nonnegative Real_Sequence holds
  Big_Oh(f) + Big_Oh(g) = Big_Oh(f+g);

theorem :: ASYMPT_0:42 :: Properties, Part 3 (page 91; Problem 3.33)
   for f,g being eventually-nonnegative Real_Sequence holds
  max(Big_Oh(f), Big_Oh(g)) = Big_Oh(max(f,g));

definition :: Definition of operators on sets (page 92)
 let F,G be FUNCTION_DOMAIN of NAT,REAL;
  func F to_power G -> FUNCTION_DOMAIN of NAT,REAL equals
:: ASYMPT_0:def 23
     { t where t is Element of Funcs(NAT,REAL) :
      ex f,g being Element of Funcs(NAT,REAL), N being Element of NAT st
       f in F & g in G &
        for n being Element of NAT st n >=
 N holds t.n = (f.n) to_power (g.n) };
end;
The abstract of the Mizar article:

Asymptotic Notation. Part I: Theory
