environ
vocabularies HIDDEN, NUMBERS, XBOOLE_0, SUBSET_1, NAT_1, REAL_1, FINSEQ_1, MATRIX_1, CARD_1, ARYTM_3, XXREAL_0, INT_1, ARYTM_1, RELAT_1, TAYLOR_1, FUNCT_1, XXREAL_1, LIMFUNC1, POWER, PARTFUN1, FDIFF_1, ORDINAL2, TARSKI, CARD_3, SEQ_1, SUPINF_2, PARTFUN3, RVSUM_1, ORDINAL4, FINSEQ_2, MATRPROB, MATRIXC1, TREES_1, INCSP_1, MATRIXR1, FVSUM_1, ZFMISC_1, FUNCOP_1, ENTROPY1, FUNCT_7, XCMPLX_0;
notations HIDDEN, TARSKI, SUBSET_1, XBOOLE_0, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, ORDINAL1, NAT_1, NAT_D, NUMBERS, RELAT_1, FUNCT_1, VALUED_1, SEQ_1, ZFMISC_1, PARTFUN1, FUNCOP_1, RVSUM_1, FINSEQ_1, NEWTON, FINSEQ_2, MATRIXR1, MATRIX_0, PARTFUN3, POWER, LIMFUNC1, RCOMP_1, MATRPROB, FDIFF_1, TAYLOR_1, FCONT_1;
definitions TARSKI, PARTFUN3;
theorems FUNCT_1, NAT_1, XREAL_1, NAT_2, MATRIXR1, XBOOLE_0, PROB_3, INTEGRA5, FINSEQ_1, MATRIX_0, FINSEQ_2, FINSEQ_3, RVSUM_1, POWER, FDIFF_1, TREES_1, XBOOLE_1, TAYLOR_1, RELAT_1, ROLLE, FCONT_1, XCMPLX_1, INTEGRA1, XXREAL_0, ORDINAL1, MATRPROB, FUNCOP_1, PEPIN, NAT_D, PARTFUN1, VALUED_1, XXREAL_1, XXREAL_2, CARD_1, XREAL_0;
schemes FINSEQ_2, SEQ_1, NAT_1, RECDEF_1, FINSEQ_1, MATRIX_0;
registrations MATRPROB, RELSET_1, NAT_1, MEMBERED, ORDINAL1, XREAL_0, FCONT_3, RCOMP_1, XXREAL_0, NUMBERS, XBOOLE_0, VALUED_0, FINSEQ_1, CARD_1, XXREAL_2, FINSEQ_2, RVSUM_1;
constructors HIDDEN, REAL_1, NAT_D, BINOP_2, MATRIX_3, MATRIXR1, MATRLIN, MATRPROB, PARTFUN3, PARTFUN2, FDIFF_1, FCONT_1, POWER, LIMFUNC1, SIN_COS, TAYLOR_1, INTEGRA1, XXREAL_2, RVSUM_1, RELSET_1, NEWTON, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities FINSEQ_2, LIMFUNC1, RCOMP_1, VALUED_1, XCMPLX_0, TAYLOR_1;
expansions PARTFUN3;
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
theorem Th2:
for
r being
Real st
r > 0 holds
(
ln . r <= r - 1 & (
r = 1 implies
ln . r = r - 1 ) & (
ln . r = r - 1 implies
r = 1 ) & (
r <> 1 implies
ln . r < r - 1 ) & (
ln . r < r - 1 implies
r <> 1 ) )
theorem Th4:
for
a,
b being
Real st
a > 1 &
b > 1 holds
log (
a,
b)
> 0
definition
let MR be
Matrix of
REAL;
assume A1:
MR is
m-nonnegative
;
existence
ex b1 being Matrix of REAL st
( len b1 = len MR & width b1 = width MR & ( for k being Nat st k in dom b1 holds
b1 . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) )
uniqueness
for b1, b2 being Matrix of REAL st len b1 = len MR & width b1 = width MR & ( for k being Nat st k in dom b1 holds
b1 . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) & len b2 = len MR & width b2 = width MR & ( for k being Nat st k in dom b2 holds
b2 . k = mlt ((Line (MR,k)),(FinSeq_log (2,(Line (MR,k))))) ) holds
b1 = b2
end;