:: Asymptotic notation. Part I: Theory :: by Richard Krueger , Piotr Rudnicki and Paul Shelley :: :: Received November 4, 1999 :: Copyright (c) 1999-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, REAL_1, SUBSET_1, NAT_1, XBOOLE_0, XXREAL_0, FINSET_1, TARSKI, CARD_1, ARYTM_3, ARYTM_1, SEQ_1, FUNCT_1, VALUED_1, RELAT_1, SEQ_2, ORDINAL2, COMPLEX1, LIMFUNC1, FUNCT_2, INT_1, POWER, NEWTON, ASYMPT_0, FUNCT_7, ASYMPT_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, FUNCT_1, FUNCT_2, XXREAL_0, XXREAL_2, INT_1, NAT_1, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, NEWTON, POWER, FUNCOP_1, FINSET_1, LIMFUNC1; constructors REAL_1, NAT_1, SEQ_2, LIMFUNC1, NEWTON, POWER, VALUED_1, PARTFUN1, XXREAL_2, RELSET_1, FUNCOP_1, COMSEQ_2, SQUARE_1, SEQ_1, NUMBERS; registrations XBOOLE_0, ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, VALUED_0, VALUED_1, FUNCT_2, POWER, XXREAL_2, FUNCT_1, NEWTON; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Preliminaries reserve c, c1, d for Real, k for Nat, n, m, N, n1, N1, N2, N3, N4, N5, M for Element of NAT, x for set; scheme :: ASYMPT_0:sch 1 FinSegRng1{m, n() -> Nat, X() -> non empty set, F(set) -> Element of X()} : {F(i) where i is Element of NAT: m() <= i & i <= n()} is finite non empty Subset of X() provided m() <= n(); scheme :: ASYMPT_0:sch 2 FinImInit1{N() -> Nat, X() -> non empty set, F(set) -> Element of X()} : {F( n) where n is Element of NAT: n <= N()} is finite non empty Subset of X(); scheme :: ASYMPT_0:sch 3 FinImInit2{N() -> Nat, X() -> non empty set, F(set) -> Element of X()} : {F( n) where n is Element of NAT: n < N()} is finite non empty Subset of X() provided N() > 0; definition let c be Real; attr c is logbase means :: ASYMPT_0:def 1 c > 0 & c <> 1; end; registration cluster positive for Real; cluster negative for Real; cluster logbase for Real; cluster non negative for Real; cluster non positive for Real; cluster non logbase for Real; end; definition let f be Real_Sequence; attr f is eventually-nonnegative means :: ASYMPT_0:def 2 ex N being Nat st for n being Nat st n >= N holds f.n >= 0; attr f is positive means :: ASYMPT_0:def 3 for n being Nat holds f.n > 0; attr f is eventually-positive means :: ASYMPT_0:def 4 ex N being Nat st for n being Nat st n >= N holds f.n > 0; attr f is eventually-nonzero means :: ASYMPT_0:def 5 ex N being Nat st for n being Nat st n >= N holds f.n <> 0; attr f is eventually-nondecreasing means :: ASYMPT_0:def 6 ex N being Nat st for n being Nat st n >= N holds f.n <= f.(n+1); end; registration cluster eventually-nonnegative eventually-nonzero positive eventually-positive eventually-nondecreasing for Real_Sequence; end; registration cluster positive -> eventually-positive for Real_Sequence; cluster eventually-positive -> eventually-nonnegative eventually-nonzero for Real_Sequence; cluster eventually-nonnegative eventually-nonzero -> eventually-positive for Real_Sequence; end; definition let f,g be eventually-nonnegative Real_Sequence; redefine func f+g -> eventually-nonnegative Real_Sequence; end; definition let f be eventually-nonnegative Real_Sequence, c be positive Real; redefine func c(#)f -> eventually-nonnegative Real_Sequence; end; definition let f be eventually-nonnegative Real_Sequence, c be non negative Real; redefine func c+f -> eventually-nonnegative Real_Sequence; end; definition let f be eventually-nonnegative Real_Sequence, c be positive Real; redefine func c+f -> eventually-positive Real_Sequence; end; definition let f,g be Real_Sequence; func max(f, g) -> Real_Sequence means :: ASYMPT_0:def 7 for n being Nat holds it.n = max( f.n, g .n ); commutativity; end; registration let f be Real_Sequence, g be eventually-nonnegative Real_Sequence; cluster max(f, g) -> eventually-nonnegative; end; registration 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 8 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 being Nat st n>= N holds f.n <= f.(n+1) 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 let f be eventually-nonnegative Real_Sequence; func Big_Oh(f) -> FUNCTION_DOMAIN of NAT, REAL equals :: ASYMPT_0:def 9 { 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 Element of 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 let f be eventually-nonnegative Real_Sequence; func Big_Omega(f) -> FUNCTION_DOMAIN of NAT, REAL equals :: ASYMPT_0:def 10 { 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 let f be eventually-nonnegative Real_Sequence; func Big_Theta(f) -> FUNCTION_DOMAIN of NAT, REAL equals :: ASYMPT_0:def 11 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 let f be eventually-nonnegative Real_Sequence, X be set; func Big_Oh(f,X) -> 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 & n in X holds t.n <= c*f.n & t.n >= 0 }; end; definition let f be eventually-nonnegative Real_Sequence, X be set; func Big_Omega(f,X) -> 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 & n in X holds t.n >= d*f.n & t.n >= 0 }; end; definition let f be eventually-nonnegative Real_Sequence, X be set; func Big_Theta(f,X) -> FUNCTION_DOMAIN of NAT, REAL equals :: ASYMPT_0:def 14 { 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 15 for n holds it.n = f.(b* n); end; definition let f be eventually-nonnegative Real_Sequence, b be Nat; pred f is_smooth_wrt b means :: ASYMPT_0:def 16 f is eventually-nondecreasing & f taken_every b in Big_Oh(f); end; definition let f be eventually-nonnegative Real_Sequence; attr f is smooth means :: ASYMPT_0:def 17 for b being Element of 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 Element of 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, the set of all b|^n where n is Element of NAT ) holds t in Big_Oh(f); theorem :: ASYMPT_0:39 :: Second half of smoothness rule proof (page 90), for f being eventually-nonnegative Real_Sequence, t being eventually-nonnegative eventually-nondecreasing Real_Sequence, b being Element of NAT st f is smooth & b >= 2 & t in Big_Omega(f, the set of all b|^n where n is Element of NAT ) holds t in Big_Omega(f); theorem :: ASYMPT_0:40 :: also Problem 3.29:: Smoothness Rule (page 90) for f being eventually-nonnegative Real_Sequence, t being eventually-nonnegative eventually-nondecreasing Real_Sequence, b being Element of NAT st f is smooth & b >= 2 & t in Big_Theta(f, the set of all b|^n where n is Element of NAT ) holds t in Big_Theta(f); :: Section 3.5 omitted begin :: Operations on Asymptotic Notation (Section 3.6) definition 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 18 { 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 19 { 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 20 { 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;