(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.|

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 A11,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;