begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
Lm1:
for r being Real
for m being Matrix of holds
( ( for i, j being Element of NAT st [i,j] in Indices m holds
m * i,j >= r ) iff for i, j being Element of NAT st i in dom m & j in dom (m . i) holds
(m . i) . j >= r )
Lm2:
for r being Real
for m being Matrix of holds
( ( for i, j being Element of NAT st [i,j] in Indices m holds
m * i,j >= r ) iff for i, j being Element of NAT st i in dom m & j in dom (Line m,i) holds
(Line m,i) . j >= r )
Lm3:
for r being Real
for m being Matrix of holds
( ( for i, j being Element of NAT st [i,j] in Indices m holds
m * i,j >= r ) iff for i, j being Element of NAT st j in Seg (width m) & i in dom (Col m,j) holds
(Col m,j) . i >= r )
:: deftheorem Def1 defines Sum MATRPROB:def 1 :
theorem Th20:
:: deftheorem Def2 defines ColSum MATRPROB:def 2 :
theorem
theorem Th22:
:: deftheorem defines SumAll MATRPROB:def 3 :
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
definition
let x,
y be
FinSequence of
REAL ;
let M be
Matrix of ;
assume that A1:
len x = len M
and A2:
len y = width M
;
func QuadraticForm x,
M,
y -> Matrix of
means :
Def4:
(
len it = len x &
width it = len y & ( for
i,
j being
Nat st
[i,j] in Indices M holds
it * i,
j = ((x . i) * (M * i,j)) * (y . j) ) );
existence
ex b1 being Matrix of st
( len b1 = len x & width b1 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b1 * i,j = ((x . i) * (M * i,j)) * (y . j) ) )
uniqueness
for b1, b2 being Matrix of st len b1 = len x & width b1 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b1 * i,j = ((x . i) * (M * i,j)) * (y . j) ) & len b2 = len x & width b2 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b2 * i,j = ((x . i) * (M * i,j)) * (y . j) ) holds
b1 = b2
end;
:: deftheorem Def4 defines QuadraticForm MATRPROB:def 4 :
theorem
theorem Th44:
theorem
theorem Th46:
theorem Th47:
theorem
theorem Th49:
theorem Th50:
theorem
theorem Th52:
:: deftheorem Def5 defines ProbFinS MATRPROB:def 5 :
theorem
theorem Th54:
:: deftheorem Def6 defines m-nonnegative MATRPROB:def 6 :
:: deftheorem Def7 defines with_sum=1 MATRPROB:def 7 :
:: deftheorem Def8 defines Joint_Probability MATRPROB:def 8 :
theorem Th55:
theorem Th56:
theorem
:: deftheorem Def9 defines with_line_sum=1 MATRPROB:def 9 :
theorem Th58:
:: deftheorem Def10 defines Conditional_Probability MATRPROB:def 10 :
theorem
theorem Th60:
theorem
theorem Th62:
theorem