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) ) )
consider s being Element of Funcs NAT ,REAL such that
A3: t = s and
A4: 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;
consider c2 being Real, M being Element of NAT such that
A5: c2 > 0 and
A6: for n being Element of NAT st n >= M holds
( t . n <= c2 * (f . n) & t . n >= 0 ) by A3, A4;
deffunc H₁( Element of NAT ) -> Element of REAL = t . $1;
set tset = { H₁(n) where n is Element of NAT : ( N <= n & n <= max M,N ) } ;
deffunc H₂( Element of NAT ) -> Element of REAL = f . $1;
set fset = { H₂(n) where n is Element of NAT : ( N <= n & n <= max M,N ) } ;
A7: M <= max M,N by XXREAL_0:25;
A8: 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(A8);
then reconsider tset = { H₁(n) where n is Element of NAT : ( N <= n & n <= max M,N ) } as non empty finite Subset of REAL ;
{ 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(A8);
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 T = max tset;
set F = min fset;
min fset in fset by XXREAL_2:def 7;
then consider n1 being Element of NAT such that
A9: ( f . n1 = min fset & n1 >= N & n1 <= max M,N ) ;
A10: min fset > 0 by A2, A9;
A11: min fset <> 0 by A2, A9;
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 A5, 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 A12: n >= N ; :: thesis: t . n <= c * (f . n)
then A13: f . n > 0 by A2;
A14: f . n <> 0 by A2, A12;

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

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

then n >= M by A12, XXREAL_0:2;
then A15: t . n <= c2 * (f . n) by A6;
c2 * (f . n) <= c * (f . n) by A13, XREAL_1:66, XXREAL_0:25;
hence t . n <= c * (f . n) by A15, XXREAL_0:2; :: thesis: verum

end;

suppose A16: 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 A17: n <= max M,N by A7, XXREAL_0:2;
then t . n in tset by A12;
then A18: t . n <= max tset by XXREAL_2:def 8;
A19: t . M >= 0 by A6;
t . M in tset by A7, A16;
then A20: t . M <= max tset by XXREAL_2:def 8;
A21: (max tset) / (min fset) >= 0 by A19, A20, A10;
f . n in fset by A12, A17;
then f . n >= min fset by XXREAL_2:def 7;
then A22: ((max tset) / (min fset)) * (f . n) >= ((max tset) / (min fset)) * (min fset) by A21, XREAL_1:66;

now

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 A13, XREAL_1:70;
then t . n > ((max tset) / (min fset)) * (f . n) by A14, XCMPLX_1:88;
then max tset > ((max tset) / (min fset)) * (f . n) by A18, XXREAL_0:2;
hence contradiction by A11, A22, XCMPLX_1:88; :: thesis: verum

end;

then ((t . n) / (f . n)) * (f . n) <= ((max tset) / (min fset)) * (f . n) by A13, XREAL_1:66;
then A23: t . n <= ((max tset) / (min fset)) * (f . n) by A14, XCMPLX_1:88;
((max tset) / (min fset)) * (f . n) <= c * (f . n) by A13, XREAL_1:66, XXREAL_0:25;
hence t . n <= c * (f . n) by A23, XXREAL_0:2; :: thesis: verum

end;

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

then A24: t . n <= c2 * (f . n) by A6;
c2 * (f . n) <= c * (f . n) by A13, XREAL_1:66, XXREAL_0:25;
hence t . n <= c * (f . n) by A24, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;

end;