:: 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 :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XBOOLE_0, SUBSET_1, NAT_1, REAL_1, FINSEQ_1, RELAT_1, FUNCT_1, TARSKI, XREAL_0, FINSEQ_2, CARD_1, XXREAL_0, SEQ_1, ARYTM_3, CARD_3, MATRIX_1, TREES_1, ZFMISC_1, INCSP_1, MATRIXC1, QC_LANG1, ORDINAL4, PRE_POLY, BINOP_2, FINSEQ_3, RVSUM_1, STRUCT_0, VECTSP_1, SUPINF_2, FVSUM_1, MATRIXR1, MATRPROB, FUNCT_7, MATRIX_0, ASYMPT_1, XCMPLX_0, VALUED_0; notations TARSKI, SUBSET_1, XBOOLE_0, XXREAL_0, XREAL_0, XCMPLX_0, REAL_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, SEQ_1, ZFMISC_1, FUNCOP_1, BINOP_1, BINOP_2, FUNCT_2, NAT_1, VALUED_0, RVSUM_1, FINSEQ_1, FINSEQ_2, FINSEQOP, NEWTON, STRUCT_0, MATRLIN, MATRIXR1, MATRIX_3, MATRIX_0, GROUP_1, FVSUM_1, RLVECT_1, VECTSP_1; constructors REAL_1, BINOP_2, NEWTON, FVSUM_1, MATRIX_3, MATRLIN, MATRIXR1, BINOP_1, RVSUM_1, RELSET_1, FINSEQ_2, FINSEQ_4, SEQ_1; registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, NAT_1, MEMBERED, FINSEQ_1, FINSEQ_2, STRUCT_0, VECTSP_1, MATRIX_0, MATRLIN, VALUED_0, CARD_1, RVSUM_1, XREAL_0; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve D for non empty set, i,j,k for Nat, n,m for Nat, r for Real, e for real-valued FinSequence; definition let d be set, g be FinSequence of d*, n be Nat; redefine func g.n -> FinSequence of d; end; definition let x be Real; redefine func <*x*> -> FinSequence of REAL; end; theorem :: MATRPROB:1 for a being Element of D, m being non zero Nat, g being FinSequence of D holds (len g = m & for i be Nat st i in dom g holds g.i = a) iff g = m |-> a; theorem :: MATRPROB:2 for a,b being Element of D holds ex g be FinSequence of D st len g = n & for i be Nat st i in Seg n holds (i in Seg k implies g.i = a) & (not i in Seg k implies g.i = b); theorem :: MATRPROB:3 (for i be Nat st i in dom e holds 0 <= e.i) implies for f being Real_Sequence st (for n be Nat st 0 <> n & n < len e holds f.(n+1) = f.n+e.(n+1 )) holds for n,m be Nat st n in dom e & m in dom e & n <= m holds f.n <= f.m; theorem :: MATRPROB:4 len e >= 1 & (for i be Nat st i in dom e holds 0 <= e.i) implies for f being Real_Sequence st f.1 = e.1 & (for n be Nat st 0 <> n & n < len e holds f.(n+1) = f.n+e.(n+1)) holds for n be Nat st n in dom e holds e.n <= f.n; theorem :: MATRPROB:5 (for i be Nat st i in dom e holds 0 <= e.i) implies for k be Nat st k in dom e holds e.k <= Sum e; theorem :: MATRPROB:6 for r1,r2 being Real, k being Nat, seq1 being Real_Sequence holds ex seq being Real_Sequence st seq.0=r1 & for n holds (n<>0 & n <= k implies seq .n=seq1.n) & (n > k implies seq.n=r2); theorem :: MATRPROB:7 for F being FinSequence of REAL ex f being Real_Sequence st f.0 = 0 & (for i be Nat st i < len F holds f.(i+1) = f.i+(F.(i+1))) & Sum F = f.len F; theorem :: MATRPROB:8 for D being set, e1 being FinSequence of D holds n |-> e1 is FinSequence of D*; theorem :: MATRPROB:9 for D being set, e1,e2 being FinSequence of D holds ex e being FinSequence of D* st len e = n & for i be Nat st i in Seg n holds (i in Seg k implies e.i = e1) & (not i in Seg k implies e.i = e2); theorem :: MATRPROB:10 for D being set, s being FinSequence holds (s is Matrix of D iff ex n st for i st i in dom s holds ex p being FinSequence of D st s.i = p & len p = n); theorem :: MATRPROB:11 for D being set, e being FinSequence of D* holds (ex n st for i st i in dom e holds len(e.i) = n) iff e is Matrix of D; theorem :: MATRPROB:12 for M being tabular FinSequence holds [i,j] in Indices M iff i in Seg len M & j in Seg width M; theorem :: MATRPROB:13 for D being non empty set, M being Matrix of D holds [i,j] in Indices M iff i in dom M & j in dom (M.i); theorem :: MATRPROB:14 for D being non empty set, M being Matrix of D st [i,j] in Indices M holds M*(i,j)=(M.i).j; theorem :: MATRPROB:15 for D being non empty set, M being Matrix of D holds [i,j] in Indices M iff i in dom Col(M,j) & j in dom Line(M,i); theorem :: MATRPROB:16 for D1,D2 being non empty set, M1 being (Matrix of D1),M2 being Matrix of D2 st M1 = M2 holds for i st i in dom M1 holds Line(M1,i) = Line(M2,i ); theorem :: MATRPROB:17 for D1,D2 being non empty set,M1 being (Matrix of D1),M2 being Matrix of D2 st M1 = M2 holds for j st j in Seg width M1 holds Col(M1,j) = Col( M2,j); theorem :: MATRPROB:18 for e1 being FinSequence of D st len e1 = m holds n |-> e1 is Matrix of n,m,D ; theorem :: MATRPROB:19 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 be Nat st i in Seg n holds (i in Seg k implies M.i = e1) & (not i in Seg k implies M.i = e2); definition let e be FinSequence of REAL*; func Sum e -> FinSequence of REAL means :: MATRPROB:def 1 len it = len e & for k st k in dom it holds it.k = Sum(e.k); end; notation let m be Matrix of REAL; synonym LineSum m for Sum m; end; theorem :: MATRPROB:20 for m being Matrix of REAL holds len Sum m = len m & for i st i in Seg len m holds (Sum m).i=Sum Line(m,i); definition let m be Matrix of REAL; func ColSum m -> FinSequence of REAL means :: MATRPROB:def 2 len it = width m & for j be Nat st j in Seg width m holds it.j=Sum Col(m,j); end; theorem :: MATRPROB:21 for M be Matrix of REAL st width M > 0 holds LineSum M = ColSum(M@); theorem :: MATRPROB:22 for M be Matrix of REAL holds ColSum M = LineSum(M@); definition let M be Matrix of REAL; func SumAll M -> Real equals :: MATRPROB:def 3 Sum Sum M; end; theorem :: MATRPROB:23 for M be Matrix of REAL st len M = 0 holds SumAll M = 0; theorem :: MATRPROB:24 for M be Matrix of m,0,REAL holds SumAll M = 0; theorem :: MATRPROB:25 for M1 be Matrix of n,k,REAL for M2 being Matrix of m,k,REAL holds Sum (M1^M2) = (Sum M1)^(Sum M2); theorem :: MATRPROB:26 for M1,M2 be Matrix of REAL holds Sum M1 + Sum M2 = Sum (M1 ^^ M2); theorem :: MATRPROB:27 for M1,M2 be Matrix of REAL st len M1 = len M2 holds SumAll M1 + SumAll M2 = SumAll(M1 ^^ M2); theorem :: MATRPROB:28 for M be Matrix of REAL holds SumAll M = SumAll(M@); theorem :: MATRPROB:29 for M be Matrix of REAL holds SumAll M = Sum ColSum M; theorem :: MATRPROB:30 for x,y being FinSequence of REAL st len x = len y holds len mlt (x,y) = len x; theorem :: MATRPROB:31 for i for R being Element of i-tuples_on REAL holds mlt(i|->1,R) = R; theorem :: MATRPROB:32 for x being FinSequence of REAL holds mlt((len x|->1),x) = x; theorem :: MATRPROB:33 for x,y being FinSequence of REAL st (for i st i in dom x holds x.i >= 0) & (for i st i in dom y holds y.i >= 0) holds for k st k in dom mlt(x, y) holds (mlt(x,y)).k >= 0; theorem :: MATRPROB:34 for i 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); theorem :: 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); theorem :: MATRPROB:36 for e being FinSequence of REAL for f being FinSequence of F_Real st e = f holds Sum e = Sum f; notation let e1,e2 be FinSequence of REAL; synonym e1 "*" e2 for |( e1,e2 )|; end; theorem :: MATRPROB:37 for i 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; theorem :: 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; theorem :: 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 st [i,j] in Indices M holds M*(i,j) = Line(M1,i) "*" Col(M2,j); theorem :: MATRPROB:40 for M being Matrix of REAL for p being FinSequence of REAL st len M = len p holds for i st i in Seg len (p*M) holds (p*M).i = p "*" Col(M,i); theorem :: 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 st i in Seg len (M*p) holds (M*p).i = Line(M,i) "*" p; theorem :: 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 st i in Seg len M holds Line(M,i) = Line(M1,i) * M2; definition let x,y be FinSequence of REAL,M be Matrix of REAL; assume that len x = len M and len y = width M; func QuadraticForm(x,M,y) -> Matrix of REAL means :: MATRPROB:def 4 len it = len x & width it = len y & for i,j be Nat st [i,j] in Indices M holds it*(i,j)=(x.i)*(M*(i,j))*(y.j); end; theorem :: MATRPROB:43 for x,y being FinSequence of REAL,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); theorem :: MATRPROB:44 for x,y being FinSequence of REAL,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); theorem :: MATRPROB:45 for x being FinSequence of REAL holds |(x,(len x |-> 1))| = Sum x; theorem :: MATRPROB:46 for x,y being FinSequence of REAL,M being Matrix of REAL st len x = len M & len y = width M holds |(x*M,y)| = SumAll QuadraticForm(x,M,y); theorem :: MATRPROB:47 for x,y being FinSequence of REAL,M being Matrix of REAL st len x = len M & len y = width M & len y>0 holds |((x*M),y)| = |(x,(M*y))|; theorem :: MATRPROB:48 for x,y being FinSequence of REAL,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))|; theorem :: MATRPROB:49 for x,y being FinSequence of REAL,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)| ; theorem :: MATRPROB:50 for x being FinSequence of REAL,M being Matrix of REAL st len x = len M & x = len x |-> 1 holds for k st k in Seg len(x*M) holds (x*M).k = Sum Col(M,k); theorem :: MATRPROB:51 for x being FinSequence of REAL,M being Matrix of REAL st len x = width M & width M > 0 & x = (len x |-> 1) holds for k st k in Seg len(M*x) holds (M*x).k = Sum Line(M,k); theorem :: MATRPROB:52 for n being non zero Nat ex P being FinSequence of REAL st len P = n & (for i st i in dom P holds P.i >= 0) & Sum P = 1; definition let p be real-valued FinSequence; attr p is ProbFinS means :: MATRPROB:def 5 (for i st i in dom p holds p.i >= 0) & Sum p = 1; end; registration cluster non empty ProbFinS for FinSequence of REAL; end; registration cluster non empty ProbFinS for real-valued FinSequence; end; theorem :: MATRPROB:53 for p being non empty ProbFinS real-valued FinSequence for k st k in dom p holds p.k <= 1; theorem :: MATRPROB:54 for M being non empty-yielding Matrix of D holds 1<=len M & 1<= width M; definition let M be Matrix of REAL; attr M is m-nonnegative means :: MATRPROB:def 6 for i,j st [i,j] in Indices M holds M*( i,j) >= 0; end; definition let M be Matrix of REAL; attr M is with_sum=1 means :: MATRPROB:def 7 SumAll M = 1; end; definition let M be Matrix of REAL; attr M is Joint_Probability means :: MATRPROB:def 8 M is m-nonnegative with_sum=1; end; registration cluster Joint_Probability -> m-nonnegative with_sum=1 for Matrix of REAL; cluster m-nonnegative with_sum=1 -> Joint_Probability for Matrix of REAL; end; theorem :: MATRPROB:55 for n,m being non zero Nat holds ex M be Matrix of n,m,REAL st M is m-nonnegative & SumAll M = 1; registration cluster non empty-yielding Joint_Probability for Matrix of REAL; end; theorem :: MATRPROB:56 for M being non empty-yielding Joint_Probability Matrix of REAL holds M@ is non empty-yielding Joint_Probability Matrix of REAL; theorem :: MATRPROB:57 for M being non empty-yielding Joint_Probability Matrix of REAL holds for i,j st [i,j] in Indices M holds M*(i,j) <= 1; definition let M be Matrix of REAL; attr M is with_line_sum=1 means :: MATRPROB:def 9 for k st k in dom M holds Sum (M.k) = 1; end; theorem :: MATRPROB:58 for n,m being non zero Nat holds ex M being Matrix of n,m,REAL st M is m-nonnegative with_line_sum=1; definition let M be Matrix of REAL; attr M is Conditional_Probability means :: MATRPROB:def 10 M is m-nonnegative with_line_sum=1; end; registration cluster Conditional_Probability -> m-nonnegative with_line_sum=1 for Matrix of REAL; cluster m-nonnegative with_line_sum=1 -> Conditional_Probability for Matrix of REAL; end; registration cluster non empty-yielding Conditional_Probability for Matrix of REAL; end; theorem :: MATRPROB:59 for M being non empty-yielding Conditional_Probability Matrix of REAL holds for i,j st [i,j] in Indices M holds M*(i,j) <= 1; theorem :: MATRPROB:60 for M being non empty-yielding Matrix of REAL holds M is non empty-yielding Conditional_Probability Matrix of REAL iff for i st i in dom M holds Line(M,i) is non empty ProbFinS FinSequence of REAL; theorem :: MATRPROB:61 for M being non empty-yielding with_line_sum=1 Matrix of REAL holds SumAll M = len M; 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 non empty-yielding Joint_Probability Matrix of REAL; cluster Row_Marginal M -> non empty ProbFinS; cluster Column_Marginal M -> non empty ProbFinS; end; registration let M be non empty-yielding Matrix of REAL; cluster M@ -> non empty-yielding; end; registration let M be non empty-yielding Joint_Probability Matrix of REAL; cluster M@ -> Joint_Probability; end; theorem :: MATRPROB:62 for p being non empty ProbFinS FinSequence of REAL for P being non empty-yielding 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 ; theorem :: MATRPROB:63 for P1, P2 being non empty-yielding Conditional_Probability Matrix of REAL st width P1 = len P2 holds P1 * P2 is non empty-yielding Conditional_Probability Matrix of REAL & len (P1 * P2) = len P1 & width (P1 * P2) = width P2;