:: Asymptotic notation. Part I: Theory :: by Richard Krueger , Piotr Rudnicki and Paul Shelley :: :: Received November 4, 1999 :: Copyright (c) 1999-2012 Association of Mizar Users begin scheme :: ASYMPT_0:sch 1 FinSegRng1{ F1() -> Nat, F2() -> Nat, F3() -> non empty set , F4( set ) -> Element of F3() } : { F4(i) where i is Element of NAT : ( F1() <= i & i <= F2() ) } is non empty finite Subset of F3() provided A1: F1() <= F2() proofend; scheme :: ASYMPT_0:sch 2 FinImInit1{ F1() -> Nat, F2() -> non empty set , F3( set ) -> Element of F2() } : { F3(n) where n is Element of NAT : n <= F1() } is non empty finite Subset of F2() proofend; scheme :: ASYMPT_0:sch 3 FinImInit2{ F1() -> Nat, F2() -> non empty set , F3( set ) -> Element of F2() } : { F3(n) where n is Element of NAT : n < F1() } is non empty finite Subset of F2() provided A1: F1() > 0 proofend; definition let c be real number ; attrc is logbase means :Def1: :: ASYMPT_0:def 1 ( c > 0 & c <> 1 ); end; :: deftheorem Def1 defines logbase ASYMPT_0:def_1_:_ for c being real number holds ( c is logbase iff ( c > 0 & c <> 1 ) ); registration clusterV11() real ext-real positive for Element of REAL ; existence ex b1 being Real st b1 is positive proofend; clusterV11() real ext-real negative for Element of REAL ; existence ex b1 being Real st b1 is negative proofend; clusterV11() real ext-real logbase for Element of REAL ; existence ex b1 being Real st b1 is logbase proofend; clusterV11() real ext-real non negative for Element of REAL ; existence not for b1 being Real holds b1 is negative by XXREAL_0:def_7; clusterV11() real ext-real non positive for Element of REAL ; existence not for b1 being Real holds b1 is positive by XXREAL_0:def_6; clusterV11() real ext-real non logbase for Element of REAL ; existence not for b1 being Real holds b1 is logbase proofend; end; definition let f be Real_Sequence; attrf is eventually-nonnegative means :Def2: :: ASYMPT_0:def 2 ex N being Element of NAT st for n being Element of NAT st n >= N holds f . n >= 0 ; attrf is positive means :Def3: :: ASYMPT_0:def 3 for n being Element of NAT holds f . n > 0 ; attrf is eventually-positive means :Def4: :: ASYMPT_0:def 4 ex N being Element of NAT st for n being Element of NAT st n >= N holds f . n > 0 ; attrf is eventually-nonzero means :Def5: :: ASYMPT_0:def 5 ex N being Element of NAT st for n being Element of NAT st n >= N holds f . n <> 0 ; attrf is eventually-nondecreasing means :Def6: :: ASYMPT_0:def 6 ex N being Element of NAT st for n being Element of NAT st n >= N holds f . n <= f . (n + 1); end; :: deftheorem Def2 defines eventually-nonnegative ASYMPT_0:def_2_:_ for f being Real_Sequence holds ( f is eventually-nonnegative iff ex N being Element of NAT st for n being Element of NAT st n >= N holds f . n >= 0 ); :: deftheorem Def3 defines positive ASYMPT_0:def_3_:_ for f being Real_Sequence holds ( f is positive iff for n being Element of NAT holds f . n > 0 ); :: deftheorem Def4 defines eventually-positive ASYMPT_0:def_4_:_ for f being Real_Sequence holds ( f is eventually-positive iff ex N being Element of NAT st for n being Element of NAT st n >= N holds f . n > 0 ); :: deftheorem Def5 defines eventually-nonzero ASYMPT_0:def_5_:_ for f being Real_Sequence holds ( f is eventually-nonzero iff ex N being Element of NAT st for n being Element of NAT st n >= N holds f . n <> 0 ); :: deftheorem Def6 defines eventually-nondecreasing ASYMPT_0:def_6_:_ for f being Real_Sequence holds ( f is eventually-nondecreasing iff ex N being Element of NAT st for n being Element of NAT st n >= N holds f . n <= f . (n + 1) ); registration cluster non empty V16() V19( NAT ) V20( REAL ) Function-like V26( NAT ) quasi_total V33() V34() V35() eventually-nonnegative positive eventually-positive eventually-nonzero eventually-nondecreasing for Element of K6(K7(NAT,REAL)); existence ex b1 being Real_Sequence st ( b1 is eventually-nonnegative & b1 is eventually-nonzero & b1 is positive & b1 is eventually-positive & b1 is eventually-nondecreasing ) proofend; end; registration cluster Function-like quasi_total positive -> eventually-positive for Element of K6(K7(NAT,REAL)); coherence for b1 being Real_Sequence st b1 is positive holds b1 is eventually-positive proofend; cluster Function-like quasi_total eventually-positive -> eventually-nonnegative eventually-nonzero for Element of K6(K7(NAT,REAL)); coherence for b1 being Real_Sequence st b1 is eventually-positive holds ( b1 is eventually-nonnegative & b1 is eventually-nonzero ) proofend; cluster Function-like quasi_total eventually-nonnegative eventually-nonzero -> eventually-positive for Element of K6(K7(NAT,REAL)); coherence for b1 being Real_Sequence st b1 is eventually-nonnegative & b1 is eventually-nonzero holds b1 is eventually-positive proofend; end; definition let f, g be eventually-nonnegative Real_Sequence; :: original:+ redefine funcf + g -> eventually-nonnegative Real_Sequence; coherence f + g is eventually-nonnegative Real_Sequence proofend; end; definition let f be eventually-nonnegative Real_Sequence; let c be positive Real; :: original:(#) redefine funcc (#) f -> eventually-nonnegative Real_Sequence; coherence c (#) f is eventually-nonnegative Real_Sequence proofend; end; definition let f be eventually-nonnegative Real_Sequence; let c be non negative Real; :: original:+ redefine funcc + f -> eventually-nonnegative Real_Sequence; coherence c + f is eventually-nonnegative Real_Sequence proofend; end; definition let f be eventually-nonnegative Real_Sequence; let c be positive Real; :: original:+ redefine funcc + f -> eventually-positive Real_Sequence; coherence c + f is eventually-positive Real_Sequence proofend; end; definition let f, g be Real_Sequence; func max (f,g) -> Real_Sequence means :Def7: :: ASYMPT_0:def 7 for n being Element of NAT holds it . n = max ((f . n),(g . n)); existence ex b1 being Real_Sequence st for n being Element of NAT holds b1 . n = max ((f . n),(g . n)) proofend; uniqueness for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = max ((f . n),(g . n)) ) & ( for n being Element of NAT holds b2 . n = max ((f . n),(g . n)) ) holds b1 = b2 proofend; commutativity for b1, f, g being Real_Sequence st ( for n being Element of NAT holds b1 . n = max ((f . n),(g . n)) ) holds for n being Element of NAT holds b1 . n = max ((g . n),(f . n)) ; end; :: deftheorem Def7 defines max ASYMPT_0:def_7_:_ for f, g, b3 being Real_Sequence holds ( b3 = max (f,g) iff for n being Element of NAT holds b3 . n = max ((f . n),(g . n)) ); registration let f be Real_Sequence; let g be eventually-nonnegative Real_Sequence; cluster max (f,g) -> eventually-nonnegative ; coherence max (f,g) is eventually-nonnegative proofend; end; registration let f be Real_Sequence; let g be eventually-positive Real_Sequence; cluster max (f,g) -> eventually-positive ; coherence max (f,g) is eventually-positive proofend; end; definition let f, g be Real_Sequence; predg majorizes f means :Def8: :: ASYMPT_0:def 8 ex N being Element of NAT st for n being Element of NAT st n >= N holds f . n <= g . n; end; :: deftheorem Def8 defines majorizes ASYMPT_0:def_8_:_ for f, g being Real_Sequence holds ( g majorizes f iff ex N being Element of NAT st for n being Element of NAT st n >= N holds f . n <= g . n ); Lm1: for f, g being Real_Sequence for n being Element of NAT holds (f /" g) . n = (f . n) / (g . n) proofend; theorem Th1: :: ASYMPT_0:1 for f being Real_Sequence for N being Element of NAT st ( for n being Element of NAT st n >= N holds f . n <= f . (n + 1) ) holds for n, m being Element of NAT st N <= n & n <= m holds f . n <= f . m proofend; theorem Th2: :: 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)) " ) proofend; theorem Th3: :: ASYMPT_0:3 for f being eventually-nonnegative Real_Sequence st f is convergent holds 0 <= lim f proofend; theorem Th4: :: ASYMPT_0:4 for f, g being Real_Sequence st f is convergent & g is convergent & g majorizes f holds lim f <= lim g proofend; theorem Th5: :: ASYMPT_0:5 for f being Real_Sequence for g being eventually-nonzero Real_Sequence st f /" g is divergent_to+infty holds ( g /" f is convergent & lim (g /" f) = 0 ) proofend; begin 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 being Real ex N being Element of NAT st ( c > 0 & ( for n being Element of NAT st n >= N holds ( t . n <= c * (f . n) & t . n >= 0 ) ) ) } ; coherence { t where t is Element of Funcs (NAT,REAL) : ex c being Real ex N being Element of NAT st ( c > 0 & ( for n being Element of NAT st n >= N holds ( t . n <= c * (f . n) & t . n >= 0 ) ) ) } is FUNCTION_DOMAIN of NAT , REAL proofend; end; :: deftheorem defines Big_Oh ASYMPT_0:def_9_:_ for f being eventually-nonnegative Real_Sequence holds Big_Oh f = { t where t is Element of Funcs (NAT,REAL) : ex c being Real ex N being Element of NAT st ( c > 0 & ( for n being Element of NAT st n >= N holds ( t . n <= c * (f . n) & t . n >= 0 ) ) ) } ; theorem Th6: :: ASYMPT_0:6 for x being set for f being eventually-nonnegative Real_Sequence st x in Big_Oh f holds x is eventually-nonnegative Real_Sequence proofend; theorem :: ASYMPT_0:7 for f being positive Real_Sequence for t being eventually-nonnegative Real_Sequence holds ( t in Big_Oh f iff ex c being Real st ( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) ) ) proofend; theorem :: ASYMPT_0:8 for f being eventually-positive Real_Sequence for t being eventually-nonnegative Real_Sequence for N being Element of NAT st t in Big_Oh f & ( for n being Element of NAT st n >= N holds f . n > 0 ) holds ex c being Real st ( c > 0 & ( for n being Element of NAT st n >= N holds t . n <= c * (f . n) ) ) proofend; theorem :: ASYMPT_0:9 for f, g being eventually-nonnegative Real_Sequence holds Big_Oh (f + g) = Big_Oh (max (f,g)) proofend; theorem Th10: :: ASYMPT_0:10 for f being eventually-nonnegative Real_Sequence holds f in Big_Oh f proofend; theorem Th11: :: 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 proofend; theorem Th12: :: ASYMPT_0:12 for f, g, h being eventually-nonnegative Real_Sequence st f in Big_Oh g & g in Big_Oh h holds f in Big_Oh h proofend; Lm2: for f, g being eventually-nonnegative Real_Sequence holds ( ( f in Big_Oh g & g in Big_Oh f ) iff Big_Oh f = Big_Oh g ) proofend; theorem :: ASYMPT_0:13 for f being eventually-nonnegative Real_Sequence for c being positive Real holds Big_Oh f = Big_Oh (c (#) f) proofend; theorem :: ASYMPT_0:14 for c being non negative Real for x, f being eventually-nonnegative Real_Sequence st x in Big_Oh f holds x in Big_Oh (c + f) proofend; Lm3: for f, g being eventually-positive Real_Sequence st f /" g is convergent & lim (f /" g) > 0 holds f in Big_Oh g proofend; theorem Th15: :: ASYMPT_0:15 for f, g being eventually-positive Real_Sequence st f /" g is convergent & lim (f /" g) > 0 holds Big_Oh f = Big_Oh g proofend; theorem Th16: :: ASYMPT_0:16 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 ) proofend; theorem Th17: :: ASYMPT_0:17 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 ) proofend; begin 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 being Real ex N being Element of NAT st ( d > 0 & ( for n being Element of NAT st n >= N holds ( t . n >= d * (f . n) & t . n >= 0 ) ) ) } ; coherence { t where t is Element of Funcs (NAT,REAL) : ex d being Real ex N being Element of NAT st ( d > 0 & ( for n being Element of NAT st n >= N holds ( t . n >= d * (f . n) & t . n >= 0 ) ) ) } is FUNCTION_DOMAIN of NAT , REAL proofend; end; :: deftheorem defines Big_Omega ASYMPT_0:def_10_:_ for f being eventually-nonnegative Real_Sequence holds Big_Omega f = { t where t is Element of Funcs (NAT,REAL) : ex d being Real ex N being Element of NAT st ( d > 0 & ( for n being Element of NAT st n >= N holds ( t . n >= d * (f . n) & t . n >= 0 ) ) ) } ; theorem :: ASYMPT_0:18 for x being set for f being eventually-nonnegative Real_Sequence st x in Big_Omega f holds x is eventually-nonnegative Real_Sequence proofend; theorem Th19: :: ASYMPT_0:19 for f, g being eventually-nonnegative Real_Sequence holds ( f in Big_Omega g iff g in Big_Oh f ) proofend; theorem Th20: :: ASYMPT_0:20 for f being eventually-nonnegative Real_Sequence holds f in Big_Omega f proofend; theorem Th21: :: ASYMPT_0:21 for f, g, h being eventually-nonnegative Real_Sequence st f in Big_Omega g & g in Big_Omega h holds f in Big_Omega h proofend; theorem :: ASYMPT_0:22 for f, g being eventually-positive Real_Sequence st f /" g is convergent & lim (f /" g) > 0 holds Big_Omega f = Big_Omega g proofend; theorem Th23: :: ASYMPT_0:23 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 ) proofend; theorem :: ASYMPT_0:24 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 ) proofend; theorem :: ASYMPT_0:25 for f, t being positive Real_Sequence holds ( t in Big_Omega f iff ex d being Real st ( d > 0 & ( for n being Element of NAT holds d * (f . n) <= t . n ) ) ) proofend; theorem :: ASYMPT_0:26 for f, g being eventually-nonnegative Real_Sequence holds Big_Omega (f + g) = Big_Omega (max (f,g)) proofend; 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); coherence (Big_Oh f) /\ (Big_Omega f) is FUNCTION_DOMAIN of NAT , REAL proofend; end; :: deftheorem defines Big_Theta ASYMPT_0:def_11_:_ for f being eventually-nonnegative Real_Sequence holds Big_Theta f = (Big_Oh f) /\ (Big_Omega f); theorem Th27: :: ASYMPT_0:27 for f being eventually-nonnegative Real_Sequence holds Big_Theta f = { t where t is Element of Funcs (NAT,REAL) : ex c, d being Real ex N being Element of NAT st ( c > 0 & d > 0 & ( for n being Element of NAT st n >= N holds ( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) } proofend; theorem :: ASYMPT_0:28 for f being eventually-nonnegative Real_Sequence holds f in Big_Theta f proofend; theorem :: ASYMPT_0:29 for f, g being eventually-nonnegative Real_Sequence st f in Big_Theta g holds g in Big_Theta f proofend; theorem :: ASYMPT_0:30 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 proofend; theorem :: ASYMPT_0:31 for f, t being positive Real_Sequence holds ( t in Big_Theta f iff ex c, d being Real st ( c > 0 & d > 0 & ( for n being Element of NAT holds ( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) ) proofend; theorem :: ASYMPT_0:32 for f, g being eventually-nonnegative Real_Sequence holds Big_Theta (f + g) = Big_Theta (max (f,g)) proofend; theorem :: ASYMPT_0:33 for f, g being eventually-positive Real_Sequence st f /" g is convergent & lim (f /" g) > 0 holds f in Big_Theta g proofend; theorem :: ASYMPT_0:34 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 ) proofend; theorem :: ASYMPT_0:35 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 ) proofend; begin definition let f be eventually-nonnegative Real_Sequence; let 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 being Real ex N being Element of NAT st ( c > 0 & ( for n being Element of NAT st n >= N & n in X holds ( t . n <= c * (f . n) & t . n >= 0 ) ) ) } ; coherence { t where t is Element of Funcs (NAT,REAL) : ex c being Real ex N being Element of NAT st ( c > 0 & ( for n being Element of NAT st n >= N & n in X holds ( t . n <= c * (f . n) & t . n >= 0 ) ) ) } is FUNCTION_DOMAIN of NAT , REAL proofend; end; :: deftheorem defines Big_Oh ASYMPT_0:def_12_:_ for f being eventually-nonnegative Real_Sequence for X being set holds Big_Oh (f,X) = { t where t is Element of Funcs (NAT,REAL) : ex c being Real ex N being Element of NAT st ( c > 0 & ( for n being Element of NAT st n >= N & n in X holds ( t . n <= c * (f . n) & t . n >= 0 ) ) ) } ; definition let f be eventually-nonnegative Real_Sequence; let 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 being Real ex N being Element of NAT st ( d > 0 & ( for n being Element of NAT st n >= N & n in X holds ( t . n >= d * (f . n) & t . n >= 0 ) ) ) } ; coherence { t where t is Element of Funcs (NAT,REAL) : ex d being Real ex N being Element of NAT st ( d > 0 & ( for n being Element of NAT st n >= N & n in X holds ( t . n >= d * (f . n) & t . n >= 0 ) ) ) } is FUNCTION_DOMAIN of NAT , REAL proofend; end; :: deftheorem defines Big_Omega ASYMPT_0:def_13_:_ for f being eventually-nonnegative Real_Sequence for X being set holds Big_Omega (f,X) = { t where t is Element of Funcs (NAT,REAL) : ex d being Real ex N being Element of NAT st ( d > 0 & ( for n being Element of NAT st n >= N & n in X holds ( t . n >= d * (f . n) & t . n >= 0 ) ) ) } ; definition let f be eventually-nonnegative Real_Sequence; let 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 being Real ex N being Element of NAT st ( c > 0 & d > 0 & ( for n being Element of NAT st n >= N & n in X holds ( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) } ; coherence { t where t is Element of Funcs (NAT,REAL) : ex c, d being Real ex N being Element of NAT st ( c > 0 & d > 0 & ( for n being Element of NAT st n >= N & n in X holds ( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) } is FUNCTION_DOMAIN of NAT , REAL proofend; end; :: deftheorem defines Big_Theta ASYMPT_0:def_14_:_ for f being eventually-nonnegative Real_Sequence for X being set holds Big_Theta (f,X) = { t where t is Element of Funcs (NAT,REAL) : ex c, d being Real ex N being Element of NAT st ( c > 0 & d > 0 & ( for n being Element of NAT st n >= N & n in X holds ( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) } ; theorem Th36: :: ASYMPT_0:36 for f being eventually-nonnegative Real_Sequence for X being set holds Big_Theta (f,X) = (Big_Oh (f,X)) /\ (Big_Omega (f,X)) proofend; definition let f be Real_Sequence; let b be Element of NAT ; funcf taken_every b -> Real_Sequence means :Def15: :: ASYMPT_0:def 15 for n being Element of NAT holds it . n = f . (b * n); existence ex b1 being Real_Sequence st for n being Element of NAT holds b1 . n = f . (b * n) proofend; uniqueness for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = f . (b * n) ) & ( for n being Element of NAT holds b2 . n = f . (b * n) ) holds b1 = b2 proofend; end; :: deftheorem Def15 defines taken_every ASYMPT_0:def_15_:_ for f being Real_Sequence for b being Element of NAT for b3 being Real_Sequence holds ( b3 = f taken_every b iff for n being Element of NAT holds b3 . n = f . (b * n) ); definition let f be eventually-nonnegative Real_Sequence; let b be Element of NAT ; predf is_smooth_wrt b means :Def16: :: ASYMPT_0:def 16 ( f is eventually-nondecreasing & f taken_every b in Big_Oh f ); end; :: deftheorem Def16 defines is_smooth_wrt ASYMPT_0:def_16_:_ for f being eventually-nonnegative Real_Sequence for b being Element of NAT holds ( f is_smooth_wrt b iff ( f is eventually-nondecreasing & f taken_every b in Big_Oh f ) ); definition let f be eventually-nonnegative Real_Sequence; attrf is smooth means :Def17: :: ASYMPT_0:def 17 for b being Element of NAT st b >= 2 holds f is_smooth_wrt b; end; :: deftheorem Def17 defines smooth ASYMPT_0:def_17_:_ for f being eventually-nonnegative Real_Sequence holds ( f is smooth iff for b being Element of NAT st b >= 2 holds f is_smooth_wrt b ); theorem :: ASYMPT_0:37 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 proofend; theorem Th38: :: ASYMPT_0:38 for f being eventually-nonnegative Real_Sequence for t being eventually-nonnegative eventually-nondecreasing Real_Sequence for b being Element of NAT st f is smooth & b >= 2 & t in Big_Oh (f, { (b |^ n) where n is Element of NAT : verum } ) holds t in Big_Oh f proofend; theorem Th39: :: ASYMPT_0:39 for f being eventually-nonnegative Real_Sequence for t being eventually-nonnegative eventually-nondecreasing Real_Sequence for b being Element of NAT st f is smooth & b >= 2 & t in Big_Omega (f, { (b |^ n) where n is Element of NAT : verum } ) holds t in Big_Omega f proofend; theorem :: ASYMPT_0:40 for f being eventually-nonnegative Real_Sequence for t being eventually-nonnegative eventually-nondecreasing Real_Sequence for b being Element of NAT st f is smooth & b >= 2 & t in Big_Theta (f, { (b |^ n) where n is Element of NAT : verum } ) holds t in Big_Theta f proofend; begin definition let X be non empty set ; let F, G be FUNCTION_DOMAIN of X, REAL ; funcF + 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) ) ) } ; coherence { 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) ) ) } is FUNCTION_DOMAIN of X, REAL proofend; end; :: deftheorem defines + ASYMPT_0:def_18_:_ for X being non empty set for F, G being FUNCTION_DOMAIN of X, REAL holds F + G = { 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) ) ) } ; definition let X be non empty set ; let 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)) ) ) } ; coherence { 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)) ) ) } is FUNCTION_DOMAIN of X, REAL proofend; end; :: deftheorem defines max ASYMPT_0:def_19_:_ for X being non empty set for F, G being FUNCTION_DOMAIN of X, REAL holds max (F,G) = { 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)) ) ) } ; theorem :: ASYMPT_0:41 for f, g being eventually-nonnegative Real_Sequence holds (Big_Oh f) + (Big_Oh g) = Big_Oh (f + g) proofend; theorem :: ASYMPT_0:42 for f, g being eventually-nonnegative Real_Sequence holds max ((Big_Oh f),(Big_Oh g)) = Big_Oh (max (f,g)) proofend; definition let F, G be FUNCTION_DOMAIN of NAT , REAL ; funcF 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) ex 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) ) ) } ; coherence { t where t is Element of Funcs (NAT,REAL) : ex f, g being Element of Funcs (NAT,REAL) ex 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) ) ) } is FUNCTION_DOMAIN of NAT , REAL proofend; end; :: deftheorem defines to_power ASYMPT_0:def_20_:_ for F, G being FUNCTION_DOMAIN of NAT , REAL holds F to_power G = { t where t is Element of Funcs (NAT,REAL) : ex f, g being Element of Funcs (NAT,REAL) ex 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) ) ) } ;