:: Asymptotic notation. Part I: Theory
:: by Richard Krueger , Piotr Rudnicki and Paul Shelley
::
:: Received November 4, 1999
:: Copyright (c) 1999-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, REAL_1, SUBSET_1, NAT_1, XBOOLE_0, XXREAL_0, FINSET_1,
TARSKI, CARD_1, ARYTM_3, ARYTM_1, SEQ_1, FUNCT_1, VALUED_1, RELAT_1,
SEQ_2, ORDINAL2, COMPLEX1, LIMFUNC1, FUNCT_2, INT_1, POWER, NEWTON,
ASYMPT_0, FUNCT_7, ASYMPT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
COMPLEX1, REAL_1, FUNCT_1, FUNCT_2, XXREAL_0, XXREAL_2, INT_1, NAT_1,
VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, NEWTON, POWER, FUNCOP_1, FINSET_1,
LIMFUNC1;
constructors REAL_1, NAT_1, SEQ_2, LIMFUNC1, NEWTON, POWER, VALUED_1,
PARTFUN1, XXREAL_2, RELSET_1, FUNCOP_1, COMSEQ_2, SQUARE_1, SEQ_1,
NUMBERS;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FINSET_1, NUMBERS, XXREAL_0,
XREAL_0, NAT_1, INT_1, MEMBERED, VALUED_0, VALUED_1, FUNCT_2, POWER,
XXREAL_2, FUNCT_1, NEWTON;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, FUNCT_1;
equalities VALUED_1;
theorems TARSKI, FUNCT_2, INT_1, NAT_1, SEQ_1, SEQ_2, ABSVALUE, LIMFUNC1,
POWER, PRE_FF, XREAL_0, XBOOLE_0, XCMPLX_0, XCMPLX_1, XREAL_1, COMPLEX1,
XXREAL_0, ORDINAL1, VALUED_1, XXREAL_2;
schemes FUNCT_2, FINSEQ_1, NAT_1;
begin :: Preliminaries
reserve c, c1, d for Real,
k for Nat,
n, m, N, n1, N1, N2, N3, N4, N5, M for Element of NAT,
x for set;
scheme
FinSegRng1{m, n() -> Nat, X() -> non empty set, F(set) -> Element of X()} :
{F(i) where i is Element of NAT: m() <= i & i <= n()} is finite non empty
Subset of X()
provided
A1: m() <= n()
proof
defpred P[Nat] means m()<=$1;
set S = {F(i) where i is Nat: i<=n() & P[i]};
A2: F(m()) in S by A1;
set S1 = {F(i) where i is Element of NAT: m()<=i & i<=n()};
A3: now
let x be object;
hereby
assume x in S;
then consider i being Nat such that
A4: x = F(i) & i<=n() & P[i];
reconsider j=i as Element of NAT by ORDINAL1:def 12;
x = F(j) by A4;
hence x in S1 by A4;
end;
assume x in S1;
then ex i being Element of NAT st x = F(i) & m()<=i & i<=n();
hence x in S;
end;
A5: S c= X()
proof
let x be object;
assume x in S;
then ex n1 being Nat st x = F(n1) & n1 <= n() & n1 >= m();
hence thesis;
end;
S is finite from FINSEQ_1:sch 6;
hence thesis by A3,A2,A5,TARSKI:2;
end;
scheme
FinImInit1{N() -> Nat, X() -> non empty set, F(set) -> Element of X()} : {F(
n) where n is Element of NAT: n <= N()} is finite non empty Subset of X() proof
set T = {F(n) where n is Element of NAT: 0<=n & n<=N()};
set S = {F(n) where n is Element of NAT: n <= N()};
A1: now
let x be object;
hereby
assume x in S;
then ex n being Element of NAT st x = F(n) & n <= N();
hence x in T;
end;
assume x in T;
then ex n being Element of NAT st x = F(n) & 0 <= n & n <= N();
hence x in S;
end;
A2: 0 <= N();
T is finite non empty Subset of X() from FinSegRng1(A2);
hence thesis by A1,TARSKI:2;
end;
scheme
FinImInit2{N() -> Nat, X() -> non empty set, F(set) -> Element of X()} : {F(
n) where n is Element of NAT: n < N()} is finite non empty Subset of X()
provided
A1: N() > 0
proof
set S = {F(n) where n is Element of NAT: n < N()};
consider m being Nat such that
A2: N() = m+1 by A1,NAT_1:6;
reconsider m as Element of NAT by ORDINAL1:def 12;
set T = {F(n) where n is Element of NAT: n <= m};
A3: now
let x be object;
hereby
assume x in S;
then consider n being Element of NAT such that
A4: x = F(n) and
A5: n < N();
n <= m by A2,A5,NAT_1:13;
hence x in T by A4;
end;
assume x in T;
then consider n being Element of NAT such that
A6: x = F(n) and
A7: n <= m;
n < m+1 by A7,NAT_1:13;
hence x in S by A2,A6;
end;
T is finite non empty Subset of X() from FinImInit1;
hence thesis by A3,TARSKI:2;
end;
definition
let c be Real;
attr c is logbase means
c > 0 & c <> 1;
end;
reconsider jj=1, dwa=2 as Element of REAL by XREAL_0:def 1;
registration
cluster positive for Real;
existence
proof
take jj;
thus thesis;
end;
cluster negative for Real;
existence
proof
take -jj;
thus thesis by XXREAL_0:def 7;
end;
cluster logbase for Real;
existence
proof
take dwa;
thus thesis;
end;
cluster non negative for Real;
existence by XXREAL_0:def 7;
cluster non positive for Real;
existence by XXREAL_0:def 6;
cluster non logbase for Real;
existence
proof
take jj;
thus thesis;
end;
end;
definition
let f be Real_Sequence;
attr f is eventually-nonnegative means
:Def2:
ex N being Nat st for n being Nat st n >= N holds f.n >= 0;
attr f is positive means
:Def3:
for n being Nat holds f.n > 0;
attr f is eventually-positive means
:Def4:
ex N being Nat st for n being Nat st n >= N holds f.n > 0;
attr f is eventually-nonzero means
:Def5:
ex N being Nat st for n being Nat st n >= N holds f.n <> 0;
attr f is eventually-nondecreasing means
:Def6:
ex N being Nat st for n being Nat st n >= N holds f.n <= f.(n+1);
end;
registration
cluster eventually-nonnegative eventually-nonzero positive
eventually-positive eventually-nondecreasing for Real_Sequence;
existence
proof
take f = seq_const 1;
thus f is eventually-nonnegative
proof
take 0;
let n be Nat;
assume n >= 0;
thus thesis by SEQ_1:57;
end;
thus f is eventually-nonzero
proof
take 0;
let n be Nat;
thus thesis by SEQ_1:57;
end;
thus f is positive
by SEQ_1:57;
thus f is eventually-positive
proof
take 0;
let n be Nat;
assume
n >= 0;
thus thesis by SEQ_1:57;
end;
thus f is eventually-nondecreasing
proof
take 0;
let n be Nat;
assume
n >= 0;
f.n = 1 by SEQ_1:57;
hence thesis by SEQ_1:57;
end;
end;
end;
registration
cluster positive -> eventually-positive for Real_Sequence;
coherence
proof
let f be Real_Sequence;
assume
A1: f is positive;
take 0;
let n be Nat;
assume n >= 0;
thus thesis by A1;
end;
cluster eventually-positive -> eventually-nonnegative eventually-nonzero
for Real_Sequence;
coherence
proof
let f be Real_Sequence;
assume f is eventually-positive;
then consider N being Nat such that
A2: for n being Nat st n >= N holds f.n > 0;
thus f is eventually-nonnegative
proof
take N;
let n be Nat;
assume n >= N;
hence thesis by A2;
end;
thus f is eventually-nonzero
proof
take N;
let n be Nat;
assume n >= N;
hence thesis by A2;
end;
end;
cluster eventually-nonnegative eventually-nonzero -> eventually-positive
for Real_Sequence;
coherence
proof
let f be Real_Sequence;
assume that
A3: f is eventually-nonnegative and
A4: f is eventually-nonzero;
consider N being Nat such that
A5: for n being Nat st n >= N holds f.n >= 0 by A3;
consider M being Nat such that
A6: for n being Nat st n >= M holds f.n <> 0 by A4;
reconsider a = max( N, M ) as Nat by TARSKI:1;
take a;
let n be Nat;
assume
A7: n >= a;
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 thesis by A5,A8;
end;
end;
definition
let f,g be eventually-nonnegative Real_Sequence;
redefine func f+g -> eventually-nonnegative Real_Sequence; :: redefines + (VALUED_1, definition)
coherence
proof
consider M being Nat such that
A1: for n being Nat st n >= M holds g.n >= 0 by Def2;
consider N being Nat such that
A2: for n being Nat st n >= N holds f.n >= 0 by Def2;
reconsider a = max(N, M) as Nat by TARSKI:1;
f+g is eventually-nonnegative
proof
take a;
let n be Nat;
assume
A3: n >= a;
a >= M by XXREAL_0:25;
then n >= M by A3,XXREAL_0:2;
then
A4: g.n >= 0 by A1;
a >= 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 thesis by SEQ_1:7;
end;
hence thesis;
end;
end;
definition
let f be eventually-nonnegative Real_Sequence, c be positive Real;
redefine func c(#)f -> eventually-nonnegative Real_Sequence; :: redefines (#) (VALUED_1, definition)
coherence
proof
consider N being Nat such that
A1: for n being Nat st n >= N holds f.n >= 0 by Def2;
c(#)f is eventually-nonnegative
proof
take N;
let n be Nat;
assume n >= N;
then f.n >= 0 by A1;
then c*f.n >= c*0;
hence thesis by SEQ_1:9;
end;
hence thesis;
end;
end;
definition
let f be eventually-nonnegative Real_Sequence, c be non negative Real;
redefine func c+f -> eventually-nonnegative Real_Sequence; :: redefines + (VALUED_1, definition)
coherence
proof
consider N being Nat such that
A1: for n being Nat st n >= N holds f.n >= 0 by Def2;
c+f is eventually-nonnegative
proof
take N;
let n be Nat;
A2: n in NAT by ORDINAL1:def 12;
assume n >= N;
then f.n >= 0 by A1;
then c + f.n >= 0 + 0;
hence thesis by VALUED_1:2,A2;
end;
hence thesis;
end;
end;
definition
let f be eventually-nonnegative Real_Sequence, c be positive Real;
redefine func c+f -> eventually-positive Real_Sequence; :: redefines + (VALUED_1, definition)
coherence
proof
consider N being Nat such that
A1: for n being Nat st n >= N holds f.n >= 0 by Def2;
c+f is eventually-positive
proof
take N;
let n be Nat;
A2: n in NAT by ORDINAL1:def 12;
assume n >= N;
then f.n >= 0 by A1;
then c + f.n > 0 + 0;
hence thesis by VALUED_1:2,A2;
end;
hence thesis;
end;
end;
definition
let f,g be Real_Sequence;
func max(f, g) -> Real_Sequence means
:Def7:
for n being Nat holds it.n = max( f.n, g .n );
existence
proof
deffunc F(Nat) = In(max(f.$1, g.$1),REAL);
consider h being sequence of REAL such that
A1: for n being Element of NAT holds h.n = F(n) from FUNCT_2:sch 4;
take h;
let n be Nat;
n in NAT by ORDINAL1:def 12;
then h.n = F(n) by A1;
hence thesis;
end;
uniqueness
proof
let j, k be Real_Sequence such that
A2: for n being Nat holds j.n = max( f.n, g.n ) and
A3: for n being Nat holds k.n = max( f.n, g.n );
now
let n;
thus j.n = max( f.n, g.n ) by A2
.= k.n by A3;
end;
hence j = k by FUNCT_2:63;
end;
commutativity;
end;
registration
let f be Real_Sequence, g be eventually-nonnegative Real_Sequence;
cluster max(f, g) -> eventually-nonnegative;
coherence
proof
consider N being Nat such that
A1: for n being Nat st n >= N holds g.n >= 0 by Def2;
take N;
let n be Nat;
assume n >= N;
then
A2: g.n >= 0 by A1;
max( f.n, g.n ) >= g.n by XXREAL_0:25;
hence thesis by A2,Def7;
end;
end;
registration
let f be Real_Sequence, g be eventually-positive Real_Sequence;
cluster max(f, g) -> eventually-positive;
coherence
proof
consider N being Nat such that
A1: for n being Nat st n >= N holds g.n > 0 by Def4;
take N;
let n be Nat;
assume n >= N;
then g.n > 0 by A1;
then max( f.n, g.n ) > 0 by XXREAL_0:25;
hence thesis by Def7;
end;
end;
definition
let f,g be Real_Sequence;
pred g majorizes f means
ex N st for n st n >= N holds f.n <= g.n;
end;
Lm1: for f,g being Real_Sequence, n being Nat holds (f/"g).n = f.n/g.n
proof
let f,g be Real_Sequence, n be Nat;
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;
end;
theorem Th1: :: Problem 3.25
for f being Real_Sequence, N being Nat
st for n being Nat st n>= N holds f.n <= f.(n+1)
for n,m being Nat st N <= n & n <= m
holds f.n <= f.m
proof
let f be Real_Sequence, N be Nat;
assume
A1: for n being Nat st n >= N holds f.n <= f.(n+1);
let n,m be Nat;
defpred P[Nat] means f.n <= f.$1;
assume
A2: n >= N;
A3: for m be Nat st m >= n & P[m] holds P[m+1]
proof
let m be Nat;
assume that
A4: m >= n and
A5: f.n <= f.m;
m in NAT & m >= N by A2,A4,ORDINAL1:def 12,XXREAL_0:2;
then f.m <= f.(m+1) by A1;
hence thesis by A5,XXREAL_0:2;
end;
A6: P[n];
for m be Nat st m >= n holds P[m] from NAT_1:sch 8(A6,A3);
hence thesis;
end;
theorem Th2:
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;
set s = f/"g;
set als = |.lim s.|;
set ls = lim s;
assume that
A1: f/"g is convergent and
A2: lim(f/"g) <> 0;
consider n1 being Nat such that
A3: for m being Nat st n1<=m holds als/2<|.s.m.| by A1,A2,SEQ_2:16;
A4: 0<als by A2,COMPLEX1:47;
then 0*0<als*als by XREAL_1:96;
then
A5: 0<(als*als)/2 by XREAL_1:215;
consider N2 being Nat such that
A6: for n being Nat st n >= N2 holds g.n > 0 by Def4;
consider N1 being Nat such that
A7: for n being Nat st n >= N1 holds f.n > 0 by Def4;
A8: 0<>als by A2,COMPLEX1:47;
A9: now
set N3=N1+N2;
let p be Real;
set N4=N3+n1;
A10: 0<>als/2 by A2,COMPLEX1:47;
A11: (p*(als/2))/(als/2 ) = (p*(als/2))*(als/2 )" by XCMPLX_0:def 9
.=p*((als/2)*(als/2 )")
.=p*1 by A10,XCMPLX_0:def 7
.=p;
assume
A12: 0 < p;
then 0*0<p*((als*als)/2) by A5,XREAL_1:96;
then consider n2 being Nat such that
A13: for m being Nat st n2<=m holds |.s.m-ls.|<p*((als*als)/2)
by A1,SEQ_2:def 7;
take n=N4+n2;
let m being Nat such that
A14: n<=m;
set asm = |.s.m.|;
A15: (p*((als*als)/2))/(asm*als) =(p*(2"*(als*als)))*(asm*als)" by
XCMPLX_0:def 9
.=p*2"*((als*als)*(als*asm)")
.=p*2"*((als*als)*(als"*asm")) by XCMPLX_1:204
.=p*2"*(als*(als*als")*asm")
.=p*2"*(als*1*asm") by A8,XCMPLX_0:def 7
.=p*(als/2)*asm"
.=(p*(als/2))/asm by XCMPLX_0:def 9;
n1 <= N4 by NAT_1:12;
then n1<=n by NAT_1:12;
then n1<=m by A14,XXREAL_0:2;
then
A16: als/2<asm by A3;
A17: 0<als/2 by A4,XREAL_1:215;
then 0*0<p*(als/2) by A12,XREAL_1:96;
then
A18: (p*(als/2))/asm < (p*(als/2))/(als/2) by A16,A17,XREAL_1:76;
N2 <= N3 by NAT_1:12;
then N2 <= N4 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 <= N3 by NAT_1:12;
then N1 <= N4 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: s.m<>0 by Lm1;
then s.m*ls<>0 by A2,XCMPLX_1:6;
then 0<|.s.m*ls.| by COMPLEX1:47;
then
A21: 0<asm*als by COMPLEX1:65;
n2<=n by NAT_1:12;
then n2<=m by A14,XXREAL_0:2;
then |.s.m-ls.|<p*((als*als)/2) by A13;
then
A22: |.s.m-ls.|/(asm*als) < (p*((als*als)/2))/(asm*als) by A21,XREAL_1:74;
|.(g/"f).m-ls".| = |.(g.m/f.m)-ls".| by Lm1
.=|.(f.m/g.m)"-ls".| by XCMPLX_1:213
.=|.(s.m)"-ls".| by Lm1
.=|.s.m-ls.|/(asm*als) by A2,A20,SEQ_2:2;
hence |.(g/"f).m-ls".|<p by A22,A15,A18,A11,XXREAL_0:2;
end;
hence g/"f is convergent by SEQ_2:def 6;
hence thesis by A9,SEQ_2:def 7;
end;
theorem Th3:
for f being eventually-nonnegative Real_Sequence st f is
convergent holds 0 <= lim f
proof
let f be eventually-nonnegative Real_Sequence such that
A1: f is convergent and
A2: not 0<=(lim f);
0<-(lim f) by A2,XREAL_1:58;
then consider N1 being Nat such that
A3: for m being Nat st N1<=m holds |.f.m-(lim f).|<-(lim f)
by A1,SEQ_2:def 7;
consider N being Nat such that
A4: for n being Nat st n >= N holds 0<=f.n by Def2;
set n1 = max( N, N1 );
A0: n1 is Nat by TARSKI:1;
A5: now
assume f.n1=0;
then |.f.n1-(lim f).| = -(lim f) by A2,ABSVALUE:def 1;
hence contradiction by A0,A3,XXREAL_0:25;
end;
|.f.n1-(lim f).|<=-(lim f) by A0,A3,XXREAL_0:25;
then f.n1-(lim f)<=-(lim f) by ABSVALUE:5;
then f.n1-(lim f)+(lim f)<=-(lim f)+(lim f) by XREAL_1:6;
hence contradiction by A0, A4,A5,XXREAL_0:25;
end;
theorem Th4:
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;
assume that
A1: f is convergent & g is convergent and
A2: ex N st for n st n >= N holds f.n <= g.n;
consider N such that
A3: for n st n >= N holds f.n <= g.n by A2;
now
let n be Nat;
A4: n in NAT by ORDINAL1:def 12;
assume n >= N;
then f.n <= g.n by A3,A4;
then
A5: 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 A5;
end;
then
A6: g-f is eventually-nonnegative;
A7: 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 A6,Th3;
then 0 + (lim(f)) <= (lim(g)) - (lim(f)) + (lim(f)) by A7,XREAL_1:6;
hence thesis;
end;
theorem Th5:
for f being Real_Sequence, g being eventually-nonzero
Real_Sequence st f/"g is divergent_to+infty holds g/"f is convergent & lim(g/"f
)=0
proof
let f be Real_Sequence, g be eventually-nonzero Real_Sequence;
consider N1 being Nat such that
A1: for n being Nat st n >= N1 holds g.n <> 0 by Def5;
assume
A2: f/"g is divergent_to+infty;
A3: now
let p be Real such that
A4: p>0;
reconsider w = 1/p as Real;
consider N being Nat such that
A5: for n being Nat st n>=N holds w<(f/"g).n by A2,LIMFUNC1:def 4;
reconsider a = max(N, N1) as Nat by TARSKI:1;
take a;
let n be Nat;
assume
A6: n >= a;
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
assume g.n*(f.n)" > g.n*0;
then g.n*f".n > 0 by VALUED_1:10;
hence (g/"f).n-0 >= 0 by SEQ_1:8;
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
assume g.n*(f.n)" < p*f.n*(f.n)";
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;
end;
per cases by A10;
suppose
A13: g.n > 0;
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 |.(g/"f).n-0.|<p by A12,A9,A13,A14,ABSVALUE:def 1,XREAL_1:68;
end;
suppose
A15: g.n < 0;
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 |.(g/"f).n-0.|<p by A12,A9,A15,A16,ABSVALUE:def 1,XREAL_1:69;
end;
end;
hence g/"f is convergent by SEQ_2:def 6;
hence thesis by A3,SEQ_2:def 7;
end;
begin :: A Notation for "the order of" (Section 3.2)
definition
let f be eventually-nonnegative Real_Sequence;
func Big_Oh(f) -> FUNCTION_DOMAIN of NAT, REAL equals
{ t where t is Element of Funcs(NAT, REAL) :
ex c,N st c > 0 & for n st n >= N holds t.n <= c*f.n & t.n >= 0 };
coherence
proof
set IT = { t where t is Element of Funcs(NAT, REAL) : ex c,N st c > 0 &
for n st n >= N holds t.n <= c*f.n & t.n >= 0 };
A1: IT is functional
proof
let x be object;
assume x in IT;
then
ex t being Element of Funcs(NAT, REAL) st x = t & ex c,N st c > 0 &
for n st n >= N holds t.n <= c*f.n & t.n >= 0;
hence thesis;
end;
consider N being Nat such that
A2: for n being Nat st n >= N holds f.n >= 0 by Def2;
A3: N in NAT by ORDINAL1:def 12;
A4: f is Element of Funcs(NAT, REAL) by FUNCT_2:8;
for n st n >= N holds f.n <= 1*f.n & f.n >= 0 by A2;
then
ex c,N st c > 0 &
for n st n >= N holds f.n <= c*f.n & f.n >= 0 by A3;
then f in IT by A4;
then reconsider IT1 = IT as functional non empty set by A1;
now
let x be Element of IT1;
x in IT;
then ex t being Element of Funcs(NAT, REAL) st x = t & ex c,N st c > 0 &
for n st n >= N holds t.n <= c*f.n & t.n >= 0;
hence x is sequence of REAL;
end;
hence thesis by FUNCT_2:def 12;
end;
end;
theorem Th6:
for x being set, f being eventually-nonnegative Real_Sequence st
x in Big_Oh(f) holds x is eventually-nonnegative Real_Sequence
proof
let t be set, f be eventually-nonnegative Real_Sequence;
assume t in Big_Oh(f);
then consider s being Element of Funcs(NAT, REAL) such that
A1: s = t and
A2: ex c,N st c > 0 & for n st n >= N holds s.n <= c*f.n & s.n >= 0;
reconsider t9 = t as Real_Sequence by A1;
consider c,N such that
c > 0 and
A3: for n st n >= N holds s.n <= c*f.n & s.n >= 0 by A2;
now
take N;
let n be Nat;
A4: n in NAT by ORDINAL1:def 12;
assume n >= N;
hence t9.n >= 0 by A1,A3,A4;
end;
hence thesis by Def2;
end;
theorem :: Threshold Rule (page 81)
for f being positive Real_Sequence, t being eventually-nonnegative
Real_Sequence holds t in Big_Oh(f) iff ex c st c > 0 & for n holds t.n <= c*f.n
proof
let f be positive Real_Sequence, t be eventually-nonnegative Real_Sequence;
hereby
assume t in Big_Oh(f);
then consider s being Element of Funcs(NAT, REAL) such that
A1: t = s and
A2: ex c,N st c > 0 & for n st n >= N holds s.n <= c*f.n & s.n >= 0;
consider c,N such that
A3: c > 0 and
A4: for n st n >= N holds s.n <= c*f.n & s.n >= 0 by A2;
per cases;
suppose
A5: N = 0;
take c;
thus c > 0 by A3;
let n;
thus t.n <= c*f.n by A1,A4,A5;
end;
suppose
A6: N > 0;
deffunc F(Element of NAT) = t.$1 / f.$1;
reconsider B = { F(n) : n < N } as finite non empty Subset of REAL from
FinImInit2(A6);
set b = max B;
A7: for n st n < N holds t.n <= b*f.n
proof
let n;
A8: f.n > 0 by Def3;
assume n < N;
then t.n / f.n in B;
then t.n / f.n <= b by XXREAL_2:def 8;
then t.n / f.n * f.n <= b * f.n by A8,XREAL_1:64;
hence thesis by A8,XCMPLX_1:87;
end;
thus ex c st c > 0 & for n holds t.n <= c*f.n
proof
per cases;
suppose
A9: b <= c;
take c;
thus c > 0 by A3;
let n;
thus t.n <= c*f.n
proof
per cases;
suppose
A10: n < N;
f.n > 0 by Def3;
then
A11: b*f.n <= c*f.n by A9,XREAL_1:64;
t.n <= b*f.n by A7,A10;
hence thesis by A11,XXREAL_0:2;
end;
suppose
n >= N;
hence thesis by A1,A4;
end;
end;
end;
suppose
A12: b > c;
reconsider b as Element of REAL by XREAL_0:def 1;
take b;
thus b > 0 by A3,A12;
let n;
thus t.n <= b*f.n
proof
per cases;
suppose
n < N;
hence thesis by A7;
end;
suppose
A13: n >= 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 thesis by A14,XXREAL_0:2;
end;
end;
end;
end;
end;
end;
given c such that
A15: c > 0 and
A16: for n holds t.n <= c*f.n;
consider N being Nat such that
A17: for n being Nat st n >= N holds t.n >= 0 by Def2;
A18: N in NAT by ORDINAL1:def 12;
t is Element of Funcs(NAT, REAL) & for n 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,A18;
end;
theorem :: Generalized Threshold Rule (page 81)
for f being eventually-positive Real_Sequence, t being
eventually-nonnegative Real_Sequence, N being Element of NAT st t in Big_Oh(f)
& for n st n >= N holds f.n > 0 holds ex c st c > 0 & for n st n >= N holds t.n
<= c*f.n
proof
let f be eventually-positive Real_Sequence, t be eventually-nonnegative
Real_Sequence, N be Element of NAT;
assume that
A1: t in Big_Oh(f) and
A2: for n st n >= N holds f.n > 0;
deffunc T(Element of NAT) = t.$1;
deffunc F(Element of NAT) = f.$1;
ex s being Element of Funcs(NAT, REAL) st t = s & ex c,N st c > 0 & for n
st n >= N holds s.n <= c*f.n & s.n >= 0 by A1;
then consider c2 being Real, M such that
A3: c2 > 0 and
A4: for n st n >= M holds t.n <= c2*f.n & t.n >= 0;
set fset = { F(n) : N <= n & n <= max(M,N) };
A5: N <= max(M,N) by XXREAL_0:25;
fset is finite non empty Subset of REAL from FinSegRng1(A5);
then reconsider fset as finite non empty Subset of REAL;
set F = min(fset);
A6: M <= max(M,N) by XXREAL_0:25;
set tset = { T(n) : N <= n & n <= max(M,N) };
tset is finite non empty Subset of REAL from FinSegRng1(A5);
then reconsider tset as finite non empty Subset of REAL;
set T = max(tset);
set c1 = T / F;
reconsider c = max(c1,c2) as Element of REAL by XREAL_0:def 1;
take c;
thus c > 0 by A3,XXREAL_0:25;
let n;
assume
A7: n >= N;
then
A8: f.n > 0 by A2;
A9: f.n <> 0 by A2,A7;
F in fset by XXREAL_2:def 7;
then
A10: ex n1 being Element of NAT st f.n1 = F & n1 >= N & n1 <= max(M,N);
then
A11: F > 0 by A2;
A12: F <> 0 by A2,A10;
per cases;
suppose
N >= M;
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 thesis by A13,XXREAL_0:2;
end;
suppose
A14: N <= M;
thus t.n <= c*f.n
proof
per cases;
suppose
n <= M;
then
A15: n <= max(M,N) by A6,XXREAL_0:2;
then t.n in tset by A7;
then
A16: t.n <= T by XXREAL_2:def 8;
f.n in fset by A7,A15;
then
A17: f.n >= F by XXREAL_2:def 7;
t.M in tset by A6,A14;
then
A18: t.M <= T by XXREAL_2:def 8;
t.M >= 0 by A4;
then
A19: c1*f.n >= c1*F by A11,A18,A17,XREAL_1:64;
now
assume t.n/f.n > c1;
then t.n/f.n*f.n > c1*f.n by A8,XREAL_1:68;
then t.n > c1*f.n by A9,XCMPLX_1:87;
then T > c1*f.n by A16,XXREAL_0:2;
hence contradiction by A12,A19,XCMPLX_1:87;
end;
then t.n/f.n*f.n <= c1*f.n by A8,XREAL_1:64;
then
A20: t.n <= c1*f.n by A9,XCMPLX_1:87;
c1*f.n <= c*f.n by A8,XREAL_1:64,XXREAL_0:25;
hence thesis by A20,XXREAL_0:2;
end;
suppose
A21: n >= M;
A22: c2*f.n <= c*f.n by A8,XREAL_1:64,XXREAL_0:25;
t.n <= c2*f.n by A4,A21;
hence thesis by A22,XXREAL_0:2;
end;
end;
end;
end;
theorem :: Maximum Rule (page 81)
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;
now
let x be object;
hereby
assume x in Big_Oh( f + g );
then consider t being Element of Funcs(NAT, REAL) such that
A1: t = x and
A2: ex c,N st c > 0 & for n st n >= N holds t.n <= c*(f+g).n & t.n >= 0;
consider c,N such that
A3: c > 0 and
A4: for n st n >= N holds t.n <= c*(f+g).n & t.n >= 0 by A2;
A5: now
let n;
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;
then t.n <= c*(f+g).n by A4;
hence t.n <= (2*c)*max(f,g).n by A8,XXREAL_0:2;
thus t.n >= 0 by A4,A9;
end;
2*c > 2*0 by A3,XREAL_1:68;
hence x in Big_Oh( max( f, g ) ) by A1,A5;
end;
assume x in Big_Oh( max( f, g ) );
then consider t being Element of Funcs(NAT, REAL) such that
A10: t = x and
A11: ex c,N st c > 0 & for n st n >= N holds t.n <= c*max(f,g).n & t.n >= 0;
consider c,N1 such that
A12: c > 0 and
A13: for n st n >= N1 holds t.n <= c*max(f,g).n & t.n >= 0 by A11;
consider M1 being Nat such that
A14: for n being Nat st n >= M1 holds f.n >= 0 by Def2;
consider M2 being Nat such that
A15: for n being Nat st n >= M2 holds g.n >= 0 by Def2;
set N = max(N1, max(M1, M2));
A16: max(M1,M2) <= N by XXREAL_0:25;
M2 <= max(M1,M2) by XXREAL_0:25;
then
A17: M2 <= N by A16,XXREAL_0:2;
A18: N1 <= N by XXREAL_0:25;
M1 <= max(M1,M2) by XXREAL_0:25;
then
A19: M1 <= N by A16,XXREAL_0:2;
reconsider N as Element of NAT by ORDINAL1:def 12;
ex c,N st c > 0 & for n st n >= N
holds t.n <= c*(f+g).n & t.n >= 0
proof
take c,N;
thus c > 0 by A12;
let n;
A20: max(f.n,g.n) = f.n or max(f.n,g.n) = g.n by XXREAL_0:16;
assume
A21: n >= N;
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;
thus t.n >= 0 by A13,A25;
end;
hence x in Big_Oh( f + g ) by A10;
end;
hence thesis by TARSKI:2;
end;
theorem Th10: :: Reflexivity of Big_Oh (page 83; Problem 3.9)
for f being eventually-nonnegative Real_Sequence holds f in Big_Oh(f)
proof
let f be eventually-nonnegative Real_Sequence;
consider N being Nat such that
A1: for n being Nat st n >= N holds f.n >= 0 by Def2;
reconsider N as Element of NAT by ORDINAL1:def 12;
f is Element of Funcs(NAT, REAL) & for n st n >= N holds f.n <= 1*f.n &
f.n >= 0 by A1,FUNCT_2:8;
hence thesis;
end;
theorem Th11:
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;
assume f in Big_Oh(g);
then consider t being Element of Funcs(NAT, REAL) such that
A1: t = f and
A2: ex c,N st c > 0 & for n 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 st n >= Nt holds t.n <= ct*g.n & t.n >= 0 by A2;
consider Ng being Nat such that
A4: for n being Nat st n >= Ng holds g.n >= 0 by Def2;
let x be object;
assume x in Big_Oh(f);
then consider s being Element of Funcs(NAT, REAL) such that
A5: s = x and
A6: ex c,N st c > 0 & for n 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 st n >= Ns holds s.n <= cs*f.n & s.n >= 0 by A6;
now
take c = max(cs*ct,max(cs,ct));
c >= max(cs,ct) by XXREAL_0:25;
hence c > 0 by A7,XXREAL_0:25;
reconsider N = max(max(Ns, Nt), Ng) as Element of NAT
by ORDINAL1:def 12;
take N;
let n;
assume
A9: n >= N;
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;
thus s.n >= 0 by A8,A13;
end;
hence thesis by A5;
end;
theorem Th12: :: Transitivity of Big_Oh (page 83; Problem 3.10)
for f,g,h being eventually-nonnegative Real_Sequence holds f in
Big_Oh(g) & g in Big_Oh(h) implies f in Big_Oh(h)
proof
let f,g,h be eventually-nonnegative Real_Sequence;
assume that
A1: f in Big_Oh(g) and
A2: g in Big_Oh(h);
Big_Oh(g) c= Big_Oh(h) by A2,Th11;
hence thesis by A1;
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;
hereby
assume f in Big_Oh(g) & g in Big_Oh(f);
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;
end;
assume Big_Oh(f) = Big_Oh(g);
hence thesis by Th10;
end;
theorem
for f being eventually-nonnegative Real_Sequence, c being positive
Real holds Big_Oh(f) = Big_Oh(c(#)f)
proof
let f be eventually-nonnegative Real_Sequence, c be positive Real;
now
let x be object;
hereby
assume x in Big_Oh(f);
then consider t being Element of Funcs(NAT, REAL) such that
A1: x = t and
A2: ex c,N st c > 0 & for n st n >= N holds t.n <= c*f.n & t.n >= 0;
consider c1,N such that
A3: c1 > 0 and
A4: for n st n >= N holds t.n <= c1*f.n & t.n >= 0 by A2;
A5: now
let n;
assume
A6: n >= N;
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;
end;
c1*c" > 0*c" by A3,XREAL_1:68;
hence x in Big_Oh(c(#)f) by A1,A5;
end;
assume x in Big_Oh(c(#)f);
then consider t being Element of Funcs(NAT, REAL) such that
A7: x = t and
A8: ex c1,N st c1 > 0 & for n st n >= N holds t.n <= c1*(c(#)f).n & t .n>= 0;
consider c1,N such that
A9: c1 > 0 and
A10: for n st n >= N holds t.n <= c1*(c(#)f).n & t.n >= 0 by A8;
A11: now
let n;
assume
A12: n >= N;
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;
end;
c1*c > 0*c by A9,XREAL_1:68;
hence x in Big_Oh(f) by A7,A11;
end;
hence thesis by TARSKI:2;
end;
theorem
:: NOTE: The reverse implication is not true. Consider the case of
:: f = 1/n, c = 1. Then 1/n in Big_Oh(1+1/n), but 1+1/n is not in Big_Oh(1/n).
for c being non negative Real, x,f being eventually-nonnegative
Real_Sequence holds x in Big_Oh(f) implies x in Big_Oh(c+f)
proof
let c be non negative Real, x,f be eventually-nonnegative Real_Sequence;
assume x in Big_Oh(f);
then consider t being Element of Funcs(NAT, REAL) such that
A1: x = t and
A2: ex c1,N st c1 > 0 & for n st n >= N holds t.n <= c1*f.n & t.n >= 0;
consider c1,N such that
A3: c1 > 0 and
A4: for n st n >= N holds t.n <= c1*f.n & t.n >= 0 by A2;
now
let n;
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;
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;
end;
hence thesis by A1,A3;
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;
assume that
A1: f/"g is convergent and
A2: lim( f/"g ) > 0;
set l = lim( f/"g ), delta = l, c = 2*l;
consider N being Nat such that
A3: for n being Nat st N <= n holds |.(f/"g).n-l.| < delta
by A1,A2,SEQ_2:def 7;
consider N2 being Nat such that
A4: for n being Nat st n >= N2 holds g.n > 0 by Def4;
consider N1 being Nat such that
A5: for n being Nat st n >= N1 holds f.n >= 0 by Def2;
reconsider b = max( N, N1 ) as Element of NAT by ORDINAL1:def 12;
reconsider a = max( b, N2 ) as Element of NAT by ORDINAL1:def 12;
A6: now
let n;
assume
A7: n >= a;
a >= N2 by XXREAL_0:25;
then n >= N2 by A7,XXREAL_0:2;
then
A8: g.n > 0 by A4;
a >= b by XXREAL_0:25;
then
A9: n >= b by A7,XXREAL_0:2;
b >= N by XXREAL_0:25;
then n >= N by A9,XXREAL_0:2;
then |.(f/"g).n-l.| < delta by A3;
then (f/"g).n - l <= delta by ABSVALUE:5;
then (f/"g).n <= 1*l + 1*l by XREAL_1:20;
then f.n*(g").n <= c by SEQ_1:8;
then f.n*(g.n)" <= c by VALUED_1:10;
then f.n*(g.n)"*g.n <= c*g.n by A8,XREAL_1:64;
then f.n*((g.n)"*g.n) <= c*g.n;
then f.n*1 <= c*g.n by A8,XCMPLX_0:def 7;
hence f.n <= c*g.n;
b >= N1 by XXREAL_0:25;
then n >= N1 by A9,XXREAL_0:2;
hence f.n >= 0 by A5;
end;
A10: f is Element of Funcs(NAT, REAL) by FUNCT_2:8;
2*l > 2*0 by A2,XREAL_1:68;
hence thesis by A10,A6;
end;
theorem Th15: :: Limit Rule, Part 1 (page 84)
for f,g being eventually-positive Real_Sequence st f/"g is
convergent & lim( f/"g ) > 0 holds Big_Oh(f) = Big_Oh(g)
proof
let f,g be eventually-positive Real_Sequence;
assume
A1: f/"g is convergent & lim( f/"g ) > 0;
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 thesis by A2,Lm2;
end;
theorem Th16: :: Limit Rule, Part 2 (page 84)
for f,g being eventually-positive Real_Sequence st f/"g is
convergent & lim( f/"g )=0 holds f in Big_Oh(g) & not g in Big_Oh(f)
proof
let f,g be eventually-positive Real_Sequence;
assume
A1: f/"g is convergent & lim( f/"g ) = 0;
then consider N being Nat such that
A2: for n being Nat st N<=n holds |.(f/"g).n-0.|<1 by SEQ_2:def 7;
consider N1 being Nat such that
A3: for n being Nat st n>=N1 holds f.n >= 0 by Def2;
consider N2 being Nat such that
A4: for n being Nat st n>=N2 holds g.n > 0 by Def4;
A5: not g in Big_Oh(f)
proof
assume g in Big_Oh(f);
then consider t being Element of Funcs(NAT, REAL) such that
A6: t = g and
A7: ex c,N st c > 0 & for n st n >= N holds t.n <= c*f.n & t.n >= 0;
consider c,N such that
A8: c > 0 and
A9: for n st n >= N holds t.n <= c*f.n & t.n >= 0 by A7;
reconsider c as Element of REAL by XREAL_0:def 1;
set q = seq_const(1/c);
reconsider a = max(N, N2) as Element of NAT by ORDINAL1:def 12;
A10: a >= N2 by XXREAL_0:25;
A11: a >= N by XXREAL_0:25;
now
take a;
let n;
assume
A12: n >= a;
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 SEQ_1:57;
end;
then
A14: f/"g majorizes q;
now
set p = 1/c;
let p1 be Real;
assume
A15: p1 > 0;
reconsider N as Nat;
take N;
let n be Nat;
assume n >= N;
|.q.n-p.| = |.1/c-1/c.| by SEQ_1:57
.= |.0.|;
hence |.q.n-p.| < p1 by A15,ABSVALUE:2;
end;
then
A16: q is convergent by SEQ_2:def 6;
now
let p1 be Real;
assume
A17: p1 > 0;
reconsider N as Nat;
take N;
let n be Nat;
assume n >= N;
|.q.n-1/c.| = |.1/c-1/c.| by SEQ_1:57
.= |.0.|;
hence |.q.n-1/c.| < p1 by A17,ABSVALUE:2;
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;
end;
reconsider b = max( N, N1 ) as Element of NAT by ORDINAL1:def 12;
reconsider a = max( b, N2 ) as Element of NAT by ORDINAL1:def 12;
A18: now
let n;
assume
A19: n >= a;
a >= b by XXREAL_0:25;
then
A20: n >= b by A19,XXREAL_0:2;
b >= N by XXREAL_0:25;
then n >= N by A20,XXREAL_0:2;
then |.(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;
a >= 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;
b >= N1 by XXREAL_0:25;
then n >= N1 by A20,XXREAL_0:2;
hence f.n >= 0 by A3;
end;
f is Element of Funcs(NAT, REAL) by FUNCT_2:8;
hence thesis by A18,A5;
end;
theorem Th17: :: Limit Rule, Part 3 (page 84)
for f,g being eventually-positive Real_Sequence st f/"g is
divergent_to+infty holds not f in Big_Oh(g) & g in Big_Oh(f)
proof
let f,g be eventually-positive Real_Sequence;
assume f/"g is divergent_to+infty;
then g/"f is convergent & lim(g/"f) = 0 by Th5;
hence thesis by Th16;
end;
begin :: Other Asymptotic Notation (Section 3.3)
definition
let f be eventually-nonnegative Real_Sequence;
func Big_Omega(f) -> FUNCTION_DOMAIN of NAT, REAL equals
{ t where t is
Element of Funcs(NAT, REAL) : ex d,N st d > 0 & for n st n >= N holds t.n >= d*
f.n & t.n >= 0 };
coherence
proof
set IT = { t where t is Element of Funcs(NAT, REAL) : ex d,N st d > 0 &
for n st n >= N holds t.n >= d*f.n & t.n >= 0 };
A1: IT is functional
proof
let x be object;
assume x in IT;
then
ex t being Element of Funcs(NAT, REAL) st x = t & ex d,N st d > 0 &
for n st n >= N holds t.n >= d*f.n & t.n >= 0;
hence thesis;
end;
consider N being Nat such that
A2: for n being Nat st n >= N holds f.n >= 0 by Def2;
reconsider N as Element of NAT by ORDINAL1:def 12;
f is Element of Funcs(NAT, REAL) & for n st n >= N holds f.n >= 1*f.n
& f.n >= 0 by A2,FUNCT_2:8;
then f in IT;
then reconsider IT1 = IT as functional non empty set by A1;
now
let x be Element of IT1;
x in IT;
then ex t being Element of Funcs(NAT, REAL) st x = t & ex d,N st d > 0 &
for n st n >= N holds t.n >= d*f.n & t.n >= 0;
hence x is sequence of REAL;
end;
hence thesis by FUNCT_2:def 12;
end;
end;
theorem
for x being set, f being eventually-nonnegative Real_Sequence st x in
Big_Omega(f) holds x is eventually-nonnegative Real_Sequence
proof
let t be set, f be eventually-nonnegative Real_Sequence;
assume t in Big_Omega(f);
then consider s being Element of Funcs(NAT, REAL) such that
A1: s = t and
A2: ex d,N st d > 0 & for n st n >= N holds s.n >= d*f.n & s.n >= 0;
reconsider t9 = t as Real_Sequence by A1;
consider d,N such that
d > 0 and
A3: for n st n >= N holds s.n >= d*f.n & s.n >= 0 by A2;
now
reconsider N as Nat;
take N;
let n be Nat;
A4: n in NAT by ORDINAL1:def 12;
assume n >= N;
hence t9.n >= 0 by A1,A3,A4;
end;
hence thesis by Def2;
end;
theorem Th19: :: Duality Rule (page 86)
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;
A1: g is Element of Funcs(NAT, REAL) by FUNCT_2:8;
hereby
consider N1 being Nat such that
A2: for n being Nat st n >= N1 holds g.n >= 0 by Def2;
assume f in Big_Omega(g);
then consider t being Element of Funcs(NAT, REAL) such that
A3: f = t and
A4: ex d,N st d > 0 & for n st n >= N holds t.n >= d*g.n & t.n >= 0;
consider d,N such that
A5: d > 0 and
A6: for n st n >= N holds t.n >= d*g.n & t.n >= 0 by A4;
reconsider a = max(N, N1) as Element of NAT by ORDINAL1:def 12;
A7: a >= N1 by XXREAL_0:25;
A8: a >= N by XXREAL_0:25;
now
take a;
let n;
assume
A9: n >= a;
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;
n >= N1 by A7,A9,XXREAL_0:2;
hence g.n >= 0 by A2;
end;
hence g in Big_Oh(f) by A1,A5;
end;
assume g in Big_Oh(f);
then consider t being Element of Funcs(NAT, REAL) such that
A10: g = t and
A11: ex c,N st c > 0 & for n st n >= N holds t.n <= c*f.n & t.n >= 0;
consider c,N such that
A12: c > 0 and
A13: for n st n >= N holds t.n <= c*f.n & t.n >= 0 by A11;
consider N1 being Nat such that
A14: for n being Nat st n >= N1 holds f.n >= 0 by Def2;
reconsider a = max(N, N1) as Element of NAT by ORDINAL1:def 12;
A15: a >= N1 by XXREAL_0:25;
A16: a >= N by XXREAL_0:25;
A17: now
take a;
let n;
assume
A18: n >= a;
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;
n >= N1 by A15,A18,XXREAL_0:2;
hence f.n >= 0 by A14;
end;
f is Element of Funcs(NAT, REAL) by FUNCT_2:8;
hence thesis by A12,A17;
end;
theorem Th20: :: Reflexivity of Big_Omega (Problem 3.12)
for f being eventually-nonnegative Real_Sequence holds f in Big_Omega(f)
proof
let f be eventually-nonnegative Real_Sequence;
f in Big_Oh(f) by Th10;
hence thesis by Th19;
end;
theorem Th21: :: Transitivity of Big_Omega (Problem 3.12)
for f,g,h being eventually-nonnegative Real_Sequence holds f in
Big_Omega(g) & g in Big_Omega(h) implies f in Big_Omega(h)
proof
let f,g,h be eventually-nonnegative Real_Sequence;
assume f in Big_Omega(g) & g 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 thesis by Th19;
end;
theorem :: Limit Rule for Big_Omega, Part 1 (page 86)
for f,g being eventually-positive Real_Sequence st f/"g is convergent
& lim( f/"g ) > 0 holds Big_Omega(f) = Big_Omega(g)
proof
let f,g be eventually-positive Real_Sequence;
assume
A1: f/"g is convergent & lim( f/"g ) > 0;
now
let x be object;
hereby
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);
then consider t being Element of Funcs(NAT, REAL) such that
A3: x = t and
A4: ex d,N st d > 0 & for n st n >= N holds d*f.n <= t.n & t.n >= 0;
consider d,N such that
d > 0 and
A5: for n st n >= N holds d*f.n <= t.n & t.n >= 0 by A4;
now
reconsider N as Nat;
take N;
let n be Nat;
A6: n in NAT by ORDINAL1:def 12;
assume n >= N;
hence t.n >= 0 by A5,A6;
end;
then
A7: t is eventually-nonnegative;
t in Big_Omega(f) by A4;
hence x in Big_Omega(g) by A3,A7,A2,Th21;
end;
assume x in Big_Omega(g);
then consider t being Element of Funcs(NAT, REAL) such that
A8: x = t and
A9: ex d,N st d > 0 & for n st n >= N holds d*g.n <= t.n & t.n >= 0;
consider d,N such that
d > 0 and
A10: for n st n >= N holds d*g.n <= t.n & t.n >= 0 by A9;
now
reconsider N as Nat;
take N;
let n be Nat;
A11: n in NAT by ORDINAL1:def 12;
assume n >= N;
hence t.n >= 0 by A10,A11;
end;
then
A12: t is eventually-nonnegative;
f in Big_Oh(f) by Th10;
then f in Big_Oh(g) by A1,Th15;
then
A13: g in Big_Omega(f) by Th19;
t in Big_Omega(g) by A9;
hence x in Big_Omega(f) by A8,A12,A13,Th21;
end;
hence thesis by TARSKI:2;
end;
theorem Th23: :: Limit Rule for Big_Omega, Part 2 (page 86)
for f,g being eventually-positive Real_Sequence st f/"g is
convergent & lim( f/"g ) = 0 holds g in Big_Omega(f) & not f in Big_Omega(g)
proof
let f,g be eventually-positive Real_Sequence;
assume f/"g is convergent & lim( f/"g ) = 0;
then f in Big_Oh(g) & not g in Big_Oh(f) by Th16;
hence thesis by Th19;
end;
theorem :: Limit Rule for Big_Omega, Part 3 (page 86)
for f,g being eventually-positive Real_Sequence st f/"g is
divergent_to+infty holds not g in Big_Omega(f) & f in Big_Omega(g)
proof
let f,g be eventually-positive Real_Sequence;
assume f/"g is divergent_to+infty;
then g/"f is convergent & lim(g/"f) = 0 by Th5;
hence thesis by Th23;
end;
theorem :: Threshold Rule for Big_Omega (page 86)
for f,t being positive Real_Sequence holds t in Big_Omega(f) iff ex d
st d > 0 & for n holds d*f.n <= t.n
proof
let f,t be positive Real_Sequence;
hereby
assume t in Big_Omega(f);
then consider s being Element of Funcs(NAT, REAL) such that
A1: s = t and
A2: ex d,N st d > 0 & for n st n >= N holds d*f.n <= s.n & s.n >= 0;
consider d,N such that
A3: d > 0 and
A4: for n st n >= N holds d*f.n <= s.n & s.n >= 0 by A2;
per cases;
suppose
A5: N = 0;
take d;
thus d > 0 by A3;
let n;
thus d*f.n <= t.n by A1,A4,A5;
end;
suppose
A6: N > 0;
deffunc F(Element of NAT) = t.$1 / f.$1;
reconsider B = { F(n) : n < N } as finite non empty Subset of REAL from
FinImInit2(A6);
set b = min B;
A7: for n st n < N holds b*f.n <= t.n
proof
let n;
A8: f.n > 0 by Def3;
assume n < N;
then t.n / f.n in B;
then t.n / f.n >= b by XXREAL_2:def 7;
then t.n / f.n * f.n >= b * f.n by A8,XREAL_1:64;
hence thesis by A8,XCMPLX_1:87;
end;
thus ex d st d > 0 & for n holds d*f.n <= t.n
proof
per cases;
suppose
A9: b <= d;
reconsider b as Element of REAL by XREAL_0:def 1;
take b;
b in B by XXREAL_2:def 7;
then consider n1 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;
let n;
thus b*f.n <= t.n
proof
per cases;
suppose
n < N;
hence thesis by A7;
end;
suppose
A11: n >= 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 thesis by A12,XXREAL_0:2;
end;
end;
end;
suppose
A13: b > d;
take d;
thus d > 0 by A3;
let n;
thus d*f.n <= t.n
proof
per cases;
suppose
A14: n < N;
f.n > 0 by Def3;
then
A15: d*f.n <= b*f.n by A13,XREAL_1:64;
b*f.n <= t.n by A7,A14;
hence thesis by A15,XXREAL_0:2;
end;
suppose
n >= N;
hence thesis by A1,A4;
end;
end;
end;
end;
end;
end;
given d such that
A16: d > 0 and
A17: for n holds d*f.n <= t.n;
t is Element of Funcs(NAT, REAL) & for n st n >= 0 holds d*f.n <= t.n &
t.n >= 0 by A17,Def3,FUNCT_2:8;
hence thesis by A16;
end;
theorem :: Maximum Rule for Big_Omega (page 86)
for f,g being eventually-nonnegative Real_Sequence holds Big_Omega(f+g
) = Big_Omega(max(f,g))
proof
let f,g be eventually-nonnegative Real_Sequence;
consider N1 being Nat such that
A1: for n being Nat st n >= N1 holds f.n >= 0 by Def2;
consider N2 being Nat such that
A2: for n being Nat st n >= N2 holds g.n >= 0 by Def2;
now
let x be object;
hereby
assume x in Big_Omega(f+g);
then consider t being Element of Funcs(NAT, REAL) such that
A3: t = x and
A4: ex d,N st d > 0 & for n st n >= N holds d*(f+g).n <= t.n & t.n >= 0;
consider d,N such that
A5: d > 0 and
A6: for n st n >= N holds d*(f+g).n <= t.n & t.n >= 0 by A4;
reconsider a = max(N, max(N1, N2)) as Element of NAT
by ORDINAL1:def 12;
A7: a >= N by XXREAL_0:25;
A8: a >= max(N1, N2) by XXREAL_0:25;
max(N1, N2) >= N2 by XXREAL_0:25;
then
A9: a >= N2 by A8,XXREAL_0:2;
max(N1, N2) >= N1 by XXREAL_0:25;
then
A10: a >= N1 by A8,XXREAL_0:2;
now
let n;
assume
A11: n >= a;
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
per cases by A14,XXREAL_0:16;
suppose
max(f,g).n = f.n;
then max(f,g).n + 0 <= f.n + g.n by A13,XREAL_1:7;
hence thesis by SEQ_1:7;
end;
suppose
max(f,g).n = g.n;
then max(f,g).n + 0 <= g.n + f.n by A12,XREAL_1:7;
hence thesis by SEQ_1:7;
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;
thus t.n >= 0 by A6,A16;
end;
hence x in Big_Omega(max(f,g)) by A3,A5;
end;
assume x in Big_Omega(max(f,g));
then consider t being Element of Funcs(NAT, REAL) such that
A17: t = x and
A18: ex d,N st d > 0 & for n st n >= N holds d*max(f,g).n <= t.n & t.n >= 0;
consider d,N such that
A19: d > 0 and
A20: for n st n >= N holds d*max(f,g).n <= t.n & t.n >= 0 by A18;
reconsider a = max(N, max(N1, N2)) as Element of NAT
by ORDINAL1:def 12;
A21: N <= a by XXREAL_0:25;
A22: now
let n;
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 >= a;
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;
thus t.n >= 0 by A20,A24;
end;
d*2" > d*0 by A19,XREAL_1:68;
hence x in Big_Omega(f+g) by A17,A22;
end;
hence thesis by TARSKI:2;
end;
definition
let f be eventually-nonnegative Real_Sequence;
func Big_Theta(f) -> FUNCTION_DOMAIN of NAT, REAL equals
Big_Oh(f) /\ Big_Omega(f);
coherence
proof
f in Big_Oh(f) & f in Big_Omega(f) by Th10,Th20;
then
A1: Big_Oh(f) /\ Big_Omega(f) is non empty by XBOOLE_0:def 4;
now
let x be Element of Big_Oh(f) /\ Big_Omega(f);
x in Big_Oh(f) by A1,XBOOLE_0:def 4;
hence x is sequence of REAL by Th6;
end;
hence thesis by A1,FUNCT_2:def 12;
end;
end;
theorem Th27: :: Alternate Definition for Big_Theta (page 87)
for f being eventually-nonnegative Real_Sequence holds Big_Theta
(f) = { t where t is Element of Funcs(NAT, REAL) : ex c,d,N st c > 0 & d > 0 &
for n st n >= N holds d*f.n <= t.n & t.n <= c*f.n }
proof
let f be eventually-nonnegative Real_Sequence;
set BT = { t where t is Element of Funcs(NAT, REAL) : ex c,d,N st c > 0 & d
> 0 & for n st n >= N holds d*f.n <= t.n & t.n <= c*f.n };
now
let x be object;
hereby
assume
A1: x in Big_Theta(f);
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,N st c > 0 & for n 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,N st d > 0 & for n st n >= N holds s.n >= d*f.n & s.n >= 0;
consider c,N such that
A6: c > 0 and
A7: for n st n >= N holds t.n <= c*f.n & t.n >= 0 by A3;
consider d,N1 such that
A8: d > 0 and
A9: for n st n >= N1 holds s.n >= d*f.n & s.n >= 0 by A5;
set a = max(N, N1);
A10: a >= N & a >= N1 by XXREAL_0:25;
now
take a;
let n;
assume n >= a;
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;
end;
hence x in BT by A2,A6,A8;
end;
assume x in BT;
then consider t being Element of Funcs(NAT, REAL) such that
A11: x = t and
A12: ex c,d,N st c > 0 & d > 0 & for n st n >= N holds d*f.n <= t.n &
t.n <= c*f.n;
consider c,d,N such that
A13: c > 0 and
A14: d > 0 and
A15: for n st n >= N holds d*f.n <= t.n & t.n <= c*f.n by A12;
consider N1 being Nat such that
A16: for n being Nat st n >= N1 holds f.n >= 0 by Def2;
reconsider a = max( N, N1 ) as Element of NAT by ORDINAL1:def 12;
A17: a >= N1 by XXREAL_0:25;
A18: a >= N by XXREAL_0:25;
now
take a;
let n;
assume
A19: n >= a;
then
A20: n >= N by A18,XXREAL_0:2;
hence d*f.n <= t.n by A15;
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;
end;
then
A21: x in Big_Omega(f) by A11,A14;
now
take a;
let n;
assume
A22: n >= a;
then
A23: n >= N by A18,XXREAL_0:2;
hence t.n <= c*f.n by A15;
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;
end;
then x in Big_Oh(f) by A11,A13;
hence x in Big_Theta(f) by A21,XBOOLE_0:def 4;
end;
hence thesis by TARSKI:2;
end;
theorem :: Reflexivity of Big_Theta (Problem 3.18 Part 1)
for f being eventually-nonnegative Real_Sequence holds f in Big_Theta( f)
proof
let f be eventually-nonnegative Real_Sequence;
f in Big_Oh(f) & f in Big_Omega(f) by Th10,Th20;
hence thesis by XBOOLE_0:def 4;
end;
theorem :: Symmetry of Big_Theta (Problem 3.18 Part 2)
for f,g being eventually-nonnegative Real_Sequence st f in Big_Theta(g
) holds g in Big_Theta(f)
proof
let f,g be eventually-nonnegative Real_Sequence;
assume
A1: f in Big_Theta(g);
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 thesis by A2,XBOOLE_0:def 4;
end;
theorem :: Transitivity of Big_Theta (Problem 3.18 Part 3)
for f,g,h being eventually-nonnegative Real_Sequence st f in Big_Theta
(g) & g in Big_Theta(h) holds f in Big_Theta(h)
proof
let f,g,h be eventually-nonnegative Real_Sequence;
assume
A1: f in Big_Theta(g) & g 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 thesis by A2,XBOOLE_0:def 4;
end;
theorem :: Threshold Rule for Big_Theta (page 87)
for f,t being positive Real_Sequence holds t in Big_Theta(f) iff ex c,
d st c > 0 & d > 0 & for n holds d*f.n <= t.n & t.n <= c*f.n
proof
let f,t be positive Real_Sequence;
A1: Big_Theta(f) = { s where s is Element of Funcs(NAT, REAL) : ex c,d,N st
c > 0 & d > 0 & for n st n >= N holds d*f.n <= s.n & s.n <= c*f.n } by Th27;
hereby
assume t in Big_Theta(f);
then consider s being Element of Funcs(NAT, REAL) such that
A2: s = t and
A3: ex c,d,N st c > 0 & d > 0 & for n st n >= N holds d*f.n <= s.n & s
.n <= c*f.n by A1;
consider c,d,N such that
A4: c > 0 and
A5: d > 0 and
A6: for n st n >= N holds d*f.n <= s.n & s.n <= c*f.n by A3;
per cases;
suppose
A7: N = 0;
take c,d;
thus c > 0 by A4;
thus d > 0 by A5;
let n;
thus d*f.n <= t.n & t.n <= c*f.n by A2,A6,A7;
end;
suppose
A8: N > 0;
deffunc F(Element of NAT) = t.$1 / f.$1;
reconsider B = { F(n) : n < N } as finite non empty Subset of REAL from
FinImInit2(A8);
set b = max B;
set a = min B;
A9: for n st n < N holds t.n >= a*f.n
proof
let n;
A10: f.n > 0 by Def3;
assume n < N;
then t.n / f.n in B;
then t.n / f.n >= a by XXREAL_2:def 7;
then t.n / f.n * f.n >= a * f.n by A10,XREAL_1:64;
hence thesis by A10,XCMPLX_1:87;
end;
A11: for n st n < N holds t.n <= b*f.n
proof
let n;
A12: f.n > 0 by Def3;
assume n < N;
then t.n / f.n in B;
then t.n / f.n <= b by XXREAL_2:def 8;
then t.n / f.n * f.n <= b * f.n by A12,XREAL_1:64;
hence thesis by A12,XCMPLX_1:87;
end;
thus ex c,d st c > 0 & d > 0 & for n holds d*f.n <= t.n & t.n <= c*f.n
proof
set D = min( a, d );
set C = max( b, c );
reconsider C,D as Element of REAL by XREAL_0:def 1;
take C,D;
thus C > 0 by A4,XXREAL_0:25;
A13: now
let 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;
end;
a > 0
proof
a in B by XXREAL_2:def 7;
then ex n st a = t.n / f.n & n < N;
hence thesis by A13;
end;
hence D > 0 by A5,XXREAL_0:15;
let n;
A14: f.n > 0 by Def3;
per cases;
suppose
A15: n < N;
A16: D*f.n <= a*f.n by A14,XREAL_1:64,XXREAL_0:17;
a*f.n <= t.n by A9,A15;
hence D*f.n <= t.n by A16,XXREAL_0:2;
A17: b*f.n <= C*f.n by A14,XREAL_1:64,XXREAL_0:25;
t.n <= b*f.n by A11,A15;
hence thesis by A17,XXREAL_0:2;
end;
suppose
A18: n >= 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;
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 thesis by A20,XXREAL_0:2;
end;
end;
end;
end;
given c,d such that
A21: c > 0 & d > 0 and
A22: for n holds d*f.n <= t.n & t.n <= c*f.n;
t is Element of Funcs(NAT, REAL) & for n st n >= 0 holds d*f.n <= t.n &
t.n <= c*f.n by A22,FUNCT_2:8;
hence thesis by A1,A21;
end;
theorem :: Maximum Rule for Big_Theta (page 87)
for f,g being eventually-nonnegative Real_Sequence holds Big_Theta(f+g
) = Big_Theta(max(f,g))
proof
let f,g be eventually-nonnegative Real_Sequence;
A1: Big_Theta(max(f,g)) = { s where s is Element of Funcs(NAT, REAL) : ex c,
d,N st c > 0 & d > 0 & for n st n >= N holds d*max(f,g).n <= s.n & s.n <= c*max
(f,g).n } by Th27;
consider N2 being Nat such that
A2: for n being Nat st n >= N2 holds g.n >= 0 by Def2;
consider N1 being Nat such that
A3: for n being 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,N
st c > 0 & d > 0 & for n st n >= N holds d*(f+g).n <= s.n & s.n <= c*(f+g).n }
by Th27;
now
let x be object;
hereby
assume x in Big_Theta(f+g);
then consider t being Element of Funcs(NAT, REAL) such that
A5: t = x and
A6: ex c,d,N st c > 0 & d > 0 & for n st n >= N holds d*(f+g).n <= t
.n & t.n <= c*(f+g).n by A4;
consider c,d,N such that
A7: c > 0 and
A8: d > 0 and
A9: for n st n >= N holds d*(f+g).n <= t.n & t.n <= c*(f+g).n by A6;
reconsider a = max(N,max(N1, N2)) as Element of NAT by ORDINAL1:def 12;
A10: a >= N by XXREAL_0:25;
A11: a >= max(N1, N2) by XXREAL_0:25;
max(N1, N2) >= N2 by XXREAL_0:25;
then
A12: a >= N2 by A11,XXREAL_0:2;
max(N1, N2) >= N1 by XXREAL_0:25;
then
A13: a >= N1 by A11,XXREAL_0:2;
A14: now
let 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 >= a;
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
per cases by A16,XXREAL_0:16;
suppose
max(f,g).n = f.n;
then max(f,g).n + 0 <= f.n + g.n by A19,XREAL_1:7;
hence thesis by SEQ_1:7;
end;
suppose
max(f,g).n = g.n;
then max(f,g).n + 0 <= g.n + f.n by A20,XREAL_1:7;
hence thesis by SEQ_1:7;
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;
end;
2*c > 2*0 by A7,XREAL_1:68;
hence x in Big_Theta(max(f,g)) by A1,A5,A8,A14;
end;
consider N1 being Nat such that
A22: for n being Nat st n >= N1 holds f.n >= 0 by Def2;
consider N2 being Nat such that
A23: for n being Nat st n >= N2 holds g.n >= 0 by Def2;
assume x in Big_Theta(max(f,g));
then consider t being Element of Funcs(NAT, REAL) such that
A24: t = x and
A25: ex c,d,N st c > 0 & d > 0 & for n st n >= N holds d*max(f,g).n <=
t.n & t.n <= c*max(f,g).n by A1;
consider c,d,N such that
A26: c > 0 and
A27: d > 0 and
A28: for n st n >= N holds d*max(f,g).n <= t.n & t.n <= c*max(f,g).n by A25;
reconsider a = max(N, max(N1, N2)) as Element of NAT
by ORDINAL1:def 12;
A29: max(N1,N2) <= a by XXREAL_0:25;
N2 <= max(N1,N2) by XXREAL_0:25;
then
A30: N2 <= a by A29,XXREAL_0:2;
A31: N <= a by XXREAL_0:25;
N1 <= max(N1,N2) by XXREAL_0:25;
then
A32: N1 <= a by A29,XXREAL_0:2;
A33: now
let n;
assume
A34: n >= a;
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;
end;
d*2" > d*0 by A27,XREAL_1:68;
hence x in Big_Theta(f+g) by A4,A24,A26,A33;
end;
hence thesis by TARSKI:2;
end;
theorem :: Limit Rule for Big_Theta, Part 1 (page 88)
for f,g being eventually-positive Real_Sequence st f/"g is convergent
& lim( f/"g ) > 0 holds f in Big_Theta(g)
proof
let f,g be eventually-positive Real_Sequence;
assume f/"g is convergent & lim( f/"g ) > 0;
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 thesis by A2,XBOOLE_0:def 4;
end;
theorem :: Limit Rule for Big_Theta, Part 2 (page 88)
for f,g being eventually-positive Real_Sequence st f/"g is convergent
& lim( f/"g ) = 0 holds f in Big_Oh(g) & not f in Big_Theta(g)
proof
let f,g be eventually-positive Real_Sequence;
assume
A1: f/"g is convergent & lim( f/"g ) = 0;
now
assume f in Big_Theta(g);
then f in Big_Omega(g) by XBOOLE_0:def 4;
then g in Big_Oh(f) by Th19;
hence contradiction by A1,Th16;
end;
hence thesis by A1,Th16;
end;
theorem :: Limit Rule for Big_Theta, Part 3 (page 88)
for f,g being eventually-positive Real_Sequence st f/"g is
divergent_to+infty holds f in Big_Omega(g) & not f in Big_Theta(g)
proof
let f,g be eventually-positive Real_Sequence;
assume f/"g is divergent_to+infty;
then ( not f in Big_Oh(g))& g in Big_Oh(f) by Th17;
hence thesis by Th19,XBOOLE_0:def 4;
end;
begin :: Conditional Asymptotic Notation (Section 3.4)
definition
let f be eventually-nonnegative Real_Sequence, X be set;
func Big_Oh(f,X) -> FUNCTION_DOMAIN of NAT, REAL equals
{ t where t is
Element of Funcs(NAT, REAL) : ex c,N st c > 0 & for n st n >= N & n in X holds
t.n <= c*f.n & t.n >= 0 };
coherence
proof
set IT = { t where t is Element of Funcs(NAT, REAL) : ex c,N st c > 0 &
for n st n >= N & n in X holds t.n <= c*f.n & t.n >= 0 };
A1: IT is functional
proof
let x be object;
assume x in IT;
then
ex t being Element of Funcs(NAT, REAL) st x = t & ex c,N st c > 0 &
for n st n >= N & n in X holds t.n <= c*f.n & t.n >= 0;
hence thesis;
end;
consider N being Nat such that
A2: for n being Nat st n >= N holds f.n >= 0 by Def2;
reconsider N as Element of NAT by ORDINAL1:def 12;
f is Element of Funcs(NAT, REAL) & for n st n >= N & n in X holds f.n
<= 1*f .n & f.n >= 0 by A2,FUNCT_2:8;
then f in IT;
then reconsider IT1 = IT as functional non empty set by A1;
now
let x be Element of IT1;
x in IT;
then ex t being Element of Funcs(NAT, REAL) st x = t & ex c,N st c > 0 &
for n st n >= N & n in X holds t.n <= c*f.n & t . n >= 0;
hence x is sequence of REAL;
end;
hence thesis by FUNCT_2:def 12;
end;
end;
definition
let f be eventually-nonnegative Real_Sequence, X be set;
func Big_Omega(f,X) -> FUNCTION_DOMAIN of NAT, REAL equals
{ t where t is
Element of Funcs(NAT, REAL) : ex d,N st d > 0 & for n st n >= N & n in X holds
t.n >= d*f.n & t.n >= 0 };
coherence
proof
set IT = { t where t is Element of Funcs(NAT, REAL) : ex d,N st d > 0 &
for n st n >= N & n in X holds t.n >= d*f.n & t.n >= 0 };
A1: IT is functional
proof
let x be object;
assume x in IT;
then
ex t being Element of Funcs(NAT, REAL) st x = t & ex d,N st d > 0 &
for n st n >= N & n in X holds t.n >= d*f.n & t.n >= 0;
hence thesis;
end;
consider N being Nat such that
A2: for n being Nat st n >= N holds f.n >= 0 by Def2;
reconsider N as Element of NAT by ORDINAL1:def 12;
f is Element of Funcs(NAT, REAL) & for n st n >= N & n in X holds f.n
>= 1*f .n & f.n >= 0 by A2,FUNCT_2:8;
then f in IT;
then reconsider IT1 = IT as functional non empty set by A1;
now
let x be Element of IT1;
x in IT;
then ex t being Element of Funcs(NAT, REAL) st x = t & ex d,N st d > 0 &
for n st n >= N & n in X holds t.n >= d*f.n & t . n >= 0;
hence x is sequence of REAL;
end;
hence thesis by FUNCT_2:def 12;
end;
end;
definition
let f be eventually-nonnegative Real_Sequence, X be set;
func Big_Theta(f,X) -> FUNCTION_DOMAIN of NAT, REAL equals
{ t where t is
Element of Funcs(NAT, REAL) : ex c,d,N st c > 0 & d > 0 & for n st n >= N & n
in X holds d*f.n <= t.n & t.n <= c*f.n };
coherence
proof
set IT = { t where t is Element of Funcs(NAT, REAL) : ex c,d,N st c > 0 &
d > 0 & for n st n >= N & n in X holds d*f.n <= t.n & t.n <= c*f.n };
A1: IT is functional
proof
let x be object;
assume x in IT;
then
ex t being Element of Funcs(NAT, REAL) st x = t & ex c,d,N st c > 0
& d > 0 & for n st n >= N & n in X holds d*f.n <= t.n & t.n <= c*f.n;
hence thesis;
end;
f is Element of Funcs(NAT, REAL) & for n st n >= 0 & n in X holds 1*f.
n <= f .n & f.n <= 1*f.n by FUNCT_2:8;
then f in IT;
then reconsider IT1 = IT as functional non empty set by A1;
now
let x be Element of IT1;
x in IT;
then
ex t being Element of Funcs(NAT, REAL) st x = t & ex c,d,N st c > 0
& d > 0 & for n st n >= N & n in X holds d*f.n <= t.n & t.n <= c*f. n;
hence x is sequence of REAL;
end;
hence thesis by FUNCT_2:def 12;
end;
end;
theorem Th36: :: Alternate definition for Big_Theta_Cond
for f being eventually-nonnegative Real_Sequence, X being set
holds Big_Theta(f,X) = Big_Oh(f,X) /\ Big_Omega(f,X)
proof
let f be eventually-nonnegative Real_Sequence, X be set;
now
let x be object;
hereby
consider N1 being Nat such that
A1: for n being Nat st n >= N1 holds f.n >= 0 by Def2;
assume x in Big_Theta(f,X);
then consider t being Element of Funcs(NAT, REAL) such that
A2: x = t and
A3: ex c,d,N st c > 0 & d > 0 & for n st n >= N & n in X holds d*f.n
<= t.n & t.n <= c*f.n;
consider c,d,N such that
A4: c > 0 and
A5: d > 0 and
A6: for n st n >= N & n in X holds d*f.n <= t.n & t.n <= c*f.n by A3;
reconsider a = max( N, N1 ) as Element of NAT by ORDINAL1:def 12;
A7: a >= N1 by XXREAL_0:25;
A8: a >= N by XXREAL_0:25;
now
take a;
let n;
assume that
A9: n >= a and
A10: n in X;
A11: n >= N by A8,A9,XXREAL_0:2;
hence d*f.n <= t.n by A6,A10;
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;
end;
then
A12: x in Big_Omega(f,X) by A2,A5;
now
take a;
let n;
assume that
A13: n >= a and
A14: n in X;
A15: n >= N by A8,A13,XXREAL_0:2;
hence t.n <= c*f.n by A6,A14;
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;
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;
end;
assume
A16: x in Big_Oh(f,X) /\ Big_Omega(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,N st c > 0 & for n 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,N st d > 0 & for n st n >= N & n in X holds s.n >= d*f.n & s .n >= 0;
consider c,N such that
A21: c > 0 and
A22: for n st n >= N & n in X holds t.n <= c*f.n & t.n >= 0 by A18;
consider d,N1 such that
A23: d > 0 and
A24: for n st n >= N1 & n in X holds s.n >= d*f.n & s.n >= 0 by A20;
set a = max(N, N1);
A25: a >= N & a >= N1 by XXREAL_0:25;
now
take a;
let n;
assume that
A26: n >= a and
A27: n in X;
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;
end;
hence x in Big_Theta(f,X) by A17,A21,A23;
end;
hence thesis by TARSKI:2;
end;
definition :: Definition of f(bn) (page 89)
let f be Real_Sequence, b be Nat;
func f taken_every b -> Real_Sequence means
:Def15:
for n holds it.n = f.(b* n);
existence
proof
deffunc F(Element of NAT) = f.(b*$1);
consider h being sequence of REAL such that
A1: for n being Element of NAT holds h.n = F(n) from FUNCT_2:sch 4;
take h;
let n;
thus thesis by A1;
end;
uniqueness
proof
let j,k be Real_Sequence such that
A2: for n holds j.n = f.(b*n) and
A3: for n holds k.n = f.(b*n);
now
let n;
thus j.n = f.(b*n) by A2
.= k.n by A3;
end;
hence j = k by FUNCT_2:63;
end;
end;
definition
let f be eventually-nonnegative Real_Sequence, b be Nat;
pred f is_smooth_wrt b means
f is eventually-nondecreasing & f taken_every b in Big_Oh(f);
end;
definition
let f be eventually-nonnegative Real_Sequence;
attr f is smooth means
for b being Element of NAT st b >= 2 holds f is_smooth_wrt b;
end;
theorem :: b-smooth implies smooth (page 90)
for f being eventually-nonnegative Real_Sequence st ex b being Element
of NAT st b >= 2 & f is_smooth_wrt b holds f is smooth
proof
let f be eventually-nonnegative Real_Sequence;
given b being Element of NAT such that
A1: b >= 2 and
A2: f is_smooth_wrt b;
A3: f is eventually-nondecreasing by A2;
then consider N3 being Nat such that
A4: for n being Nat st n >= N3 holds f.n <= f.(n+1);
f taken_every b in Big_Oh(f) by A2;
then consider t being Element of Funcs(NAT, REAL) such that
A5: f taken_every b = t and
A6: ex c,N st c > 0 & for n st n >= N holds t.n <= c*f.n & t.n >= 0;
consider c,N2 such that
A7: c > 0 and
A8: for n st n >= N2 holds t.n <= c*f.n & t.n >= 0 by A6;
reconsider N = max(N2, N3) as Element of NAT by ORDINAL1:def 12;
A9: N >= N2 by XXREAL_0:25;
A10: N >= N3 by XXREAL_0:25;
now
let a be Element of NAT;
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;
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 as Element of NAT by INT_1:3;
reconsider i1 = b|^i as Element of NAT;
A15: now
let n;
defpred P[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 >= N;
then
A19: n >= N2 by A9,XXREAL_0:2;
then
A20: t.n <= c*f.n by A8;
A21: now
assume f.n < 0;
then c*f.n < c*0 by A7,XREAL_1:68;
hence contradiction by A8,A19,A20;
end;
A22: for k st P[k] holds P[k+1]
proof
let k;
set m = b|^k*n;
assume
A23: f.m <= c|^k*f.n;
reconsider m as Element of NAT by ORDINAL1:def 12;
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;
then
A24: c*f.m <= (c to_power (k+1))*f.n by A7,POWER:27;
m >= N2
proof
per cases;
suppose
k = 0;
then b|^k*n = (b to_power 0)*n .= 1*n by POWER:24
.= n;
hence thesis by A9,A18,XXREAL_0:2;
end;
suppose
k > 0;
then b to_power k > 1 by A12,POWER:35;
then b|^k*n >= 1*n by XREAL_1:64;
hence thesis by A19,XXREAL_0:2;
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)
.= f.(b*(b|^k*n));
hence thesis by A25,A24,XXREAL_0:2;
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: P[0];
for k holds P[k] from NAT_1:sch 2( 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;
f.n <= f.(a*n) by A4,A28,A16,Th1;
hence (f taken_every a).n >= 0 by A21,Def15;
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;
end;
hence thesis;
end;
theorem Th38: :: First half of smoothness rule proof (page 90)
for f being eventually-nonnegative Real_Sequence, t being
eventually-nonnegative eventually-nondecreasing Real_Sequence,
b being Nat
st f is smooth & b >= 2 & t in Big_Oh(f, the set of all
b|^n where n is Element of
NAT ) holds t in Big_Oh(f)
proof
let f be eventually-nonnegative Real_Sequence, t be eventually-nonnegative
eventually-nondecreasing Real_Sequence, b be Nat;
assume that
A1: f is smooth and
A2: b >= 2 and
A3: t in Big_Oh(f, the set of all b|^n where n is Element of NAT );
reconsider b as Element of NAT by ORDINAL1:def 12;
A4: f is_smooth_wrt b by A1,A2;
then f taken_every b in Big_Oh(f);
then consider s being Element of Funcs(NAT,REAL) such that
A5: f taken_every b = s and
A6: ex c,N st c > 0 & for n st n >= N holds s.n <= c*f.n & s.n >= 0;
consider c,N3 such that
A7: c > 0 and
A8: for n 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;
then consider N1 being Nat such that
A10: for m being Nat st m >= N1 holds f.m <= f.(m+1);
consider N2 being Nat such that
A11: for m being Nat st m >= N2 holds t.m <= t.(m+1) by Def6;
set X = the set of all b|^n where n is Element of NAT ;
consider r being Element of Funcs(NAT, REAL) such that
A12: r = t and
A13: ex c,N st c > 0 & for n st n >= N & n in X holds r.n <= c*f.n & r.n
>= 0 by A3;
consider a being Real, N4 such that
A14: a > 0 and
A15: for n st n >= N4 & n in X holds r.n <= a*f.n & r.n >= 0 by A13;
reconsider N0 = max(max(N1,N2),max(N3,N4)) as Element of NAT
by ORDINAL1:def 12;
A16: N0 >= max(N1,N2) by XXREAL_0:25;
max(N1,N2) >= N2 by XXREAL_0:25;
then
A17: N0 >= N2 by A16,XXREAL_0:2;
max(N1,N2) >= N1 by XXREAL_0:25;
then
A18: N0 >= N1 by A16,XXREAL_0:2;
A19: N0 >= max(N3,N4) by XXREAL_0:25;
max(N3,N4) >= N4 by XXREAL_0:25;
then
A20: N0 >= N4 by A19,XXREAL_0:2;
max(N3,N4) >= N3 by XXREAL_0:25;
then
A21: N0 >= N3 by A19,XXREAL_0:2;
consider N5 being Nat such that
A22: for n being Nat st n >= N5 holds t.n >= 0 by Def2;
reconsider N = max(N5, max(1, b*N0)) as Element of NAT by ORDINAL1:def 12;
A23: N >= max(1, b*N0) by XXREAL_0:25;
max(1, b*N0) >= b*N0 by XXREAL_0:25;
then
A24: N >= b*N0 by A23,XXREAL_0:2;
b >= 1 by A2,XXREAL_0:2;
then b*N0 >= 1*N0 by XREAL_1:64;
then
A25: N >= N0 by A24,XXREAL_0:2;
A26: N >= N5 by XXREAL_0:25;
A27: max(1, b*N0) >= 1 by XXREAL_0:25;
then
A28: N >= 1 by A23,XXREAL_0:2;
A29: now
N*b" >= b"*(b*N0) by A24,XREAL_1:64;
then N*b" >= (b"*b)*N0;
then
A30: N*b" >= 1*N0 by A2,XCMPLX_0:def 7;
let n;
set n1 = b to_power [\log(b,n)/];
assume
A31: n >= N;
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
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;
then [\log(b,n)/] <= -1 by INT_1:8;
hence contradiction by A33,A35,XREAL_1:6;
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;
n1 = b|^i by POWER:41;
then reconsider n1 as Element of NAT;
set n2 = b*n1;
A36: n2 = (b to_power 1)*(b to_power [\log(b,n)/])
.= b to_power ([\log(b,n)/] + 1) by A2,POWER:27;
then n2 = b|^n3 by POWER:41;
then
A37: n2 in X;
n*b" >= N*b" by A31,XREAL_1:64;
then n*b" >= N0 by A30,XXREAL_0:2;
then
A38: n/b >= N0 by XCMPLX_0:def 9;
log(b,n) <= [\log(b,n)/] + 1 by INT_1:29;
then
A39: n <= n2 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 >= N0 by A38,XXREAL_0:2;
then
A41: n1 >= N3 by A21,XXREAL_0:2;
A42: n >= N0 by A25,A31,XXREAL_0:2;
then n >= N4 by A20,XXREAL_0:2;
then n2 >= N4 by A39,XXREAL_0:2;
then
A43: t.n2 <= a*f.n2 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.n2 by A11,A39,Th1;
then t.n <= a*f.n2 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;
n >= N5 by A26,A31,XXREAL_0:2;
hence t.n >= 0 by A22;
end;
A47: t is Element of Funcs(NAT, REAL) by FUNCT_2:8;
a*c > c*0 by A7,A14,XREAL_1:68;
hence thesis by A47,A29;
end;
theorem Th39: :: Second half of smoothness rule proof (page 90),
for f being eventually-nonnegative Real_Sequence, t being
eventually-nonnegative eventually-nondecreasing Real_Sequence, b being Element
of NAT st f is smooth & b >= 2 & t in Big_Omega(f, the set of all
b|^n where n is Element of
NAT ) holds t in Big_Omega(f)
proof
let f be eventually-nonnegative Real_Sequence, t be eventually-nonnegative
eventually-nondecreasing Real_Sequence, b be Element of NAT;
assume that
A1: f is smooth and
A2: b >= 2 and
A3: t in Big_Omega(f, the set of all b|^n where n is Element of NAT );
consider N2 being Nat such that
A4: for m being Nat st m >= N2 holds t.m <= t.(m+1) by Def6;
A5: f is_smooth_wrt b by A1,A2;
then (f taken_every b) in Big_Oh(f);
then consider s being Element of Funcs(NAT,REAL) such that
A6: (f taken_every b) = s and
A7: ex c,N st c > 0 & for n st n >= N holds s.n <= c*f.n & s.n >= 0;
consider c,N3 such that
A8: c > 0 and
A9: for n st n >= N3 holds s.n <= c*f.n & s.n >= 0 by A7;
f is eventually-nondecreasing by A5;
then consider N1 being Nat such that
A10: for m being Nat st m >= N1 holds f.m <= f.(m+1);
consider N5 being Nat such that
A11: for n being Nat st n >= N5 holds t.n >= 0 by Def2;
set X = the set of all b|^n where n is Element of NAT ;
consider r being Element of Funcs(NAT, REAL) such that
A12: r = t and
A13: ex d,N st d > 0 & for n st n >= N & n in X holds d*f.n <= r.n & r.n
>= 0 by A3;
consider a being Real, N4 such that
A14: a > 0 and
A15: for n st n >= N4 & n in X holds a*f.n <= r.n & r.n >= 0 by A13;
A16: b > 1 by A2,XXREAL_0:2;
reconsider N0 = max(max(N1,N2),max(N3,N4)) as Element of NAT
by ORDINAL1:def 12;
A17: N0 >= max(N1,N2) by XXREAL_0:25;
max(N1,N2) >= N2 by XXREAL_0:25;
then
A18: N0 >= N2 by A17,XXREAL_0:2;
max(N1,N2) >= N1 by XXREAL_0:25;
then
A19: N0 >= N1 by A17,XXREAL_0:2;
A20: N0 >= max(N3,N4) by XXREAL_0:25;
max(N3,N4) >= N4 by XXREAL_0:25;
then
A21: N0 >= N4 by A20,XXREAL_0:2;
max(N3,N4) >= N3 by XXREAL_0:25;
then
A22: N0 >= N3 by A20,XXREAL_0:2;
reconsider N = max(N5, max(1, b*N0)) as Element of NAT
by ORDINAL1:def 12;
A23: N >= max(1, b*N0) by XXREAL_0:25;
max(1, b*N0) >= b*N0 by XXREAL_0:25;
then
A24: N >= b*N0 by A23,XXREAL_0:2;
b >= 1 by A2,XXREAL_0:2;
then b*N0 >= 1*N0 by XREAL_1:64;
then
A25: N >= N0 by A24,XXREAL_0:2;
A26: N >= N5 by XXREAL_0:25;
A27: max(1, b*N0) >= 1 by XXREAL_0:25;
then
A28: N >= 1 by A23,XXREAL_0:2;
A29: now
N*b" >= b"*(b*N0) by A24,XREAL_1:64;
then N*b" >= (b"*b)*N0;
then
A30: N*b" >= 1*N0 by A2,XCMPLX_0:def 7;
let n;
set n1 = b to_power [\log(b,n)/];
A31: log(b,n) <= [\log(b,n)/] + 1 by INT_1:29;
assume
A32: n >= N;
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;
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;
end;
then reconsider i = [\log(b,n)/] as Element of NAT by INT_1:3;
A36: n1 = b|^i by POWER:41;
n*b" >= N*b" by A32,XREAL_1:64;
then n*b" >= N0 by A30,XXREAL_0:2;
then
A37: n/b >= N0 by XCMPLX_0:def 9;
reconsider n1 as Element of NAT by A36;
A38: n1 in X by A36;
set n2 = b*n1;
n2 = (b to_power 1)*(b to_power [\log(b,n)/])
.= b to_power ([\log(b,n)/] + 1) by A2,POWER:27;
then
A39: n <= n2 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 >= N0 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 >= N0 by A25,A32,XXREAL_0:2;
then n >= N1 by A19,XXREAL_0:2;
then f.n <= f.n2 by A10,A39,Th1;
then
A44: a*c"*f.n <= a*c"*f.n2 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.n2 <= t.n by A42,XXREAL_0:2;
hence a*c"*f.n <= t.n by A44,XXREAL_0:2;
n >= N5 by A26,A32,XXREAL_0:2;
hence t.n >= 0 by A11;
end;
A45: t is Element of Funcs(NAT, REAL) by FUNCT_2:8;
a*c" > c"*0 by A8,A14,XREAL_1:68;
hence thesis by A45,A29;
end;
theorem :: also Problem 3.29:: Smoothness Rule (page 90)
for f being eventually-nonnegative Real_Sequence, t being
eventually-nonnegative eventually-nondecreasing Real_Sequence, b being Element
of NAT st f is smooth & b >= 2 & t in Big_Theta(f, the set of all
b|^n where n is Element of
NAT ) holds t in Big_Theta(f)
proof
let f be eventually-nonnegative Real_Sequence, t be eventually-nonnegative
eventually-nondecreasing Real_Sequence, b be Element of NAT;
assume that
A1: f is smooth & b >= 2 and
A2: t in Big_Theta(f, the set of all b|^n where n is Element of NAT );
set X = the set of all b|^n where n is Element of NAT ;
A3: t in Big_Oh(f,X) /\ Big_Omega(f,X) by A2,Th36;
then t in Big_Omega(f,X) by XBOOLE_0:def 4;
then
A4: t in Big_Omega(f) by A1,Th39;
t in Big_Oh(f,X) by A3,XBOOLE_0:def 4;
then t in Big_Oh(f) by A1,Th38;
hence thesis by A4,XBOOLE_0:def 4;
end;
:: Section 3.5 omitted
begin :: Operations on Asymptotic Notation (Section 3.6)
definition
let X be non empty set, F,G be FUNCTION_DOMAIN of X,REAL;
func F + G -> FUNCTION_DOMAIN of X,REAL equals
{ 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
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
consider g be object 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 as Element of Funcs(X,REAL) by FUNCT_2:8;
consider f be object 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 as Element of Funcs(X,REAL) by FUNCT_2:8;
defpred P[Element of X,Real] means $2 = f.$1 + g.$1;
A4: for x being Element of X ex y being Element of REAL st P[x,y];
consider t being Function of X,REAL such that
A5: for x being Element of X holds P[x,t.x] from FUNCT_2:sch 3(A4);
reconsider t as Element of Funcs(X, REAL) by FUNCT_2:8;
t in IT by A3,A2,A5;
hence IT is non empty;
end;
IT is functional
proof
let x be object;
assume x in IT;
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 thesis;
end;
then reconsider IT1 = IT as functional non empty set by A1;
now
let x be Element of IT1;
x in IT;
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;
end;
hence thesis by FUNCT_2:def 12;
end;
end;
definition :: (page 91)
let X be non empty set, F,G be FUNCTION_DOMAIN of X,REAL;
func max(F, G) -> FUNCTION_DOMAIN of X,REAL equals
{ 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
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
consider g be object 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 as Element of Funcs(X,REAL) by FUNCT_2:8;
consider f be object 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 as Element of Funcs(X,REAL) by FUNCT_2:8;
defpred P[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 P[x,y]
proof let x be Element of X;
consider y being Real such that
A5: P[x,y];
reconsider y as Element of REAL by XREAL_0:def 1;
take y;
thus thesis by A5;
end;
consider t being Function of X,REAL such that
A6: for x being Element of X holds P[x,t.x] from FUNCT_2:sch 3(A4);
reconsider t as Element of Funcs(X, REAL) by FUNCT_2:8;
t in IT by A3,A2,A6;
hence IT is non empty;
end;
IT is functional
proof
let x be object;
assume x in IT;
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 thesis;
end;
then reconsider IT1 = IT as functional non empty set by A1;
now
let x be Element of IT1;
x in IT;
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;
end;
hence thesis by FUNCT_2:def 12;
end;
end;
theorem :: Properties, Part 1 (page 91; Problem 3.33)
for f,g being eventually-nonnegative Real_Sequence holds Big_Oh(f) +
Big_Oh(g) = Big_Oh(f+g)
proof
let f,g be eventually-nonnegative Real_Sequence;
now
let x be object;
hereby
assume x in Big_Oh(f) + Big_Oh(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,N st c > 0 & for n st n >= N holds r.n <= c*f.n & r.n >= 0 by A3;
consider c,N1 such that
A8: c > 0 and
A9: for n 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,N st c > 0 & for n st n >= N holds s.n <= c*g.n & s.n >= 0 by A4;
consider d,N2 such that
A12: d > 0 and
A13: for n 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: N >= N2 by XXREAL_0:25;
A15: N >= N1 by XXREAL_0:25;
A16: now
let n;
assume
A17: n >= N;
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 <= e*f.n by XREAL_1:64,XXREAL_0:25;
r.n <= c*f.n by A9,A18;
then r.n <= e*f.n by A20,XXREAL_0:2;
then
A21: r.n + s.n <= e*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 <= e*g.n by XREAL_1:64,XXREAL_0:25;
s.n <= d*g.n by A13,A22;
then s.n <= e*g.n by A23,XXREAL_0:2;
then e*f.n + s.n <= e*f.n + e*g.n by XREAL_1:6;
then r.n + s.n <= e*(f.n + g.n) by A21,XXREAL_0:2;
then r.n + s.n <= e*(f+g).n by SEQ_1:7;
hence t.n <= e*(f+g).n by A5,A6,A10;
0 + g9.n >= 0 by A10,A13,A22;
hence t.n >= 0 by A5,A19;
end;
e > 0 by A8,XXREAL_0:25;
hence x in Big_Oh(f+g) by A1,A16;
end;
assume x in Big_Oh(f+g);
then consider t being Element of Funcs(NAT,REAL) such that
A24: x = t and
A25: ex c,N st c > 0 & for n st n >= N holds t.n <= c*(f+g).n & t.n >= 0;
consider c,N3 such that
A26: c > 0 and
A27: for n st n >= N3 holds t.n <= c*(f+g).n & t.n >= 0 by A25;
consider N1 being Nat such that
A28: for n being Nat st n >= N1 holds f.n >= 0 by Def2;
consider N2 being Nat such that
A29: for n being Nat st n >= N2 holds g.n >= 0 by Def2;
reconsider N = max(N3,max(N1,N2)) as Element of NAT
by ORDINAL1:def 12;
A30: N >= max(N1,N2) by XXREAL_0:25;
defpred Q[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 Q[x,y]
proof
let n;
per cases;
suppose
A32: t.n <= c*f.n;
0 in REAL by XREAL_0:def 1;
hence thesis by A32 ;
end;
suppose
A33: c*f.n < t.n;
reconsider y = t.n-c*f.n as Element of REAL by XREAL_0:def 1;
take y;
thus thesis by A33;
end;
end;
consider g9 being sequence of REAL such that
A34: for x being Element of NAT holds Q[x,g9.x] from FUNCT_2:sch 3(A31);
A35: N >= N3 by XXREAL_0:25;
A36: g9 is Element of Funcs(NAT,REAL) by FUNCT_2:8;
max(N1,N2) >= N2 by XXREAL_0:25;
then
A37: N >= N2 by A30,XXREAL_0:2;
now
let n;
assume
A38: n >= N;
then n >= N3 by A35,XXREAL_0:2;
then
A39: t.n <= c*(f+g).n by A27;
n >= N2 by A37,A38,XXREAL_0:2;
then g.n >= 0 by A29;
then
A40: 0*g.n <= c*g.n by A26;
per cases;
suppose
t.n <= c*f.n;
hence g9.n <= c*g.n & g9.n >= 0 by A34,A40;
end;
suppose
A41: t.n > c*f.n;
t.n <= c*(f.n+g.n) by A39,SEQ_1:7;
then t.n <= c*f.n + c*g.n;
then
A42: t.n - c*f.n <= c*g.n by XREAL_1:20;
t.n > 0 + c*f.n by A41;
then t.n - c*f.n >= 0 by XREAL_1:19;
hence g9.n <= c*g.n & g9.n >= 0 by A34,A42;
end;
end;
then
A43: g9 in Big_Oh(g) by A26,A36;
defpred P[Element of NAT,Real] means (t.$1 <= c*f.$1 implies $2 = t.$1) &
(c*f.$1 < t.$1 implies $2 = c*f.$1);
A44: for x being Element of NAT ex y being Element of REAL st P[x,y]
proof
let n;
per cases;
suppose
t.n <= c*f.n;
hence thesis;
end;
suppose
A45: c*f.n < t.n;
reconsider y = c*f.n as Element of REAL by XREAL_0:def 1;
take y;
thus thesis by A45;
end;
end;
consider f9 being sequence of REAL such that
A46: for x being Element of NAT holds P[x,f9.x] from FUNCT_2:sch 3(A44
);
A47: now
let n be Element of NAT;
per cases;
suppose
A48: t.n <= c*f.n;
then g9.n = 0 by A34;
hence t.n = f9.n + g9.n by A46,A48;
end;
suppose
c*f.n < t.n;
then f9.n = c*f.n & g9.n = t.n - c*f.n by A46,A34;
hence f9.n + g9.n = t.n;
end;
end;
A49: f9 is Element of Funcs(NAT,REAL) by FUNCT_2:8;
max(N1,N2) >= N1 by XXREAL_0:25;
then
A50: N >= N1 by A30,XXREAL_0:2;
now
let n;
assume
A51: n >= N;
then n >= N3 by A35,XXREAL_0:2;
then
A52: t.n >= 0 by A27;
n >= N1 by A50,A51,XXREAL_0:2;
then
A53: f.n >= 0 by A28;
per cases;
suppose
t.n <= c*f.n;
hence f9.n <= c*f.n & f9.n >= 0 by A46,A52;
end;
suppose
t.n > c*f.n;
hence f9.n <= c*f.n & f9.n >= 0 by A26,A46,A53;
end;
end;
then f9 in Big_Oh(f) by A26,A49;
hence x in Big_Oh(f) + Big_Oh(g) by A24,A49,A36,A43,A47;
end;
hence thesis by TARSKI:2;
end;
theorem :: Properties, Part 3 (page 91; Problem 3.33)
for f,g being eventually-nonnegative Real_Sequence holds max(Big_Oh(f)
, Big_Oh(g)) = Big_Oh(max(f,g))
proof
let f,g be eventually-nonnegative Real_Sequence;
now
let x be object;
hereby
assume x in max(Big_Oh(f), Big_Oh(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,N st c > 0 & for n st n >= N holds s.n <= c*g.n & s.n >= 0 by A4;
consider d,N2 such that
A8: d > 0 and
A9: for n 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,N st c > 0 & for n st n >= N holds r.n <= c*f.n & r.n >= 0 by A3;
consider c,N1 such that
A12: c > 0 and
A13: for n st n >= N1 holds r.n <= c*f.n & r.n >= 0 by A11;
set e = max(c,d);
A14: e > 0 by A12,XXREAL_0:25;
reconsider N = max(N1,N2) as Element of NAT;
A15: N >= N2 by XXREAL_0:25;
A16: N >= N1 by XXREAL_0:25;
now
let n;
assume
A17: n >= N;
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 <= e*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 <= e*g.n by XREAL_1:64,XXREAL_0:25;
s.n <= d*g.n by A9,A20;
then
A22: s.n <= e*g.n by A21,XXREAL_0:2;
e*g.n <= e*max(f.n, g.n) by A14,XREAL_1:64,XXREAL_0:25;
then
A23: s.n <= e*max(f.n, g.n) by A22,XXREAL_0:2;
r.n <= c*f.n by A13,A18;
then
A24: r.n <= e*f.n by A19,XXREAL_0:2;
e*f.n <= e*max(f.n, g.n) by A14,XREAL_1:64,XXREAL_0:25;
then r.n <= e*max(f.n, g.n) by A24,XXREAL_0:2;
then max(r.n, s.n) <= e*max(f.n, g.n) by A23,XXREAL_0:28;
then max(r.n, s.n) <= e*max(f,g).n by Def7;
hence t.n <= e*max(f,g).n by A5,A10,A6;
max(f9.n, g9.n) >= f9.n & f9.n >= 0 by A10,A13,A18,XXREAL_0:25;
hence t.n >= 0 by A5;
end;
hence x in Big_Oh(max(f,g)) by A1,A14;
end;
assume x in Big_Oh(max(f,g));
then consider t being Element of Funcs(NAT,REAL) such that
A25: x = t and
A26: ex c,N st c > 0 & for n st n >= N holds t.n <= c*max(f,g).n & t.n >= 0;
consider c,N3 such that
A27: c > 0 and
A28: for n st n >= N3 holds t.n <= c*max(f,g).n & t.n >= 0 by A26;
consider N1 being Nat such that
A29: for n being Nat st n >= N1 holds f.n >= 0 by Def2;
consider N2 being Nat such that
A30: for n being Nat st n >= N2 holds g.n >= 0 by Def2;
reconsider N = max(N3,max(N1,N2)) as Element of NAT
by ORDINAL1:def 12;
defpred P[Element of NAT,Real] means (f.$1 >= g.$1 or $1 < N implies $2 =
t.$1) & (f.$1 < g.$1 & $1 >= N implies $2 = 0);
defpred Q[Element of NAT,Real] means (f.$1 >= g.$1 & $1 >= N implies $2 =
0) & (f.$1 < g.$1 or $1 < N implies $2 = t.$1);
A31: for x being Element of NAT ex y being Element of REAL st P[x,y]
proof
let n;
per cases;
suppose
f.n >= g.n;
hence thesis;
end;
suppose
A32: f.n < g.n;
thus thesis
proof
per cases;
suppose
n < N;
hence thesis;
end;
suppose
A33: n >= N;
0 in REAL by XREAL_0:def 1;
hence thesis by A32,A33;
end;
end;
end;
end;
consider f9 being sequence of REAL such that
A34: for x being Element of NAT holds P[x,f9.x] from FUNCT_2:sch 3(A31
);
A35: for x being Element of NAT ex y being Element of REAL st Q[x,y]
proof
let n;
per cases;
suppose
A36: f.n >= g.n;
thus thesis
proof
per cases;
suppose
n < N;
hence thesis;
end;
suppose
A37: n >= N;
0 in REAL by XREAL_0:def 1;
hence thesis by A36,A37;
end;
end;
end;
suppose
f.n < g.n;
hence thesis;
end;
end;
consider g9 being sequence of REAL such that
A38: for x being Element of NAT holds Q[x,g9.x] from FUNCT_2:sch 3(A35
);
A39: N >= N3 by XXREAL_0:25;
A40: now
let n be Element of NAT;
per cases;
suppose
n < N;
then f9.n = t.n & g9.n = t.n by A34,A38;
hence t.n = max(f9.n, g9.n);
end;
suppose
A41: n >= N;
then
A42: n >= N3 by A39,XXREAL_0:2;
thus t.n = max(f9.n, g9.n)
proof
per cases;
suppose
A43: f.n >= g.n;
A44: t.n >= 0 by A28,A42;
f9.n = t.n & g9.n = 0 by A34,A38,A41,A43;
hence thesis by A44,XXREAL_0:def 10;
end;
suppose
A45: f.n < g.n;
A46: t.n >= 0 by A28,A42;
f9.n = 0 & g9.n = t.n by A34,A38,A41,A45;
hence thesis by A46,XXREAL_0:def 10;
end;
end;
end;
end;
A47: g9 is Element of Funcs(NAT,REAL) by FUNCT_2:8;
A48: N >= max(N1,N2) by XXREAL_0:25;
max(N1,N2) >= N2 by XXREAL_0:25;
then
A49: N >= N2 by A48,XXREAL_0:2;
now
let n;
assume
A50: n >= N;
then n >= N3 by A39,XXREAL_0:2;
then
A51: t.n >= 0 & t.n <= c*max(f,g).n by A28;
n >= N2 by A49,A50,XXREAL_0:2;
then g.n >= 0 by A30;
then
A52: 0*g.n <= c*g.n by A27;
per cases;
suppose
f.n >= g.n;
hence g9.n <= c*g.n & g9.n >= 0 by A38,A50,A52;
end;
suppose
A53: f.n < g.n;
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 A38,A51,A53;
end;
end;
then
A54: g9 in Big_Oh(g) by A27,A47;
A55: f9 is Element of Funcs(NAT,REAL) by FUNCT_2:8;
max(N1,N2) >= N1 by XXREAL_0:25;
then
A56: N >= N1 by A48,XXREAL_0:2;
now
let n;
assume
A57: n >= N;
then n >= N3 by A39,XXREAL_0:2;
then
A58: t.n >= 0 & t.n <= c*max(f,g).n by A28;
n >= N1 by A56,A57,XXREAL_0:2;
then f.n >= 0 by A29;
then
A59: 0*f.n <= c*f.n by A27;
per cases;
suppose
A60: f.n >= g.n;
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 A34,A58,A60;
end;
suppose
f.n < g.n;
hence f9.n <= c*f.n & f9.n >= 0 by A34,A57,A59;
end;
end;
then f9 in Big_Oh(f) by A27,A55;
hence x in max(Big_Oh(f), Big_Oh(g)) by A25,A55,A47,A54,A40;
end;
hence thesis by TARSKI:2;
end;
definition :: Definition of operators on sets (page 92)
let F,G be FUNCTION_DOMAIN of NAT,REAL;
func F to_power G -> FUNCTION_DOMAIN of NAT,REAL equals
{ t where t is
Element of Funcs(NAT,REAL) : ex f,g being Element of Funcs(NAT,REAL), N being
Element of NAT st f in F & g in G & for n being Element of NAT st n >= N holds
t.n = (f.n) to_power (g.n) };
coherence
proof
set IT = { t where t is Element of Funcs(NAT,REAL) : ex f,g being Element
of Funcs(NAT,REAL), N being Element of NAT st f in F & g in G & for n being
Element of NAT st n >= N holds t.n = (f.n) to_power (g.n) };
A1: now
consider g be object such that
A2: g in G by XBOOLE_0:def 1;
g is sequence of REAL by A2,FUNCT_2:def 12;
then reconsider g as Element of Funcs(NAT,REAL) by FUNCT_2:8;
consider f be object such that
A3: f in F by XBOOLE_0:def 1;
f is sequence of REAL by A3,FUNCT_2:def 12;
then reconsider f as Element of Funcs(NAT,REAL) by FUNCT_2:8;
defpred P[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 P[x,y]
proof let x being Element of NAT;
reconsider y = (f.x) to_power (g.x) as Element of REAL
by XREAL_0:def 1;
take y;
thus thesis;
end;
consider t being sequence of REAL such that
A5: for x being Element of NAT holds P[x,t.x] from FUNCT_2:sch 3(A4
);
reconsider 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 IT by A3,A2;
hence IT is non empty;
end;
IT is functional
proof
let x be object;
assume x in IT;
then ex t being Element of Funcs(NAT, REAL) st x = t & ex f,g being
Element of Funcs(NAT,REAL), N being Element of NAT st f in F & g in G & for n
being Element of NAT st n >= N holds t.n = (f.n) to_power (g.n);
hence thesis;
end;
then reconsider IT1 = IT as functional non empty set by A1;
now
let x be Element of IT1;
x in IT;
then ex t being Element of Funcs(NAT, REAL) st x = t & ex f,g being
Element of Funcs(NAT,REAL), N being Element of NAT st f in F & g in G & for n
being Element of NAT st n >= N holds t.n = (f.n) to_power (g.n);
hence x is sequence of REAL;
end;
hence thesis by FUNCT_2:def 12;
end;
end;