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