let f be positive Real_Sequence; :: thesis: for t being eventually-nonnegative Real_Sequence holds
( t in Big_Oh f iff ex c being Real st
( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) ) )
let t be eventually-nonnegative Real_Sequence; :: thesis: ( t in Big_Oh f iff ex c being Real st
( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) ) )

hereby :: thesis: ( ex c being Real st
( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) ) implies t in Big_Oh f )

assume t in Big_Oh f ; :: thesis: ex c being Real st
( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) )
then consider s being Element of Funcs (NAT,REAL) such that
A1: t = s and
A2: ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( s . n <= c * (f . n) & s . n >= 0 ) ) ) ;
consider c being Real, N being Element of NAT such that
A3: c > 0 and
A4: for n being Element of NAT st n >= N holds
( s . n <= c * (f . n) & s . n >= 0 ) by A2;

per cases ( N = 0 or N > 0 ) ;

suppose A5: N = 0 ; :: thesis: ex c being Real st
( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) )

take c = c; :: thesis: ( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) )
thus c > 0 by A3; :: thesis: for n being Element of NAT holds t . n <= c * (f . n)
let n be Element of NAT ; :: thesis: t . n <= c * (f . n)
thus t . n <= c * (f . n) by A1, A4, A5; :: thesis: verum

end;

suppose A6: N > 0 ; :: thesis: ex c being Real st
( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) )

deffunc H₁( Element of NAT ) -> Element of REAL = (t . $1) / (f . $1);
reconsider B = { H₁(n) where n is Element of NAT : n < N } as non empty finite Subset of REAL from ASYMPT_0:sch 3(A6);
set b = max B;
A7: for n being Element of NAT st n < N holds
t . n <= (max B) * (f . n)

proof

let n be Element of NAT ; :: thesis: ( n < N implies t . n <= (max B) * (f . n) )
A8: f . n > 0 by Def3;
assume n < N ; :: thesis: t . n <= (max B) * (f . n)
then (t . n) / (f . n) in B ;
then (t . n) / (f . n) <= max B by XXREAL_2:def 8;
then ((t . n) / (f . n)) * (f . n) <= (max B) * (f . n) by A8, XREAL_1:64;
hence t . n <= (max B) * (f . n) by A8, XCMPLX_1:87; :: thesis: verum

end;

thus ex c being Real st
( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) ) :: thesis: verum

proof

per cases ( max B <= c or max B > c ) ;

suppose A9: max B <= c ; :: thesis: ex c being Real st
( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) )

take c ; :: thesis: ( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) )
thus c > 0 by A3; :: thesis: for n being Element of NAT holds t . n <= c * (f . n)
let n be Element of NAT ; :: thesis: t . n <= c * (f . n)
thus t . n <= c * (f . n) :: thesis: verum

proof

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

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

f . n > 0 by Def3;
then A11: (max B) * (f . n) <= c * (f . n) by A9, XREAL_1:64;
t . n <= (max B) * (f . n) by A7, A10;
hence t . n <= c * (f . n) by A11, XXREAL_0:2; :: thesis: verum

end;

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

hence t . n <= c * (f . n) by A1, A4; :: thesis: verum

end;

end;

end;

end;

suppose A12: max B > c ; :: thesis: ex c being Real st
( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) )

reconsider b = max B as Element of REAL by XREAL_0:def 1;
take b ; :: thesis: ( b > 0 & ( for n being Element of NAT holds t . n <= b * (f . n) ) )
thus b > 0 by A3, A12; :: thesis: for n being Element of NAT holds t . n <= b * (f . n)
let n be Element of NAT ; :: thesis: t . n <= b * (f . n)
thus t . n <= b * (f . n) :: thesis: verum

proof

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

suppose n < N ; :: thesis: t . n <= b * (f . n)

hence t . n <= b * (f . n) by A7; :: thesis: verum

end;

suppose A13: n >= N ; :: thesis: t . n <= b * (f . n)

f . n > 0 by Def3;
then A14: c * (f . n) <= b * (f . n) by A12, XREAL_1:64;
t . n <= c * (f . n) by A1, A4, A13;
hence t . n <= b * (f . n) by A14, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

end;

end;

given c being Real such that A15: c > 0 and
A16: for n being Element of NAT holds t . n <= c * (f . n) ; :: thesis: t in Big_Oh f
consider N being 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 being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) ) ) by A16, A17, FUNCT_2:8;
hence t in Big_Oh f by A15, A18; :: thesis: verum