let f be eventually-positive Real_Sequence; :: thesis: for t being eventually-nonnegative Real_Sequence
for N being Element of NAT st t in Big_Oh f & ( for n being Element of NAT st n >= N holds
f . n > 0 ) holds
ex c being Real st
( c > 0 & ( for n being Element of NAT st n >= N holds
t . n <= c * (f . n) ) )
let t be eventually-nonnegative Real_Sequence; :: thesis: for N being Element of NAT st t in Big_Oh f & ( for n being Element of NAT st n >= N holds
f . n > 0 ) holds
ex c being Real st
( c > 0 & ( for n being Element of NAT st n >= N holds
t . n <= c * (f . n) ) )
let N be Element of NAT ; :: thesis: ( t in Big_Oh f & ( for n being Element of NAT st n >= N holds
f . n > 0 ) implies ex c being Real st
( c > 0 & ( for n being Element of NAT st n >= N holds
t . n <= c * (f . n) ) ) )
assume that
A1: t in Big_Oh f and
A2: for n being Element of NAT st n >= N holds
f . n > 0 ; :: thesis: ex c being Real st
( c > 0 & ( for n being Element of NAT st n >= N holds
t . n <= c * (f . n) ) )
deffunc H₁( Element of NAT ) -> Element of REAL = t . $1;
deffunc H₂( Element of NAT ) -> Element of REAL = f . $1;
ex s being Element of Funcs (NAT,REAL) st
( t = s & ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( s . n <= c * (f . n) & s . n >= 0 ) ) ) ) by A1;
then consider c2 being Real, M being Element of NAT such that
A3: c2 > 0 and
A4: for n being Element of NAT st n >= M holds
( t . n <= c2 * (f . n) & t . n >= 0 ) ;
set fset = { H₂(n) where n is Element of NAT : ( N <= n & n <= max (M,N) ) } ;
A5: N <= max (M,N) by XXREAL_0:25;
{ H₂(n) where n is Element of NAT : ( N <= n & n <= max (M,N) ) } is non empty finite Subset of REAL from ASYMPT_0:sch 1(A5);
then reconsider fset = { H₂(n) where n is Element of NAT : ( N <= n & n <= max (M,N) ) } as non empty finite Subset of REAL ;
set F = min fset;
A6: M <= max (M,N) by XXREAL_0:25;
set tset = { H₁(n) where n is Element of NAT : ( N <= n & n <= max (M,N) ) } ;
{ H₁(n) where n is Element of NAT : ( N <= n & n <= max (M,N) ) } is non empty finite Subset of REAL from ASYMPT_0:sch 1(A5);
then reconsider tset = { H₁(n) where n is Element of NAT : ( N <= n & n <= max (M,N) ) } as non empty finite Subset of REAL ;
set T = max tset;
set c1 = (max tset) / (min fset);
reconsider c = max (((max tset) / (min fset)),c2) as Element of REAL by XREAL_0:def 1;
take c ; :: thesis: ( c > 0 & ( for n being Element of NAT st n >= N holds
t . n <= c * (f . n) ) )
thus c > 0 by A3, XXREAL_0:25; :: thesis: for n being Element of NAT st n >= N holds
t . n <= c * (f . n)
let n be Element of NAT ; :: thesis: ( n >= N implies t . n <= c * (f . n) )
assume A7: n >= N ; :: thesis: t . n <= c * (f . n)
then A8: f . n > 0 by A2;
A9: f . n <> 0 by A2, A7;
min fset in fset by XXREAL_2:def 7;
then A10: ex n1 being Element of NAT st
( f . n1 = min fset & n1 >= N & n1 <= max (M,N) ) ;
then A11: min fset > 0 by A2;
A12: min fset <> 0 by A2, A10;

per cases ( N >= M or N <= M ) ;

suppose N >= M ; :: thesis: t . n <= c * (f . n)

then n >= M by A7, XXREAL_0:2;
then A13: t . n <= c2 * (f . n) by A4;
c2 * (f . n) <= c * (f . n) by A8, XREAL_1:64, XXREAL_0:25;
hence t . n <= c * (f . n) by A13, XXREAL_0:2; :: thesis: verum

end;

suppose A14: N <= M ; :: thesis: t . n <= c * (f . n)

thus t . n <= c * (f . n) :: thesis: verum

proof

per cases ( n <= M or n >= M ) ;

suppose n <= M ; :: thesis: t . n <= c * (f . n)

then A15: n <= max (M,N) by A6, XXREAL_0:2;
then t . n in tset by A7;
then A16: t . n <= max tset by XXREAL_2:def 8;
f . n in fset by A7, A15;
then A17: f . n >= min fset by XXREAL_2:def 7;
t . M in tset by A6, A14;
then A18: t . M <= max tset by XXREAL_2:def 8;
t . M >= 0 by A4;
then A19: ((max tset) / (min fset)) * (f . n) >= ((max tset) / (min fset)) * (min fset) by A11, A18, A17, XREAL_1:64;

now :: thesis: not (t . n) / (f . n) > (max tset) / (min fset)

assume (t . n) / (f . n) > (max tset) / (min fset) ; :: thesis: contradiction
then ((t . n) / (f . n)) * (f . n) > ((max tset) / (min fset)) * (f . n) by A8, XREAL_1:68;
then t . n > ((max tset) / (min fset)) * (f . n) by A9, XCMPLX_1:87;
then max tset > ((max tset) / (min fset)) * (f . n) by A16, XXREAL_0:2;
hence contradiction by A12, A19, XCMPLX_1:87; :: thesis: verum

end;

then ((t . n) / (f . n)) * (f . n) <= ((max tset) / (min fset)) * (f . n) by A8, XREAL_1:64;
then A20: t . n <= ((max tset) / (min fset)) * (f . n) by A9, XCMPLX_1:87;
((max tset) / (min fset)) * (f . n) <= c * (f . n) by A8, XREAL_1:64, XXREAL_0:25;
hence t . n <= c * (f . n) by A20, XXREAL_0:2; :: thesis: verum

end;

suppose A21: n >= M ; :: thesis: t . n <= c * (f . n)

A22: c2 * (f . n) <= c * (f . n) by A8, XREAL_1:64, XXREAL_0:25;
t . n <= c2 * (f . n) by A4, A21;
hence t . n <= c * (f . n) by A22, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;

end;