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 H1( Element of NAT ) -> Element of REAL = (t . $1) / (f . $1);
reconsider B = { H1(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) )
assume n < N ; :: thesis: t . n <= (max B) * (f . n)
then (t . n) / (f . n) in B ;
then A8: (t . n) / (f . n) <= max B by XXREAL_2:def 8;
A9: f . n > 0 by Def5;
then ((t . n) / (f . n)) * (f . n) <= (max B) * (f . n) by A8, XREAL_1:66;
hence t . n <= (max B) * (f . n) by A9, XCMPLX_1:88; :: 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 A10: 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 A11: n < N ; :: thesis: t . n <= c * (f . n)
f . n > 0 by Def5;
then ( t . n <= (max B) * (f . n) & (max B) * (f . n) <= c * (f . n) ) by A7, A10, A11, XREAL_1:66;
hence t . n <= c * (f . n) by 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 Def5;
then ( t . n <= c * (f . n) & c * (f . n) <= b * (f . n) ) by A1, A4, A12, A13, XREAL_1:66;
hence t . n <= b * (f . n) by XXREAL_0:2; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;
end;
given c being Real such that A14: ( c > 0 & ( for n being Element of NAT holds t . n <= c * (f . n) ) ) ; :: thesis: t in Big_Oh f
A15: t is Element of Funcs NAT ,REAL by FUNCT_2:11;
consider N being Element of NAT such that
A16: for n being Element of NAT st n >= N holds
t . n >= 0 by Def4;
for n being Element of NAT st n >= N holds
( t . n <= c * (f . n) & t . n >= 0 ) by A14, A16;
hence t in Big_Oh f by A14, A15; :: thesis: verum