:: The Definition of Finite Sequences and Matrices of Probability, and Addition of Matrices of Real Elements
:: by Bo Zhang and Yatsuka Nakamura
::
:: Received August 18, 2006
:: Copyright (c) 2006-2021 Association of Mizar Users

definition
let d be set ;
let g be FinSequence of d * ;
let n be Nat;
:: original: .
redefine func g . n -> FinSequence of d;
correctness
coherence
g . n is FinSequence of d
;
proof end;
end;

definition
let x be Real;
:: original: <*
redefine func <*x*> -> FinSequence of REAL ;
coherence
<*x*> is FinSequence of REAL
proof end;
end;

theorem Th1: :: MATRPROB:1
for D being non empty set
for a being Element of D
for m being non zero Nat
for g being FinSequence of D holds
( ( len g = m & ( for i being Nat st i in dom g holds
g . i = a ) ) iff g = m |-> a )
proof end;

theorem Th2: :: MATRPROB:2
for D being non empty set
for k, n being Nat
for a, b being Element of D ex g being FinSequence of D st
( len g = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies g . i = a ) & ( not i in Seg k implies g . i = b ) ) ) )
proof end;

theorem Th3: :: MATRPROB:3
for e being real-valued FinSequence st ( for i being Nat st i in dom e holds
0 <= e . i ) holds
for f being Real_Sequence st ( for n being Nat st 0 <> n & n < len e holds
f . (n + 1) = (f . n) + (e . (n + 1)) ) holds
for n, m being Nat st n in dom e & m in dom e & n <= m holds
f . n <= f . m
proof end;

theorem Th4: :: MATRPROB:4
for e being real-valued FinSequence st len e >= 1 & ( for i being Nat st i in dom e holds
0 <= e . i ) holds
for f being Real_Sequence st f . 1 = e . 1 & ( for n being Nat st 0 <> n & n < len e holds
f . (n + 1) = (f . n) + (e . (n + 1)) ) holds
for n being Nat st n in dom e holds
e . n <= f . n
proof end;

theorem Th5: :: MATRPROB:5
for e being real-valued FinSequence st ( for i being Nat st i in dom e holds
0 <= e . i ) holds
for k being Nat st k in dom e holds
e . k <= Sum e
proof end;

theorem Th6: :: MATRPROB:6
for r1, r2 being Real
for k being Nat
for seq1 being Real_Sequence ex seq being Real_Sequence st
( seq . 0 = r1 & ( for n being Nat holds
( ( n <> 0 & n <= k implies seq . n = seq1 . n ) & ( n > k implies seq . n = r2 ) ) ) )
proof end;

theorem Th7: :: MATRPROB:7
for F being FinSequence of REAL ex f being Real_Sequence st
( f . 0 = 0 & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) & Sum F = f . (len F) )
proof end;

theorem Th8: :: MATRPROB:8
for n being Nat
for D being set
for e1 being FinSequence of D holds n |-> e1 is FinSequence of D *
proof end;

theorem Th9: :: MATRPROB:9
for k, n being Nat
for D being set
for e1, e2 being FinSequence of D ex e being FinSequence of D * st
( len e = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies e . i = e1 ) & ( not i in Seg k implies e . i = e2 ) ) ) )
proof end;

theorem Th10: :: MATRPROB:10
for D being set
for s being FinSequence holds
( s is Matrix of D iff ex n being Nat st
for i being Nat st i in dom s holds
ex p being FinSequence of D st
( s . i = p & len p = n ) )
proof end;

theorem Th11: :: MATRPROB:11
for D being set
for e being FinSequence of D * holds
( ex n being Nat st
for i being Nat st i in dom e holds
len (e . i) = n iff e is Matrix of D )
proof end;

theorem Th12: :: MATRPROB:12
for i, j being Nat
for M being tabular FinSequence holds
( [i,j] in Indices M iff ( i in Seg (len M) & j in Seg () ) )
proof end;

theorem Th13: :: MATRPROB:13
for i, j being Nat
for D being non empty set
for M being Matrix of D holds
( [i,j] in Indices M iff ( i in dom M & j in dom (M . i) ) )
proof end;

theorem Th14: :: MATRPROB:14
for i, j being Nat
for D being non empty set
for M being Matrix of D st [i,j] in Indices M holds
M * (i,j) = (M . i) . j
proof end;

theorem Th15: :: MATRPROB:15
for i, j being Nat
for D being non empty set
for M being Matrix of D holds
( [i,j] in Indices M iff ( i in dom (Col (M,j)) & j in dom (Line (M,i)) ) )
proof end;

theorem Th16: :: MATRPROB:16
for D1, D2 being non empty set
for M1 being Matrix of D1
for M2 being Matrix of D2 st M1 = M2 holds
for i being Nat st i in dom M1 holds
Line (M1,i) = Line (M2,i)
proof end;

theorem Th17: :: MATRPROB:17
for D1, D2 being non empty set
for M1 being Matrix of D1
for M2 being Matrix of D2 st M1 = M2 holds
for j being Nat st j in Seg (width M1) holds
Col (M1,j) = Col (M2,j)
proof end;

theorem Th18: :: MATRPROB:18
for D being non empty set
for n, m being Nat
for e1 being FinSequence of D st len e1 = m holds
n |-> e1 is Matrix of n,m,D
proof end;

theorem Th19: :: MATRPROB:19
for D being non empty set
for k, n, m being Nat
for e1, e2 being FinSequence of D st len e1 = m & len e2 = m holds
ex M being Matrix of n,m,D st
for i being Nat st i in Seg n holds
( ( i in Seg k implies M . i = e1 ) & ( not i in Seg k implies M . i = e2 ) )
proof end;

Lm1: for r being Real
for m being Matrix of REAL holds
( ( for i, j being Nat st [i,j] in Indices m holds
m * (i,j) >= r ) iff for i, j being Nat st i in dom m & j in dom (m . i) holds
(m . i) . j >= r )

proof end;

Lm2: for r being Real
for m being Matrix of REAL holds
( ( for i, j being Nat st [i,j] in Indices m holds
m * (i,j) >= r ) iff for i, j being Nat st i in dom m & j in dom (Line (m,i)) holds
(Line (m,i)) . j >= r )

proof end;

Lm3: for r being Real
for m being Matrix of REAL holds
( ( for i, j being Nat st [i,j] in Indices m holds
m * (i,j) >= r ) iff for i, j being Nat st j in Seg () & i in dom (Col (m,j)) holds
(Col (m,j)) . i >= r )

proof end;

definition
let e be FinSequence of REAL * ;
func Sum e -> FinSequence of REAL means :Def1: :: MATRPROB:def 1
( len it = len e & ( for k being Nat st k in dom it holds
it . k = Sum (e . k) ) );
existence
ex b1 being FinSequence of REAL st
( len b1 = len e & ( for k being Nat st k in dom b1 holds
b1 . k = Sum (e . k) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = len e & ( for k being Nat st k in dom b1 holds
b1 . k = Sum (e . k) ) & len b2 = len e & ( for k being Nat st k in dom b2 holds
b2 . k = Sum (e . k) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Sum MATRPROB:def 1 :
for e being FinSequence of REAL *
for b2 being FinSequence of REAL holds
( b2 = Sum e iff ( len b2 = len e & ( for k being Nat st k in dom b2 holds
b2 . k = Sum (e . k) ) ) );

notation
let m be Matrix of REAL;
synonym LineSum m for Sum m;
end;

theorem Th20: :: MATRPROB:20
for m being Matrix of REAL holds
( len (Sum m) = len m & ( for i being Nat st i in Seg (len m) holds
(Sum m) . i = Sum (Line (m,i)) ) )
proof end;

definition
let m be Matrix of REAL;
func ColSum m -> FinSequence of REAL means :Def2: :: MATRPROB:def 2
( len it = width m & ( for j being Nat st j in Seg () holds
it . j = Sum (Col (m,j)) ) );
existence
ex b1 being FinSequence of REAL st
( len b1 = width m & ( for j being Nat st j in Seg () holds
b1 . j = Sum (Col (m,j)) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of REAL st len b1 = width m & ( for j being Nat st j in Seg () holds
b1 . j = Sum (Col (m,j)) ) & len b2 = width m & ( for j being Nat st j in Seg () holds
b2 . j = Sum (Col (m,j)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines ColSum MATRPROB:def 2 :
for m being Matrix of REAL
for b2 being FinSequence of REAL holds
( b2 = ColSum m iff ( len b2 = width m & ( for j being Nat st j in Seg () holds
b2 . j = Sum (Col (m,j)) ) ) );

theorem :: MATRPROB:21
for M being Matrix of REAL st width M > 0 holds
LineSum M = ColSum (M @)
proof end;

theorem Th22: :: MATRPROB:22
for M being Matrix of REAL holds ColSum M = LineSum (M @)
proof end;

definition
let M be Matrix of REAL;
func SumAll M -> Real equals :: MATRPROB:def 3
Sum (Sum M);
coherence
Sum (Sum M) is Real
;
end;

:: deftheorem defines SumAll MATRPROB:def 3 :
for M being Matrix of REAL holds SumAll M = Sum (Sum M);

theorem Th23: :: MATRPROB:23
for M being Matrix of REAL st len M = 0 holds
SumAll M = 0
proof end;

Lm4:
by XREAL_0:def 1;

theorem Th24: :: MATRPROB:24
for m being Nat
for M being Matrix of m, 0 ,REAL holds SumAll M = 0
proof end;

theorem Th25: :: MATRPROB:25
for k, n, m being Nat
for M1 being Matrix of n,k,REAL
for M2 being Matrix of m,k,REAL holds Sum (M1 ^ M2) = (Sum M1) ^ (Sum M2)
proof end;

theorem Th26: :: MATRPROB:26
for M1, M2 being Matrix of REAL holds (Sum M1) + (Sum M2) = Sum (M1 ^^ M2)
proof end;

theorem Th27: :: MATRPROB:27
for M1, M2 being Matrix of REAL st len M1 = len M2 holds
(SumAll M1) + (SumAll M2) = SumAll (M1 ^^ M2)
proof end;

theorem Th28: :: MATRPROB:28
for M being Matrix of REAL holds SumAll M = SumAll (M @)
proof end;

theorem Th29: :: MATRPROB:29
for M being Matrix of REAL holds SumAll M = Sum ()
proof end;

theorem Th30: :: MATRPROB:30
for x, y being FinSequence of REAL st len x = len y holds
len (mlt (x,y)) = len x by FINSEQ_2:72;

theorem Th31: :: MATRPROB:31
for i being Nat
for R being Element of i -tuples_on REAL holds mlt ((i |-> 1),R) = R
proof end;

theorem Th32: :: MATRPROB:32
for x being FinSequence of REAL holds mlt (((len x) |-> 1),x) = x
proof end;

theorem Th33: :: MATRPROB:33
for x, y being FinSequence of REAL st ( for i being Nat st i in dom x holds
x . i >= 0 ) & ( for i being Nat st i in dom y holds
y . i >= 0 ) holds
for k being Nat st k in dom (mlt (x,y)) holds
(mlt (x,y)) . k >= 0
proof end;

theorem Th34: :: MATRPROB:34
for i being Nat
for e1, e2 being Element of i -tuples_on REAL
for f1, f2 being Element of i -tuples_on the carrier of F_Real st e1 = f1 & e2 = f2 holds
mlt (e1,e2) = mlt (f1,f2)
proof end;

theorem Th35: :: MATRPROB:35
for e1, e2 being FinSequence of REAL
for f1, f2 being FinSequence of F_Real st len e1 = len e2 & e1 = f1 & e2 = f2 holds
mlt (e1,e2) = mlt (f1,f2)
proof end;

theorem Th36: :: MATRPROB:36
for e being FinSequence of REAL
for f being FinSequence of F_Real st e = f holds
Sum e = Sum f
proof end;

notation
let e1, e2 be FinSequence of REAL ;
synonym e1 "*" e2 for |(e1,e2)|;
end;

theorem :: MATRPROB:37
for i being Nat
for e1, e2 being Element of i -tuples_on REAL
for f1, f2 being Element of i -tuples_on the carrier of F_Real st e1 = f1 & e2 = f2 holds
e1 "*" e2 = f1 "*" f2
proof end;

theorem Th38: :: MATRPROB:38
for e1, e2 being FinSequence of REAL
for f1, f2 being FinSequence of F_Real st len e1 = len e2 & e1 = f1 & e2 = f2 holds
e1 "*" e2 = f1 "*" f2
proof end;

theorem Th39: :: MATRPROB:39
for M, M1, M2 being Matrix of REAL st width M1 = len M2 holds
( M = M1 * M2 iff ( len M = len M1 & width M = width M2 & ( for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ) ) )
proof end;

theorem Th40: :: MATRPROB:40
for M being Matrix of REAL
for p being FinSequence of REAL st len M = len p holds
for i being Nat st i in Seg (len (p * M)) holds
(p * M) . i = p "*" (Col (M,i))
proof end;

theorem Th41: :: MATRPROB:41
for M being Matrix of REAL
for p being FinSequence of REAL st width M = len p & width M > 0 holds
for i being Nat st i in Seg (len (M * p)) holds
(M * p) . i = (Line (M,i)) "*" p
proof end;

theorem Th42: :: MATRPROB:42
for M, M1, M2 being Matrix of REAL st width M1 = len M2 holds
( M = M1 * M2 iff ( len M = len M1 & width M = width M2 & ( for i being Nat st i in Seg (len M) holds
Line (M,i) = (Line (M1,i)) * M2 ) ) )
proof end;

definition
let x, y be FinSequence of REAL ;
let M be Matrix of REAL;
assume that
A1: len x = len M and
A2: 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) ) )
proof end;
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
proof end;
end;

:: deftheorem Def4 defines QuadraticForm MATRPROB:def 4 :
for x, y being FinSequence of REAL
for M being Matrix of REAL st len x = len M & len y = width M holds
for b4 being Matrix of REAL holds
( b4 = QuadraticForm (x,M,y) iff ( len b4 = len x & width b4 = len y & ( for i, j being Nat st [i,j] in Indices M holds
b4 * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) ) );

theorem :: MATRPROB:43
for x, y being FinSequence of REAL
for M being Matrix of REAL st len x = len M & len y = width M & len y > 0 holds
(QuadraticForm (x,M,y)) @ = QuadraticForm (y,(M @),x)
proof end;

theorem Th44: :: MATRPROB:44
for x, y being FinSequence of REAL
for M being Matrix of REAL st len x = len M & len y = width M & len y > 0 holds
|(x,(M * y))| = SumAll (QuadraticForm (x,M,y))
proof end;

theorem :: MATRPROB:45
for x being FinSequence of REAL holds |(x,((len x) |-> 1))| = Sum x by Th32;

theorem Th46: :: MATRPROB:46
for x, y being FinSequence of REAL
for M being Matrix of REAL st len x = len M & len y = width M holds
|((x * M),y)| = SumAll (QuadraticForm (x,M,y))
proof end;

theorem Th47: :: MATRPROB:47
for x, y being FinSequence of REAL
for M being Matrix of REAL st len x = len M & len y = width M & len y > 0 holds
|((x * M),y)| = |(x,(M * y))|
proof end;

theorem :: MATRPROB:48
for x, y being FinSequence of REAL
for M being Matrix of REAL st len y = len M & len x = width M & len x > 0 & len y > 0 holds
|((M * x),y)| = |(x,((M @) * y))|
proof end;

theorem Th49: :: MATRPROB:49
for x, y being FinSequence of REAL
for M being Matrix of REAL st len y = len M & len x = width M & len x > 0 & len y > 0 holds
|(x,(y * M))| = |((x * (M @)),y)|
proof end;

theorem Th50: :: MATRPROB:50
for x being FinSequence of REAL
for M being Matrix of REAL st len x = len M & x = (len x) |-> 1 holds
for k being Nat st k in Seg (len (x * M)) holds
(x * M) . k = Sum (Col (M,k))
proof end;

theorem :: MATRPROB:51
for x being FinSequence of REAL
for M being Matrix of REAL st len x = width M & width M > 0 & x = (len x) |-> 1 holds
for k being Nat st k in Seg (len (M * x)) holds
(M * x) . k = Sum (Line (M,k))
proof end;

reconsider jj = 1, zz = 0 as Element of REAL by XREAL_0:def 1;

theorem Th52: :: MATRPROB:52
for n being non zero Nat ex P being FinSequence of REAL st
( len P = n & ( for i being Nat st i in dom P holds
P . i >= 0 ) & Sum P = 1 )
proof end;

definition
let p be real-valued FinSequence;
attr p is ProbFinS means :Def5: :: MATRPROB:def 5
( ( for i being Nat st i in dom p holds
p . i >= 0 ) & Sum p = 1 );
end;

:: deftheorem Def5 defines ProbFinS MATRPROB:def 5 :
for p being real-valued FinSequence holds
( p is ProbFinS iff ( ( for i being Nat st i in dom p holds
p . i >= 0 ) & Sum p = 1 ) );

registration
existence
ex b1 being FinSequence of REAL st
( not b1 is empty & b1 is ProbFinS )
proof end;
end;

registration
existence
ex b1 being real-valued FinSequence st
( not b1 is empty & b1 is ProbFinS )
proof end;
end;

theorem :: MATRPROB:53
for p being non empty real-valued ProbFinS FinSequence
for k being Nat st k in dom p holds
p . k <= 1
proof end;

theorem Th54: :: MATRPROB:54
for D being non empty set
for M being V3() Matrix of D holds
( 1 <= len M & 1 <= width M )
proof end;

definition
let M be Matrix of REAL;
attr M is m-nonnegative means :Def6: :: MATRPROB:def 6
for i, j being Nat st [i,j] in Indices M holds
M * (i,j) >= 0 ;
end;

:: deftheorem Def6 defines m-nonnegative MATRPROB:def 6 :
for M being Matrix of REAL holds
( M is m-nonnegative iff for i, j being Nat st [i,j] in Indices M holds
M * (i,j) >= 0 );

definition
let M be Matrix of REAL;
attr M is with_sum=1 means :Def7: :: MATRPROB:def 7
SumAll M = 1;
end;

:: deftheorem Def7 defines with_sum=1 MATRPROB:def 7 :
for M being Matrix of REAL holds
( M is with_sum=1 iff SumAll M = 1 );

definition
let M be Matrix of REAL;
attr M is Joint_Probability means :: MATRPROB:def 8
( M is m-nonnegative & M is with_sum=1 );
end;

:: deftheorem defines Joint_Probability MATRPROB:def 8 :
for M being Matrix of REAL holds
( M is Joint_Probability iff ( M is m-nonnegative & M is with_sum=1 ) );

registration
coherence
for b1 being Matrix of REAL st b1 is Joint_Probability holds
( b1 is m-nonnegative & b1 is with_sum=1 )
;
coherence
for b1 being Matrix of REAL st b1 is m-nonnegative & b1 is with_sum=1 holds
b1 is Joint_Probability
;
end;

theorem Th55: :: MATRPROB:55
for n, m being non zero Nat ex M being Matrix of n,m,REAL st
( M is m-nonnegative & SumAll M = 1 )
proof end;

registration
existence
ex b1 being Matrix of REAL st
( b1 is V3() & b1 is Joint_Probability )
proof end;
end;

theorem Th56: :: MATRPROB:56
for M being V3() Joint_Probability Matrix of REAL holds M @ is V3() Joint_Probability Matrix of REAL
proof end;

theorem :: MATRPROB:57
for M being V3() Joint_Probability Matrix of REAL
for i, j being Nat st [i,j] in Indices M holds
M * (i,j) <= 1
proof end;

definition
let M be Matrix of REAL;
attr M is with_line_sum=1 means :Def9: :: MATRPROB:def 9
for k being Nat st k in dom M holds
Sum (M . k) = 1;
end;

:: deftheorem Def9 defines with_line_sum=1 MATRPROB:def 9 :
for M being Matrix of REAL holds
( M is with_line_sum=1 iff for k being Nat st k in dom M holds
Sum (M . k) = 1 );

theorem Th58: :: MATRPROB:58
for n, m being non zero Nat ex M being Matrix of n,m,REAL st
( M is m-nonnegative & M is with_line_sum=1 )
proof end;

definition
let M be Matrix of REAL;
end;

:: deftheorem defines Conditional_Probability MATRPROB:def 10 :
for M being Matrix of REAL holds
( M is Conditional_Probability iff ( M is m-nonnegative & M is with_line_sum=1 ) );

registration
coherence
for b1 being Matrix of REAL st b1 is Conditional_Probability holds
( b1 is m-nonnegative & b1 is with_line_sum=1 )
;
coherence
for b1 being Matrix of REAL st b1 is m-nonnegative & b1 is with_line_sum=1 holds
b1 is Conditional_Probability
;
end;

registration
existence
ex b1 being Matrix of REAL st
( b1 is V3() & b1 is Conditional_Probability )
proof end;
end;

theorem :: MATRPROB:59
for M being V3() Conditional_Probability Matrix of REAL
for i, j being Nat st [i,j] in Indices M holds
M * (i,j) <= 1
proof end;

theorem Th60: :: MATRPROB:60
for M being V3() Matrix of REAL holds
( M is V3() Conditional_Probability Matrix of REAL iff for i being Nat st i in dom M holds
Line (M,i) is non empty ProbFinS FinSequence of REAL )
proof end;

theorem :: MATRPROB:61
for M being V3() with_line_sum=1 Matrix of REAL holds SumAll M = len M
proof end;

notation
let M be Matrix of REAL;
synonym Row_Marginal M for LineSum M;
synonym Column_Marginal M for ColSum M;
end;

registration
let M be V3() Joint_Probability Matrix of REAL;
cluster Sum M -> non empty ProbFinS ;
coherence
( not Row_Marginal M is empty & Row_Marginal M is ProbFinS )
proof end;
cluster ColSum M -> non empty ProbFinS ;
coherence
( not Column_Marginal M is empty & Column_Marginal M is ProbFinS )
proof end;
end;

registration
let M be V3() Matrix of REAL;
cluster M @ -> V3() ;
coherence
not M @ is empty-yielding
proof end;
end;

registration
let M be V3() Joint_Probability Matrix of REAL;
coherence by Th56;
end;

theorem Th62: :: MATRPROB:62
for p being non empty ProbFinS FinSequence of REAL
for P being V3() Conditional_Probability Matrix of REAL st len p = len P holds
( p * P is non empty ProbFinS FinSequence of REAL & len (p * P) = width P )
proof end;

theorem :: MATRPROB:63
for P1, P2 being V3() Conditional_Probability Matrix of REAL st width P1 = len P2 holds
( P1 * P2 is V3() Conditional_Probability Matrix of REAL & len (P1 * P2) = len P1 & width (P1 * P2) = width P2 )
proof end;