:: ASYMPT_0 semantic presentation 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() proof defpred S1[ Element of NAT ] means verum; set S = { F4(i) where i is Element of NAT : ( F1() <= i & i <= F2() & S1[i] ) } ; F1() in NAT by ORDINAL1:def_12; then A2: F4(F1()) in { F4(i) where i is Element of NAT : ( F1() <= i & i <= F2() & S1[i] ) } by A1; set S1 = { F4(i) where i is Element of NAT : ( F1() <= i & i <= F2() ) } ; A3: now__::_thesis:_for_x_being_set_holds_ (_(_x_in__{__F4(i)_where_i_is_Element_of_NAT_:_(_F1()_<=_i_&_i_<=_F2()_&_S1[i]_)__}__implies_x_in__{__F4(i)_where_i_is_Element_of_NAT_:_(_F1()_<=_i_&_i_<=_F2()_)__}__)_&_(_x_in__{__F4(i)_where_i_is_Element_of_NAT_:_(_F1()_<=_i_&_i_<=_F2()_)__}__implies_x_in__{__F4(i)_where_i_is_Element_of_NAT_:_(_F1()_<=_i_&_i_<=_F2()_&_S1[i]_)__}__)_) let x be set ; ::_thesis: ( ( x in { F4(i) where i is Element of NAT : ( F1() <= i & i <= F2() & S1[i] ) } implies x in { F4(i) where i is Element of NAT : ( F1() <= i & i <= F2() ) } ) & ( x in { F4(i) where i is Element of NAT : ( F1() <= i & i <= F2() ) } implies x in { F4(i) where i is Element of NAT : ( F1() <= i & i <= F2() & S1[i] ) } ) ) hereby ::_thesis: ( x in { F4(i) where i is Element of NAT : ( F1() <= i & i <= F2() ) } implies x in { F4(i) where i is Element of NAT : ( F1() <= i & i <= F2() & S1[i] ) } ) assume x in { F4(i) where i is Element of NAT : ( F1() <= i & i <= F2() & S1[i] ) } ; ::_thesis: x in { F4(i) where i is Element of NAT : ( F1() <= i & i <= F2() ) } then ex i being Element of NAT st ( x = F4(i) & F1() <= i & i <= F2() & S1[i] ) ; hence x in { F4(i) where i is Element of NAT : ( F1() <= i & i <= F2() ) } ; ::_thesis: verum end; assume x in { F4(i) where i is Element of NAT : ( F1() <= i & i <= F2() ) } ; ::_thesis: x in { F4(i) where i is Element of NAT : ( F1() <= i & i <= F2() & S1[i] ) } then ex i being Element of NAT st ( x = F4(i) & F1() <= i & i <= F2() ) ; hence x in { F4(i) where i is Element of NAT : ( F1() <= i & i <= F2() & S1[i] ) } ; ::_thesis: verum end; A4: { F4(i) where i is Element of NAT : ( F1() <= i & i <= F2() & S1[i] ) } c= F3() proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { F4(i) where i is Element of NAT : ( F1() <= i & i <= F2() & S1[i] ) } or x in F3() ) assume x in { F4(i) where i is Element of NAT : ( F1() <= i & i <= F2() & S1[i] ) } ; ::_thesis: x in F3() then ex n1 being Element of NAT st ( x = F4(n1) & n1 >= F1() & n1 <= F2() ) ; hence x in F3() ; ::_thesis: verum end; { F4(i) where i is Element of NAT : ( F1() <= i & i <= F2() & S1[i] ) } is finite from FINSEQ_1:sch_6(); hence { F4(i) where i is Element of NAT : ( F1() <= i & i <= F2() ) } is non empty finite Subset of F3() by A3, A2, A4, TARSKI:1; ::_thesis: verum end; 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() proof set T = { F3(n) where n is Element of NAT : ( 0 <= n & n <= F1() ) } ; set S = { F3(n) where n is Element of NAT : n <= F1() } ; A1: now__::_thesis:_for_x_being_set_holds_ (_(_x_in__{__F3(n)_where_n_is_Element_of_NAT_:_n_<=_F1()__}__implies_x_in__{__F3(n)_where_n_is_Element_of_NAT_:_(_0_<=_n_&_n_<=_F1()_)__}__)_&_(_x_in__{__F3(n)_where_n_is_Element_of_NAT_:_(_0_<=_n_&_n_<=_F1()_)__}__implies_x_in__{__F3(n)_where_n_is_Element_of_NAT_:_n_<=_F1()__}__)_) let x be set ; ::_thesis: ( ( x in { F3(n) where n is Element of NAT : n <= F1() } implies x in { F3(n) where n is Element of NAT : ( 0 <= n & n <= F1() ) } ) & ( x in { F3(n) where n is Element of NAT : ( 0 <= n & n <= F1() ) } implies x in { F3(n) where n is Element of NAT : n <= F1() } ) ) hereby ::_thesis: ( x in { F3(n) where n is Element of NAT : ( 0 <= n & n <= F1() ) } implies x in { F3(n) where n is Element of NAT : n <= F1() } ) assume x in { F3(n) where n is Element of NAT : n <= F1() } ; ::_thesis: x in { F3(n) where n is Element of NAT : ( 0 <= n & n <= F1() ) } then ex n being Element of NAT st ( x = F3(n) & n <= F1() ) ; hence x in { F3(n) where n is Element of NAT : ( 0 <= n & n <= F1() ) } ; ::_thesis: verum end; assume x in { F3(n) where n is Element of NAT : ( 0 <= n & n <= F1() ) } ; ::_thesis: x in { F3(n) where n is Element of NAT : n <= F1() } then ex n being Element of NAT st ( x = F3(n) & 0 <= n & n <= F1() ) ; hence x in { F3(n) where n is Element of NAT : n <= F1() } ; ::_thesis: verum end; A2: 0 <= F1() ; { F3(n) where n is Element of NAT : ( 0 <= n & n <= F1() ) } is non empty finite Subset of F2() from ASYMPT_0:sch_1(A2); hence { F3(n) where n is Element of NAT : n <= F1() } is non empty finite Subset of F2() by A1, TARSKI:1; ::_thesis: verum end; 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 proof set S = { F3(n) where n is Element of NAT : n < F1() } ; consider m being Nat such that A2: F1() = m + 1 by A1, NAT_1:6; reconsider m = m as Element of NAT by ORDINAL1:def_12; set T = { F3(n) where n is Element of NAT : n <= m } ; A3: now__::_thesis:_for_x_being_set_holds_ (_(_x_in__{__F3(n)_where_n_is_Element_of_NAT_:_n_<_F1()__}__implies_x_in__{__F3(n)_where_n_is_Element_of_NAT_:_n_<=_m__}__)_&_(_x_in__{__F3(n)_where_n_is_Element_of_NAT_:_n_<=_m__}__implies_x_in__{__F3(n)_where_n_is_Element_of_NAT_:_n_<_F1()__}__)_) let x be set ; ::_thesis: ( ( x in { F3(n) where n is Element of NAT : n < F1() } implies x in { F3(n) where n is Element of NAT : n <= m } ) & ( x in { F3(n) where n is Element of NAT : n <= m } implies x in { F3(n) where n is Element of NAT : n < F1() } ) ) hereby ::_thesis: ( x in { F3(n) where n is Element of NAT : n <= m } implies x in { F3(n) where n is Element of NAT : n < F1() } ) assume x in { F3(n) where n is Element of NAT : n < F1() } ; ::_thesis: x in { F3(n) where n is Element of NAT : n <= m } then consider n being Element of NAT such that A4: x = F3(n) and A5: n < F1() ; n <= m by A2, A5, NAT_1:13; hence x in { F3(n) where n is Element of NAT : n <= m } by A4; ::_thesis: verum end; assume x in { F3(n) where n is Element of NAT : n <= m } ; ::_thesis: x in { F3(n) where n is Element of NAT : n < F1() } then consider n being Element of NAT such that A6: x = F3(n) and A7: n <= m ; n < m + 1 by A7, NAT_1:13; hence x in { F3(n) where n is Element of NAT : n < F1() } by A2, A6; ::_thesis: verum end; { F3(n) where n is Element of NAT : n <= m } is non empty finite Subset of F2() from ASYMPT_0:sch_2(); hence { F3(n) where n is Element of NAT : n < F1() } is non empty finite Subset of F2() by A3, TARSKI:1; ::_thesis: verum end; 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 proof take 1 ; ::_thesis: 1 is positive thus 1 is positive ; ::_thesis: verum end; clusterV11() real ext-real negative for Element of REAL ; existence ex b1 being Real st b1 is negative proof take - 1 ; ::_thesis: - 1 is negative thus - 1 is negative by XXREAL_0:def_7; ::_thesis: verum end; clusterV11() real ext-real logbase for Element of REAL ; existence ex b1 being Real st b1 is logbase proof take 2 ; ::_thesis: 2 is logbase thus 2 is logbase by Def1; ::_thesis: verum end; 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 proof take 1 ; ::_thesis: not 1 is logbase thus not 1 is logbase by Def1; ::_thesis: verum end; 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 ) proof reconsider f = NAT --> 1 as Function of NAT,REAL by FUNCOP_1:45; take f ; ::_thesis: ( f is eventually-nonnegative & f is eventually-nonzero & f is positive & f is eventually-positive & f is eventually-nondecreasing ) thus f is eventually-nonnegative ::_thesis: ( f is eventually-nonzero & f is positive & f is eventually-positive & f is eventually-nondecreasing ) proof take 0 ; :: according to ASYMPT_0:def_2 ::_thesis: for n being Element of NAT st n >= 0 holds f . n >= 0 let n be Element of NAT ; ::_thesis: ( n >= 0 implies f . n >= 0 ) assume n >= 0 ; ::_thesis: f . n >= 0 thus f . n >= 0 ; ::_thesis: verum end; thus f is eventually-nonzero ::_thesis: ( f is positive & f is eventually-positive & f is eventually-nondecreasing ) proof take 0 ; :: according to ASYMPT_0:def_5 ::_thesis: for n being Element of NAT st n >= 0 holds f . n <> 0 let n be Element of NAT ; ::_thesis: ( n >= 0 implies f . n <> 0 ) thus ( n >= 0 implies f . n <> 0 ) by FUNCOP_1:7; ::_thesis: verum end; thus f is positive ::_thesis: ( f is eventually-positive & f is eventually-nondecreasing ) proof let n be Element of NAT ; :: according to ASYMPT_0:def_3 ::_thesis: f . n > 0 thus f . n > 0 by FUNCOP_1:7; ::_thesis: verum end; thus f is eventually-positive ::_thesis: f is eventually-nondecreasing proof take 0 ; :: according to ASYMPT_0:def_4 ::_thesis: for n being Element of NAT st n >= 0 holds f . n > 0 let n be Element of NAT ; ::_thesis: ( n >= 0 implies f . n > 0 ) assume n >= 0 ; ::_thesis: f . n > 0 thus f . n > 0 by FUNCOP_1:7; ::_thesis: verum end; thus f is eventually-nondecreasing ::_thesis: verum proof take 0 ; :: according to ASYMPT_0:def_6 ::_thesis: for n being Element of NAT st n >= 0 holds f . n <= f . (n + 1) let n be Element of NAT ; ::_thesis: ( n >= 0 implies f . n <= f . (n + 1) ) assume n >= 0 ; ::_thesis: f . n <= f . (n + 1) f . n = 1 by FUNCOP_1:7; hence f . n <= f . (n + 1) by FUNCOP_1:7; ::_thesis: verum end; end; 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 proof let f be Real_Sequence; ::_thesis: ( f is positive implies f is eventually-positive ) assume A1: f is positive ; ::_thesis: f is eventually-positive take 0 ; :: according to ASYMPT_0:def_4 ::_thesis: for n being Element of NAT st n >= 0 holds f . n > 0 let n be Element of NAT ; ::_thesis: ( n >= 0 implies f . n > 0 ) assume n >= 0 ; ::_thesis: f . n > 0 thus f . n > 0 by A1, Def3; ::_thesis: verum end; 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 ) proof let f be Real_Sequence; ::_thesis: ( f is eventually-positive implies ( f is eventually-nonnegative & f is eventually-nonzero ) ) assume f is eventually-positive ; ::_thesis: ( f is eventually-nonnegative & f is eventually-nonzero ) then consider N being Element of NAT such that A2: for n being Element of NAT st n >= N holds f . n > 0 by Def4; thus f is eventually-nonnegative ::_thesis: f is eventually-nonzero proof take N ; :: according to ASYMPT_0:def_2 ::_thesis: for n being Element of NAT st n >= N holds f . n >= 0 let n be Element of NAT ; ::_thesis: ( n >= N implies f . n >= 0 ) assume n >= N ; ::_thesis: f . n >= 0 hence f . n >= 0 by A2; ::_thesis: verum end; thus f is eventually-nonzero ::_thesis: verum proof take N ; :: according to ASYMPT_0:def_5 ::_thesis: for n being Element of NAT st n >= N holds f . n <> 0 let n be Element of NAT ; ::_thesis: ( n >= N implies f . n <> 0 ) assume n >= N ; ::_thesis: f . n <> 0 hence f . n <> 0 by A2; ::_thesis: verum end; end; 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 proof let f be Real_Sequence; ::_thesis: ( f is eventually-nonnegative & f is eventually-nonzero implies f is eventually-positive ) assume that A3: f is eventually-nonnegative and A4: f is eventually-nonzero ; ::_thesis: f is eventually-positive consider N being Element of NAT such that A5: for n being Element of NAT st n >= N holds f . n >= 0 by A3, Def2; consider M being Element of NAT such that A6: for n being Element of NAT st n >= M holds f . n <> 0 by A4, Def5; take a = max (N,M); :: according to ASYMPT_0:def_4 ::_thesis: for n being Element of NAT st n >= a holds f . n > 0 let n be Element of NAT ; ::_thesis: ( n >= a implies f . n > 0 ) assume A7: n >= a ; ::_thesis: f . n > 0 a >= N by XXREAL_0:25; then A8: n >= N by A7, XXREAL_0:2; a >= M by XXREAL_0:25; then f . n <> 0 by A6, A7, XXREAL_0:2; hence f . n > 0 by A5, A8; ::_thesis: verum end; 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 proof consider M being Element of NAT such that A1: for n being Element of NAT st n >= M holds g . n >= 0 by Def2; consider N being Element of NAT such that A2: for n being Element of NAT st n >= N holds f . n >= 0 by Def2; set a = max (N,M); f + g is eventually-nonnegative proof take max (N,M) ; :: according to ASYMPT_0:def_2 ::_thesis: for n being Element of NAT st n >= max (N,M) holds (f + g) . n >= 0 let n be Element of NAT ; ::_thesis: ( n >= max (N,M) implies (f + g) . n >= 0 ) assume A3: n >= max (N,M) ; ::_thesis: (f + g) . n >= 0 max (N,M) >= M by XXREAL_0:25; then n >= M by A3, XXREAL_0:2; then A4: g . n >= 0 by A1; max (N,M) >= N by XXREAL_0:25; then n >= N by A3, XXREAL_0:2; then f . n >= 0 by A2; then 0 + 0 <= (f . n) + (g . n) by A4; hence (f + g) . n >= 0 by SEQ_1:7; ::_thesis: verum end; hence f + g is eventually-nonnegative Real_Sequence ; ::_thesis: verum end; 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 proof consider N being Element of NAT such that A1: for n being Element of NAT st n >= N holds f . n >= 0 by Def2; c (#) f is eventually-nonnegative proof take N ; :: according to ASYMPT_0:def_2 ::_thesis: for n being Element of NAT st n >= N holds (c (#) f) . n >= 0 let n be Element of NAT ; ::_thesis: ( n >= N implies (c (#) f) . n >= 0 ) assume n >= N ; ::_thesis: (c (#) f) . n >= 0 then f . n >= 0 by A1; then c * (f . n) >= c * 0 ; hence (c (#) f) . n >= 0 by SEQ_1:9; ::_thesis: verum end; hence c (#) f is eventually-nonnegative Real_Sequence ; ::_thesis: verum end; 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 proof consider N being Element of NAT such that A1: for n being Element of NAT st n >= N holds f . n >= 0 by Def2; c + f is eventually-nonnegative proof take N ; :: according to ASYMPT_0:def_2 ::_thesis: for n being Element of NAT st n >= N holds (c + f) . n >= 0 let n be Element of NAT ; ::_thesis: ( n >= N implies (c + f) . n >= 0 ) assume n >= N ; ::_thesis: (c + f) . n >= 0 then f . n >= 0 by A1; then c + (f . n) >= 0 + 0 ; hence (c + f) . n >= 0 by VALUED_1:2; ::_thesis: verum end; hence c + f is eventually-nonnegative Real_Sequence ; ::_thesis: verum end; 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 proof consider N being Element of NAT such that A1: for n being Element of NAT st n >= N holds f . n >= 0 by Def2; c + f is eventually-positive proof take N ; :: according to ASYMPT_0:def_4 ::_thesis: for n being Element of NAT st n >= N holds (c + f) . n > 0 let n be Element of NAT ; ::_thesis: ( n >= N implies (c + f) . n > 0 ) assume n >= N ; ::_thesis: (c + f) . n > 0 then f . n >= 0 by A1; then c + (f . n) > 0 + 0 ; hence (c + f) . n > 0 by VALUED_1:2; ::_thesis: verum end; hence c + f is eventually-positive Real_Sequence ; ::_thesis: verum end; 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)) proof deffunc H1( Element of NAT ) -> Element of REAL = max ((f . $1),(g . $1)); consider h being Function of NAT,REAL such that A1: for n being Element of NAT holds h . n = H1(n) from FUNCT_2:sch_4(); take h ; ::_thesis: for n being Element of NAT holds h . n = max ((f . n),(g . n)) let n be Element of NAT ; ::_thesis: h . n = max ((f . n),(g . n)) thus h . n = max ((f . n),(g . n)) by A1; ::_thesis: verum end; 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 proof let j, k be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds j . n = max ((f . n),(g . n)) ) & ( for n being Element of NAT holds k . n = max ((f . n),(g . n)) ) implies j = k ) assume that A2: for n being Element of NAT holds j . n = max ((f . n),(g . n)) and A3: for n being Element of NAT holds k . n = max ((f . n),(g . n)) ; ::_thesis: j = k now__::_thesis:_for_n_being_Element_of_NAT_holds_j_._n_=_k_._n let n be Element of NAT ; ::_thesis: j . n = k . n thus j . n = max ((f . n),(g . n)) by A2 .= k . n by A3 ; ::_thesis: verum end; hence j = k by FUNCT_2:63; ::_thesis: verum end; 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 proof consider N being Element of NAT such that A1: for n being Element of NAT st n >= N holds g . n >= 0 by Def2; take N ; :: according to ASYMPT_0:def_2 ::_thesis: for n being Element of NAT st n >= N holds (max (f,g)) . n >= 0 let n be Element of NAT ; ::_thesis: ( n >= N implies (max (f,g)) . n >= 0 ) assume n >= N ; ::_thesis: (max (f,g)) . n >= 0 then A2: g . n >= 0 by A1; max ((f . n),(g . n)) >= g . n by XXREAL_0:25; hence (max (f,g)) . n >= 0 by A2, Def7; ::_thesis: verum end; 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 proof consider N being Element of NAT such that A1: for n being Element of NAT st n >= N holds g . n > 0 by Def4; take N ; :: according to ASYMPT_0:def_4 ::_thesis: for n being Element of NAT st n >= N holds (max (f,g)) . n > 0 let n be Element of NAT ; ::_thesis: ( n >= N implies (max (f,g)) . n > 0 ) assume n >= N ; ::_thesis: (max (f,g)) . n > 0 then g . n > 0 by A1; then max ((f . n),(g . n)) > 0 by XXREAL_0:25; hence (max (f,g)) . n > 0 by Def7; ::_thesis: verum end; 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) proof let f, g be Real_Sequence; ::_thesis: for n being Element of NAT holds (f /" g) . n = (f . n) / (g . n) let n be Element of NAT ; ::_thesis: (f /" g) . n = (f . n) / (g . n) thus (f /" g) . n = (f . n) * ((g ") . n) by SEQ_1:8 .= (f . n) * ((g . n) ") by VALUED_1:10 .= (f . n) / (g . n) by XCMPLX_0:def_9 ; ::_thesis: verum end; 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 proof let f be Real_Sequence; ::_thesis: 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 let N be Element of NAT ; ::_thesis: ( ( for n being Element of NAT st n >= N holds f . n <= f . (n + 1) ) implies for n, m being Element of NAT st N <= n & n <= m holds f . n <= f . m ) assume A1: for n being Element of NAT st n >= N holds f . n <= f . (n + 1) ; ::_thesis: for n, m being Element of NAT st N <= n & n <= m holds f . n <= f . m let n, m be Element of NAT ; ::_thesis: ( N <= n & n <= m implies f . n <= f . m ) defpred S1[ Nat] means f . n <= f . $1; assume A2: n >= N ; ::_thesis: ( not n <= m or f . n <= f . m ) A3: for m being Nat st m >= n & S1[m] holds S1[m + 1] proof let m be Nat; ::_thesis: ( m >= n & S1[m] implies S1[m + 1] ) assume that A4: m >= n and A5: f . n <= f . m ; ::_thesis: S1[m + 1] ( m in NAT & m >= N ) by A2, A4, ORDINAL1:def_12, XXREAL_0:2; then f . m <= f . (m + 1) by A1; hence S1[m + 1] by A5, XXREAL_0:2; ::_thesis: verum end; A6: S1[n] ; for m being Nat st m >= n holds S1[m] from NAT_1:sch_8(A6, A3); hence ( not n <= m or f . n <= f . m ) ; ::_thesis: verum end; 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)) " ) proof let f, g be eventually-positive Real_Sequence; ::_thesis: ( f /" g is convergent & lim (f /" g) <> 0 implies ( g /" f is convergent & lim (g /" f) = (lim (f /" g)) " ) ) set s = f /" g; set als = abs (lim (f /" g)); set ls = lim (f /" g); assume that A1: f /" g is convergent and A2: lim (f /" g) <> 0 ; ::_thesis: ( g /" f is convergent & lim (g /" f) = (lim (f /" g)) " ) consider n1 being Element of NAT such that A3: for m being Element of NAT st n1 <= m holds (abs (lim (f /" g))) / 2 < abs ((f /" g) . m) by A1, A2, SEQ_2:16; A4: 0 < abs (lim (f /" g)) by A2, COMPLEX1:47; then 0 * 0 < (abs (lim (f /" g))) * (abs (lim (f /" g))) by XREAL_1:96; then A5: 0 < ((abs (lim (f /" g))) * (abs (lim (f /" g)))) / 2 by XREAL_1:215; consider N2 being Element of NAT such that A6: for n being Element of NAT st n >= N2 holds g . n > 0 by Def4; consider N1 being Element of NAT such that A7: for n being Element of NAT st n >= N1 holds f . n > 0 by Def4; A8: 0 <> abs (lim (f /" g)) by A2, COMPLEX1:47; A9: now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_ ex_n_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_n_<=_m_holds_ abs_(((g_/"_f)_._m)_-_((lim_(f_/"_g))_"))_<_p set N3 = N1 + N2; let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((g /" f) . m) - ((lim (f /" g)) ")) < p ) set N4 = (N1 + N2) + n1; A10: 0 <> (abs (lim (f /" g))) / 2 by A2, COMPLEX1:47; A11: (p * ((abs (lim (f /" g))) / 2)) / ((abs (lim (f /" g))) / 2) = (p * ((abs (lim (f /" g))) / 2)) * (((abs (lim (f /" g))) / 2) ") by XCMPLX_0:def_9 .= p * (((abs (lim (f /" g))) / 2) * (((abs (lim (f /" g))) / 2) ")) .= p * 1 by A10, XCMPLX_0:def_7 .= p ; assume A12: 0 < p ; ::_thesis: ex n being Element of NAT st for m being Element of NAT st n <= m holds abs (((g /" f) . m) - ((lim (f /" g)) ")) < p then 0 * 0 < p * (((abs (lim (f /" g))) * (abs (lim (f /" g)))) / 2) by A5, XREAL_1:96; then consider n2 being Element of NAT such that A13: for m being Element of NAT st n2 <= m holds abs (((f /" g) . m) - (lim (f /" g))) < p * (((abs (lim (f /" g))) * (abs (lim (f /" g)))) / 2) by A1, SEQ_2:def_7; take n = ((N1 + N2) + n1) + n2; ::_thesis: for m being Element of NAT st n <= m holds abs (((g /" f) . m) - ((lim (f /" g)) ")) < p let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((g /" f) . m) - ((lim (f /" g)) ")) < p ) assume A14: n <= m ; ::_thesis: abs (((g /" f) . m) - ((lim (f /" g)) ")) < p set asm = abs ((f /" g) . m); A15: (p * (((abs (lim (f /" g))) * (abs (lim (f /" g)))) / 2)) / ((abs ((f /" g) . m)) * (abs (lim (f /" g)))) = (p * ((2 ") * ((abs (lim (f /" g))) * (abs (lim (f /" g)))))) * (((abs ((f /" g) . m)) * (abs (lim (f /" g)))) ") by XCMPLX_0:def_9 .= (p * (2 ")) * (((abs (lim (f /" g))) * (abs (lim (f /" g)))) * (((abs (lim (f /" g))) * (abs ((f /" g) . m))) ")) .= (p * (2 ")) * (((abs (lim (f /" g))) * (abs (lim (f /" g)))) * (((abs (lim (f /" g))) ") * ((abs ((f /" g) . m)) "))) by XCMPLX_1:204 .= (p * (2 ")) * (((abs (lim (f /" g))) * ((abs (lim (f /" g))) * ((abs (lim (f /" g))) "))) * ((abs ((f /" g) . m)) ")) .= (p * (2 ")) * (((abs (lim (f /" g))) * 1) * ((abs ((f /" g) . m)) ")) by A8, XCMPLX_0:def_7 .= (p * ((abs (lim (f /" g))) / 2)) * ((abs ((f /" g) . m)) ") .= (p * ((abs (lim (f /" g))) / 2)) / (abs ((f /" g) . m)) by XCMPLX_0:def_9 ; n1 <= (N1 + N2) + n1 by NAT_1:12; then n1 <= n by NAT_1:12; then n1 <= m by A14, XXREAL_0:2; then A16: (abs (lim (f /" g))) / 2 < abs ((f /" g) . m) by A3; A17: 0 < (abs (lim (f /" g))) / 2 by A4, XREAL_1:215; then 0 * 0 < p * ((abs (lim (f /" g))) / 2) by A12, XREAL_1:96; then A18: (p * ((abs (lim (f /" g))) / 2)) / (abs ((f /" g) . m)) < (p * ((abs (lim (f /" g))) / 2)) / ((abs (lim (f /" g))) / 2) by A16, A17, XREAL_1:76; N2 <= N1 + N2 by NAT_1:12; then N2 <= (N1 + N2) + n1 by NAT_1:12; then N2 <= n by NAT_1:12; then N2 <= m by A14, XXREAL_0:2; then A19: g . m <> 0 by A6; N1 <= N1 + N2 by NAT_1:12; then N1 <= (N1 + N2) + n1 by NAT_1:12; then N1 <= n by NAT_1:12; then N1 <= m by A14, XXREAL_0:2; then f . m <> 0 by A7; then (f . m) / (g . m) <> 0 by A19, XCMPLX_1:50; then A20: (f /" g) . m <> 0 by Lm1; then ((f /" g) . m) * (lim (f /" g)) <> 0 by A2, XCMPLX_1:6; then 0 < abs (((f /" g) . m) * (lim (f /" g))) by COMPLEX1:47; then A21: 0 < (abs ((f /" g) . m)) * (abs (lim (f /" g))) by COMPLEX1:65; n2 <= n by NAT_1:12; then n2 <= m by A14, XXREAL_0:2; then abs (((f /" g) . m) - (lim (f /" g))) < p * (((abs (lim (f /" g))) * (abs (lim (f /" g)))) / 2) by A13; then A22: (abs (((f /" g) . m) - (lim (f /" g)))) / ((abs ((f /" g) . m)) * (abs (lim (f /" g)))) < (p * (((abs (lim (f /" g))) * (abs (lim (f /" g)))) / 2)) / ((abs ((f /" g) . m)) * (abs (lim (f /" g)))) by A21, XREAL_1:74; abs (((g /" f) . m) - ((lim (f /" g)) ")) = abs (((g . m) / (f . m)) - ((lim (f /" g)) ")) by Lm1 .= abs ((((f . m) / (g . m)) ") - ((lim (f /" g)) ")) by XCMPLX_1:213 .= abs ((((f /" g) . m) ") - ((lim (f /" g)) ")) by Lm1 .= (abs (((f /" g) . m) - (lim (f /" g)))) / ((abs ((f /" g) . m)) * (abs (lim (f /" g)))) by A2, A20, SEQ_2:2 ; hence abs (((g /" f) . m) - ((lim (f /" g)) ")) < p by A22, A15, A18, A11, XXREAL_0:2; ::_thesis: verum end; hence g /" f is convergent by SEQ_2:def_6; ::_thesis: lim (g /" f) = (lim (f /" g)) " hence lim (g /" f) = (lim (f /" g)) " by A9, SEQ_2:def_7; ::_thesis: verum end; theorem Th3: :: ASYMPT_0:3 for f being eventually-nonnegative Real_Sequence st f is convergent holds 0 <= lim f proof let f be eventually-nonnegative Real_Sequence; ::_thesis: ( f is convergent implies 0 <= lim f ) assume that A1: f is convergent and A2: not 0 <= lim f ; ::_thesis: contradiction 0 < - (lim f) by A2, XREAL_1:58; then consider N1 being Element of NAT such that A3: for m being Element of NAT st N1 <= m holds abs ((f . m) - (lim f)) < - (lim f) by A1, SEQ_2:def_7; consider N being Element of NAT such that A4: for n being Element of NAT st n >= N holds 0 <= f . n by Def2; set n1 = max (N,N1); A5: now__::_thesis:_not_f_._(max_(N,N1))_=_0 assume f . (max (N,N1)) = 0 ; ::_thesis: contradiction then abs ((f . (max (N,N1))) - (lim f)) = - (lim f) by A2, ABSVALUE:def_1; hence contradiction by A3, XXREAL_0:25; ::_thesis: verum end; abs ((f . (max (N,N1))) - (lim f)) <= - (lim f) by A3, XXREAL_0:25; then (f . (max (N,N1))) - (lim f) <= - (lim f) by ABSVALUE:5; then ((f . (max (N,N1))) - (lim f)) + (lim f) <= (- (lim f)) + (lim f) by XREAL_1:6; hence contradiction by A4, A5, XXREAL_0:25; ::_thesis: verum end; 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 proof let f, g be Real_Sequence; ::_thesis: ( f is convergent & g is convergent & g majorizes f implies lim f <= lim g ) assume that A1: ( f is convergent & g is convergent ) and A2: ex N being Element of NAT st for n being Element of NAT st n >= N holds f . n <= g . n ; :: according to ASYMPT_0:def_8 ::_thesis: lim f <= lim g consider N being Element of NAT such that A3: for n being Element of NAT st n >= N holds f . n <= g . n by A2; now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_N_holds_ 0_<=_(g_-_f)_._n let n be Element of NAT ; ::_thesis: ( n >= N implies 0 <= (g - f) . n ) assume n >= N ; ::_thesis: 0 <= (g - f) . n then f . n <= g . n by A3; then A4: (f . n) - (f . n) <= (g . n) - (f . n) by XREAL_1:9; (g - f) . n = (g . n) + ((- f) . n) by SEQ_1:7 .= (g . n) + (- (f . n)) by SEQ_1:10 .= (g . n) - (f . n) ; hence 0 <= (g - f) . n by A4; ::_thesis: verum end; then A5: g - f is eventually-nonnegative by Def2; A6: lim (g - f) = (lim g) - (lim f) by A1, SEQ_2:12; g - f is convergent by A1, SEQ_2:11; then 0 <= lim (g - f) by A5, Th3; then 0 + (lim f) <= ((lim g) - (lim f)) + (lim f) by A6, XREAL_1:6; hence lim f <= lim g ; ::_thesis: verum end; 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 ) proof let f be Real_Sequence; ::_thesis: for g being eventually-nonzero Real_Sequence st f /" g is divergent_to+infty holds ( g /" f is convergent & lim (g /" f) = 0 ) let g be eventually-nonzero Real_Sequence; ::_thesis: ( f /" g is divergent_to+infty implies ( g /" f is convergent & lim (g /" f) = 0 ) ) consider N1 being Element of NAT such that A1: for n being Element of NAT st n >= N1 holds g . n <> 0 by Def5; assume A2: f /" g is divergent_to+infty ; ::_thesis: ( g /" f is convergent & lim (g /" f) = 0 ) A3: now__::_thesis:_for_p_being_real_number_st_p_>_0_holds_ ex_a_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_a_holds_ abs_(((g_/"_f)_._n)_-_0)_<_p let p be real number ; ::_thesis: ( p > 0 implies ex a being Element of NAT st for n being Element of NAT st n >= a holds abs (((g /" f) . b5) - 0) < b3 ) assume A4: p > 0 ; ::_thesis: ex a being Element of NAT st for n being Element of NAT st n >= a holds abs (((g /" f) . b5) - 0) < b3 reconsider w = 1 / p as Real ; consider N being Element of NAT such that A5: for n being Element of NAT st n >= N holds w < (f /" g) . n by A2, LIMFUNC1:def_4; set a = max (N,N1); take a = max (N,N1); ::_thesis: for n being Element of NAT st n >= a holds abs (((g /" f) . b4) - 0) < b2 let n be Element of NAT ; ::_thesis: ( n >= a implies abs (((g /" f) . b3) - 0) < b1 ) assume A6: n >= a ; ::_thesis: abs (((g /" f) . b3) - 0) < b1 a >= N by XXREAL_0:25; then n >= N by A6, XXREAL_0:2; then 1 / p < (f /" g) . n by A5; then (1 / p) * p < p * ((f /" g) . n) by A4, XREAL_1:68; then 1 < p * ((f /" g) . n) by A4, XCMPLX_1:106; then A7: 1 < p * ((f . n) / (g . n)) by Lm1; then A8: 1 < p * ((f . n) * ((g . n) ")) by XCMPLX_0:def_9; A9: now__::_thesis:_(_(g_._n)_*_((f_._n)_")_>_(g_._n)_*_0_implies_((g_/"_f)_._n)_-_0_>=_0_) assume (g . n) * ((f . n) ") > (g . n) * 0 ; ::_thesis: ((g /" f) . n) - 0 >= 0 then (g . n) * ((f ") . n) > 0 by VALUED_1:10; hence ((g /" f) . n) - 0 >= 0 by SEQ_1:8; ::_thesis: verum end; a >= N1 by XXREAL_0:25; then A10: g . n <> 0 by A1, A6, XXREAL_0:2; A11: f . n <> 0 by A7; A12: now__::_thesis:_(_(g_._n)_*_((f_._n)_")_<_(p_*_(f_._n))_*_((f_._n)_")_implies_((g_/"_f)_._n)_-_0_<_p_) assume (g . n) * ((f . n) ") < (p * (f . n)) * ((f . n) ") ; ::_thesis: ((g /" f) . n) - 0 < p then (g . n) * ((f ") . n) < (p * (f . n)) * ((f . n) ") by VALUED_1:10; then (g (#) (f ")) . n < p * ((f . n) * ((f . n) ")) by SEQ_1:8; then (g (#) (f ")) . n < p * 1 by A11, XCMPLX_0:def_7; hence ((g /" f) . n) - 0 < p ; ::_thesis: verum end; percases ( g . n > 0 or g . n < 0 ) by A10; supposeA13: g . n > 0 ; ::_thesis: abs (((g /" f) . b3) - 0) < b1 then 1 * (g . n) < ((p * (f . n)) * ((g . n) ")) * (g . n) by A8, XREAL_1:68; then g . n < (p * (f . n)) * (((g . n) ") * (g . n)) ; then A14: g . n < (p * (f . n)) * 1 by A10, XCMPLX_0:def_7; f . n > 0 by A4, A7, A13; hence abs (((g /" f) . n) - 0) < p by A12, A9, A13, A14, ABSVALUE:def_1, XREAL_1:68; ::_thesis: verum end; supposeA15: g . n < 0 ; ::_thesis: abs (((g /" f) . b3) - 0) < b1 then 1 * (g . n) > ((p * (f . n)) * ((g . n) ")) * (g . n) by A8, XREAL_1:69; then g . n > (p * (f . n)) * (((g . n) ") * (g . n)) ; then A16: g . n > (p * (f . n)) * 1 by A10, XCMPLX_0:def_7; f . n < 0 by A4, A7, A15; hence abs (((g /" f) . n) - 0) < p by A12, A9, A15, A16, ABSVALUE:def_1, XREAL_1:69; ::_thesis: verum end; end; end; hence g /" f is convergent by SEQ_2:def_6; ::_thesis: lim (g /" f) = 0 hence lim (g /" f) = 0 by A3, SEQ_2:def_7; ::_thesis: verum end; 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 proof set IT = { 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 ) ) ) } ; A1: { 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 functional proof let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in { 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 ) ) ) } or x is set ) assume x in { 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 ) ) ) } ; ::_thesis: x is set then ex t being Element of Funcs (NAT,REAL) st ( x = t & 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 ) ) ) ) ; hence x is set ; ::_thesis: verum end; consider N being Element of NAT such that A2: for n being Element of NAT st n >= N holds f . n >= 0 by Def2; ( f is Element of Funcs (NAT,REAL) & ( for n being Element of NAT st n >= N holds ( f . n <= 1 * (f . n) & f . n >= 0 ) ) ) by A2, FUNCT_2:8; then f in { 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 ) ) ) } ; then reconsider IT1 = { 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 ) ) ) } as non empty functional set by A1; now__::_thesis:_for_x_being_Element_of_IT1_holds_x_is_Function_of_NAT,REAL let x be Element of IT1; ::_thesis: x is Function of NAT,REAL x in { 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 ) ) ) } ; then ex t being Element of Funcs (NAT,REAL) st ( x = t & 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 ) ) ) ) ; hence x is Function of NAT,REAL ; ::_thesis: verum end; hence { 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 by FUNCT_2:def_12; ::_thesis: verum end; 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 proof let t be set ; ::_thesis: for f being eventually-nonnegative Real_Sequence st t in Big_Oh f holds t is eventually-nonnegative Real_Sequence let f be eventually-nonnegative Real_Sequence; ::_thesis: ( t in Big_Oh f implies t is eventually-nonnegative Real_Sequence ) assume t in Big_Oh f ; ::_thesis: t is eventually-nonnegative Real_Sequence then consider s being Element of Funcs (NAT,REAL) such that A1: s = t and A2: ex c being Real ex N being Element of NAT st ( c > 0 & ( for n being Element of NAT st n >= N holds ( s . n <= c * (f . n) & s . n >= 0 ) ) ) ; reconsider t9 = t as Real_Sequence by A1; consider c being Real, N being Element of NAT such that c > 0 and A3: for n being Element of NAT st n >= N holds ( s . n <= c * (f . n) & s . n >= 0 ) by A2; now__::_thesis:_ex_N_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_N_holds_ t9_._n_>=_0 take N = N; ::_thesis: for n being Element of NAT st n >= N holds t9 . n >= 0 let n be Element of NAT ; ::_thesis: ( n >= N implies t9 . n >= 0 ) assume n >= N ; ::_thesis: t9 . n >= 0 hence t9 . n >= 0 by A1, A3; ::_thesis: verum end; hence t is eventually-nonnegative Real_Sequence by Def2; ::_thesis: verum end; 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) ) ) ) proof let f be positive Real_Sequence; ::_thesis: 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) ) ) ) let t be eventually-nonnegative Real_Sequence; ::_thesis: ( 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) ) ) ) hereby ::_thesis: ( ex c being Real st ( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) ) implies t in Big_Oh f ) assume t in Big_Oh f ; ::_thesis: ex c being Real st ( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) ) then consider s being Element of Funcs (NAT,REAL) such that A1: t = s and A2: ex c being Real ex N being Element of NAT st ( c > 0 & ( for n being Element of NAT st n >= N holds ( s . n <= c * (f . n) & s . n >= 0 ) ) ) ; consider c being Real, N being Element of NAT such that A3: c > 0 and A4: for n being Element of NAT st n >= N holds ( s . n <= c * (f . n) & s . n >= 0 ) by A2; percases ( N = 0 or N > 0 ) ; supposeA5: N = 0 ; ::_thesis: ex c being Real st ( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) ) take c = c; ::_thesis: ( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) ) thus c > 0 by A3; ::_thesis: for n being Element of NAT holds t . n <= c * (f . n) let n be Element of NAT ; ::_thesis: t . n <= c * (f . n) thus t . n <= c * (f . n) by A1, A4, A5; ::_thesis: verum end; supposeA6: N > 0 ; ::_thesis: ex c being Real st ( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) ) deffunc H1( Element of NAT ) -> Element of REAL = (t . $1) / (f . $1); reconsider B = { H1(n) where n is Element of NAT : n < N } as non empty finite Subset of REAL from ASYMPT_0:sch_3(A6); set b = max B; A7: for n being Element of NAT st n < N holds t . n <= (max B) * (f . n) proof let n be Element of NAT ; ::_thesis: ( n < N implies t . n <= (max B) * (f . n) ) A8: f . n > 0 by Def3; assume n < N ; ::_thesis: t . n <= (max B) * (f . n) then (t . n) / (f . n) in B ; then (t . n) / (f . n) <= max B by XXREAL_2:def_8; then ((t . n) / (f . n)) * (f . n) <= (max B) * (f . n) by A8, XREAL_1:64; hence t . n <= (max B) * (f . n) by A8, XCMPLX_1:87; ::_thesis: verum end; thus ex c being Real st ( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) ) ::_thesis: verum proof percases ( max B <= c or max B > c ) ; supposeA9: max B <= c ; ::_thesis: ex c being Real st ( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) ) take c ; ::_thesis: ( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) ) thus c > 0 by A3; ::_thesis: for n being Element of NAT holds t . n <= c * (f . n) let n be Element of NAT ; ::_thesis: t . n <= c * (f . n) thus t . n <= c * (f . n) ::_thesis: verum proof percases ( n < N or n >= N ) ; supposeA10: n < N ; ::_thesis: t . n <= c * (f . n) f . n > 0 by Def3; then A11: (max B) * (f . n) <= c * (f . n) by A9, XREAL_1:64; t . n <= (max B) * (f . n) by A7, A10; hence t . n <= c * (f . n) by A11, XXREAL_0:2; ::_thesis: verum end; suppose n >= N ; ::_thesis: t . n <= c * (f . n) hence t . n <= c * (f . n) by A1, A4; ::_thesis: verum end; end; end; end; supposeA12: max B > c ; ::_thesis: ex c being Real st ( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) ) reconsider b = max B as Element of REAL by XREAL_0:def_1; take b ; ::_thesis: ( b > 0 & ( for n being Element of NAT holds t . n <= b * (f . n) ) ) thus b > 0 by A3, A12; ::_thesis: for n being Element of NAT holds t . n <= b * (f . n) let n be Element of NAT ; ::_thesis: t . n <= b * (f . n) thus t . n <= b * (f . n) ::_thesis: verum proof percases ( n < N or n >= N ) ; suppose n < N ; ::_thesis: t . n <= b * (f . n) hence t . n <= b * (f . n) by A7; ::_thesis: verum end; supposeA13: n >= N ; ::_thesis: t . n <= b * (f . n) f . n > 0 by Def3; then A14: c * (f . n) <= b * (f . n) by A12, XREAL_1:64; t . n <= c * (f . n) by A1, A4, A13; hence t . n <= b * (f . n) by A14, XXREAL_0:2; ::_thesis: verum end; end; end; end; end; end; end; end; end; given c being Real such that A15: c > 0 and A16: for n being Element of NAT holds t . n <= c * (f . n) ; ::_thesis: t in Big_Oh f consider N being Element of NAT such that A17: for n being Element of NAT st n >= N holds t . n >= 0 by Def2; ( t is Element of Funcs (NAT,REAL) & ( for n being Element of NAT st n >= N holds ( t . n <= c * (f . n) & t . n >= 0 ) ) ) by A16, A17, FUNCT_2:8; hence t in Big_Oh f by A15; ::_thesis: verum end; 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) ) ) proof let f be eventually-positive Real_Sequence; ::_thesis: 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) ) ) let t be eventually-nonnegative Real_Sequence; ::_thesis: 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) ) ) let N be Element of NAT ; ::_thesis: ( t in Big_Oh f & ( for n being Element of NAT st n >= N holds f . n > 0 ) implies ex c being Real st ( c > 0 & ( for n being Element of NAT st n >= N holds t . n <= c * (f . n) ) ) ) assume that A1: t in Big_Oh f and A2: for n being Element of NAT st n >= N holds f . n > 0 ; ::_thesis: ex c being Real st ( c > 0 & ( for n being Element of NAT st n >= N holds t . n <= c * (f . n) ) ) deffunc H1( Element of NAT ) -> Element of REAL = t . $1; deffunc H2( Element of NAT ) -> Element of REAL = f . $1; ex s being Element of Funcs (NAT,REAL) st ( t = s & ex c being Real ex N being Element of NAT st ( c > 0 & ( for n being Element of NAT st n >= N holds ( s . n <= c * (f . n) & s . n >= 0 ) ) ) ) by A1; then consider c2 being Real, M being Element of NAT such that A3: c2 > 0 and A4: for n being Element of NAT st n >= M holds ( t . n <= c2 * (f . n) & t . n >= 0 ) ; set fset = { H2(n) where n is Element of NAT : ( N <= n & n <= max (M,N) ) } ; A5: N <= max (M,N) by XXREAL_0:25; { H2(n) where n is Element of NAT : ( N <= n & n <= max (M,N) ) } is non empty finite Subset of REAL from ASYMPT_0:sch_1(A5); then reconsider fset = { H2(n) where n is Element of NAT : ( N <= n & n <= max (M,N) ) } as non empty finite Subset of REAL ; set F = min fset; A6: M <= max (M,N) by XXREAL_0:25; set tset = { H1(n) where n is Element of NAT : ( N <= n & n <= max (M,N) ) } ; { H1(n) where n is Element of NAT : ( N <= n & n <= max (M,N) ) } is non empty finite Subset of REAL from ASYMPT_0:sch_1(A5); then reconsider tset = { H1(n) where n is Element of NAT : ( N <= n & n <= max (M,N) ) } as non empty finite Subset of REAL ; set T = max tset; set c1 = (max tset) / (min fset); reconsider c = max (((max tset) / (min fset)),c2) as Element of REAL by XREAL_0:def_1; take c ; ::_thesis: ( c > 0 & ( for n being Element of NAT st n >= N holds t . n <= c * (f . n) ) ) thus c > 0 by A3, XXREAL_0:25; ::_thesis: for n being Element of NAT st n >= N holds t . n <= c * (f . n) let n be Element of NAT ; ::_thesis: ( n >= N implies t . n <= c * (f . n) ) assume A7: n >= N ; ::_thesis: t . n <= c * (f . n) then A8: f . n > 0 by A2; A9: f . n <> 0 by A2, A7; min fset in fset by XXREAL_2:def_7; then A10: ex n1 being Element of NAT st ( f . n1 = min fset & n1 >= N & n1 <= max (M,N) ) ; then A11: min fset > 0 by A2; A12: min fset <> 0 by A2, A10; percases ( N >= M or N <= M ) ; suppose N >= M ; ::_thesis: t . n <= c * (f . n) then n >= M by A7, XXREAL_0:2; then A13: t . n <= c2 * (f . n) by A4; c2 * (f . n) <= c * (f . n) by A8, XREAL_1:64, XXREAL_0:25; hence t . n <= c * (f . n) by A13, XXREAL_0:2; ::_thesis: verum end; supposeA14: N <= M ; ::_thesis: t . n <= c * (f . n) thus t . n <= c * (f . n) ::_thesis: verum proof percases ( n <= M or n >= M ) ; suppose n <= M ; ::_thesis: t . n <= c * (f . n) then A15: n <= max (M,N) by A6, XXREAL_0:2; then t . n in tset by A7; then A16: t . n <= max tset by XXREAL_2:def_8; f . n in fset by A7, A15; then A17: f . n >= min fset by XXREAL_2:def_7; t . M in tset by A6, A14; then A18: t . M <= max tset by XXREAL_2:def_8; t . M >= 0 by A4; then A19: ((max tset) / (min fset)) * (f . n) >= ((max tset) / (min fset)) * (min fset) by A11, A18, A17, XREAL_1:64; now__::_thesis:_not_(t_._n)_/_(f_._n)_>_(max_tset)_/_(min_fset) assume (t . n) / (f . n) > (max tset) / (min fset) ; ::_thesis: contradiction then ((t . n) / (f . n)) * (f . n) > ((max tset) / (min fset)) * (f . n) by A8, XREAL_1:68; then t . n > ((max tset) / (min fset)) * (f . n) by A9, XCMPLX_1:87; then max tset > ((max tset) / (min fset)) * (f . n) by A16, XXREAL_0:2; hence contradiction by A12, A19, XCMPLX_1:87; ::_thesis: verum end; then ((t . n) / (f . n)) * (f . n) <= ((max tset) / (min fset)) * (f . n) by A8, XREAL_1:64; then A20: t . n <= ((max tset) / (min fset)) * (f . n) by A9, XCMPLX_1:87; ((max tset) / (min fset)) * (f . n) <= c * (f . n) by A8, XREAL_1:64, XXREAL_0:25; hence t . n <= c * (f . n) by A20, XXREAL_0:2; ::_thesis: verum end; supposeA21: n >= M ; ::_thesis: t . n <= c * (f . n) A22: c2 * (f . n) <= c * (f . n) by A8, XREAL_1:64, XXREAL_0:25; t . n <= c2 * (f . n) by A4, A21; hence t . n <= c * (f . n) by A22, XXREAL_0:2; ::_thesis: verum end; end; end; end; end; end; theorem :: ASYMPT_0:9 for f, g being eventually-nonnegative Real_Sequence holds Big_Oh (f + g) = Big_Oh (max (f,g)) proof let f, g be eventually-nonnegative Real_Sequence; ::_thesis: Big_Oh (f + g) = Big_Oh (max (f,g)) now__::_thesis:_for_x_being_set_holds_ (_(_x_in_Big_Oh_(f_+_g)_implies_x_in_Big_Oh_(max_(f,g))_)_&_(_x_in_Big_Oh_(max_(f,g))_implies_x_in_Big_Oh_(f_+_g)_)_) let x be set ; ::_thesis: ( ( x in Big_Oh (f + g) implies x in Big_Oh (max (f,g)) ) & ( x in Big_Oh (max (f,g)) implies x in Big_Oh (f + g) ) ) hereby ::_thesis: ( x in Big_Oh (max (f,g)) implies x in Big_Oh (f + g) ) assume x in Big_Oh (f + g) ; ::_thesis: x in Big_Oh (max (f,g)) then consider t being Element of Funcs (NAT,REAL) such that A1: t = x and A2: 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 + g) . n) & t . n >= 0 ) ) ) ; consider c being Real, N being Element of NAT such that A3: c > 0 and A4: for n being Element of NAT st n >= N holds ( t . n <= c * ((f + g) . n) & t . n >= 0 ) by A2; A5: now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_N_holds_ (_t_._n_<=_(2_*_c)_*_((max_(f,g))_._n)_&_t_._n_>=_0_) let n be Element of NAT ; ::_thesis: ( n >= N implies ( t . n <= (2 * c) * ((max (f,g)) . n) & t . n >= 0 ) ) A6: ( f . n <= max ((f . n),(g . n)) & g . n <= max ((f . n),(g . n)) ) by XXREAL_0:25; A7: (1 * ((max (f,g)) . n)) + (1 * ((max (f,g)) . n)) = (1 + 1) * ((max (f,g)) . n) ; ( (f + g) . n = (f . n) + (g . n) & (max (f,g)) . n = max ((f . n),(g . n)) ) by Def7, SEQ_1:7; then (f + g) . n <= 2 * ((max (f,g)) . n) by A6, A7, XREAL_1:7; then A8: c * ((f + g) . n) <= c * (2 * ((max (f,g)) . n)) by A3, XREAL_1:64; assume A9: n >= N ; ::_thesis: ( t . n <= (2 * c) * ((max (f,g)) . n) & t . n >= 0 ) then t . n <= c * ((f + g) . n) by A4; hence t . n <= (2 * c) * ((max (f,g)) . n) by A8, XXREAL_0:2; ::_thesis: t . n >= 0 thus t . n >= 0 by A4, A9; ::_thesis: verum end; 2 * c > 2 * 0 by A3, XREAL_1:68; hence x in Big_Oh (max (f,g)) by A1, A5; ::_thesis: verum end; assume x in Big_Oh (max (f,g)) ; ::_thesis: x in Big_Oh (f + g) then consider t being Element of Funcs (NAT,REAL) such that A10: t = x and A11: 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 * ((max (f,g)) . n) & t . n >= 0 ) ) ) ; consider c being Real, N1 being Element of NAT such that A12: c > 0 and A13: for n being Element of NAT st n >= N1 holds ( t . n <= c * ((max (f,g)) . n) & t . n >= 0 ) by A11; consider M1 being Element of NAT such that A14: for n being Element of NAT st n >= M1 holds f . n >= 0 by Def2; consider M2 being Element of NAT such that A15: for n being Element of NAT st n >= M2 holds g . n >= 0 by Def2; set N = max (N1,(max (M1,M2))); A16: max (M1,M2) <= max (N1,(max (M1,M2))) by XXREAL_0:25; M2 <= max (M1,M2) by XXREAL_0:25; then A17: M2 <= max (N1,(max (M1,M2))) by A16, XXREAL_0:2; A18: N1 <= max (N1,(max (M1,M2))) by XXREAL_0:25; M1 <= max (M1,M2) by XXREAL_0:25; then A19: M1 <= max (N1,(max (M1,M2))) by A16, XXREAL_0:2; now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_max_(N1,(max_(M1,M2)))_holds_ (_t_._n_<=_c_*_((f_+_g)_._n)_&_t_._n_>=_0_) let n be Element of NAT ; ::_thesis: ( n >= max (N1,(max (M1,M2))) implies ( t . n <= c * ((f + g) . n) & t . n >= 0 ) ) A20: ( max ((f . n),(g . n)) = f . n or max ((f . n),(g . n)) = g . n ) by XXREAL_0:16; assume A21: n >= max (N1,(max (M1,M2))) ; ::_thesis: ( t . n <= c * ((f + g) . n) & t . n >= 0 ) then n >= M1 by A19, XXREAL_0:2; then f . n >= 0 by A14; then A22: (f . n) + (g . n) >= 0 + (g . n) by XREAL_1:7; n >= M2 by A17, A21, XXREAL_0:2; then g . n >= 0 by A15; then A23: (f . n) + (g . n) >= (f . n) + 0 by XREAL_1:7; ( (max (f,g)) . n = max ((f . n),(g . n)) & (f + g) . n = (f . n) + (g . n) ) by Def7, SEQ_1:7; then A24: c * ((max (f,g)) . n) <= c * ((f + g) . n) by A12, A23, A22, A20, XREAL_1:64; A25: n >= N1 by A18, A21, XXREAL_0:2; then t . n <= c * ((max (f,g)) . n) by A13; hence t . n <= c * ((f + g) . n) by A24, XXREAL_0:2; ::_thesis: t . n >= 0 thus t . n >= 0 by A13, A25; ::_thesis: verum end; hence x in Big_Oh (f + g) by A10, A12; ::_thesis: verum end; hence Big_Oh (f + g) = Big_Oh (max (f,g)) by TARSKI:1; ::_thesis: verum end; theorem Th10: :: ASYMPT_0:10 for f being eventually-nonnegative Real_Sequence holds f in Big_Oh f proof let f be eventually-nonnegative Real_Sequence; ::_thesis: f in Big_Oh f consider N being Element of NAT such that A1: for n being Element of NAT st n >= N holds f . n >= 0 by Def2; ( f is Element of Funcs (NAT,REAL) & ( for n being Element of NAT st n >= N holds ( f . n <= 1 * (f . n) & f . n >= 0 ) ) ) by A1, FUNCT_2:8; hence f in Big_Oh f ; ::_thesis: verum end; 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 proof let f, g be eventually-nonnegative Real_Sequence; ::_thesis: ( f in Big_Oh g implies Big_Oh f c= Big_Oh g ) assume f in Big_Oh g ; ::_thesis: Big_Oh f c= Big_Oh g then consider t being Element of Funcs (NAT,REAL) such that A1: t = f and A2: 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 * (g . n) & t . n >= 0 ) ) ) ; consider ct being Real, Nt being Element of NAT such that ct > 0 and A3: for n being Element of NAT st n >= Nt holds ( t . n <= ct * (g . n) & t . n >= 0 ) by A2; consider Ng being Element of NAT such that A4: for n being Element of NAT st n >= Ng holds g . n >= 0 by Def2; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Big_Oh f or x in Big_Oh g ) assume x in Big_Oh f ; ::_thesis: x in Big_Oh g then consider s being Element of Funcs (NAT,REAL) such that A5: s = x and A6: ex c being Real ex N being Element of NAT st ( c > 0 & ( for n being Element of NAT st n >= N holds ( s . n <= c * (f . n) & s . n >= 0 ) ) ) ; consider cs being Real, Ns being Element of NAT such that A7: cs > 0 and A8: for n being Element of NAT st n >= Ns holds ( s . n <= cs * (f . n) & s . n >= 0 ) by A6; now__::_thesis:_ex_c_being_Element_of_REAL_st_ (_c_>_0_&_ex_N_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_N_holds_ (_s_._n_<=_c_*_(g_._n)_&_s_._n_>=_0_)_) take c = max ((cs * ct),(max (cs,ct))); ::_thesis: ( c > 0 & ex N being Element of NAT st for n being Element of NAT st n >= N holds ( s . n <= c * (g . n) & s . n >= 0 ) ) c >= max (cs,ct) by XXREAL_0:25; hence c > 0 by A7, XXREAL_0:25; ::_thesis: ex N being Element of NAT st for n being Element of NAT st n >= N holds ( s . n <= c * (g . n) & s . n >= 0 ) take N = max ((max (Ns,Nt)),Ng); ::_thesis: for n being Element of NAT st n >= N holds ( s . n <= c * (g . n) & s . n >= 0 ) let n be Element of NAT ; ::_thesis: ( n >= N implies ( s . n <= c * (g . n) & s . n >= 0 ) ) assume A9: n >= N ; ::_thesis: ( s . n <= c * (g . n) & s . n >= 0 ) A10: N >= max (Ns,Nt) by XXREAL_0:25; max (Ns,Nt) >= Nt by XXREAL_0:25; then N >= Nt by A10, XXREAL_0:2; then n >= Nt by A9, XXREAL_0:2; then t . n <= ct * (g . n) by A3; then A11: cs * (t . n) <= cs * (ct * (g . n)) by A7, XREAL_1:64; N >= Ng by XXREAL_0:25; then n >= Ng by A9, XXREAL_0:2; then g . n >= 0 by A4; then (cs * ct) * (g . n) <= c * (g . n) by XREAL_1:64, XXREAL_0:25; then A12: cs * (t . n) <= c * (g . n) by A11, XXREAL_0:2; max (Ns,Nt) >= Ns by XXREAL_0:25; then N >= Ns by A10, XXREAL_0:2; then A13: n >= Ns by A9, XXREAL_0:2; then s . n <= cs * (f . n) by A8; hence s . n <= c * (g . n) by A1, A12, XXREAL_0:2; ::_thesis: s . n >= 0 thus s . n >= 0 by A8, A13; ::_thesis: verum end; hence x in Big_Oh g by A5; ::_thesis: verum end; 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 proof let f, g, h be eventually-nonnegative Real_Sequence; ::_thesis: ( f in Big_Oh g & g in Big_Oh h implies f in Big_Oh h ) assume that A1: f in Big_Oh g and A2: g in Big_Oh h ; ::_thesis: f in Big_Oh h Big_Oh g c= Big_Oh h by A2, Th11; hence f in Big_Oh h by A1; ::_thesis: verum end; 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 ) proof let f, g be eventually-nonnegative Real_Sequence; ::_thesis: ( ( f in Big_Oh g & g in Big_Oh f ) iff Big_Oh f = Big_Oh g ) hereby ::_thesis: ( Big_Oh f = Big_Oh g implies ( f in Big_Oh g & g in Big_Oh f ) ) assume ( f in Big_Oh g & g in Big_Oh f ) ; ::_thesis: Big_Oh f = Big_Oh g then ( Big_Oh f c= Big_Oh g & Big_Oh g c= Big_Oh f ) by Th11; hence Big_Oh f = Big_Oh g by XBOOLE_0:def_10; ::_thesis: verum end; assume Big_Oh f = Big_Oh g ; ::_thesis: ( f in Big_Oh g & g in Big_Oh f ) hence ( f in Big_Oh g & g in Big_Oh f ) by Th10; ::_thesis: verum end; theorem :: ASYMPT_0:13 for f being eventually-nonnegative Real_Sequence for c being positive Real holds Big_Oh f = Big_Oh (c (#) f) proof let f be eventually-nonnegative Real_Sequence; ::_thesis: for c being positive Real holds Big_Oh f = Big_Oh (c (#) f) let c be positive Real; ::_thesis: Big_Oh f = Big_Oh (c (#) f) now__::_thesis:_for_x_being_set_holds_ (_(_x_in_Big_Oh_f_implies_x_in_Big_Oh_(c_(#)_f)_)_&_(_x_in_Big_Oh_(c_(#)_f)_implies_x_in_Big_Oh_f_)_) let x be set ; ::_thesis: ( ( x in Big_Oh f implies x in Big_Oh (c (#) f) ) & ( x in Big_Oh (c (#) f) implies x in Big_Oh f ) ) hereby ::_thesis: ( x in Big_Oh (c (#) f) implies x in Big_Oh f ) assume x in Big_Oh f ; ::_thesis: x in Big_Oh (c (#) f) then consider t being Element of Funcs (NAT,REAL) such that A1: x = t and A2: 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 ) ) ) ; consider c1 being Real, N being Element of NAT such that A3: c1 > 0 and A4: for n being Element of NAT st n >= N holds ( t . n <= c1 * (f . n) & t . n >= 0 ) by A2; A5: now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_N_holds_ (_t_._n_<=_(c1_*_(c_"))_*_((c_(#)_f)_._n)_&_t_._n_>=_0_) let n be Element of NAT ; ::_thesis: ( n >= N implies ( t . n <= (c1 * (c ")) * ((c (#) f) . n) & t . n >= 0 ) ) assume A6: n >= N ; ::_thesis: ( t . n <= (c1 * (c ")) * ((c (#) f) . n) & t . n >= 0 ) then t . n <= (c1 * 1) * (f . n) by A4; then t . n <= (c1 * ((c ") * c)) * (f . n) by XCMPLX_0:def_7; then t . n <= (c1 * (c ")) * (c * (f . n)) ; hence ( t . n <= (c1 * (c ")) * ((c (#) f) . n) & t . n >= 0 ) by A4, A6, SEQ_1:9; ::_thesis: verum end; c1 * (c ") > 0 * (c ") by A3, XREAL_1:68; hence x in Big_Oh (c (#) f) by A1, A5; ::_thesis: verum end; assume x in Big_Oh (c (#) f) ; ::_thesis: x in Big_Oh f then consider t being Element of Funcs (NAT,REAL) such that A7: x = t and A8: ex c1 being Real ex N being Element of NAT st ( c1 > 0 & ( for n being Element of NAT st n >= N holds ( t . n <= c1 * ((c (#) f) . n) & t . n >= 0 ) ) ) ; consider c1 being Real, N being Element of NAT such that A9: c1 > 0 and A10: for n being Element of NAT st n >= N holds ( t . n <= c1 * ((c (#) f) . n) & t . n >= 0 ) by A8; A11: now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_N_holds_ (_t_._n_<=_(c1_*_c)_*_(f_._n)_&_t_._n_>=_0_) let n be Element of NAT ; ::_thesis: ( n >= N implies ( t . n <= (c1 * c) * (f . n) & t . n >= 0 ) ) assume A12: n >= N ; ::_thesis: ( t . n <= (c1 * c) * (f . n) & t . n >= 0 ) then t . n <= c1 * ((c (#) f) . n) by A10; then t . n <= c1 * (c * (f . n)) by SEQ_1:9; hence ( t . n <= (c1 * c) * (f . n) & t . n >= 0 ) by A10, A12; ::_thesis: verum end; c1 * c > 0 * c by A9, XREAL_1:68; hence x in Big_Oh f by A7, A11; ::_thesis: verum end; hence Big_Oh f = Big_Oh (c (#) f) by TARSKI:1; ::_thesis: verum end; 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) proof let c be non negative Real; ::_thesis: for x, f being eventually-nonnegative Real_Sequence st x in Big_Oh f holds x in Big_Oh (c + f) let x, f be eventually-nonnegative Real_Sequence; ::_thesis: ( x in Big_Oh f implies x in Big_Oh (c + f) ) assume x in Big_Oh f ; ::_thesis: x in Big_Oh (c + f) then consider t being Element of Funcs (NAT,REAL) such that A1: x = t and A2: ex c1 being Real ex N being Element of NAT st ( c1 > 0 & ( for n being Element of NAT st n >= N holds ( t . n <= c1 * (f . n) & t . n >= 0 ) ) ) ; consider c1 being Real, N being Element of NAT such that A3: c1 > 0 and A4: for n being Element of NAT st n >= N holds ( t . n <= c1 * (f . n) & t . n >= 0 ) by A2; now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_N_holds_ (_t_._n_<=_c1_*_((c_+_f)_._n)_&_t_._n_>=_0_) let n be Element of NAT ; ::_thesis: ( n >= N implies ( t . n <= c1 * ((c + f) . n) & t . n >= 0 ) ) (f . n) + 0 <= (f . n) + c by XREAL_1:7; then f . n <= (c + f) . n by VALUED_1:2; then A5: c1 * (f . n) <= c1 * ((c + f) . n) by A3, XREAL_1:64; assume A6: n >= N ; ::_thesis: ( t . n <= c1 * ((c + f) . n) & t . n >= 0 ) then t . n <= c1 * (f . n) by A4; hence ( t . n <= c1 * ((c + f) . n) & t . n >= 0 ) by A4, A6, A5, XXREAL_0:2; ::_thesis: verum end; hence x in Big_Oh (c + f) by A1, A3; ::_thesis: verum end; Lm3: for f, g being eventually-positive Real_Sequence st f /" g is convergent & lim (f /" g) > 0 holds f in Big_Oh g proof let f, g be eventually-positive Real_Sequence; ::_thesis: ( f /" g is convergent & lim (f /" g) > 0 implies f in Big_Oh g ) assume that A1: f /" g is convergent and A2: lim (f /" g) > 0 ; ::_thesis: f in Big_Oh g set l = lim (f /" g); set delta = lim (f /" g); set c = 2 * (lim (f /" g)); consider N being Element of NAT such that A3: for n being Element of NAT st N <= n holds abs (((f /" g) . n) - (lim (f /" g))) < lim (f /" g) by A1, A2, SEQ_2:def_7; consider N2 being Element of NAT such that A4: for n being Element of NAT st n >= N2 holds g . n > 0 by Def4; consider N1 being Element of NAT such that A5: for n being Element of NAT st n >= N1 holds f . n >= 0 by Def2; set b = max (N,N1); set a = max ((max (N,N1)),N2); A6: now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_max_((max_(N,N1)),N2)_holds_ (_f_._n_<=_(2_*_(lim_(f_/"_g)))_*_(g_._n)_&_f_._n_>=_0_) let n be Element of NAT ; ::_thesis: ( n >= max ((max (N,N1)),N2) implies ( f . n <= (2 * (lim (f /" g))) * (g . n) & f . n >= 0 ) ) assume A7: n >= max ((max (N,N1)),N2) ; ::_thesis: ( f . n <= (2 * (lim (f /" g))) * (g . n) & f . n >= 0 ) max ((max (N,N1)),N2) >= N2 by XXREAL_0:25; then n >= N2 by A7, XXREAL_0:2; then A8: g . n > 0 by A4; max ((max (N,N1)),N2) >= max (N,N1) by XXREAL_0:25; then A9: n >= max (N,N1) by A7, XXREAL_0:2; max (N,N1) >= N by XXREAL_0:25; then n >= N by A9, XXREAL_0:2; then abs (((f /" g) . n) - (lim (f /" g))) < lim (f /" g) by A3; then ((f /" g) . n) - (lim (f /" g)) <= lim (f /" g) by ABSVALUE:5; then (f /" g) . n <= (1 * (lim (f /" g))) + (1 * (lim (f /" g))) by XREAL_1:20; then (f . n) * ((g ") . n) <= 2 * (lim (f /" g)) by SEQ_1:8; then (f . n) * ((g . n) ") <= 2 * (lim (f /" g)) by VALUED_1:10; then ((f . n) * ((g . n) ")) * (g . n) <= (2 * (lim (f /" g))) * (g . n) by A8, XREAL_1:64; then (f . n) * (((g . n) ") * (g . n)) <= (2 * (lim (f /" g))) * (g . n) ; then (f . n) * 1 <= (2 * (lim (f /" g))) * (g . n) by A8, XCMPLX_0:def_7; hence f . n <= (2 * (lim (f /" g))) * (g . n) ; ::_thesis: f . n >= 0 max (N,N1) >= N1 by XXREAL_0:25; then n >= N1 by A9, XXREAL_0:2; hence f . n >= 0 by A5; ::_thesis: verum end; A10: f is Element of Funcs (NAT,REAL) by FUNCT_2:8; 2 * (lim (f /" g)) > 2 * 0 by A2, XREAL_1:68; hence f in Big_Oh g by A10, A6; ::_thesis: verum end; 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 proof let f, g be eventually-positive Real_Sequence; ::_thesis: ( f /" g is convergent & lim (f /" g) > 0 implies Big_Oh f = Big_Oh g ) assume A1: ( f /" g is convergent & lim (f /" g) > 0 ) ; ::_thesis: Big_Oh f = Big_Oh g then lim (g /" f) = (lim (f /" g)) " by Th2; then A2: g in Big_Oh f by A1, Lm3, Th2; f in Big_Oh g by A1, Lm3; hence Big_Oh f = Big_Oh g by A2, Lm2; ::_thesis: verum end; 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 ) proof let f, g be eventually-positive Real_Sequence; ::_thesis: ( f /" g is convergent & lim (f /" g) = 0 implies ( f in Big_Oh g & not g in Big_Oh f ) ) assume A1: ( f /" g is convergent & lim (f /" g) = 0 ) ; ::_thesis: ( f in Big_Oh g & not g in Big_Oh f ) then consider N being Element of NAT such that A2: for n being Element of NAT st N <= n holds abs (((f /" g) . n) - 0) < 1 by SEQ_2:def_7; consider N1 being Element of NAT such that A3: for n being Element of NAT st n >= N1 holds f . n >= 0 by Def2; consider N2 being Element of NAT such that A4: for n being Element of NAT st n >= N2 holds g . n > 0 by Def4; A5: not g in Big_Oh f proof assume g in Big_Oh f ; ::_thesis: contradiction then consider t being Element of Funcs (NAT,REAL) such that A6: t = g and A7: 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 ) ) ) ; consider c being Real, N being Element of NAT such that A8: c > 0 and A9: for n being Element of NAT st n >= N holds ( t . n <= c * (f . n) & t . n >= 0 ) by A7; reconsider q = NAT --> (1 / c) as Real_Sequence ; set a = max (N,N2); A10: max (N,N2) >= N2 by XXREAL_0:25; A11: max (N,N2) >= N by XXREAL_0:25; now__::_thesis:_ex_a_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_a_holds_ q_._n_<=_(f_/"_g)_._n take a = max (N,N2); ::_thesis: for n being Element of NAT st n >= a holds q . n <= (f /" g) . n let n be Element of NAT ; ::_thesis: ( n >= a implies q . n <= (f /" g) . n ) assume A12: n >= a ; ::_thesis: q . n <= (f /" g) . n then n >= N by A11, XXREAL_0:2; then ( g . n <= c * (f . n) & g . n >= 0 ) by A6, A9; then A13: (g . n) * ((g . n) ") <= (c * (f . n)) * ((g . n) ") by XREAL_1:64; n >= N2 by A10, A12, XXREAL_0:2; then g . n > 0 by A4; then 1 <= (c * (f . n)) * ((g . n) ") by A13, XCMPLX_0:def_7; then (c ") * 1 <= (c ") * (c * ((f . n) * ((g . n) "))) by A8, XREAL_1:64; then (c ") * 1 <= ((c ") * c) * ((f . n) * ((g . n) ")) ; then (c ") * 1 <= 1 * ((f . n) * ((g . n) ")) by A8, XCMPLX_0:def_7; then 1 / c <= (1 * (f . n)) * ((g . n) ") by XCMPLX_0:def_9; then 1 / c <= (1 * (f . n)) / (g . n) by XCMPLX_0:def_9; then 1 / c <= (f /" g) . n by Lm1; hence q . n <= (f /" g) . n by FUNCOP_1:7; ::_thesis: verum end; then A14: f /" g majorizes q by Def8; now__::_thesis:_ex_p_being_Element_of_REAL_st_ for_p1_being_real_number_st_p1_>_0_holds_ ex_N_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_N_holds_ abs_((q_._n)_-_p)_<_p1 take p = 1 / c; ::_thesis: for p1 being real number st p1 > 0 holds ex N being Element of NAT st for n being Element of NAT st n >= N holds abs ((q . n) - p) < p1 let p1 be real number ; ::_thesis: ( p1 > 0 implies ex N being Element of NAT st for n being Element of NAT st n >= N holds abs ((q . n) - p) < p1 ) assume A15: p1 > 0 ; ::_thesis: ex N being Element of NAT st for n being Element of NAT st n >= N holds abs ((q . n) - p) < p1 take N = N; ::_thesis: for n being Element of NAT st n >= N holds abs ((q . n) - p) < p1 let n be Element of NAT ; ::_thesis: ( n >= N implies abs ((q . n) - p) < p1 ) assume n >= N ; ::_thesis: abs ((q . n) - p) < p1 abs ((q . n) - p) = abs ((1 / c) - (1 / c)) by FUNCOP_1:7 .= abs 0 ; hence abs ((q . n) - p) < p1 by A15, ABSVALUE:2; ::_thesis: verum end; then A16: q is convergent by SEQ_2:def_6; now__::_thesis:_for_p1_being_real_number_st_p1_>_0_holds_ ex_N_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_N_holds_ abs_((q_._n)_-_(1_/_c))_<_p1 let p1 be real number ; ::_thesis: ( p1 > 0 implies ex N being Element of NAT st for n being Element of NAT st n >= N holds abs ((q . n) - (1 / c)) < p1 ) assume A17: p1 > 0 ; ::_thesis: ex N being Element of NAT st for n being Element of NAT st n >= N holds abs ((q . n) - (1 / c)) < p1 take N = N; ::_thesis: for n being Element of NAT st n >= N holds abs ((q . n) - (1 / c)) < p1 let n be Element of NAT ; ::_thesis: ( n >= N implies abs ((q . n) - (1 / c)) < p1 ) assume n >= N ; ::_thesis: abs ((q . n) - (1 / c)) < p1 abs ((q . n) - (1 / c)) = abs ((1 / c) - (1 / c)) by FUNCOP_1:7 .= abs 0 ; hence abs ((q . n) - (1 / c)) < p1 by A17, ABSVALUE:2; ::_thesis: verum end; then lim q = 1 / c by A16, SEQ_2:def_7; then 1 / c <= 0 by A1, A14, A16, Th4; then (1 / c) * c <= 0 * c by A8; hence contradiction by A8, XCMPLX_1:106; ::_thesis: verum end; set b = max (N,N1); set a = max ((max (N,N1)),N2); A18: now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_max_((max_(N,N1)),N2)_holds_ (_f_._n_<=_1_*_(g_._n)_&_f_._n_>=_0_) let n be Element of NAT ; ::_thesis: ( n >= max ((max (N,N1)),N2) implies ( f . n <= 1 * (g . n) & f . n >= 0 ) ) assume A19: n >= max ((max (N,N1)),N2) ; ::_thesis: ( f . n <= 1 * (g . n) & f . n >= 0 ) max ((max (N,N1)),N2) >= max (N,N1) by XXREAL_0:25; then A20: n >= max (N,N1) by A19, XXREAL_0:2; max (N,N1) >= N by XXREAL_0:25; then n >= N by A20, XXREAL_0:2; then abs (((f /" g) . n) - 0) < 1 by A2; then (f /" g) . n <= 1 by ABSVALUE:5; then (f . n) * ((g ") . n) <= 1 by SEQ_1:8; then A21: (f . n) * ((g . n) ") <= 1 by VALUED_1:10; max ((max (N,N1)),N2) >= N2 by XXREAL_0:25; then A22: n >= N2 by A19, XXREAL_0:2; then A23: g . n <> 0 by A4; g . n > 0 by A4, A22; then ((f . n) * ((g . n) ")) * (g . n) <= 1 * (g . n) by A21, XREAL_1:64; then (f . n) * (((g . n) ") * (g . n)) <= 1 * (g . n) ; then (f . n) * 1 <= 1 * (g . n) by A23, XCMPLX_0:def_7; hence f . n <= 1 * (g . n) ; ::_thesis: f . n >= 0 max (N,N1) >= N1 by XXREAL_0:25; then n >= N1 by A20, XXREAL_0:2; hence f . n >= 0 by A3; ::_thesis: verum end; f is Element of Funcs (NAT,REAL) by FUNCT_2:8; hence ( f in Big_Oh g & not g in Big_Oh f ) by A18, A5; ::_thesis: verum end; 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 ) proof let f, g be eventually-positive Real_Sequence; ::_thesis: ( f /" g is divergent_to+infty implies ( not f in Big_Oh g & g in Big_Oh f ) ) assume f /" g is divergent_to+infty ; ::_thesis: ( not f in Big_Oh g & g in Big_Oh f ) then ( g /" f is convergent & lim (g /" f) = 0 ) by Th5; hence ( not f in Big_Oh g & g in Big_Oh f ) by Th16; ::_thesis: verum end; 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 proof set IT = { 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 ) ) ) } ; A1: { 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 functional proof let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in { 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 ) ) ) } or x is set ) assume x in { 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 ) ) ) } ; ::_thesis: x is set then ex t being Element of Funcs (NAT,REAL) st ( x = t & 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 ) ) ) ) ; hence x is set ; ::_thesis: verum end; consider N being Element of NAT such that A2: for n being Element of NAT st n >= N holds f . n >= 0 by Def2; ( f is Element of Funcs (NAT,REAL) & ( for n being Element of NAT st n >= N holds ( f . n >= 1 * (f . n) & f . n >= 0 ) ) ) by A2, FUNCT_2:8; then f in { 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 ) ) ) } ; then reconsider IT1 = { 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 ) ) ) } as non empty functional set by A1; now__::_thesis:_for_x_being_Element_of_IT1_holds_x_is_Function_of_NAT,REAL let x be Element of IT1; ::_thesis: x is Function of NAT,REAL x in { 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 ) ) ) } ; then ex t being Element of Funcs (NAT,REAL) st ( x = t & 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 ) ) ) ) ; hence x is Function of NAT,REAL ; ::_thesis: verum end; hence { 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 by FUNCT_2:def_12; ::_thesis: verum end; 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 proof let t be set ; ::_thesis: for f being eventually-nonnegative Real_Sequence st t in Big_Omega f holds t is eventually-nonnegative Real_Sequence let f be eventually-nonnegative Real_Sequence; ::_thesis: ( t in Big_Omega f implies t is eventually-nonnegative Real_Sequence ) assume t in Big_Omega f ; ::_thesis: t is eventually-nonnegative Real_Sequence then consider s being Element of Funcs (NAT,REAL) such that A1: s = t and A2: ex d being Real ex N being Element of NAT st ( d > 0 & ( for n being Element of NAT st n >= N holds ( s . n >= d * (f . n) & s . n >= 0 ) ) ) ; reconsider t9 = t as Real_Sequence by A1; consider d being Real, N being Element of NAT such that d > 0 and A3: for n being Element of NAT st n >= N holds ( s . n >= d * (f . n) & s . n >= 0 ) by A2; now__::_thesis:_ex_N_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_N_holds_ t9_._n_>=_0 take N = N; ::_thesis: for n being Element of NAT st n >= N holds t9 . n >= 0 let n be Element of NAT ; ::_thesis: ( n >= N implies t9 . n >= 0 ) assume n >= N ; ::_thesis: t9 . n >= 0 hence t9 . n >= 0 by A1, A3; ::_thesis: verum end; hence t is eventually-nonnegative Real_Sequence by Def2; ::_thesis: verum end; 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 ) proof let f, g be eventually-nonnegative Real_Sequence; ::_thesis: ( f in Big_Omega g iff g in Big_Oh f ) A1: g is Element of Funcs (NAT,REAL) by FUNCT_2:8; hereby ::_thesis: ( g in Big_Oh f implies f in Big_Omega g ) consider N1 being Element of NAT such that A2: for n being Element of NAT st n >= N1 holds g . n >= 0 by Def2; assume f in Big_Omega g ; ::_thesis: g in Big_Oh f then consider t being Element of Funcs (NAT,REAL) such that A3: f = t and A4: 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 * (g . n) & t . n >= 0 ) ) ) ; consider d being Real, N being Element of NAT such that A5: d > 0 and A6: for n being Element of NAT st n >= N holds ( t . n >= d * (g . n) & t . n >= 0 ) by A4; set a = max (N,N1); A7: max (N,N1) >= N1 by XXREAL_0:25; A8: max (N,N1) >= N by XXREAL_0:25; now__::_thesis:_ex_a_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_a_holds_ (_g_._n_<=_(d_")_*_(f_._n)_&_g_._n_>=_0_) take a = max (N,N1); ::_thesis: for n being Element of NAT st n >= a holds ( g . n <= (d ") * (f . n) & g . n >= 0 ) let n be Element of NAT ; ::_thesis: ( n >= a implies ( g . n <= (d ") * (f . n) & g . n >= 0 ) ) assume A9: n >= a ; ::_thesis: ( g . n <= (d ") * (f . n) & g . n >= 0 ) then n >= N by A8, XXREAL_0:2; then t . n >= d * (g . n) by A6; then (d ") * (t . n) >= (d ") * (d * (g . n)) by A5, XREAL_1:64; then (d ") * (t . n) >= ((d ") * d) * (g . n) ; then (d ") * (t . n) >= 1 * (g . n) by A5, XCMPLX_0:def_7; hence g . n <= (d ") * (f . n) by A3; ::_thesis: g . n >= 0 n >= N1 by A7, A9, XXREAL_0:2; hence g . n >= 0 by A2; ::_thesis: verum end; hence g in Big_Oh f by A1, A5; ::_thesis: verum end; assume g in Big_Oh f ; ::_thesis: f in Big_Omega g then consider t being Element of Funcs (NAT,REAL) such that A10: g = t and A11: 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 ) ) ) ; consider c being Real, N being Element of NAT such that A12: c > 0 and A13: for n being Element of NAT st n >= N holds ( t . n <= c * (f . n) & t . n >= 0 ) by A11; consider N1 being Element of NAT such that A14: for n being Element of NAT st n >= N1 holds f . n >= 0 by Def2; set a = max (N,N1); A15: max (N,N1) >= N1 by XXREAL_0:25; A16: max (N,N1) >= N by XXREAL_0:25; A17: now__::_thesis:_ex_a_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_a_holds_ (_f_._n_>=_(c_")_*_(g_._n)_&_f_._n_>=_0_) take a = max (N,N1); ::_thesis: for n being Element of NAT st n >= a holds ( f . n >= (c ") * (g . n) & f . n >= 0 ) let n be Element of NAT ; ::_thesis: ( n >= a implies ( f . n >= (c ") * (g . n) & f . n >= 0 ) ) assume A18: n >= a ; ::_thesis: ( f . n >= (c ") * (g . n) & f . n >= 0 ) then n >= N by A16, XXREAL_0:2; then t . n <= c * (f . n) by A13; then (c ") * (t . n) <= (c ") * (c * (f . n)) by A12, XREAL_1:64; then (c ") * (t . n) <= ((c ") * c) * (f . n) ; then (c ") * (t . n) <= 1 * (f . n) by A12, XCMPLX_0:def_7; hence f . n >= (c ") * (g . n) by A10; ::_thesis: f . n >= 0 n >= N1 by A15, A18, XXREAL_0:2; hence f . n >= 0 by A14; ::_thesis: verum end; f is Element of Funcs (NAT,REAL) by FUNCT_2:8; hence f in Big_Omega g by A12, A17; ::_thesis: verum end; theorem Th20: :: ASYMPT_0:20 for f being eventually-nonnegative Real_Sequence holds f in Big_Omega f proof let f be eventually-nonnegative Real_Sequence; ::_thesis: f in Big_Omega f f in Big_Oh f by Th10; hence f in Big_Omega f by Th19; ::_thesis: verum end; 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 proof let f, g, h be eventually-nonnegative Real_Sequence; ::_thesis: ( f in Big_Omega g & g in Big_Omega h implies f in Big_Omega h ) assume ( f in Big_Omega g & g in Big_Omega h ) ; ::_thesis: f in Big_Omega h then ( h in Big_Oh g & g in Big_Oh f ) by Th19; then h in Big_Oh f by Th12; hence f in Big_Omega h by Th19; ::_thesis: verum end; 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 proof let f, g be eventually-positive Real_Sequence; ::_thesis: ( f /" g is convergent & lim (f /" g) > 0 implies Big_Omega f = Big_Omega g ) assume A1: ( f /" g is convergent & lim (f /" g) > 0 ) ; ::_thesis: Big_Omega f = Big_Omega g now__::_thesis:_for_x_being_set_holds_ (_(_x_in_Big_Omega_f_implies_x_in_Big_Omega_g_)_&_(_x_in_Big_Omega_g_implies_x_in_Big_Omega_f_)_) let x be set ; ::_thesis: ( ( x in Big_Omega f implies x in Big_Omega g ) & ( x in Big_Omega g implies x in Big_Omega f ) ) hereby ::_thesis: ( x in Big_Omega g implies x in Big_Omega f ) g in Big_Oh g by Th10; then g in Big_Oh f by A1, Th15; then A2: f in Big_Omega g by Th19; assume x in Big_Omega f ; ::_thesis: x in Big_Omega g then consider t being Element of Funcs (NAT,REAL) such that A3: x = t and A4: ex d being Real ex N being Element of NAT st ( d > 0 & ( for n being Element of NAT st n >= N holds ( d * (f . n) <= t . n & t . n >= 0 ) ) ) ; consider d being Real, N being Element of NAT such that d > 0 and A5: for n being Element of NAT st n >= N holds ( d * (f . n) <= t . n & t . n >= 0 ) by A4; now__::_thesis:_ex_N_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_N_holds_ t_._n_>=_0 take N = N; ::_thesis: for n being Element of NAT st n >= N holds t . n >= 0 let n be Element of NAT ; ::_thesis: ( n >= N implies t . n >= 0 ) assume n >= N ; ::_thesis: t . n >= 0 hence t . n >= 0 by A5; ::_thesis: verum end; then A6: t is eventually-nonnegative by Def2; t in Big_Omega f by A4; hence x in Big_Omega g by A3, A6, A2, Th21; ::_thesis: verum end; assume x in Big_Omega g ; ::_thesis: x in Big_Omega f then consider t being Element of Funcs (NAT,REAL) such that A7: x = t and A8: ex d being Real ex N being Element of NAT st ( d > 0 & ( for n being Element of NAT st n >= N holds ( d * (g . n) <= t . n & t . n >= 0 ) ) ) ; consider d being Real, N being Element of NAT such that d > 0 and A9: for n being Element of NAT st n >= N holds ( d * (g . n) <= t . n & t . n >= 0 ) by A8; now__::_thesis:_ex_N_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_N_holds_ t_._n_>=_0 take N = N; ::_thesis: for n being Element of NAT st n >= N holds t . n >= 0 let n be Element of NAT ; ::_thesis: ( n >= N implies t . n >= 0 ) assume n >= N ; ::_thesis: t . n >= 0 hence t . n >= 0 by A9; ::_thesis: verum end; then A10: t is eventually-nonnegative by Def2; f in Big_Oh f by Th10; then f in Big_Oh g by A1, Th15; then A11: g in Big_Omega f by Th19; t in Big_Omega g by A8; hence x in Big_Omega f by A7, A10, A11, Th21; ::_thesis: verum end; hence Big_Omega f = Big_Omega g by TARSKI:1; ::_thesis: verum end; 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 ) proof let f, g be eventually-positive Real_Sequence; ::_thesis: ( f /" g is convergent & lim (f /" g) = 0 implies ( g in Big_Omega f & not f in Big_Omega g ) ) assume ( f /" g is convergent & lim (f /" g) = 0 ) ; ::_thesis: ( g in Big_Omega f & not f in Big_Omega g ) then ( f in Big_Oh g & not g in Big_Oh f ) by Th16; hence ( g in Big_Omega f & not f in Big_Omega g ) by Th19; ::_thesis: verum end; 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 ) proof let f, g be eventually-positive Real_Sequence; ::_thesis: ( f /" g is divergent_to+infty implies ( not g in Big_Omega f & f in Big_Omega g ) ) assume f /" g is divergent_to+infty ; ::_thesis: ( not g in Big_Omega f & f in Big_Omega g ) then ( g /" f is convergent & lim (g /" f) = 0 ) by Th5; hence ( not g in Big_Omega f & f in Big_Omega g ) by Th23; ::_thesis: verum end; 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 ) ) ) proof let f, t be positive Real_Sequence; ::_thesis: ( 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 ) ) ) hereby ::_thesis: ( ex d being Real st ( d > 0 & ( for n being Element of NAT holds d * (f . n) <= t . n ) ) implies t in Big_Omega f ) assume t in Big_Omega f ; ::_thesis: ex d being Real st ( d > 0 & ( for n being Element of NAT holds d * (f . n) <= t . n ) ) then consider s being Element of Funcs (NAT,REAL) such that A1: s = t and A2: ex d being Real ex N being Element of NAT st ( d > 0 & ( for n being Element of NAT st n >= N holds ( d * (f . n) <= s . n & s . n >= 0 ) ) ) ; consider d being Real, N being Element of NAT such that A3: d > 0 and A4: for n being Element of NAT st n >= N holds ( d * (f . n) <= s . n & s . n >= 0 ) by A2; percases ( N = 0 or N > 0 ) ; supposeA5: N = 0 ; ::_thesis: ex d being Real st ( d > 0 & ( for n being Element of NAT holds d * (f . n) <= t . n ) ) take d = d; ::_thesis: ( d > 0 & ( for n being Element of NAT holds d * (f . n) <= t . n ) ) thus d > 0 by A3; ::_thesis: for n being Element of NAT holds d * (f . n) <= t . n let n be Element of NAT ; ::_thesis: d * (f . n) <= t . n thus d * (f . n) <= t . n by A1, A4, A5; ::_thesis: verum end; supposeA6: N > 0 ; ::_thesis: ex d being Real st ( d > 0 & ( for n being Element of NAT holds d * (f . n) <= t . n ) ) deffunc H1( Element of NAT ) -> Element of REAL = (t . $1) / (f . $1); reconsider B = { H1(n) where n is Element of NAT : n < N } as non empty finite Subset of REAL from ASYMPT_0:sch_3(A6); set b = min B; A7: for n being Element of NAT st n < N holds (min B) * (f . n) <= t . n proof let n be Element of NAT ; ::_thesis: ( n < N implies (min B) * (f . n) <= t . n ) A8: f . n > 0 by Def3; assume n < N ; ::_thesis: (min B) * (f . n) <= t . n then (t . n) / (f . n) in B ; then (t . n) / (f . n) >= min B by XXREAL_2:def_7; then ((t . n) / (f . n)) * (f . n) >= (min B) * (f . n) by A8, XREAL_1:64; hence (min B) * (f . n) <= t . n by A8, XCMPLX_1:87; ::_thesis: verum end; thus ex d being Real st ( d > 0 & ( for n being Element of NAT holds d * (f . n) <= t . n ) ) ::_thesis: verum proof percases ( min B <= d or min B > d ) ; supposeA9: min B <= d ; ::_thesis: ex d being Real st ( d > 0 & ( for n being Element of NAT holds d * (f . n) <= t . n ) ) reconsider b = min B as Element of REAL by XREAL_0:def_1; take b ; ::_thesis: ( b > 0 & ( for n being Element of NAT holds b * (f . n) <= t . n ) ) b in B by XXREAL_2:def_7; then consider n1 being Element of NAT such that A10: b = (t . n1) / (f . n1) and n1 < N ; ( t . n1 > 0 & f . n1 > 0 ) by Def3; then (t . n1) * ((f . n1) ") > 0 * ((f . n1) ") by XREAL_1:68; hence b > 0 by A10, XCMPLX_0:def_9; ::_thesis: for n being Element of NAT holds b * (f . n) <= t . n let n be Element of NAT ; ::_thesis: b * (f . n) <= t . n thus b * (f . n) <= t . n ::_thesis: verum proof percases ( n < N or n >= N ) ; suppose n < N ; ::_thesis: b * (f . n) <= t . n hence b * (f . n) <= t . n by A7; ::_thesis: verum end; supposeA11: n >= N ; ::_thesis: b * (f . n) <= t . n f . n > 0 by Def3; then A12: b * (f . n) <= d * (f . n) by A9, XREAL_1:64; d * (f . n) <= t . n by A1, A4, A11; hence b * (f . n) <= t . n by A12, XXREAL_0:2; ::_thesis: verum end; end; end; end; supposeA13: min B > d ; ::_thesis: ex d being Real st ( d > 0 & ( for n being Element of NAT holds d * (f . n) <= t . n ) ) take d ; ::_thesis: ( d > 0 & ( for n being Element of NAT holds d * (f . n) <= t . n ) ) thus d > 0 by A3; ::_thesis: for n being Element of NAT holds d * (f . n) <= t . n let n be Element of NAT ; ::_thesis: d * (f . n) <= t . n thus d * (f . n) <= t . n ::_thesis: verum proof percases ( n < N or n >= N ) ; supposeA14: n < N ; ::_thesis: d * (f . n) <= t . n f . n > 0 by Def3; then A15: d * (f . n) <= (min B) * (f . n) by A13, XREAL_1:64; (min B) * (f . n) <= t . n by A7, A14; hence d * (f . n) <= t . n by A15, XXREAL_0:2; ::_thesis: verum end; suppose n >= N ; ::_thesis: d * (f . n) <= t . n hence d * (f . n) <= t . n by A1, A4; ::_thesis: verum end; end; end; end; end; end; end; end; end; given d being Real such that A16: d > 0 and A17: for n being Element of NAT holds d * (f . n) <= t . n ; ::_thesis: t in Big_Omega f ( t is Element of Funcs (NAT,REAL) & ( for n being Element of NAT st n >= 0 holds ( d * (f . n) <= t . n & t . n >= 0 ) ) ) by A17, Def3, FUNCT_2:8; hence t in Big_Omega f by A16; ::_thesis: verum end; theorem :: ASYMPT_0:26 for f, g being eventually-nonnegative Real_Sequence holds Big_Omega (f + g) = Big_Omega (max (f,g)) proof let f, g be eventually-nonnegative Real_Sequence; ::_thesis: Big_Omega (f + g) = Big_Omega (max (f,g)) consider N1 being Element of NAT such that A1: for n being Element of NAT st n >= N1 holds f . n >= 0 by Def2; consider N2 being Element of NAT such that A2: for n being Element of NAT st n >= N2 holds g . n >= 0 by Def2; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_Big_Omega_(f_+_g)_implies_x_in_Big_Omega_(max_(f,g))_)_&_(_x_in_Big_Omega_(max_(f,g))_implies_x_in_Big_Omega_(f_+_g)_)_) let x be set ; ::_thesis: ( ( x in Big_Omega (f + g) implies x in Big_Omega (max (f,g)) ) & ( x in Big_Omega (max (f,g)) implies x in Big_Omega (f + g) ) ) hereby ::_thesis: ( x in Big_Omega (max (f,g)) implies x in Big_Omega (f + g) ) assume x in Big_Omega (f + g) ; ::_thesis: x in Big_Omega (max (f,g)) then consider t being Element of Funcs (NAT,REAL) such that A3: t = x and A4: ex d being Real ex N being Element of NAT st ( d > 0 & ( for n being Element of NAT st n >= N holds ( d * ((f + g) . n) <= t . n & t . n >= 0 ) ) ) ; consider d being Real, N being Element of NAT such that A5: d > 0 and A6: for n being Element of NAT st n >= N holds ( d * ((f + g) . n) <= t . n & t . n >= 0 ) by A4; set a = max (N,(max (N1,N2))); A7: max (N,(max (N1,N2))) >= N by XXREAL_0:25; A8: max (N,(max (N1,N2))) >= max (N1,N2) by XXREAL_0:25; max (N1,N2) >= N2 by XXREAL_0:25; then A9: max (N,(max (N1,N2))) >= N2 by A8, XXREAL_0:2; max (N1,N2) >= N1 by XXREAL_0:25; then A10: max (N,(max (N1,N2))) >= N1 by A8, XXREAL_0:2; now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_max_(N,(max_(N1,N2)))_holds_ (_d_*_((max_(f,g))_._n)_<=_t_._n_&_t_._n_>=_0_) let n be Element of NAT ; ::_thesis: ( n >= max (N,(max (N1,N2))) implies ( d * ((max (f,g)) . n) <= t . n & t . n >= 0 ) ) assume A11: n >= max (N,(max (N1,N2))) ; ::_thesis: ( d * ((max (f,g)) . n) <= t . n & t . n >= 0 ) then n >= N1 by A10, XXREAL_0:2; then A12: f . n >= 0 by A1; n >= N2 by A9, A11, XXREAL_0:2; then A13: g . n >= 0 by A2; A14: (max (f,g)) . n = max ((f . n),(g . n)) by Def7; (max (f,g)) . n <= (f + g) . n proof percases ( (max (f,g)) . n = f . n or (max (f,g)) . n = g . n ) by A14, XXREAL_0:16; suppose (max (f,g)) . n = f . n ; ::_thesis: (max (f,g)) . n <= (f + g) . n then ((max (f,g)) . n) + 0 <= (f . n) + (g . n) by A13, XREAL_1:7; hence (max (f,g)) . n <= (f + g) . n by SEQ_1:7; ::_thesis: verum end; suppose (max (f,g)) . n = g . n ; ::_thesis: (max (f,g)) . n <= (f + g) . n then ((max (f,g)) . n) + 0 <= (g . n) + (f . n) by A12, XREAL_1:7; hence (max (f,g)) . n <= (f + g) . n by SEQ_1:7; ::_thesis: verum end; end; end; then A15: d * ((max (f,g)) . n) <= d * ((f + g) . n) by A5, XREAL_1:64; A16: n >= N by A7, A11, XXREAL_0:2; then d * ((f + g) . n) <= t . n by A6; hence d * ((max (f,g)) . n) <= t . n by A15, XXREAL_0:2; ::_thesis: t . n >= 0 thus t . n >= 0 by A6, A16; ::_thesis: verum end; hence x in Big_Omega (max (f,g)) by A3, A5; ::_thesis: verum end; assume x in Big_Omega (max (f,g)) ; ::_thesis: x in Big_Omega (f + g) then consider t being Element of Funcs (NAT,REAL) such that A17: t = x and A18: ex d being Real ex N being Element of NAT st ( d > 0 & ( for n being Element of NAT st n >= N holds ( d * ((max (f,g)) . n) <= t . n & t . n >= 0 ) ) ) ; consider d being Real, N being Element of NAT such that A19: d > 0 and A20: for n being Element of NAT st n >= N holds ( d * ((max (f,g)) . n) <= t . n & t . n >= 0 ) by A18; set a = max (N,(max (N1,N2))); A21: N <= max (N,(max (N1,N2))) by XXREAL_0:25; A22: now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_max_(N,(max_(N1,N2)))_holds_ (_(d_*_(2_"))_*_((f_+_g)_._n)_<=_t_._n_&_t_._n_>=_0_) let n be Element of NAT ; ::_thesis: ( n >= max (N,(max (N1,N2))) implies ( (d * (2 ")) * ((f + g) . n) <= t . n & t . n >= 0 ) ) ( f . n <= max ((f . n),(g . n)) & g . n <= max ((f . n),(g . n)) ) by XXREAL_0:25; then (f . n) + (g . n) <= (1 * (max ((f . n),(g . n)))) + (1 * (max ((f . n),(g . n)))) by XREAL_1:7; then (2 ") * ((f . n) + (g . n)) <= (2 ") * (2 * (max ((f . n),(g . n)))) by XREAL_1:64; then (2 ") * ((f + g) . n) <= max ((f . n),(g . n)) by SEQ_1:7; then d * ((2 ") * ((f + g) . n)) <= d * (max ((f . n),(g . n))) by A19, XREAL_1:64; then A23: d * ((2 ") * ((f + g) . n)) <= d * ((max (f,g)) . n) by Def7; assume n >= max (N,(max (N1,N2))) ; ::_thesis: ( (d * (2 ")) * ((f + g) . n) <= t . n & t . n >= 0 ) then A24: n >= N by A21, XXREAL_0:2; then d * ((max (f,g)) . n) <= t . n by A20; hence (d * (2 ")) * ((f + g) . n) <= t . n by A23, XXREAL_0:2; ::_thesis: t . n >= 0 thus t . n >= 0 by A20, A24; ::_thesis: verum end; d * (2 ") > d * 0 by A19, XREAL_1:68; hence x in Big_Omega (f + g) by A17, A22; ::_thesis: verum end; hence Big_Omega (f + g) = Big_Omega (max (f,g)) by TARSKI:1; ::_thesis: verum end; 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 proof ( f in Big_Oh f & f in Big_Omega f ) by Th10, Th20; then A1: not (Big_Oh f) /\ (Big_Omega f) is empty by XBOOLE_0:def_4; now__::_thesis:_for_x_being_Element_of_(Big_Oh_f)_/\_(Big_Omega_f)_holds_x_is_Function_of_NAT,REAL let x be Element of (Big_Oh f) /\ (Big_Omega f); ::_thesis: x is Function of NAT,REAL x in Big_Oh f by A1, XBOOLE_0:def_4; hence x is Function of NAT,REAL by Th6; ::_thesis: verum end; hence (Big_Oh f) /\ (Big_Omega f) is FUNCTION_DOMAIN of NAT , REAL by A1, FUNCT_2:def_12; ::_thesis: verum end; 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) ) ) ) } proof let f be eventually-nonnegative Real_Sequence; ::_thesis: 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) ) ) ) } set BT = { 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) ) ) ) } ; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_Big_Theta_f_implies_x_in__{__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)_)_)_)__}__)_&_(_x_in__{__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)_)_)_)__}__implies_x_in_Big_Theta_f_)_) let x be set ; ::_thesis: ( ( x in Big_Theta f implies x in { 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) ) ) ) } ) & ( x in { 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) ) ) ) } implies x in Big_Theta f ) ) hereby ::_thesis: ( x in { 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) ) ) ) } implies x in Big_Theta f ) assume A1: x in Big_Theta f ; ::_thesis: x in { 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) ) ) ) } then x in Big_Oh f by XBOOLE_0:def_4; then consider t being Element of Funcs (NAT,REAL) such that A2: x = t and A3: 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 ) ) ) ; x in Big_Omega f by A1, XBOOLE_0:def_4; then consider s being Element of Funcs (NAT,REAL) such that A4: x = s and A5: ex d being Real ex N being Element of NAT st ( d > 0 & ( for n being Element of NAT st n >= N holds ( s . n >= d * (f . n) & s . n >= 0 ) ) ) ; consider c being Real, N being Element of NAT such that A6: c > 0 and A7: for n being Element of NAT st n >= N holds ( t . n <= c * (f . n) & t . n >= 0 ) by A3; consider d being Real, N1 being Element of NAT such that A8: d > 0 and A9: for n being Element of NAT st n >= N1 holds ( s . n >= d * (f . n) & s . n >= 0 ) by A5; set a = max (N,N1); A10: ( max (N,N1) >= N & max (N,N1) >= N1 ) by XXREAL_0:25; now__::_thesis:_ex_a_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_a_holds_ (_d_*_(f_._n)_<=_t_._n_&_t_._n_<=_c_*_(f_._n)_) take a = max (N,N1); ::_thesis: for n being Element of NAT st n >= a holds ( d * (f . n) <= t . n & t . n <= c * (f . n) ) let n be Element of NAT ; ::_thesis: ( n >= a implies ( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) assume n >= a ; ::_thesis: ( d * (f . n) <= t . n & t . n <= c * (f . n) ) then ( n >= N & n >= N1 ) by A10, XXREAL_0:2; hence ( d * (f . n) <= t . n & t . n <= c * (f . n) ) by A2, A4, A7, A9; ::_thesis: verum end; hence x in { 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) ) ) ) } by A2, A6, A8; ::_thesis: verum end; assume x in { 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) ) ) ) } ; ::_thesis: x in Big_Theta f then consider t being Element of Funcs (NAT,REAL) such that A11: x = t and A12: 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) ) ) ) ; consider c, d being Real, N being Element of NAT such that A13: c > 0 and A14: d > 0 and A15: for n being Element of NAT st n >= N holds ( d * (f . n) <= t . n & t . n <= c * (f . n) ) by A12; consider N1 being Element of NAT such that A16: for n being Element of NAT st n >= N1 holds f . n >= 0 by Def2; set a = max (N,N1); A17: max (N,N1) >= N1 by XXREAL_0:25; A18: max (N,N1) >= N by XXREAL_0:25; now__::_thesis:_ex_a_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_a_holds_ (_d_*_(f_._n)_<=_t_._n_&_t_._n_>=_0_) take a = max (N,N1); ::_thesis: for n being Element of NAT st n >= a holds ( d * (f . n) <= t . n & t . n >= 0 ) let n be Element of NAT ; ::_thesis: ( n >= a implies ( d * (f . n) <= t . n & t . n >= 0 ) ) assume A19: n >= a ; ::_thesis: ( d * (f . n) <= t . n & t . n >= 0 ) then A20: n >= N by A18, XXREAL_0:2; hence d * (f . n) <= t . n by A15; ::_thesis: t . n >= 0 n >= N1 by A17, A19, XXREAL_0:2; then f . n >= 0 by A16; then d * (f . n) >= d * 0 by A14; hence t . n >= 0 by A15, A20; ::_thesis: verum end; then A21: x in Big_Omega f by A11, A14; now__::_thesis:_ex_a_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_a_holds_ (_t_._n_<=_c_*_(f_._n)_&_t_._n_>=_0_) take a = max (N,N1); ::_thesis: for n being Element of NAT st n >= a holds ( t . n <= c * (f . n) & t . n >= 0 ) let n be Element of NAT ; ::_thesis: ( n >= a implies ( t . n <= c * (f . n) & t . n >= 0 ) ) assume A22: n >= a ; ::_thesis: ( t . n <= c * (f . n) & t . n >= 0 ) then A23: n >= N by A18, XXREAL_0:2; hence t . n <= c * (f . n) by A15; ::_thesis: t . n >= 0 n >= N1 by A17, A22, XXREAL_0:2; then f . n >= 0 by A16; then d * (f . n) >= d * 0 by A14; hence t . n >= 0 by A15, A23; ::_thesis: verum end; then x in Big_Oh f by A11, A13; hence x in Big_Theta f by A21, XBOOLE_0:def_4; ::_thesis: verum end; hence 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) ) ) ) } by TARSKI:1; ::_thesis: verum end; theorem :: ASYMPT_0:28 for f being eventually-nonnegative Real_Sequence holds f in Big_Theta f proof let f be eventually-nonnegative Real_Sequence; ::_thesis: f in Big_Theta f ( f in Big_Oh f & f in Big_Omega f ) by Th10, Th20; hence f in Big_Theta f by XBOOLE_0:def_4; ::_thesis: verum end; theorem :: ASYMPT_0:29 for f, g being eventually-nonnegative Real_Sequence st f in Big_Theta g holds g in Big_Theta f proof let f, g be eventually-nonnegative Real_Sequence; ::_thesis: ( f in Big_Theta g implies g in Big_Theta f ) assume A1: f in Big_Theta g ; ::_thesis: g in Big_Theta f then f in Big_Omega g by XBOOLE_0:def_4; then A2: g in Big_Oh f by Th19; f in Big_Oh g by A1, XBOOLE_0:def_4; then g in Big_Omega f by Th19; hence g in Big_Theta f by A2, XBOOLE_0:def_4; ::_thesis: verum end; 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 proof let f, g, h be eventually-nonnegative Real_Sequence; ::_thesis: ( f in Big_Theta g & g in Big_Theta h implies f in Big_Theta h ) assume A1: ( f in Big_Theta g & g in Big_Theta h ) ; ::_thesis: f in Big_Theta h then ( f in Big_Omega g & g in Big_Omega h ) by XBOOLE_0:def_4; then A2: f in Big_Omega h by Th21; ( f in Big_Oh g & g in Big_Oh h ) by A1, XBOOLE_0:def_4; then f in Big_Oh h by Th12; hence f in Big_Theta h by A2, XBOOLE_0:def_4; ::_thesis: verum end; 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) ) ) ) ) proof let f, t be positive Real_Sequence; ::_thesis: ( 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) ) ) ) ) A1: Big_Theta f = { s where s 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) <= s . n & s . n <= c * (f . n) ) ) ) } by Th27; hereby ::_thesis: ( 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) ) ) ) implies t in Big_Theta f ) assume t in Big_Theta f ; ::_thesis: 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) ) ) ) then consider s being Element of Funcs (NAT,REAL) such that A2: s = t and A3: 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) <= s . n & s . n <= c * (f . n) ) ) ) by A1; consider c, d being Real, N being Element of NAT such that A4: c > 0 and A5: d > 0 and A6: for n being Element of NAT st n >= N holds ( d * (f . n) <= s . n & s . n <= c * (f . n) ) by A3; percases ( N = 0 or N > 0 ) ; supposeA7: N = 0 ; ::_thesis: 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) ) ) ) take c = c; ::_thesis: ex 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) ) ) ) take d = d; ::_thesis: ( c > 0 & d > 0 & ( for n being Element of NAT holds ( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) thus c > 0 by A4; ::_thesis: ( d > 0 & ( for n being Element of NAT holds ( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) thus d > 0 by A5; ::_thesis: for n being Element of NAT holds ( d * (f . n) <= t . n & t . n <= c * (f . n) ) let n be Element of NAT ; ::_thesis: ( d * (f . n) <= t . n & t . n <= c * (f . n) ) thus ( d * (f . n) <= t . n & t . n <= c * (f . n) ) by A2, A6, A7; ::_thesis: verum end; supposeA8: N > 0 ; ::_thesis: 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) ) ) ) deffunc H1( Element of NAT ) -> Element of REAL = (t . $1) / (f . $1); reconsider B = { H1(n) where n is Element of NAT : n < N } as non empty finite Subset of REAL from ASYMPT_0:sch_3(A8); set b = max B; set a = min B; A9: for n being Element of NAT st n < N holds t . n >= (min B) * (f . n) proof let n be Element of NAT ; ::_thesis: ( n < N implies t . n >= (min B) * (f . n) ) A10: f . n > 0 by Def3; assume n < N ; ::_thesis: t . n >= (min B) * (f . n) then (t . n) / (f . n) in B ; then (t . n) / (f . n) >= min B by XXREAL_2:def_7; then ((t . n) / (f . n)) * (f . n) >= (min B) * (f . n) by A10, XREAL_1:64; hence t . n >= (min B) * (f . n) by A10, XCMPLX_1:87; ::_thesis: verum end; A11: for n being Element of NAT st n < N holds t . n <= (max B) * (f . n) proof let n be Element of NAT ; ::_thesis: ( n < N implies t . n <= (max B) * (f . n) ) A12: f . n > 0 by Def3; assume n < N ; ::_thesis: t . n <= (max B) * (f . n) then (t . n) / (f . n) in B ; then (t . n) / (f . n) <= max B by XXREAL_2:def_8; then ((t . n) / (f . n)) * (f . n) <= (max B) * (f . n) by A12, XREAL_1:64; hence t . n <= (max B) * (f . n) by A12, XCMPLX_1:87; ::_thesis: verum end; thus 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) ) ) ) ::_thesis: verum proof set D = min ((min B),d); set C = max ((max B),c); reconsider C = max ((max B),c), D = min ((min B),d) as Element of REAL by XREAL_0:def_1; take C ; ::_thesis: ex 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) ) ) ) take D ; ::_thesis: ( C > 0 & D > 0 & ( for n being Element of NAT holds ( D * (f . n) <= t . n & t . n <= C * (f . n) ) ) ) thus C > 0 by A4, XXREAL_0:25; ::_thesis: ( D > 0 & ( for n being Element of NAT holds ( D * (f . n) <= t . n & t . n <= C * (f . n) ) ) ) A13: now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<_(t_._n)_/_(f_._n) let n be Element of NAT ; ::_thesis: 0 < (t . n) / (f . n) ( f . n > 0 & t . n > 0 ) by Def3; then 0 * ((f . n) ") < (t . n) * ((f . n) ") by XREAL_1:68; hence 0 < (t . n) / (f . n) by XCMPLX_0:def_9; ::_thesis: verum end; min B > 0 proof min B in B by XXREAL_2:def_7; then ex n being Element of NAT st ( min B = (t . n) / (f . n) & n < N ) ; hence min B > 0 by A13; ::_thesis: verum end; hence D > 0 by A5, XXREAL_0:15; ::_thesis: for n being Element of NAT holds ( D * (f . n) <= t . n & t . n <= C * (f . n) ) let n be Element of NAT ; ::_thesis: ( D * (f . n) <= t . n & t . n <= C * (f . n) ) A14: f . n > 0 by Def3; percases ( n < N or n >= N ) ; supposeA15: n < N ; ::_thesis: ( D * (f . n) <= t . n & t . n <= C * (f . n) ) A16: D * (f . n) <= (min B) * (f . n) by A14, XREAL_1:64, XXREAL_0:17; (min B) * (f . n) <= t . n by A9, A15; hence D * (f . n) <= t . n by A16, XXREAL_0:2; ::_thesis: t . n <= C * (f . n) A17: (max B) * (f . n) <= C * (f . n) by A14, XREAL_1:64, XXREAL_0:25; t . n <= (max B) * (f . n) by A11, A15; hence t . n <= C * (f . n) by A17, XXREAL_0:2; ::_thesis: verum end; supposeA18: n >= N ; ::_thesis: ( D * (f . n) <= t . n & t . n <= C * (f . n) ) A19: D * (f . n) <= d * (f . n) by A14, XREAL_1:64, XXREAL_0:17; d * (f . n) <= t . n by A2, A6, A18; hence D * (f . n) <= t . n by A19, XXREAL_0:2; ::_thesis: t . n <= C * (f . n) A20: c * (f . n) <= C * (f . n) by A14, XREAL_1:64, XXREAL_0:25; t . n <= c * (f . n) by A2, A6, A18; hence t . n <= C * (f . n) by A20, XXREAL_0:2; ::_thesis: verum end; end; end; end; end; end; given c, d being Real such that A21: ( c > 0 & d > 0 ) and A22: for n being Element of NAT holds ( d * (f . n) <= t . n & t . n <= c * (f . n) ) ; ::_thesis: t in Big_Theta f ( t is Element of Funcs (NAT,REAL) & ( for n being Element of NAT st n >= 0 holds ( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) ) by A22, FUNCT_2:8; hence t in Big_Theta f by A1, A21; ::_thesis: verum end; theorem :: ASYMPT_0:32 for f, g being eventually-nonnegative Real_Sequence holds Big_Theta (f + g) = Big_Theta (max (f,g)) proof let f, g be eventually-nonnegative Real_Sequence; ::_thesis: Big_Theta (f + g) = Big_Theta (max (f,g)) A1: Big_Theta (max (f,g)) = { s where s 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 * ((max (f,g)) . n) <= s . n & s . n <= c * ((max (f,g)) . n) ) ) ) } by Th27; consider N2 being Element of NAT such that A2: for n being Element of NAT st n >= N2 holds g . n >= 0 by Def2; consider N1 being Element of NAT such that A3: for n being Element of NAT st n >= N1 holds f . n >= 0 by Def2; A4: Big_Theta (f + g) = { s where s 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 + g) . n) <= s . n & s . n <= c * ((f + g) . n) ) ) ) } by Th27; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_Big_Theta_(f_+_g)_implies_x_in_Big_Theta_(max_(f,g))_)_&_(_x_in_Big_Theta_(max_(f,g))_implies_x_in_Big_Theta_(f_+_g)_)_) let x be set ; ::_thesis: ( ( x in Big_Theta (f + g) implies x in Big_Theta (max (f,g)) ) & ( x in Big_Theta (max (f,g)) implies x in Big_Theta (f + g) ) ) hereby ::_thesis: ( x in Big_Theta (max (f,g)) implies x in Big_Theta (f + g) ) assume x in Big_Theta (f + g) ; ::_thesis: x in Big_Theta (max (f,g)) then consider t being Element of Funcs (NAT,REAL) such that A5: t = x and A6: 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 + g) . n) <= t . n & t . n <= c * ((f + g) . n) ) ) ) by A4; consider c, d being Real, N being Element of NAT such that A7: c > 0 and A8: d > 0 and A9: for n being Element of NAT st n >= N holds ( d * ((f + g) . n) <= t . n & t . n <= c * ((f + g) . n) ) by A6; set a = max (N,(max (N1,N2))); A10: max (N,(max (N1,N2))) >= N by XXREAL_0:25; A11: max (N,(max (N1,N2))) >= max (N1,N2) by XXREAL_0:25; max (N1,N2) >= N2 by XXREAL_0:25; then A12: max (N,(max (N1,N2))) >= N2 by A11, XXREAL_0:2; max (N1,N2) >= N1 by XXREAL_0:25; then A13: max (N,(max (N1,N2))) >= N1 by A11, XXREAL_0:2; A14: now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_max_(N,(max_(N1,N2)))_holds_ (_d_*_((max_(f,g))_._n)_<=_t_._n_&_t_._n_<=_(2_*_c)_*_((max_(f,g))_._n)_) let n be Element of NAT ; ::_thesis: ( n >= max (N,(max (N1,N2))) implies ( d * ((max (f,g)) . n) <= t . n & t . n <= (2 * c) * ((max (f,g)) . n) ) ) A15: ( g . n <= max ((f . n),(g . n)) & (1 * ((max (f,g)) . n)) + (1 * ((max (f,g)) . n)) = (1 + 1) * ((max (f,g)) . n) ) by XXREAL_0:25; A16: (max (f,g)) . n = max ((f . n),(g . n)) by Def7; ( (f + g) . n = (f . n) + (g . n) & f . n <= max ((f . n),(g . n)) ) by SEQ_1:7, XXREAL_0:25; then (f + g) . n <= 2 * ((max (f,g)) . n) by A16, A15, XREAL_1:7; then A17: c * ((f + g) . n) <= c * (2 * ((max (f,g)) . n)) by A7, XREAL_1:64; assume A18: n >= max (N,(max (N1,N2))) ; ::_thesis: ( d * ((max (f,g)) . n) <= t . n & t . n <= (2 * c) * ((max (f,g)) . n) ) then n >= N2 by A12, XXREAL_0:2; then A19: g . n >= 0 by A2; n >= N1 by A13, A18, XXREAL_0:2; then A20: f . n >= 0 by A3; (max (f,g)) . n <= (f + g) . n proof percases ( (max (f,g)) . n = f . n or (max (f,g)) . n = g . n ) by A16, XXREAL_0:16; suppose (max (f,g)) . n = f . n ; ::_thesis: (max (f,g)) . n <= (f + g) . n then ((max (f,g)) . n) + 0 <= (f . n) + (g . n) by A19, XREAL_1:7; hence (max (f,g)) . n <= (f + g) . n by SEQ_1:7; ::_thesis: verum end; suppose (max (f,g)) . n = g . n ; ::_thesis: (max (f,g)) . n <= (f + g) . n then ((max (f,g)) . n) + 0 <= (g . n) + (f . n) by A20, XREAL_1:7; hence (max (f,g)) . n <= (f + g) . n by SEQ_1:7; ::_thesis: verum end; end; end; then A21: d * ((max (f,g)) . n) <= d * ((f + g) . n) by A8, XREAL_1:64; n >= N by A10, A18, XXREAL_0:2; then ( t . n <= c * ((f + g) . n) & d * ((f + g) . n) <= t . n ) by A9; hence ( d * ((max (f,g)) . n) <= t . n & t . n <= (2 * c) * ((max (f,g)) . n) ) by A17, A21, XXREAL_0:2; ::_thesis: verum end; 2 * c > 2 * 0 by A7, XREAL_1:68; hence x in Big_Theta (max (f,g)) by A1, A5, A8, A14; ::_thesis: verum end; consider N1 being Element of NAT such that A22: for n being Element of NAT st n >= N1 holds f . n >= 0 by Def2; consider N2 being Element of NAT such that A23: for n being Element of NAT st n >= N2 holds g . n >= 0 by Def2; assume x in Big_Theta (max (f,g)) ; ::_thesis: x in Big_Theta (f + g) then consider t being Element of Funcs (NAT,REAL) such that A24: t = x and A25: 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 * ((max (f,g)) . n) <= t . n & t . n <= c * ((max (f,g)) . n) ) ) ) by A1; consider c, d being Real, N being Element of NAT such that A26: c > 0 and A27: d > 0 and A28: for n being Element of NAT st n >= N holds ( d * ((max (f,g)) . n) <= t . n & t . n <= c * ((max (f,g)) . n) ) by A25; set a = max (N,(max (N1,N2))); A29: max (N1,N2) <= max (N,(max (N1,N2))) by XXREAL_0:25; N2 <= max (N1,N2) by XXREAL_0:25; then A30: N2 <= max (N,(max (N1,N2))) by A29, XXREAL_0:2; A31: N <= max (N,(max (N1,N2))) by XXREAL_0:25; N1 <= max (N1,N2) by XXREAL_0:25; then A32: N1 <= max (N,(max (N1,N2))) by A29, XXREAL_0:2; A33: now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_max_(N,(max_(N1,N2)))_holds_ (_(d_*_(2_"))_*_((f_+_g)_._n)_<=_t_._n_&_t_._n_<=_c_*_((f_+_g)_._n)_) let n be Element of NAT ; ::_thesis: ( n >= max (N,(max (N1,N2))) implies ( (d * (2 ")) * ((f + g) . n) <= t . n & t . n <= c * ((f + g) . n) ) ) assume A34: n >= max (N,(max (N1,N2))) ; ::_thesis: ( (d * (2 ")) * ((f + g) . n) <= t . n & t . n <= c * ((f + g) . n) ) then n >= N1 by A32, XXREAL_0:2; then f . n >= 0 by A22; then A35: (f . n) + (g . n) >= 0 + (g . n) by XREAL_1:7; ( f . n <= max ((f . n),(g . n)) & g . n <= max ((f . n),(g . n)) ) by XXREAL_0:25; then (f . n) + (g . n) <= (1 * (max ((f . n),(g . n)))) + (1 * (max ((f . n),(g . n)))) by XREAL_1:7; then (2 ") * ((f . n) + (g . n)) <= (2 ") * (2 * (max ((f . n),(g . n)))) by XREAL_1:64; then (2 ") * ((f + g) . n) <= max ((f . n),(g . n)) by SEQ_1:7; then d * ((2 ") * ((f + g) . n)) <= d * (max ((f . n),(g . n))) by A27, XREAL_1:64; then A36: d * ((2 ") * ((f + g) . n)) <= d * ((max (f,g)) . n) by Def7; n >= N2 by A30, A34, XXREAL_0:2; then g . n >= 0 by A23; then A37: (f . n) + (g . n) >= (f . n) + 0 by XREAL_1:7; ( (max (f,g)) . n = max ((f . n),(g . n)) & (f + g) . n = (f . n) + (g . n) ) by Def7, SEQ_1:7; then (max (f,g)) . n <= (f + g) . n by A37, A35, XXREAL_0:16; then A38: c * ((max (f,g)) . n) <= c * ((f + g) . n) by A26, XREAL_1:64; n >= N by A31, A34, XXREAL_0:2; then ( t . n <= c * ((max (f,g)) . n) & d * ((max (f,g)) . n) <= t . n ) by A28; hence ( (d * (2 ")) * ((f + g) . n) <= t . n & t . n <= c * ((f + g) . n) ) by A38, A36, XXREAL_0:2; ::_thesis: verum end; d * (2 ") > d * 0 by A27, XREAL_1:68; hence x in Big_Theta (f + g) by A4, A24, A26, A33; ::_thesis: verum end; hence Big_Theta (f + g) = Big_Theta (max (f,g)) by TARSKI:1; ::_thesis: verum end; 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 proof let f, g be eventually-positive Real_Sequence; ::_thesis: ( f /" g is convergent & lim (f /" g) > 0 implies f in Big_Theta g ) assume ( f /" g is convergent & lim (f /" g) > 0 ) ; ::_thesis: f in Big_Theta g then A1: Big_Oh f = Big_Oh g by Th15; then g in Big_Oh f by Th10; then A2: f in Big_Omega g by Th19; f in Big_Oh g by A1, Th10; hence f in Big_Theta g by A2, XBOOLE_0:def_4; ::_thesis: verum end; 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 ) proof let f, g be eventually-positive Real_Sequence; ::_thesis: ( f /" g is convergent & lim (f /" g) = 0 implies ( f in Big_Oh g & not f in Big_Theta g ) ) assume A1: ( f /" g is convergent & lim (f /" g) = 0 ) ; ::_thesis: ( f in Big_Oh g & not f in Big_Theta g ) now__::_thesis:_not_f_in_Big_Theta_g assume f in Big_Theta g ; ::_thesis: contradiction then f in Big_Omega g by XBOOLE_0:def_4; then g in Big_Oh f by Th19; hence contradiction by A1, Th16; ::_thesis: verum end; hence ( f in Big_Oh g & not f in Big_Theta g ) by A1, Th16; ::_thesis: verum end; 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 ) proof let f, g be eventually-positive Real_Sequence; ::_thesis: ( f /" g is divergent_to+infty implies ( f in Big_Omega g & not f in Big_Theta g ) ) assume f /" g is divergent_to+infty ; ::_thesis: ( f in Big_Omega g & not f in Big_Theta g ) then ( not f in Big_Oh g & g in Big_Oh f ) by Th17; hence ( f in Big_Omega g & not f in Big_Theta g ) by Th19, XBOOLE_0:def_4; ::_thesis: verum end; 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 proof set IT = { 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 ) ) ) } ; A1: { 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 functional proof let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in { 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 ) ) ) } or x is set ) assume x in { 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 ) ) ) } ; ::_thesis: x is set then ex t being Element of Funcs (NAT,REAL) st ( x = t & 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 ) ) ) ) ; hence x is set ; ::_thesis: verum end; consider N being Element of NAT such that A2: for n being Element of NAT st n >= N holds f . n >= 0 by Def2; ( f is Element of Funcs (NAT,REAL) & ( for n being Element of NAT st n >= N & n in X holds ( f . n <= 1 * (f . n) & f . n >= 0 ) ) ) by A2, FUNCT_2:8; then f in { 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 ) ) ) } ; then reconsider IT1 = { 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 ) ) ) } as non empty functional set by A1; now__::_thesis:_for_x_being_Element_of_IT1_holds_x_is_Function_of_NAT,REAL let x be Element of IT1; ::_thesis: x is Function of NAT,REAL x in { 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 ) ) ) } ; then ex t being Element of Funcs (NAT,REAL) st ( x = t & 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 ) ) ) ) ; hence x is Function of NAT,REAL ; ::_thesis: verum end; hence { 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 by FUNCT_2:def_12; ::_thesis: verum end; 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 proof set IT = { 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 ) ) ) } ; A1: { 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 functional proof let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in { 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 ) ) ) } or x is set ) assume x in { 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 ) ) ) } ; ::_thesis: x is set then ex t being Element of Funcs (NAT,REAL) st ( x = t & 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 ) ) ) ) ; hence x is set ; ::_thesis: verum end; consider N being Element of NAT such that A2: for n being Element of NAT st n >= N holds f . n >= 0 by Def2; ( f is Element of Funcs (NAT,REAL) & ( for n being Element of NAT st n >= N & n in X holds ( f . n >= 1 * (f . n) & f . n >= 0 ) ) ) by A2, FUNCT_2:8; then f in { 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 ) ) ) } ; then reconsider IT1 = { 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 ) ) ) } as non empty functional set by A1; now__::_thesis:_for_x_being_Element_of_IT1_holds_x_is_Function_of_NAT,REAL let x be Element of IT1; ::_thesis: x is Function of NAT,REAL x in { 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 ) ) ) } ; then ex t being Element of Funcs (NAT,REAL) st ( x = t & 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 ) ) ) ) ; hence x is Function of NAT,REAL ; ::_thesis: verum end; hence { 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 by FUNCT_2:def_12; ::_thesis: verum end; 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 proof set IT = { 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) ) ) ) } ; A1: { 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 functional proof let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in { 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) ) ) ) } or x is set ) assume x in { 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) ) ) ) } ; ::_thesis: x is set then ex t being Element of Funcs (NAT,REAL) st ( x = t & 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) ) ) ) ) ; hence x is set ; ::_thesis: verum end; ( f is Element of Funcs (NAT,REAL) & ( for n being Element of NAT st n >= 0 & n in X holds ( 1 * (f . n) <= f . n & f . n <= 1 * (f . n) ) ) ) by FUNCT_2:8; then f in { 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) ) ) ) } ; then reconsider IT1 = { 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) ) ) ) } as non empty functional set by A1; now__::_thesis:_for_x_being_Element_of_IT1_holds_x_is_Function_of_NAT,REAL let x be Element of IT1; ::_thesis: x is Function of NAT,REAL x in { 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) ) ) ) } ; then ex t being Element of Funcs (NAT,REAL) st ( x = t & 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) ) ) ) ) ; hence x is Function of NAT,REAL ; ::_thesis: verum end; hence { 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 by FUNCT_2:def_12; ::_thesis: verum end; 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)) proof let f be eventually-nonnegative Real_Sequence; ::_thesis: for X being set holds Big_Theta (f,X) = (Big_Oh (f,X)) /\ (Big_Omega (f,X)) let X be set ; ::_thesis: Big_Theta (f,X) = (Big_Oh (f,X)) /\ (Big_Omega (f,X)) now__::_thesis:_for_x_being_set_holds_ (_(_x_in_Big_Theta_(f,X)_implies_x_in_(Big_Oh_(f,X))_/\_(Big_Omega_(f,X))_)_&_(_x_in_(Big_Oh_(f,X))_/\_(Big_Omega_(f,X))_implies_x_in_Big_Theta_(f,X)_)_) let x be set ; ::_thesis: ( ( x in Big_Theta (f,X) implies x in (Big_Oh (f,X)) /\ (Big_Omega (f,X)) ) & ( x in (Big_Oh (f,X)) /\ (Big_Omega (f,X)) implies x in Big_Theta (f,X) ) ) hereby ::_thesis: ( x in (Big_Oh (f,X)) /\ (Big_Omega (f,X)) implies x in Big_Theta (f,X) ) consider N1 being Element of NAT such that A1: for n being Element of NAT st n >= N1 holds f . n >= 0 by Def2; assume x in Big_Theta (f,X) ; ::_thesis: x in (Big_Oh (f,X)) /\ (Big_Omega (f,X)) then consider t being Element of Funcs (NAT,REAL) such that A2: x = t and A3: 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) ) ) ) ; consider c, d being Real, N being Element of NAT such that A4: c > 0 and A5: d > 0 and A6: for n being Element of NAT st n >= N & n in X holds ( d * (f . n) <= t . n & t . n <= c * (f . n) ) by A3; set a = max (N,N1); A7: max (N,N1) >= N1 by XXREAL_0:25; A8: max (N,N1) >= N by XXREAL_0:25; now__::_thesis:_ex_a_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_a_&_n_in_X_holds_ (_d_*_(f_._n)_<=_t_._n_&_t_._n_>=_0_) take a = max (N,N1); ::_thesis: for n being Element of NAT st n >= a & n in X holds ( d * (f . n) <= t . n & t . n >= 0 ) let n be Element of NAT ; ::_thesis: ( n >= a & n in X implies ( d * (f . n) <= t . n & t . n >= 0 ) ) assume that A9: n >= a and A10: n in X ; ::_thesis: ( d * (f . n) <= t . n & t . n >= 0 ) A11: n >= N by A8, A9, XXREAL_0:2; hence d * (f . n) <= t . n by A6, A10; ::_thesis: t . n >= 0 n >= N1 by A7, A9, XXREAL_0:2; then f . n >= 0 by A1; then d * (f . n) >= d * 0 by A5; hence t . n >= 0 by A6, A10, A11; ::_thesis: verum end; then A12: x in Big_Omega (f,X) by A2, A5; now__::_thesis:_ex_a_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_a_&_n_in_X_holds_ (_t_._n_<=_c_*_(f_._n)_&_t_._n_>=_0_) take a = max (N,N1); ::_thesis: for n being Element of NAT st n >= a & n in X holds ( t . n <= c * (f . n) & t . n >= 0 ) let n be Element of NAT ; ::_thesis: ( n >= a & n in X implies ( t . n <= c * (f . n) & t . n >= 0 ) ) assume that A13: n >= a and A14: n in X ; ::_thesis: ( t . n <= c * (f . n) & t . n >= 0 ) A15: n >= N by A8, A13, XXREAL_0:2; hence t . n <= c * (f . n) by A6, A14; ::_thesis: t . n >= 0 n >= N1 by A7, A13, XXREAL_0:2; then f . n >= 0 by A1; then d * (f . n) >= d * 0 by A5; hence t . n >= 0 by A6, A14, A15; ::_thesis: verum end; then x in Big_Oh (f,X) by A2, A4; hence x in (Big_Oh (f,X)) /\ (Big_Omega (f,X)) by A12, XBOOLE_0:def_4; ::_thesis: verum end; assume A16: x in (Big_Oh (f,X)) /\ (Big_Omega (f,X)) ; ::_thesis: x in Big_Theta (f,X) then x in Big_Oh (f,X) by XBOOLE_0:def_4; then consider t being Element of Funcs (NAT,REAL) such that A17: x = t and A18: 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 ) ) ) ; x in Big_Omega (f,X) by A16, XBOOLE_0:def_4; then consider s being Element of Funcs (NAT,REAL) such that A19: x = s and A20: 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 ( s . n >= d * (f . n) & s . n >= 0 ) ) ) ; consider c being Real, N being Element of NAT such that A21: c > 0 and A22: for n being Element of NAT st n >= N & n in X holds ( t . n <= c * (f . n) & t . n >= 0 ) by A18; consider d being Real, N1 being Element of NAT such that A23: d > 0 and A24: for n being Element of NAT st n >= N1 & n in X holds ( s . n >= d * (f . n) & s . n >= 0 ) by A20; set a = max (N,N1); A25: ( max (N,N1) >= N & max (N,N1) >= N1 ) by XXREAL_0:25; now__::_thesis:_ex_a_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_a_&_n_in_X_holds_ (_d_*_(f_._n)_<=_t_._n_&_t_._n_<=_c_*_(f_._n)_) take a = max (N,N1); ::_thesis: for n being Element of NAT st n >= a & n in X holds ( d * (f . n) <= t . n & t . n <= c * (f . n) ) let n be Element of NAT ; ::_thesis: ( n >= a & n in X implies ( d * (f . n) <= t . n & t . n <= c * (f . n) ) ) assume that A26: n >= a and A27: n in X ; ::_thesis: ( d * (f . n) <= t . n & t . n <= c * (f . n) ) ( n >= N & n >= N1 ) by A25, A26, XXREAL_0:2; hence ( d * (f . n) <= t . n & t . n <= c * (f . n) ) by A17, A19, A22, A24, A27; ::_thesis: verum end; hence x in Big_Theta (f,X) by A17, A21, A23; ::_thesis: verum end; hence Big_Theta (f,X) = (Big_Oh (f,X)) /\ (Big_Omega (f,X)) by TARSKI:1; ::_thesis: verum end; 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) proof deffunc H1( Element of NAT ) -> Element of REAL = f . (b * $1); consider h being Function of NAT,REAL such that A1: for n being Element of NAT holds h . n = H1(n) from FUNCT_2:sch_4(); take h ; ::_thesis: for n being Element of NAT holds h . n = f . (b * n) let n be Element of NAT ; ::_thesis: h . n = f . (b * n) thus h . n = f . (b * n) by A1; ::_thesis: verum end; 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 proof let j, k be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds j . n = f . (b * n) ) & ( for n being Element of NAT holds k . n = f . (b * n) ) implies j = k ) assume that A2: for n being Element of NAT holds j . n = f . (b * n) and A3: for n being Element of NAT holds k . n = f . (b * n) ; ::_thesis: j = k now__::_thesis:_for_n_being_Element_of_NAT_holds_j_._n_=_k_._n let n be Element of NAT ; ::_thesis: j . n = k . n thus j . n = f . (b * n) by A2 .= k . n by A3 ; ::_thesis: verum end; hence j = k by FUNCT_2:63; ::_thesis: verum end; 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 proof let f be eventually-nonnegative Real_Sequence; ::_thesis: ( ex b being Element of NAT st ( b >= 2 & f is_smooth_wrt b ) implies f is smooth ) given b being Element of NAT such that A1: b >= 2 and A2: f is_smooth_wrt b ; ::_thesis: f is smooth A3: f is eventually-nondecreasing by A2, Def16; then consider N3 being Element of NAT such that A4: for n being Element of NAT st n >= N3 holds f . n <= f . (n + 1) by Def6; f taken_every b in Big_Oh f by A2, Def16; then consider t being Element of Funcs (NAT,REAL) such that A5: f taken_every b = t and A6: 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 ) ) ) ; consider c being Real, N2 being Element of NAT such that A7: c > 0 and A8: for n being Element of NAT st n >= N2 holds ( t . n <= c * (f . n) & t . n >= 0 ) by A6; set N = max (N2,N3); A9: max (N2,N3) >= N2 by XXREAL_0:25; A10: max (N2,N3) >= N3 by XXREAL_0:25; now__::_thesis:_for_a_being_Element_of_NAT_st_a_>=_2_holds_ f_is_smooth_wrt_a let a be Element of NAT ; ::_thesis: ( a >= 2 implies f is_smooth_wrt a ) set i = [/(log (b,a))\]; A11: [/(log (b,a))\] >= log (b,a) by INT_1:def_7; A12: b > 1 by A1, XXREAL_0:2; A13: b <> 1 by A1; assume A14: a >= 2 ; ::_thesis: f is_smooth_wrt a then a > 1 by XXREAL_0:2; then log (b,a) > log (b,1) by A12, POWER:57; then log (b,a) > 0 by A1, A13, POWER:51; then reconsider i = [/(log (b,a))\] as Element of NAT by A11, INT_1:3; reconsider i1 = b |^ i as Element of NAT ; A15: now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_max_(N2,N3)_holds_ (_(f_taken_every_a)_._n_<=_(c_|^_i)_*_(f_._n)_&_(f_taken_every_a)_._n_>=_0_) let n be Element of NAT ; ::_thesis: ( n >= max (N2,N3) implies ( (f taken_every a) . n <= (c |^ i) * (f . n) & (f taken_every a) . n >= 0 ) ) defpred S1[ Element of NAT ] means f . ((b |^ $1) * n) <= (c |^ $1) * (f . n); a >= 1 by A14, XXREAL_0:2; then A16: a * n >= 1 * n by XREAL_1:64; b to_power (log (b,a)) <= b to_power i by A12, A11, PRE_FF:8; then a <= b |^ i by A1, A13, POWER:def_3; then A17: a * n <= i1 * n by XREAL_1:64; assume A18: n >= max (N2,N3) ; ::_thesis: ( (f taken_every a) . n <= (c |^ i) * (f . n) & (f taken_every a) . n >= 0 ) then A19: n >= N2 by A9, XXREAL_0:2; then A20: t . n <= c * (f . n) by A8; A21: now__::_thesis:_not_f_._n_<_0 assume f . n < 0 ; ::_thesis: contradiction then c * (f . n) < c * 0 by A7, XREAL_1:68; hence contradiction by A8, A19, A20; ::_thesis: verum end; A22: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) set m = (b |^ k) * n; assume A23: f . ((b |^ k) * n) <= (c |^ k) * (f . n) ; ::_thesis: S1[k + 1] reconsider m = (b |^ k) * n as Element of NAT ; c * (f . m) <= c * ((c |^ k) * (f . n)) by A7, A23, XREAL_1:64; then c * (f . m) <= (c * (c |^ k)) * (f . n) ; then c * (f . m) <= ((c to_power 1) * (c to_power k)) * (f . n) by POWER:25; then A24: c * (f . m) <= (c to_power (k + 1)) * (f . n) by A7, POWER:27; m >= N2 proof percases ( k = 0 or k > 0 ) ; suppose k = 0 ; ::_thesis: m >= N2 then (b |^ k) * n = (b to_power 0) * n .= 1 * n by POWER:24 .= n ; hence m >= N2 by A9, A18, XXREAL_0:2; ::_thesis: verum end; suppose k > 0 ; ::_thesis: m >= N2 then b to_power k > 1 by A12, POWER:35; then (b |^ k) * n >= 1 * n by XREAL_1:64; hence m >= N2 by A19, XXREAL_0:2; ::_thesis: verum end; end; end; then (f taken_every b) . m <= c * (f . m) by A5, A8; then A25: f . (b * m) <= c * (f . m) by Def15; f . ((b |^ (k + 1)) * n) = f . ((b to_power (k + 1)) * n) .= f . (((b to_power 1) * (b to_power k)) * n) by A1, POWER:27 .= f . ((b * (b |^ k)) * n) by POWER:25 .= f . (b * ((b |^ k) * n)) ; hence S1[k + 1] by A25, A24, XXREAL_0:2; ::_thesis: verum end; f . ((b |^ 0) * n) = f . ((b to_power 0) * n) .= f . (1 * n) by POWER:24 .= 1 * (f . n) .= (c to_power 0) * (f . n) by POWER:24 ; then A26: S1[ 0 ] ; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A26, A22); then f . ((b |^ i) * n) <= (c |^ i) * (f . n) ; then A27: (f taken_every i1) . n <= (c |^ i) * (f . n) by Def15; A28: n >= N3 by A10, A18, XXREAL_0:2; then a * n >= N3 by A16, XXREAL_0:2; then f . (a * n) <= f . (i1 * n) by A4, A17, Th1; then (f taken_every a) . n <= f . (i1 * n) by Def15; then (f taken_every a) . n <= (f taken_every i1) . n by Def15; hence (f taken_every a) . n <= (c |^ i) * (f . n) by A27, XXREAL_0:2; ::_thesis: (f taken_every a) . n >= 0 f . n <= f . (a * n) by A4, A28, A16, Th1; hence (f taken_every a) . n >= 0 by A21, Def15; ::_thesis: verum end; c |^ i = c to_power i ; then ( f taken_every a is Element of Funcs (NAT,REAL) & c |^ i > 0 ) by A7, FUNCT_2:8, POWER:34; then f taken_every a in Big_Oh f by A15; hence f is_smooth_wrt a by A3, Def16; ::_thesis: verum end; hence f is smooth by Def17; ::_thesis: verum end; 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 proof let f be eventually-nonnegative Real_Sequence; ::_thesis: 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 let t be eventually-nonnegative eventually-nondecreasing Real_Sequence; ::_thesis: 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 let b be Element of NAT ; ::_thesis: ( f is smooth & b >= 2 & t in Big_Oh (f, { (b |^ n) where n is Element of NAT : verum } ) implies t in Big_Oh f ) assume that A1: f is smooth and A2: b >= 2 and A3: t in Big_Oh (f, { (b |^ n) where n is Element of NAT : verum } ) ; ::_thesis: t in Big_Oh f A4: f is_smooth_wrt b by A1, A2, Def17; then f taken_every b in Big_Oh f by Def16; then consider s being Element of Funcs (NAT,REAL) such that A5: f taken_every b = s and A6: ex c being Real ex N being Element of NAT st ( c > 0 & ( for n being Element of NAT st n >= N holds ( s . n <= c * (f . n) & s . n >= 0 ) ) ) ; consider c being Real, N3 being Element of NAT such that A7: c > 0 and A8: for n being Element of NAT st n >= N3 holds ( s . n <= c * (f . n) & s . n >= 0 ) by A6; A9: b > 1 by A2, XXREAL_0:2; f is eventually-nondecreasing by A4, Def16; then consider N1 being Element of NAT such that A10: for m being Element of NAT st m >= N1 holds f . m <= f . (m + 1) by Def6; consider N2 being Element of NAT such that A11: for m being Element of NAT st m >= N2 holds t . m <= t . (m + 1) by Def6; set X = { (b |^ n) where n is Element of NAT : verum } ; consider r being Element of Funcs (NAT,REAL) such that A12: r = t and A13: ex c being Real ex N being Element of NAT st ( c > 0 & ( for n being Element of NAT st n >= N & n in { (b |^ n) where n is Element of NAT : verum } holds ( r . n <= c * (f . n) & r . n >= 0 ) ) ) by A3; consider a being Real, N4 being Element of NAT such that A14: a > 0 and A15: for n being Element of NAT st n >= N4 & n in { (b |^ n) where n is Element of NAT : verum } holds ( r . n <= a * (f . n) & r . n >= 0 ) by A13; set N0 = max ((max (N1,N2)),(max (N3,N4))); A16: max ((max (N1,N2)),(max (N3,N4))) >= max (N1,N2) by XXREAL_0:25; max (N1,N2) >= N2 by XXREAL_0:25; then A17: max ((max (N1,N2)),(max (N3,N4))) >= N2 by A16, XXREAL_0:2; max (N1,N2) >= N1 by XXREAL_0:25; then A18: max ((max (N1,N2)),(max (N3,N4))) >= N1 by A16, XXREAL_0:2; A19: max ((max (N1,N2)),(max (N3,N4))) >= max (N3,N4) by XXREAL_0:25; max (N3,N4) >= N4 by XXREAL_0:25; then A20: max ((max (N1,N2)),(max (N3,N4))) >= N4 by A19, XXREAL_0:2; max (N3,N4) >= N3 by XXREAL_0:25; then A21: max ((max (N1,N2)),(max (N3,N4))) >= N3 by A19, XXREAL_0:2; consider N5 being Element of NAT such that A22: for n being Element of NAT st n >= N5 holds t . n >= 0 by Def2; set N = max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4)))))))); A23: max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4)))))))) >= max (1,(b * (max ((max (N1,N2)),(max (N3,N4)))))) by XXREAL_0:25; max (1,(b * (max ((max (N1,N2)),(max (N3,N4)))))) >= b * (max ((max (N1,N2)),(max (N3,N4)))) by XXREAL_0:25; then A24: max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4)))))))) >= b * (max ((max (N1,N2)),(max (N3,N4)))) by A23, XXREAL_0:2; b >= 1 by A2, XXREAL_0:2; then b * (max ((max (N1,N2)),(max (N3,N4)))) >= 1 * (max ((max (N1,N2)),(max (N3,N4)))) by XREAL_1:64; then A25: max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4)))))))) >= max ((max (N1,N2)),(max (N3,N4))) by A24, XXREAL_0:2; A26: max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4)))))))) >= N5 by XXREAL_0:25; A27: max (1,(b * (max ((max (N1,N2)),(max (N3,N4)))))) >= 1 by XXREAL_0:25; then A28: max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4)))))))) >= 1 by A23, XXREAL_0:2; A29: now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_max_(N5,(max_(1,(b_*_(max_((max_(N1,N2)),(max_(N3,N4))))))))_holds_ (_t_._n_<=_(a_*_c)_*_(f_._n)_&_t_._n_>=_0_) (max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4))))))))) * (b ") >= (b ") * (b * (max ((max (N1,N2)),(max (N3,N4))))) by A24, XREAL_1:64; then (max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4))))))))) * (b ") >= ((b ") * b) * (max ((max (N1,N2)),(max (N3,N4)))) ; then A30: (max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4))))))))) * (b ") >= 1 * (max ((max (N1,N2)),(max (N3,N4)))) by A2, XCMPLX_0:def_7; let n be Element of NAT ; ::_thesis: ( n >= max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4)))))))) implies ( t . n <= (a * c) * (f . n) & t . n >= 0 ) ) set n1 = b to_power [\(log (b,n))/]; assume A31: n >= max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4)))))))) ; ::_thesis: ( t . n <= (a * c) * (f . n) & t . n >= 0 ) then A32: n = b to_power (log (b,n)) by A23, A27, A9, POWER:def_3; n >= 1 by A28, A31, XXREAL_0:2; then log (b,n) >= log (b,1) by A9, PRE_FF:10; then A33: log (b,n) >= 0 by A9, POWER:51; A34: now__::_thesis:_not_[\(log_(b,n))/]_<_0 (log (b,n)) - 1 < [\(log (b,n))/] by INT_1:def_6; then 1 + ((log (b,n)) - 1) < [\(log (b,n))/] + 1 by XREAL_1:6; then A35: (1 + (- 1)) + (log (b,n)) < [\(log (b,n))/] + 1 ; assume [\(log (b,n))/] < 0 ; ::_thesis: contradiction then [\(log (b,n))/] <= - 1 by INT_1:8; hence contradiction by A33, A35, XREAL_1:6; ::_thesis: verum end; then reconsider i = [\(log (b,n))/] as Element of NAT by INT_1:3; reconsider n3 = [\(log (b,n))/] + 1 as Element of NAT by A34, INT_1:3; b to_power [\(log (b,n))/] = b |^ i by POWER:41; then reconsider n1 = b to_power [\(log (b,n))/] as Element of NAT ; set n2 = b * n1; A36: b * n1 = (b to_power 1) * (b to_power [\(log (b,n))/]) by POWER:25 .= b to_power ([\(log (b,n))/] + 1) by A2, POWER:27 ; then b * n1 = b |^ n3 by POWER:41; then A37: b * n1 in { (b |^ n) where n is Element of NAT : verum } ; n * (b ") >= (max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4))))))))) * (b ") by A31, XREAL_1:64; then n * (b ") >= max ((max (N1,N2)),(max (N3,N4))) by A30, XXREAL_0:2; then A38: n / b >= max ((max (N1,N2)),(max (N3,N4))) by XCMPLX_0:def_9; log (b,n) <= [\(log (b,n))/] + 1 by INT_1:29; then A39: n <= b * n1 by A9, A32, A36, PRE_FF:8; then n * (b ") <= (b ") * (b * (b to_power [\(log (b,n))/])) by XREAL_1:64; then n * (b ") <= ((b ") * b) * (b to_power [\(log (b,n))/]) ; then n * (b ") <= 1 * (b to_power [\(log (b,n))/]) by A2, XCMPLX_0:def_7; then n / b <= n1 by XCMPLX_0:def_9; then A40: n1 >= max ((max (N1,N2)),(max (N3,N4))) by A38, XXREAL_0:2; then A41: n1 >= N3 by A21, XXREAL_0:2; A42: n >= max ((max (N1,N2)),(max (N3,N4))) by A25, A31, XXREAL_0:2; then n >= N4 by A20, XXREAL_0:2; then b * n1 >= N4 by A39, XXREAL_0:2; then A43: t . (b * n1) <= a * (f . (b * n1)) by A12, A15, A37; f . (b * n1) = s . n1 by A5, Def15; then f . (b * n1) <= c * (f . n1) by A8, A41; then A44: a * (f . (b * n1)) <= a * (c * (f . n1)) by A14, XREAL_1:64; n >= N2 by A17, A42, XXREAL_0:2; then t . n <= t . (b * n1) by A11, A39, Th1; then t . n <= a * (f . (b * n1)) by A43, XXREAL_0:2; then A45: t . n <= (a * c) * (f . n1) by A44, XXREAL_0:2; A46: n1 >= N1 by A18, A40, XXREAL_0:2; [\(log (b,n))/] <= log (b,n) by INT_1:def_6; then n1 <= n by A9, A32, PRE_FF:8; then (a * c) * (f . n1) <= (a * c) * (f . n) by A10, A7, A14, A46, Th1, XREAL_1:64; hence t . n <= (a * c) * (f . n) by A45, XXREAL_0:2; ::_thesis: t . n >= 0 n >= N5 by A26, A31, XXREAL_0:2; hence t . n >= 0 by A22; ::_thesis: verum end; A47: t is Element of Funcs (NAT,REAL) by FUNCT_2:8; a * c > c * 0 by A7, A14, XREAL_1:68; hence t in Big_Oh f by A47, A29; ::_thesis: verum end; 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 proof let f be eventually-nonnegative Real_Sequence; ::_thesis: 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 let t be eventually-nonnegative eventually-nondecreasing Real_Sequence; ::_thesis: 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 let b be Element of NAT ; ::_thesis: ( f is smooth & b >= 2 & t in Big_Omega (f, { (b |^ n) where n is Element of NAT : verum } ) implies t in Big_Omega f ) assume that A1: f is smooth and A2: b >= 2 and A3: t in Big_Omega (f, { (b |^ n) where n is Element of NAT : verum } ) ; ::_thesis: t in Big_Omega f consider N2 being Element of NAT such that A4: for m being Element of NAT st m >= N2 holds t . m <= t . (m + 1) by Def6; A5: f is_smooth_wrt b by A1, A2, Def17; then f taken_every b in Big_Oh f by Def16; then consider s being Element of Funcs (NAT,REAL) such that A6: f taken_every b = s and A7: ex c being Real ex N being Element of NAT st ( c > 0 & ( for n being Element of NAT st n >= N holds ( s . n <= c * (f . n) & s . n >= 0 ) ) ) ; consider c being Real, N3 being Element of NAT such that A8: c > 0 and A9: for n being Element of NAT st n >= N3 holds ( s . n <= c * (f . n) & s . n >= 0 ) by A7; f is eventually-nondecreasing by A5, Def16; then consider N1 being Element of NAT such that A10: for m being Element of NAT st m >= N1 holds f . m <= f . (m + 1) by Def6; consider N5 being Element of NAT such that A11: for n being Element of NAT st n >= N5 holds t . n >= 0 by Def2; set X = { (b |^ n) where n is Element of NAT : verum } ; consider r being Element of Funcs (NAT,REAL) such that A12: r = t and A13: ex d being Real ex N being Element of NAT st ( d > 0 & ( for n being Element of NAT st n >= N & n in { (b |^ n) where n is Element of NAT : verum } holds ( d * (f . n) <= r . n & r . n >= 0 ) ) ) by A3; consider a being Real, N4 being Element of NAT such that A14: a > 0 and A15: for n being Element of NAT st n >= N4 & n in { (b |^ n) where n is Element of NAT : verum } holds ( a * (f . n) <= r . n & r . n >= 0 ) by A13; A16: b > 1 by A2, XXREAL_0:2; set N0 = max ((max (N1,N2)),(max (N3,N4))); A17: max ((max (N1,N2)),(max (N3,N4))) >= max (N1,N2) by XXREAL_0:25; max (N1,N2) >= N2 by XXREAL_0:25; then A18: max ((max (N1,N2)),(max (N3,N4))) >= N2 by A17, XXREAL_0:2; max (N1,N2) >= N1 by XXREAL_0:25; then A19: max ((max (N1,N2)),(max (N3,N4))) >= N1 by A17, XXREAL_0:2; A20: max ((max (N1,N2)),(max (N3,N4))) >= max (N3,N4) by XXREAL_0:25; max (N3,N4) >= N4 by XXREAL_0:25; then A21: max ((max (N1,N2)),(max (N3,N4))) >= N4 by A20, XXREAL_0:2; max (N3,N4) >= N3 by XXREAL_0:25; then A22: max ((max (N1,N2)),(max (N3,N4))) >= N3 by A20, XXREAL_0:2; set N = max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4)))))))); A23: max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4)))))))) >= max (1,(b * (max ((max (N1,N2)),(max (N3,N4)))))) by XXREAL_0:25; max (1,(b * (max ((max (N1,N2)),(max (N3,N4)))))) >= b * (max ((max (N1,N2)),(max (N3,N4)))) by XXREAL_0:25; then A24: max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4)))))))) >= b * (max ((max (N1,N2)),(max (N3,N4)))) by A23, XXREAL_0:2; b >= 1 by A2, XXREAL_0:2; then b * (max ((max (N1,N2)),(max (N3,N4)))) >= 1 * (max ((max (N1,N2)),(max (N3,N4)))) by XREAL_1:64; then A25: max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4)))))))) >= max ((max (N1,N2)),(max (N3,N4))) by A24, XXREAL_0:2; A26: max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4)))))))) >= N5 by XXREAL_0:25; A27: max (1,(b * (max ((max (N1,N2)),(max (N3,N4)))))) >= 1 by XXREAL_0:25; then A28: max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4)))))))) >= 1 by A23, XXREAL_0:2; A29: now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_max_(N5,(max_(1,(b_*_(max_((max_(N1,N2)),(max_(N3,N4))))))))_holds_ (_(a_*_(c_"))_*_(f_._n)_<=_t_._n_&_t_._n_>=_0_) (max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4))))))))) * (b ") >= (b ") * (b * (max ((max (N1,N2)),(max (N3,N4))))) by A24, XREAL_1:64; then (max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4))))))))) * (b ") >= ((b ") * b) * (max ((max (N1,N2)),(max (N3,N4)))) ; then A30: (max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4))))))))) * (b ") >= 1 * (max ((max (N1,N2)),(max (N3,N4)))) by A2, XCMPLX_0:def_7; let n be Element of NAT ; ::_thesis: ( n >= max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4)))))))) implies ( (a * (c ")) * (f . n) <= t . n & t . n >= 0 ) ) set n1 = b to_power [\(log (b,n))/]; A31: log (b,n) <= [\(log (b,n))/] + 1 by INT_1:29; assume A32: n >= max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4)))))))) ; ::_thesis: ( (a * (c ")) * (f . n) <= t . n & t . n >= 0 ) then A33: n = b to_power (log (b,n)) by A23, A27, A16, POWER:def_3; n >= 1 by A28, A32, XXREAL_0:2; then A34: log (b,n) >= log (b,1) by A16, PRE_FF:10; [\(log (b,n))/] >= 0 proof (log (b,n)) - 1 < [\(log (b,n))/] by INT_1:def_6; then 1 + ((log (b,n)) - 1) < [\(log (b,n))/] + 1 by XREAL_1:6; then A35: (1 + (- 1)) + (log (b,n)) < [\(log (b,n))/] + 1 ; assume [\(log (b,n))/] < 0 ; ::_thesis: contradiction then [\(log (b,n))/] <= - 1 by INT_1:8; then log (b,n) < 0 by A35, XREAL_1:6; hence contradiction by A16, A34, POWER:51; ::_thesis: verum end; then reconsider i = [\(log (b,n))/] as Element of NAT by INT_1:3; A36: b to_power [\(log (b,n))/] = b |^ i by POWER:41; n * (b ") >= (max (N5,(max (1,(b * (max ((max (N1,N2)),(max (N3,N4))))))))) * (b ") by A32, XREAL_1:64; then n * (b ") >= max ((max (N1,N2)),(max (N3,N4))) by A30, XXREAL_0:2; then A37: n / b >= max ((max (N1,N2)),(max (N3,N4))) by XCMPLX_0:def_9; reconsider n1 = b to_power [\(log (b,n))/] as Element of NAT by A36; A38: n1 in { (b |^ n) where n is Element of NAT : verum } by A36; set n2 = b * n1; b * n1 = (b to_power 1) * (b to_power [\(log (b,n))/]) by POWER:25 .= b to_power ([\(log (b,n))/] + 1) by A2, POWER:27 ; then A39: n <= b * n1 by A16, A33, A31, PRE_FF:8; then n * (b ") <= (b ") * (b * (b to_power [\(log (b,n))/])) by XREAL_1:64; then n * (b ") <= ((b ") * b) * (b to_power [\(log (b,n))/]) ; then n * (b ") <= 1 * (b to_power [\(log (b,n))/]) by A2, XCMPLX_0:def_7; then n / b <= n1 by XCMPLX_0:def_9; then A40: n1 >= max ((max (N1,N2)),(max (N3,N4))) by A37, XXREAL_0:2; then n1 >= N4 by A21, XXREAL_0:2; then A41: a * (f . n1) <= t . n1 by A12, A15, A38; n1 >= N3 by A22, A40, XXREAL_0:2; then s . n1 <= c * (f . n1) by A9; then (c ") * (s . n1) <= (c ") * (c * (f . n1)) by A8, XREAL_1:64; then (c ") * (s . n1) <= ((c ") * c) * (f . n1) ; then (c ") * (s . n1) <= 1 * (f . n1) by A8, XCMPLX_0:def_7; then (c ") * (f . (b * n1)) <= f . n1 by A6, Def15; then A42: a * ((c ") * (f . (b * n1))) <= a * (f . n1) by A14, XREAL_1:64; [\(log (b,n))/] <= log (b,n) by INT_1:def_6; then A43: b to_power [\(log (b,n))/] <= b to_power (log (b,n)) by A16, PRE_FF:8; n >= max ((max (N1,N2)),(max (N3,N4))) by A25, A32, XXREAL_0:2; then n >= N1 by A19, XXREAL_0:2; then f . n <= f . (b * n1) by A10, A39, Th1; then A44: (a * (c ")) * (f . n) <= (a * (c ")) * (f . (b * n1)) by A8, A14, XREAL_1:64; n1 >= N2 by A18, A40, XXREAL_0:2; then t . n1 <= t . n by A4, A33, A43, Th1; then a * (f . n1) <= t . n by A41, XXREAL_0:2; then (a * (c ")) * (f . (b * n1)) <= t . n by A42, XXREAL_0:2; hence (a * (c ")) * (f . n) <= t . n by A44, XXREAL_0:2; ::_thesis: t . n >= 0 n >= N5 by A26, A32, XXREAL_0:2; hence t . n >= 0 by A11; ::_thesis: verum end; A45: t is Element of Funcs (NAT,REAL) by FUNCT_2:8; a * (c ") > (c ") * 0 by A8, A14, XREAL_1:68; hence t in Big_Omega f by A45, A29; ::_thesis: verum end; 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 proof let f be eventually-nonnegative Real_Sequence; ::_thesis: 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 let t be eventually-nonnegative eventually-nondecreasing Real_Sequence; ::_thesis: 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 let b be Element of NAT ; ::_thesis: ( f is smooth & b >= 2 & t in Big_Theta (f, { (b |^ n) where n is Element of NAT : verum } ) implies t in Big_Theta f ) assume that A1: ( f is smooth & b >= 2 ) and A2: t in Big_Theta (f, { (b |^ n) where n is Element of NAT : verum } ) ; ::_thesis: t in Big_Theta f set X = { (b |^ n) where n is Element of NAT : verum } ; A3: t in (Big_Oh (f, { (b |^ n) where n is Element of NAT : verum } )) /\ (Big_Omega (f, { (b |^ n) where n is Element of NAT : verum } )) by A2, Th36; then t in Big_Omega (f, { (b |^ n) where n is Element of NAT : verum } ) by XBOOLE_0:def_4; then A4: t in Big_Omega f by A1, Th39; t in Big_Oh (f, { (b |^ n) where n is Element of NAT : verum } ) by A3, XBOOLE_0:def_4; then t in Big_Oh f by A1, Th38; hence t in Big_Theta f by A4, XBOOLE_0:def_4; ::_thesis: verum end; 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 proof set IT = { 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) ) ) } ; A1: now__::_thesis:_not__{__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_empty consider g being set such that A2: g in G by XBOOLE_0:def_1; g is Function of X,REAL by A2, FUNCT_2:def_12; then reconsider g = g as Element of Funcs (X,REAL) by FUNCT_2:8; consider f being set such that A3: f in F by XBOOLE_0:def_1; f is Function of X,REAL by A3, FUNCT_2:def_12; then reconsider f = f as Element of Funcs (X,REAL) by FUNCT_2:8; defpred S1[ Element of X, Real] means $2 = (f . $1) + (g . $1); A4: for x being Element of X ex y being Element of REAL st S1[x,y] ; consider t being Function of X,REAL such that A5: for x being Element of X holds S1[x,t . x] from FUNCT_2:sch_3(A4); reconsider t = t as Element of Funcs (X,REAL) by FUNCT_2:8; t in { 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) ) ) } by A3, A2, A5; hence not { 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 empty ; ::_thesis: verum end; { 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 functional proof let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in { 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) ) ) } or x is set ) assume x in { 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) ) ) } ; ::_thesis: x is set then ex t being Element of Funcs (X,REAL) st ( x = t & 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) ) ) ) ; hence x is set ; ::_thesis: verum end; then reconsider IT1 = { 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) ) ) } as non empty functional set by A1; now__::_thesis:_for_x_being_Element_of_IT1_holds_x_is_Function_of_X,REAL let x be Element of IT1; ::_thesis: x is Function of X,REAL x in { 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) ) ) } ; then ex t being Element of Funcs (X,REAL) st ( x = t & 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) ) ) ) ; hence x is Function of X,REAL ; ::_thesis: verum end; hence { 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 by FUNCT_2:def_12; ::_thesis: verum end; 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 proof set IT = { 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)) ) ) } ; A1: now__::_thesis:_not__{__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_empty consider g being set such that A2: g in G by XBOOLE_0:def_1; g is Function of X,REAL by A2, FUNCT_2:def_12; then reconsider g = g as Element of Funcs (X,REAL) by FUNCT_2:8; consider f being set such that A3: f in F by XBOOLE_0:def_1; f is Function of X,REAL by A3, FUNCT_2:def_12; then reconsider f = f as Element of Funcs (X,REAL) by FUNCT_2:8; defpred S1[ Element of X, Real] means $2 = max ((f . $1),(g . $1)); A4: for x being Element of X ex y being Element of REAL st S1[x,y] ; consider t being Function of X,REAL such that A5: for x being Element of X holds S1[x,t . x] from FUNCT_2:sch_3(A4); reconsider t = t as Element of Funcs (X,REAL) by FUNCT_2:8; t in { 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)) ) ) } by A3, A2, A5; hence not { 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 empty ; ::_thesis: verum end; { 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 functional proof let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in { 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)) ) ) } or x is set ) assume x in { 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)) ) ) } ; ::_thesis: x is set then ex t being Element of Funcs (X,REAL) st ( x = t & 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)) ) ) ) ; hence x is set ; ::_thesis: verum end; then reconsider IT1 = { 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)) ) ) } as non empty functional set by A1; now__::_thesis:_for_x_being_Element_of_IT1_holds_x_is_Function_of_X,REAL let x be Element of IT1; ::_thesis: x is Function of X,REAL x in { 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)) ) ) } ; then ex t being Element of Funcs (X,REAL) st ( x = t & 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)) ) ) ) ; hence x is Function of X,REAL ; ::_thesis: verum end; hence { 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 by FUNCT_2:def_12; ::_thesis: verum end; 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) proof let f, g be eventually-nonnegative Real_Sequence; ::_thesis: (Big_Oh f) + (Big_Oh g) = Big_Oh (f + g) now__::_thesis:_for_x_being_set_holds_ (_(_x_in_(Big_Oh_f)_+_(Big_Oh_g)_implies_x_in_Big_Oh_(f_+_g)_)_&_(_x_in_Big_Oh_(f_+_g)_implies_x_in_(Big_Oh_f)_+_(Big_Oh_g)_)_) let x be set ; ::_thesis: ( ( x in (Big_Oh f) + (Big_Oh g) implies x in Big_Oh (f + g) ) & ( x in Big_Oh (f + g) implies x in (Big_Oh f) + (Big_Oh g) ) ) hereby ::_thesis: ( x in Big_Oh (f + g) implies x in (Big_Oh f) + (Big_Oh g) ) assume x in (Big_Oh f) + (Big_Oh g) ; ::_thesis: x in Big_Oh (f + g) then consider t being Element of Funcs (NAT,REAL) such that A1: x = t and A2: ex f9, g9 being Element of Funcs (NAT,REAL) st ( f9 in Big_Oh f & g9 in Big_Oh g & ( for n being Element of NAT holds t . n = (f9 . n) + (g9 . n) ) ) ; consider f9, g9 being Element of Funcs (NAT,REAL) such that A3: f9 in Big_Oh f and A4: g9 in Big_Oh g and A5: for n being Element of NAT holds t . n = (f9 . n) + (g9 . n) by A2; consider r being Element of Funcs (NAT,REAL) such that A6: r = f9 and A7: ex c being Real ex N being Element of NAT st ( c > 0 & ( for n being Element of NAT st n >= N holds ( r . n <= c * (f . n) & r . n >= 0 ) ) ) by A3; consider c being Real, N1 being Element of NAT such that A8: c > 0 and A9: for n being Element of NAT st n >= N1 holds ( r . n <= c * (f . n) & r . n >= 0 ) by A7; consider s being Element of Funcs (NAT,REAL) such that A10: s = g9 and A11: ex c being Real ex N being Element of NAT st ( c > 0 & ( for n being Element of NAT st n >= N holds ( s . n <= c * (g . n) & s . n >= 0 ) ) ) by A4; consider d being Real, N2 being Element of NAT such that A12: d > 0 and A13: for n being Element of NAT st n >= N2 holds ( s . n <= d * (g . n) & s . n >= 0 ) by A11; set N = max (N1,N2); set e = max (c,d); A14: max (N1,N2) >= N2 by XXREAL_0:25; A15: max (N1,N2) >= N1 by XXREAL_0:25; A16: now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_max_(N1,N2)_holds_ (_t_._n_<=_(max_(c,d))_*_((f_+_g)_._n)_&_t_._n_>=_0_) let n be Element of NAT ; ::_thesis: ( n >= max (N1,N2) implies ( t . n <= (max (c,d)) * ((f + g) . n) & t . n >= 0 ) ) assume A17: n >= max (N1,N2) ; ::_thesis: ( t . n <= (max (c,d)) * ((f + g) . n) & t . n >= 0 ) then A18: n >= N1 by A15, XXREAL_0:2; then f9 . n >= 0 by A6, A9; then A19: (f9 . n) + (g9 . n) >= 0 + (g9 . n) by XREAL_1:6; r . n <= c * (f . n) by A9, A18; then (f . n) * c >= 0 * c by A9, A18; then f . n >= 0 by A8, XREAL_1:68; then A20: c * (f . n) <= (max (c,d)) * (f . n) by XREAL_1:64, XXREAL_0:25; r . n <= c * (f . n) by A9, A18; then r . n <= (max (c,d)) * (f . n) by A20, XXREAL_0:2; then A21: (r . n) + (s . n) <= ((max (c,d)) * (f . n)) + (s . n) by XREAL_1:6; A22: n >= N2 by A14, A17, XXREAL_0:2; then s . n <= d * (g . n) by A13; then (g . n) * d >= 0 * d by A13, A22; then g . n >= 0 by A12, XREAL_1:68; then A23: d * (g . n) <= (max (c,d)) * (g . n) by XREAL_1:64, XXREAL_0:25; s . n <= d * (g . n) by A13, A22; then s . n <= (max (c,d)) * (g . n) by A23, XXREAL_0:2; then ((max (c,d)) * (f . n)) + (s . n) <= ((max (c,d)) * (f . n)) + ((max (c,d)) * (g . n)) by XREAL_1:6; then (r . n) + (s . n) <= (max (c,d)) * ((f . n) + (g . n)) by A21, XXREAL_0:2; then (r . n) + (s . n) <= (max (c,d)) * ((f + g) . n) by SEQ_1:7; hence t . n <= (max (c,d)) * ((f + g) . n) by A5, A6, A10; ::_thesis: t . n >= 0 0 + (g9 . n) >= 0 by A10, A13, A22; hence t . n >= 0 by A5, A19; ::_thesis: verum end; max (c,d) > 0 by A8, XXREAL_0:25; hence x in Big_Oh (f + g) by A1, A16; ::_thesis: verum end; assume x in Big_Oh (f + g) ; ::_thesis: x in (Big_Oh f) + (Big_Oh g) then consider t being Element of Funcs (NAT,REAL) such that A24: x = t and A25: 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 + g) . n) & t . n >= 0 ) ) ) ; consider c being Real, N3 being Element of NAT such that A26: c > 0 and A27: for n being Element of NAT st n >= N3 holds ( t . n <= c * ((f + g) . n) & t . n >= 0 ) by A25; consider N1 being Element of NAT such that A28: for n being Element of NAT st n >= N1 holds f . n >= 0 by Def2; consider N2 being Element of NAT such that A29: for n being Element of NAT st n >= N2 holds g . n >= 0 by Def2; set N = max (N3,(max (N1,N2))); A30: max (N3,(max (N1,N2))) >= max (N1,N2) by XXREAL_0:25; defpred S1[ Element of NAT , Real] means ( ( t . $1 <= c * (f . $1) implies $2 = 0 ) & ( c * (f . $1) < t . $1 implies $2 = (t . $1) - (c * (f . $1)) ) ); A31: for x being Element of NAT ex y being Element of REAL st S1[x,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of REAL st S1[n,y] percases ( t . n <= c * (f . n) or c * (f . n) < t . n ) ; suppose t . n <= c * (f . n) ; ::_thesis: ex y being Element of REAL st S1[n,y] hence ex y being Element of REAL st S1[n,y] ; ::_thesis: verum end; suppose c * (f . n) < t . n ; ::_thesis: ex y being Element of REAL st S1[n,y] hence ex y being Element of REAL st S1[n,y] ; ::_thesis: verum end; end; end; consider g9 being Function of NAT,REAL such that A32: for x being Element of NAT holds S1[x,g9 . x] from FUNCT_2:sch_3(A31); A33: max (N3,(max (N1,N2))) >= N3 by XXREAL_0:25; A34: g9 is Element of Funcs (NAT,REAL) by FUNCT_2:8; max (N1,N2) >= N2 by XXREAL_0:25; then A35: max (N3,(max (N1,N2))) >= N2 by A30, XXREAL_0:2; now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_max_(N3,(max_(N1,N2)))_holds_ (_g9_._n_<=_c_*_(g_._n)_&_g9_._n_>=_0_) let n be Element of NAT ; ::_thesis: ( n >= max (N3,(max (N1,N2))) implies ( g9 . b1 <= c * (g . b1) & g9 . b1 >= 0 ) ) assume A36: n >= max (N3,(max (N1,N2))) ; ::_thesis: ( g9 . b1 <= c * (g . b1) & g9 . b1 >= 0 ) then n >= N3 by A33, XXREAL_0:2; then A37: t . n <= c * ((f + g) . n) by A27; n >= N2 by A35, A36, XXREAL_0:2; then g . n >= 0 by A29; then A38: 0 * (g . n) <= c * (g . n) by A26; percases ( t . n <= c * (f . n) or t . n > c * (f . n) ) ; suppose t . n <= c * (f . n) ; ::_thesis: ( g9 . b1 <= c * (g . b1) & g9 . b1 >= 0 ) hence ( g9 . n <= c * (g . n) & g9 . n >= 0 ) by A32, A38; ::_thesis: verum end; supposeA39: t . n > c * (f . n) ; ::_thesis: ( g9 . b1 <= c * (g . b1) & g9 . b1 >= 0 ) t . n <= c * ((f . n) + (g . n)) by A37, SEQ_1:7; then t . n <= (c * (f . n)) + (c * (g . n)) ; then A40: (t . n) - (c * (f . n)) <= c * (g . n) by XREAL_1:20; t . n > 0 + (c * (f . n)) by A39; then (t . n) - (c * (f . n)) >= 0 by XREAL_1:19; hence ( g9 . n <= c * (g . n) & g9 . n >= 0 ) by A32, A40; ::_thesis: verum end; end; end; then A41: g9 in Big_Oh g by A26, A34; defpred S2[ Element of NAT , Real] means ( ( t . $1 <= c * (f . $1) implies $2 = t . $1 ) & ( c * (f . $1) < t . $1 implies $2 = c * (f . $1) ) ); A42: for x being Element of NAT ex y being Element of REAL st S2[x,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of REAL st S2[n,y] percases ( t . n <= c * (f . n) or c * (f . n) < t . n ) ; suppose t . n <= c * (f . n) ; ::_thesis: ex y being Element of REAL st S2[n,y] hence ex y being Element of REAL st S2[n,y] ; ::_thesis: verum end; suppose c * (f . n) < t . n ; ::_thesis: ex y being Element of REAL st S2[n,y] hence ex y being Element of REAL st S2[n,y] ; ::_thesis: verum end; end; end; consider f9 being Function of NAT,REAL such that A43: for x being Element of NAT holds S2[x,f9 . x] from FUNCT_2:sch_3(A42); A44: now__::_thesis:_for_n_being_Element_of_NAT_holds_t_._n_=_(f9_._n)_+_(g9_._n) let n be Element of NAT ; ::_thesis: t . b1 = (f9 . b1) + (g9 . b1) percases ( t . n <= c * (f . n) or c * (f . n) < t . n ) ; supposeA45: t . n <= c * (f . n) ; ::_thesis: t . b1 = (f9 . b1) + (g9 . b1) then g9 . n = 0 by A32; hence t . n = (f9 . n) + (g9 . n) by A43, A45; ::_thesis: verum end; suppose c * (f . n) < t . n ; ::_thesis: (f9 . b1) + (g9 . b1) = t . b1 then ( f9 . n = c * (f . n) & g9 . n = (t . n) - (c * (f . n)) ) by A43, A32; hence (f9 . n) + (g9 . n) = t . n ; ::_thesis: verum end; end; end; A46: f9 is Element of Funcs (NAT,REAL) by FUNCT_2:8; max (N1,N2) >= N1 by XXREAL_0:25; then A47: max (N3,(max (N1,N2))) >= N1 by A30, XXREAL_0:2; now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_max_(N3,(max_(N1,N2)))_holds_ (_f9_._n_<=_c_*_(f_._n)_&_f9_._n_>=_0_) let n be Element of NAT ; ::_thesis: ( n >= max (N3,(max (N1,N2))) implies ( f9 . b1 <= c * (f . b1) & f9 . b1 >= 0 ) ) assume A48: n >= max (N3,(max (N1,N2))) ; ::_thesis: ( f9 . b1 <= c * (f . b1) & f9 . b1 >= 0 ) then n >= N3 by A33, XXREAL_0:2; then A49: t . n >= 0 by A27; n >= N1 by A47, A48, XXREAL_0:2; then A50: f . n >= 0 by A28; percases ( t . n <= c * (f . n) or t . n > c * (f . n) ) ; suppose t . n <= c * (f . n) ; ::_thesis: ( f9 . b1 <= c * (f . b1) & f9 . b1 >= 0 ) hence ( f9 . n <= c * (f . n) & f9 . n >= 0 ) by A43, A49; ::_thesis: verum end; suppose t . n > c * (f . n) ; ::_thesis: ( f9 . b1 <= c * (f . b1) & f9 . b1 >= 0 ) hence ( f9 . n <= c * (f . n) & f9 . n >= 0 ) by A26, A43, A50; ::_thesis: verum end; end; end; then f9 in Big_Oh f by A26, A46; hence x in (Big_Oh f) + (Big_Oh g) by A24, A46, A34, A41, A44; ::_thesis: verum end; hence (Big_Oh f) + (Big_Oh g) = Big_Oh (f + g) by TARSKI:1; ::_thesis: verum end; 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)) proof let f, g be eventually-nonnegative Real_Sequence; ::_thesis: max ((Big_Oh f),(Big_Oh g)) = Big_Oh (max (f,g)) now__::_thesis:_for_x_being_set_holds_ (_(_x_in_max_((Big_Oh_f),(Big_Oh_g))_implies_x_in_Big_Oh_(max_(f,g))_)_&_(_x_in_Big_Oh_(max_(f,g))_implies_x_in_max_((Big_Oh_f),(Big_Oh_g))_)_) let x be set ; ::_thesis: ( ( x in max ((Big_Oh f),(Big_Oh g)) implies x in Big_Oh (max (f,g)) ) & ( x in Big_Oh (max (f,g)) implies x in max ((Big_Oh f),(Big_Oh g)) ) ) hereby ::_thesis: ( x in Big_Oh (max (f,g)) implies x in max ((Big_Oh f),(Big_Oh g)) ) assume x in max ((Big_Oh f),(Big_Oh g)) ; ::_thesis: x in Big_Oh (max (f,g)) then consider t being Element of Funcs (NAT,REAL) such that A1: x = t and A2: ex f9, g9 being Element of Funcs (NAT,REAL) st ( f9 in Big_Oh f & g9 in Big_Oh g & ( for n being Element of NAT holds t . n = max ((f9 . n),(g9 . n)) ) ) ; consider f9, g9 being Element of Funcs (NAT,REAL) such that A3: f9 in Big_Oh f and A4: g9 in Big_Oh g and A5: for n being Element of NAT holds t . n = max ((f9 . n),(g9 . n)) by A2; consider s being Element of Funcs (NAT,REAL) such that A6: s = g9 and A7: ex c being Real ex N being Element of NAT st ( c > 0 & ( for n being Element of NAT st n >= N holds ( s . n <= c * (g . n) & s . n >= 0 ) ) ) by A4; consider d being Real, N2 being Element of NAT such that A8: d > 0 and A9: for n being Element of NAT st n >= N2 holds ( s . n <= d * (g . n) & s . n >= 0 ) by A7; consider r being Element of Funcs (NAT,REAL) such that A10: r = f9 and A11: ex c being Real ex N being Element of NAT st ( c > 0 & ( for n being Element of NAT st n >= N holds ( r . n <= c * (f . n) & r . n >= 0 ) ) ) by A3; consider c being Real, N1 being Element of NAT such that A12: c > 0 and A13: for n being Element of NAT st n >= N1 holds ( r . n <= c * (f . n) & r . n >= 0 ) by A11; set e = max (c,d); A14: max (c,d) > 0 by A12, XXREAL_0:25; set N = max (N1,N2); A15: max (N1,N2) >= N2 by XXREAL_0:25; A16: max (N1,N2) >= N1 by XXREAL_0:25; now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_max_(N1,N2)_holds_ (_t_._n_<=_(max_(c,d))_*_((max_(f,g))_._n)_&_t_._n_>=_0_) let n be Element of NAT ; ::_thesis: ( n >= max (N1,N2) implies ( t . n <= (max (c,d)) * ((max (f,g)) . n) & t . n >= 0 ) ) assume A17: n >= max (N1,N2) ; ::_thesis: ( t . n <= (max (c,d)) * ((max (f,g)) . n) & t . n >= 0 ) then A18: n >= N1 by A16, XXREAL_0:2; then r . n <= c * (f . n) by A13; then (f . n) * c >= 0 * c by A13, A18; then f . n >= 0 by A12, XREAL_1:68; then A19: c * (f . n) <= (max (c,d)) * (f . n) by XREAL_1:64, XXREAL_0:25; A20: n >= N2 by A15, A17, XXREAL_0:2; then s . n <= d * (g . n) by A9; then (g . n) * d >= 0 * d by A9, A20; then g . n >= 0 by A8, XREAL_1:68; then A21: d * (g . n) <= (max (c,d)) * (g . n) by XREAL_1:64, XXREAL_0:25; s . n <= d * (g . n) by A9, A20; then A22: s . n <= (max (c,d)) * (g . n) by A21, XXREAL_0:2; (max (c,d)) * (g . n) <= (max (c,d)) * (max ((f . n),(g . n))) by A14, XREAL_1:64, XXREAL_0:25; then A23: s . n <= (max (c,d)) * (max ((f . n),(g . n))) by A22, XXREAL_0:2; r . n <= c * (f . n) by A13, A18; then A24: r . n <= (max (c,d)) * (f . n) by A19, XXREAL_0:2; (max (c,d)) * (f . n) <= (max (c,d)) * (max ((f . n),(g . n))) by A14, XREAL_1:64, XXREAL_0:25; then r . n <= (max (c,d)) * (max ((f . n),(g . n))) by A24, XXREAL_0:2; then max ((r . n),(s . n)) <= (max (c,d)) * (max ((f . n),(g . n))) by A23, XXREAL_0:28; then max ((r . n),(s . n)) <= (max (c,d)) * ((max (f,g)) . n) by Def7; hence t . n <= (max (c,d)) * ((max (f,g)) . n) by A5, A10, A6; ::_thesis: t . n >= 0 ( max ((f9 . n),(g9 . n)) >= f9 . n & f9 . n >= 0 ) by A10, A13, A18, XXREAL_0:25; hence t . n >= 0 by A5; ::_thesis: verum end; hence x in Big_Oh (max (f,g)) by A1, A14; ::_thesis: verum end; assume x in Big_Oh (max (f,g)) ; ::_thesis: x in max ((Big_Oh f),(Big_Oh g)) then consider t being Element of Funcs (NAT,REAL) such that A25: x = t and A26: 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 * ((max (f,g)) . n) & t . n >= 0 ) ) ) ; consider c being Real, N3 being Element of NAT such that A27: c > 0 and A28: for n being Element of NAT st n >= N3 holds ( t . n <= c * ((max (f,g)) . n) & t . n >= 0 ) by A26; consider N1 being Element of NAT such that A29: for n being Element of NAT st n >= N1 holds f . n >= 0 by Def2; consider N2 being Element of NAT such that A30: for n being Element of NAT st n >= N2 holds g . n >= 0 by Def2; set N = max (N3,(max (N1,N2))); defpred S1[ Element of NAT , Real] means ( ( ( f . $1 >= g . $1 or $1 < max (N3,(max (N1,N2))) ) implies $2 = t . $1 ) & ( f . $1 < g . $1 & $1 >= max (N3,(max (N1,N2))) implies $2 = 0 ) ); defpred S2[ Element of NAT , Real] means ( ( f . $1 >= g . $1 & $1 >= max (N3,(max (N1,N2))) implies $2 = 0 ) & ( ( f . $1 < g . $1 or $1 < max (N3,(max (N1,N2))) ) implies $2 = t . $1 ) ); A31: for x being Element of NAT ex y being Element of REAL st S1[x,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of REAL st S1[n,y] percases ( f . n >= g . n or f . n < g . n ) ; suppose f . n >= g . n ; ::_thesis: ex y being Element of REAL st S1[n,y] hence ex y being Element of REAL st S1[n,y] ; ::_thesis: verum end; supposeA32: f . n < g . n ; ::_thesis: ex y being Element of REAL st S1[n,y] thus ex y being Element of REAL st S1[n,y] ::_thesis: verum proof percases ( n < max (N3,(max (N1,N2))) or n >= max (N3,(max (N1,N2))) ) ; suppose n < max (N3,(max (N1,N2))) ; ::_thesis: ex y being Element of REAL st S1[n,y] hence ex y being Element of REAL st S1[n,y] ; ::_thesis: verum end; suppose n >= max (N3,(max (N1,N2))) ; ::_thesis: ex y being Element of REAL st S1[n,y] hence ex y being Element of REAL st S1[n,y] by A32; ::_thesis: verum end; end; end; end; end; end; consider f9 being Function of NAT,REAL such that A33: for x being Element of NAT holds S1[x,f9 . x] from FUNCT_2:sch_3(A31); A34: for x being Element of NAT ex y being Element of REAL st S2[x,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of REAL st S2[n,y] percases ( f . n >= g . n or f . n < g . n ) ; supposeA35: f . n >= g . n ; ::_thesis: ex y being Element of REAL st S2[n,y] thus ex y being Element of REAL st S2[n,y] ::_thesis: verum proof percases ( n < max (N3,(max (N1,N2))) or n >= max (N3,(max (N1,N2))) ) ; suppose n < max (N3,(max (N1,N2))) ; ::_thesis: ex y being Element of REAL st S2[n,y] hence ex y being Element of REAL st S2[n,y] ; ::_thesis: verum end; suppose n >= max (N3,(max (N1,N2))) ; ::_thesis: ex y being Element of REAL st S2[n,y] hence ex y being Element of REAL st S2[n,y] by A35; ::_thesis: verum end; end; end; end; suppose f . n < g . n ; ::_thesis: ex y being Element of REAL st S2[n,y] hence ex y being Element of REAL st S2[n,y] ; ::_thesis: verum end; end; end; consider g9 being Function of NAT,REAL such that A36: for x being Element of NAT holds S2[x,g9 . x] from FUNCT_2:sch_3(A34); A37: max (N3,(max (N1,N2))) >= N3 by XXREAL_0:25; A38: now__::_thesis:_for_n_being_Element_of_NAT_holds_t_._n_=_max_((f9_._n),(g9_._n)) let n be Element of NAT ; ::_thesis: t . b1 = max ((f9 . b1),(g9 . b1)) percases ( n < max (N3,(max (N1,N2))) or n >= max (N3,(max (N1,N2))) ) ; suppose n < max (N3,(max (N1,N2))) ; ::_thesis: t . b1 = max ((f9 . b1),(g9 . b1)) then ( f9 . n = t . n & g9 . n = t . n ) by A33, A36; hence t . n = max ((f9 . n),(g9 . n)) ; ::_thesis: verum end; supposeA39: n >= max (N3,(max (N1,N2))) ; ::_thesis: t . b1 = max ((f9 . b1),(g9 . b1)) then A40: n >= N3 by A37, XXREAL_0:2; thus t . n = max ((f9 . n),(g9 . n)) ::_thesis: verum proof percases ( f . n >= g . n or f . n < g . n ) ; supposeA41: f . n >= g . n ; ::_thesis: t . n = max ((f9 . n),(g9 . n)) A42: t . n >= 0 by A28, A40; ( f9 . n = t . n & g9 . n = 0 ) by A33, A36, A39, A41; hence t . n = max ((f9 . n),(g9 . n)) by A42, XXREAL_0:def_10; ::_thesis: verum end; supposeA43: f . n < g . n ; ::_thesis: t . n = max ((f9 . n),(g9 . n)) A44: t . n >= 0 by A28, A40; ( f9 . n = 0 & g9 . n = t . n ) by A33, A36, A39, A43; hence t . n = max ((f9 . n),(g9 . n)) by A44, XXREAL_0:def_10; ::_thesis: verum end; end; end; end; end; end; A45: g9 is Element of Funcs (NAT,REAL) by FUNCT_2:8; A46: max (N3,(max (N1,N2))) >= max (N1,N2) by XXREAL_0:25; max (N1,N2) >= N2 by XXREAL_0:25; then A47: max (N3,(max (N1,N2))) >= N2 by A46, XXREAL_0:2; now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_max_(N3,(max_(N1,N2)))_holds_ (_g9_._n_<=_c_*_(g_._n)_&_g9_._n_>=_0_) let n be Element of NAT ; ::_thesis: ( n >= max (N3,(max (N1,N2))) implies ( g9 . b1 <= c * (g . b1) & g9 . b1 >= 0 ) ) assume A48: n >= max (N3,(max (N1,N2))) ; ::_thesis: ( g9 . b1 <= c * (g . b1) & g9 . b1 >= 0 ) then n >= N3 by A37, XXREAL_0:2; then A49: ( t . n >= 0 & t . n <= c * ((max (f,g)) . n) ) by A28; n >= N2 by A47, A48, XXREAL_0:2; then g . n >= 0 by A30; then A50: 0 * (g . n) <= c * (g . n) by A27; percases ( f . n >= g . n or f . n < g . n ) ; suppose f . n >= g . n ; ::_thesis: ( g9 . b1 <= c * (g . b1) & g9 . b1 >= 0 ) hence ( g9 . n <= c * (g . n) & g9 . n >= 0 ) by A36, A48, A50; ::_thesis: verum end; supposeA51: f . n < g . n ; ::_thesis: ( g9 . b1 <= c * (g . b1) & g9 . b1 >= 0 ) then max ((f . n),(g . n)) = g . n by XXREAL_0:def_10; then (max (f,g)) . n = g . n by Def7; hence ( g9 . n <= c * (g . n) & g9 . n >= 0 ) by A36, A49, A51; ::_thesis: verum end; end; end; then A52: g9 in Big_Oh g by A27, A45; A53: f9 is Element of Funcs (NAT,REAL) by FUNCT_2:8; max (N1,N2) >= N1 by XXREAL_0:25; then A54: max (N3,(max (N1,N2))) >= N1 by A46, XXREAL_0:2; now__::_thesis:_for_n_being_Element_of_NAT_st_n_>=_max_(N3,(max_(N1,N2)))_holds_ (_f9_._n_<=_c_*_(f_._n)_&_f9_._n_>=_0_) let n be Element of NAT ; ::_thesis: ( n >= max (N3,(max (N1,N2))) implies ( f9 . b1 <= c * (f . b1) & f9 . b1 >= 0 ) ) assume A55: n >= max (N3,(max (N1,N2))) ; ::_thesis: ( f9 . b1 <= c * (f . b1) & f9 . b1 >= 0 ) then n >= N3 by A37, XXREAL_0:2; then A56: ( t . n >= 0 & t . n <= c * ((max (f,g)) . n) ) by A28; n >= N1 by A54, A55, XXREAL_0:2; then f . n >= 0 by A29; then A57: 0 * (f . n) <= c * (f . n) by A27; percases ( f . n >= g . n or f . n < g . n ) ; supposeA58: f . n >= g . n ; ::_thesis: ( f9 . b1 <= c * (f . b1) & f9 . b1 >= 0 ) then max ((f . n),(g . n)) = f . n by XXREAL_0:def_10; then (max (f,g)) . n = f . n by Def7; hence ( f9 . n <= c * (f . n) & f9 . n >= 0 ) by A33, A56, A58; ::_thesis: verum end; suppose f . n < g . n ; ::_thesis: ( f9 . b1 <= c * (f . b1) & f9 . b1 >= 0 ) hence ( f9 . n <= c * (f . n) & f9 . n >= 0 ) by A33, A55, A57; ::_thesis: verum end; end; end; then f9 in Big_Oh f by A27, A53; hence x in max ((Big_Oh f),(Big_Oh g)) by A25, A53, A45, A52, A38; ::_thesis: verum end; hence max ((Big_Oh f),(Big_Oh g)) = Big_Oh (max (f,g)) by TARSKI:1; ::_thesis: verum end; 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 proof set IT = { 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) ) ) } ; A1: now__::_thesis:_not__{__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_empty consider g being set such that A2: g in G by XBOOLE_0:def_1; g is Function of NAT,REAL by A2, FUNCT_2:def_12; then reconsider g = g as Element of Funcs (NAT,REAL) by FUNCT_2:8; consider f being set such that A3: f in F by XBOOLE_0:def_1; f is Function of NAT,REAL by A3, FUNCT_2:def_12; then reconsider f = f as Element of Funcs (NAT,REAL) by FUNCT_2:8; defpred S1[ Element of NAT , Real] means $2 = (f . $1) to_power (g . $1); A4: for x being Element of NAT ex y being Element of REAL st S1[x,y] ; consider t being Function of NAT,REAL such that A5: for x being Element of NAT holds S1[x,t . x] from FUNCT_2:sch_3(A4); reconsider t = t as Element of Funcs (NAT,REAL) by FUNCT_2:8; for x being Element of NAT st x >= 0 holds t . x = (f . x) to_power (g . x) by A5; then t in { 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) ) ) } by A3, A2; hence not { 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 empty ; ::_thesis: verum end; { 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 functional proof let x be set ; :: according to FUNCT_1:def_13 ::_thesis: ( not x in { 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) ) ) } or x is set ) assume x in { 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) ) ) } ; ::_thesis: x is set then ex t being Element of Funcs (NAT,REAL) st ( x = t & 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) ) ) ) ; hence x is set ; ::_thesis: verum end; then reconsider IT1 = { 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) ) ) } as non empty functional set by A1; now__::_thesis:_for_x_being_Element_of_IT1_holds_x_is_Function_of_NAT,REAL let x be Element of IT1; ::_thesis: x is Function of NAT,REAL x in { 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) ) ) } ; then ex t being Element of Funcs (NAT,REAL) st ( x = t & 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) ) ) ) ; hence x is Function of NAT,REAL ; ::_thesis: verum end; hence { 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 by FUNCT_2:def_12; ::_thesis: verum end; 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) ) ) } ;