environ
vocabularies HIDDEN, NUMBERS, REAL_1, SUBSET_1, SEQ_1, FDIFF_1, FUNCT_1, PARTFUN1, PARTFUN3, ARYTM_1, VALUED_0, ORDINAL2, CARD_1, RELAT_1, ARYTM_3, XXREAL_0, COMPLEX1, NAT_1, TARSKI, VALUED_1, FUNCT_2, SQUARE_1, XBOOLE_0, ORDINAL4, LIMFUNC1, FUNCT_7, ASYMPT_1, POWER, ASYMPT_0, FINSET_1, ORDINAL1, INT_1, CARD_3, AFINSQ_1, FINSEQ_1, TAYLOR_1, ASYMPT_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FINSET_1, PARTFUN2, PARTFUN3, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, INT_1, VALUED_0, COMPLEX1, VALUED_1, SEQ_1, RFUNCT_1, RVSUM_1, FDIFF_1, POWER, SERIES_1, LIMFUNC1, ASYMPT_0, ASYMPT_1, AFINSQ_1, TAYLOR_1, AFINSQ_2;
definitions ;
theorems TARSKI, FUNCT_1, FUNCT_2, NAT_1, SEQ_1, SEQM_3, ABSVALUE, PARTFUN3, RFUNCT_1, FDIFF_1, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, COMPLEX1, XREAL_1, XXREAL_0, ORDINAL1, VALUED_1, XXREAL_1, VALUED_0, XREAL_0, AFINSQ_1, AFINSQ_2, INT_1, ASYMPT_0, ASYMPT_1, POWER, PRE_FF, FDIFF_2, TAYLOR_1, FIB_NUM2, ENTROPY1, PREPOWER, NEWTON;
schemes NAT_1, SEQ_1, AFINSQ_2;
registrations ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, MEMBERED, POWER, FCONT_3, VALUED_0, VALUED_1, SQUARE_1, AFINSQ_1, AFINSQ_2, XBOOLE_0, RELAT_1, INT_1, ASYMPT_0, ASYMPT_1, FUNCT_1, PARTFUN3;
constructors HIDDEN, REAL_1, SQUARE_1, RCOMP_1, PARTFUN2, PARTFUN3, LIMFUNC1, FDIFF_1, RELSET_1, RVSUM_1, NEWTON, PREPOWER, SERIES_1, ASYMPT_0, AFINSQ_2, ASYMPT_1, TAYLOR_1, SIN_COS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities SQUARE_1, SUBSET_1, LIMFUNC1, AFINSQ_1, ORDINAL1, TAYLOR_1, ASYMPT_0, POWER;
expansions TARSKI, FUNCT_1, FUNCT_2, FDIFF_1, ASYMPT_0, PARTFUN3;
LMC31X:
for m, n being Nat st 2 <= m holds
n < m to_power n
by NEWTON:86;
Lm5:
( dom (id ([#] REAL)) = [#] REAL & ( for x being Real holds (id ([#] REAL)) . x = x ) & ( for x being Real holds
( id ([#] REAL) is_differentiable_in x & diff ((id ([#] REAL)),x) = 1 ) ) )
LEMC01:
for x, n, a being Nat st 0 < a & a <= x holds
a to_power n <= x to_power n
by PREPOWER:9;
LMC31:
for r being Real ex N being Element of NAT st
for n being Nat st N <= n holds
r < n / (log (2,n))
LMC31HC:
ex N being Element of NAT st
for n being Nat st N <= n holds
4 < n / (log (2,n))
theorem
for
x being
Nat st 1
< x holds
ex
N being
Nat st
for
n being
Nat st
N <= n holds
4
< n / (log (x,n))
FROMASYMPT1t11:
for a, b being Nat st a < b holds
seq_n^ a in Big_Oh (seq_n^ b)
LMXFIN3:
for d being XFinSequence of REAL
for k being Nat st len d = k + 1 holds
ex a being Real ex d1 being XFinSequence of REAL st
( len d1 = k & d1 = d | k & a = d . k & d = d1 ^ <%a%> )
LMXFIN7:
for k being Nat
for x, y being Real_Sequence st x in Big_Oh (seq_n^ k) & y in Big_Oh (seq_n^ k) holds
x + y in Big_Oh (seq_n^ k)
LMXFIN9:
for k being Nat holds Big_Oh (seq_n^ k) c= Big_Oh (seq_n^ (k + 1))
TLNEG42:
for d being XFinSequence of REAL st ( for i being Nat st i in dom d holds
0 <= d . i ) holds
ex M being Real st
( 0 <= M & ( for i being Nat st i in dom d holds
d . i <= M ) )