:: The Definition of Finite Sequences and Matrices of Probability, andAddition of Matrices of Real Elements
:: by Bo Zhang and Yatsuka Nakamura
::
:: Received August 18, 2006
:: Copyright (c) 2006 Association of Mizar Users
theorem Th1: :: MATRPROB:1
theorem Th2: :: MATRPROB:2
theorem Th3: :: MATRPROB:3
theorem Th4: :: MATRPROB:4
theorem Th5: :: MATRPROB:5
theorem Th6: :: MATRPROB:6
theorem Th7: :: MATRPROB:7
theorem Th8: :: MATRPROB:8
theorem Th9: :: MATRPROB:9
theorem Th10: :: MATRPROB:10
theorem Th11: :: MATRPROB:11
theorem Th12: :: MATRPROB:12
theorem Th13: :: MATRPROB:13
theorem Th14: :: MATRPROB:14
theorem Th15: :: MATRPROB:15
theorem Th16: :: MATRPROB:16
theorem Th17: :: MATRPROB:17
theorem Th18: :: MATRPROB:18
theorem Th19: :: MATRPROB:19
Lm1:
for r being Real
for m being Matrix of REAL 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 REAL 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 REAL 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: :: MATRPROB:20
:: deftheorem Def2 defines ColSum MATRPROB:def 2 :
theorem :: MATRPROB:21
theorem Th22: :: MATRPROB:22
:: deftheorem defines SumAll MATRPROB:def 3 :
theorem Th23: :: MATRPROB:23
theorem Th24: :: MATRPROB:24
theorem Th25: :: MATRPROB:25
theorem Th26: :: MATRPROB:26
theorem Th27: :: MATRPROB:27
theorem Th28: :: MATRPROB:28
theorem Th29: :: MATRPROB:29
theorem Th30: :: MATRPROB:30
theorem Th31: :: MATRPROB:31
theorem Th32: :: MATRPROB:32
theorem Th33: :: MATRPROB:33
theorem Th34: :: MATRPROB:34
theorem Th35: :: MATRPROB:35
theorem Th36: :: MATRPROB:36
theorem :: MATRPROB:37
theorem Th38: :: MATRPROB:38
theorem Th39: :: MATRPROB:39
theorem Th40: :: MATRPROB:40
theorem Th41: :: MATRPROB:41
theorem Th42: :: MATRPROB:42
definition
let x,
y be
FinSequence of
REAL ;
let M be
Matrix of
REAL ;
assume A1:
(
len x = len M &
len y = width M )
;
func QuadraticForm x,
M,
y -> Matrix of
REAL means :
Def4:
:: MATRPROB:def 4
(
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 REAL 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 REAL 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 :: MATRPROB:43
theorem Th44: :: MATRPROB:44
theorem :: MATRPROB:45
theorem Th46: :: MATRPROB:46
theorem Th47: :: MATRPROB:47
theorem :: MATRPROB:48
theorem Th49: :: MATRPROB:49
theorem Th50: :: MATRPROB:50
theorem :: MATRPROB:51
theorem Th52: :: MATRPROB:52
:: deftheorem Def5 defines ProbFinS MATRPROB:def 5 :
theorem :: MATRPROB:53
theorem Th54: :: MATRPROB:54
:: 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: :: MATRPROB:55
theorem Th56: :: MATRPROB:56
theorem :: MATRPROB:57
:: deftheorem Def9 defines with_line_sum=1 MATRPROB:def 9 :
theorem Th58: :: MATRPROB:58
:: deftheorem Def10 defines Conditional_Probability MATRPROB:def 10 :
theorem :: MATRPROB:59
theorem Th60: :: MATRPROB:60
theorem :: MATRPROB:61
theorem Th62: :: MATRPROB:62
theorem :: MATRPROB:63