:: by Bo Zhang and Yatsuka Nakamura

::

:: Received August 18, 2006

:: Copyright (c) 2006-2012 Association of Mizar Users

begin

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;

end;
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;

definition

let x be real number ;

:: original: <*

redefine func <*x*> -> FinSequence of REAL ;

coherence

<*x*> is FinSequence of REAL

end;
:: original: <*

redefine func <*x*> -> FinSequence of REAL ;

coherence

<*x*> is FinSequence of REAL

proof end;

theorem Th1: :: MATRPROB:1

for D being non empty set

for a being Element of D

for m being non empty 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 )

for a being Element of D

for m being non empty 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 being Element of NAT

for 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 ) ) ) )

for k being Element of NAT

for 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 FinSequence of REAL 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

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 FinSequence of REAL 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

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 FinSequence of REAL 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

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 ) ) ) )

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) )

( 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 Th9: :: MATRPROB:9

for k being Element of NAT

for 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 ) ) ) )

for 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 Element of NAT st i in dom s holds

ex p being FinSequence of D st

( s . i = p & len p = n ) )

for s being FinSequence holds

( s is Matrix of D iff ex n being Nat st

for i being Element of 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 Element of NAT st i in dom e holds

len (e . i) = n iff e is Matrix of D )

for e being FinSequence of D * holds

( ex n being Nat st

for i being Element of 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 Element of NAT

for M being tabular FinSequence holds

( [i,j] in Indices M iff ( i in Seg (len M) & j in Seg (width M) ) )

for M being tabular FinSequence holds

( [i,j] in Indices M iff ( i in Seg (len M) & j in Seg (width M) ) )

proof end;

theorem Th13: :: MATRPROB:13

for i, j being Element of 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) ) )

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 Element of 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

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 Element of 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)) ) )

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 Element of NAT st i in dom M1 holds

Line (M1,i) = Line (M2,i)

for M1 being Matrix of D1

for M2 being Matrix of D2 st M1 = M2 holds

for i being Element of 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 Element of NAT st j in Seg (width M1) holds

Col (M1,j) = Col (M2,j)

for M1 being Matrix of D1

for M2 being Matrix of D2 st M1 = M2 holds

for j being Element of 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 m, n being Nat

for e1 being FinSequence of D st len e1 = m holds

n |-> e1 is Matrix of n,m,D

for m, n 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 being Element of NAT

for m, n 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 ) )

for k being Element of NAT

for m, n 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 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 )

proof end;

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 )

proof end;

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 )

proof end;

definition

let e be FinSequence of REAL * ;

ex b_{1} being FinSequence of REAL st

( len b_{1} = len e & ( for k being Element of NAT st k in dom b_{1} holds

b_{1} . k = Sum (e . k) ) )

for b_{1}, b_{2} being FinSequence of REAL st len b_{1} = len e & ( for k being Element of NAT st k in dom b_{1} holds

b_{1} . k = Sum (e . k) ) & len b_{2} = len e & ( for k being Element of NAT st k in dom b_{2} holds

b_{2} . k = Sum (e . k) ) holds

b_{1} = b_{2}

end;
func Sum e -> FinSequence of REAL means :Def1: :: MATRPROB:def 1

( len it = len e & ( for k being Element of NAT st k in dom it holds

it . k = Sum (e . k) ) );

existence ( len it = len e & ( for k being Element of NAT st k in dom it holds

it . k = Sum (e . k) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines Sum MATRPROB:def 1 :

for e being FinSequence of REAL *

for b_{2} being FinSequence of REAL holds

( b_{2} = Sum e iff ( len b_{2} = len e & ( for k being Element of NAT st k in dom b_{2} holds

b_{2} . k = Sum (e . k) ) ) );

for e being FinSequence of REAL *

for b

( b

b

theorem Th20: :: MATRPROB:20

for m being Matrix of REAL holds

( len (Sum m) = len m & ( for i being Element of NAT st i in Seg (len m) holds

(Sum m) . i = Sum (Line (m,i)) ) )

( len (Sum m) = len m & ( for i being Element of NAT st i in Seg (len m) holds

(Sum m) . i = Sum (Line (m,i)) ) )

proof end;

definition

let m be Matrix of REAL;

ex b_{1} being FinSequence of REAL st

( len b_{1} = width m & ( for j being Nat st j in Seg (width m) holds

b_{1} . j = Sum (Col (m,j)) ) )

for b_{1}, b_{2} being FinSequence of REAL st len b_{1} = width m & ( for j being Nat st j in Seg (width m) holds

b_{1} . j = Sum (Col (m,j)) ) & len b_{2} = width m & ( for j being Nat st j in Seg (width m) holds

b_{2} . j = Sum (Col (m,j)) ) holds

b_{1} = b_{2}

end;
func ColSum m -> FinSequence of REAL means :Def2: :: MATRPROB:def 2

( len it = width m & ( for j being Nat st j in Seg (width m) holds

it . j = Sum (Col (m,j)) ) );

existence ( len it = width m & ( for j being Nat st j in Seg (width m) holds

it . j = Sum (Col (m,j)) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines ColSum MATRPROB:def 2 :

for m being Matrix of REAL

for b_{2} being FinSequence of REAL holds

( b_{2} = ColSum m iff ( len b_{2} = width m & ( for j being Nat st j in Seg (width m) holds

b_{2} . j = Sum (Col (m,j)) ) ) );

for m being Matrix of REAL

for b

( b

b

:: deftheorem defines SumAll MATRPROB:def 3 :

for M being Matrix of REAL holds SumAll M = Sum (Sum M);

for M being Matrix of REAL holds SumAll M = Sum (Sum M);

theorem Th25: :: MATRPROB:25

for k being Element of NAT

for 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)

for 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 Th27: :: MATRPROB:27

for M1, M2 being Matrix of REAL st len M1 = len M2 holds

(SumAll M1) + (SumAll M2) = SumAll (M1 ^^ M2)

(SumAll M1) + (SumAll M2) = SumAll (M1 ^^ M2)

proof end;

theorem Th33: :: MATRPROB:33

for x, y being FinSequence of REAL st ( for i being Element of NAT st i in dom x holds

x . i >= 0 ) & ( for i being Element of NAT st i in dom y holds

y . i >= 0 ) holds

for k being Element of NAT st k in dom (mlt (x,y)) holds

(mlt (x,y)) . k >= 0

x . i >= 0 ) & ( for i being Element of NAT st i in dom y holds

y . i >= 0 ) holds

for k being Element of NAT st k in dom (mlt (x,y)) holds

(mlt (x,y)) . k >= 0

proof end;

theorem Th34: :: MATRPROB:34

for i being Element of 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)

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)

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 :: MATRPROB:37

for i being Element of 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

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

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 Element of NAT st [i,j] in Indices M holds

M * (i,j) = (Line (M1,i)) "*" (Col (M2,j)) ) ) )

( M = M1 * M2 iff ( len M = len M1 & width M = width M2 & ( for i, j being Element of 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 Element of NAT st i in Seg (len (p * M)) holds

(p * M) . i = p "*" (Col (M,i))

for p being FinSequence of REAL st len M = len p holds

for i being Element of 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 Element of NAT st i in Seg (len (M * p)) holds

(M * p) . i = (Line (M,i)) "*" p

for p being FinSequence of REAL st width M = len p & width M > 0 holds

for i being Element of 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 Element of NAT st i in Seg (len M) holds

Line (M,i) = (Line (M1,i)) * M2 ) ) )

( M = M1 * M2 iff ( len M = len M1 & width M = width M2 & ( for i being Element of 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 ;

ex b_{1} being Matrix of REAL st

( len b_{1} = len x & width b_{1} = len y & ( for i, j being Nat st [i,j] in Indices M holds

b_{1} * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) )

for b_{1}, b_{2} being Matrix of REAL st len b_{1} = len x & width b_{1} = len y & ( for i, j being Nat st [i,j] in Indices M holds

b_{1} * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) & len b_{2} = len x & width b_{2} = len y & ( for i, j being Nat st [i,j] in Indices M holds

b_{2} * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) holds

b_{1} = b_{2}

end;
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 ( 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) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{4} being Matrix of REAL holds

( b_{4} = QuadraticForm (x,M,y) iff ( len b_{4} = len x & width b_{4} = len y & ( for i, j being Nat st [i,j] in Indices M holds

b_{4} * (i,j) = ((x . i) * (M * (i,j))) * (y . j) ) ) );

for x, y being FinSequence of REAL

for M being Matrix of REAL st len x = len M & len y = width M holds

for b

( b

b

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)

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))

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 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))

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))|

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))|

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)|

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 Element of NAT st k in Seg (len (x * M)) holds

(x * M) . k = Sum (Col (M,k))

for M being Matrix of REAL st len x = len M & x = (len x) |-> 1 holds

for k being Element of 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 Element of NAT st k in Seg (len (M * x)) holds

(M * x) . k = Sum (Line (M,k))

for M being Matrix of REAL st len x = width M & width M > 0 & x = (len x) |-> 1 holds

for k being Element of NAT st k in Seg (len (M * x)) holds

(M * x) . k = Sum (Line (M,k))

proof end;

theorem Th52: :: MATRPROB:52

for n being non empty Nat ex P being FinSequence of REAL st

( len P = n & ( for i being Element of NAT st i in dom P holds

P . i >= 0 ) & Sum P = 1 )

( len P = n & ( for i being Element of NAT st i in dom P holds

P . i >= 0 ) & Sum P = 1 )

proof end;

:: deftheorem Def5 defines ProbFinS MATRPROB:def 5 :

for p being FinSequence of REAL holds

( p is ProbFinS iff ( ( for i being Element of NAT st i in dom p holds

p . i >= 0 ) & Sum p = 1 ) );

for p being FinSequence of REAL holds

( p is ProbFinS iff ( ( for i being Element of NAT st i in dom p holds

p . i >= 0 ) & Sum p = 1 ) );

registration

ex b_{1} being FinSequence of REAL st

( not b_{1} is empty & b_{1} is ProbFinS )
end;

cluster non empty Relation-like NAT -defined REAL -valued Function-like V33() FinSequence-like FinSubsequence-like complex-yielding V158() V159() ProbFinS for FinSequence of REAL ;

existence ex b

( not b

proof end;

theorem :: MATRPROB:53

for p being non empty ProbFinS FinSequence of REAL

for k being Element of NAT st k in dom p holds

p . k <= 1

for k being Element of 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 non empty-yielding Matrix of D holds

( 1 <= len M & 1 <= width M )

for M being non empty-yielding Matrix of D holds

( 1 <= len M & 1 <= width M )

proof 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 Element of NAT st [i,j] in Indices M holds

M * (i,j) >= 0 );

for M being Matrix of REAL holds

( M is m-nonnegative iff for i, j being Element of NAT st [i,j] in Indices M holds

M * (i,j) >= 0 );

definition
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 );

for M being Matrix of REAL holds

( M is with_sum=1 iff SumAll M = 1 );

:: deftheorem Def8 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 ) );

for M being Matrix of REAL holds

( M is Joint_Probability iff ( M is m-nonnegative & M is with_sum=1 ) );

registration

coherence

for b_{1} being Matrix of REAL st b_{1} is Joint_Probability holds

( b_{1} is m-nonnegative & b_{1} is with_sum=1 )
by Def8;

coherence

for b_{1} being Matrix of REAL st b_{1} is m-nonnegative & b_{1} is with_sum=1 holds

b_{1} is Joint_Probability
by Def8;

end;
for b

( b

coherence

for b

b

theorem Th55: :: MATRPROB:55

for n, m being non empty Nat ex M being Matrix of n,m, REAL st

( M is m-nonnegative & SumAll M = 1 )

( M is m-nonnegative & SumAll M = 1 )

proof end;

registration

ex b_{1} being Matrix of REAL st

( not b_{1} is empty-yielding & b_{1} is Joint_Probability )
end;

cluster Relation-like non empty-yielding NAT -defined REAL * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() Joint_Probability for FinSequence of REAL * ;

existence ex b

( not b

proof end;

theorem Th56: :: MATRPROB:56

for M being non empty-yielding Joint_Probability Matrix of REAL holds M @ is non empty-yielding Joint_Probability Matrix of REAL

proof end;

theorem :: MATRPROB:57

for M being non empty-yielding Joint_Probability Matrix of REAL

for i, j being Element of NAT st [i,j] in Indices M holds

M * (i,j) <= 1

for i, j being Element of NAT st [i,j] in Indices M holds

M * (i,j) <= 1

proof end;

definition

let M be Matrix of REAL;

end;
attr M is with_line_sum=1 means :Def9: :: MATRPROB:def 9

for k being Element of NAT st k in dom M holds

Sum (M . k) = 1;

for k being Element of NAT st k in dom M holds

Sum (M . k) = 1;

:: 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 Element of NAT st k in dom M holds

Sum (M . k) = 1 );

for M being Matrix of REAL holds

( M is with_line_sum=1 iff for k being Element of NAT st k in dom M holds

Sum (M . k) = 1 );

theorem Th58: :: MATRPROB:58

for n, m being non empty Nat ex M being Matrix of n,m, REAL st

( M is m-nonnegative & M is with_line_sum=1 )

( M is m-nonnegative & M is with_line_sum=1 )

proof end;

definition

let M be Matrix of REAL;

end;
attr M is Conditional_Probability means :Def10: :: MATRPROB:def 10

( M is m-nonnegative & M is with_line_sum=1 );

( M is m-nonnegative & M is with_line_sum=1 );

:: deftheorem Def10 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 ) );

for M being Matrix of REAL holds

( M is Conditional_Probability iff ( M is m-nonnegative & M is with_line_sum=1 ) );

registration

for b_{1} being Matrix of REAL st b_{1} is Conditional_Probability holds

( b_{1} is m-nonnegative & b_{1} is with_line_sum=1 )
by Def10;

for b_{1} being Matrix of REAL st b_{1} is m-nonnegative & b_{1} is with_line_sum=1 holds

b_{1} is Conditional_Probability
by Def10;

end;

cluster tabular Conditional_Probability -> m-nonnegative with_line_sum=1 for FinSequence of REAL * ;

coherence for b

( b

cluster tabular m-nonnegative with_line_sum=1 -> Conditional_Probability for FinSequence of REAL * ;

coherence for b

b

registration

ex b_{1} being Matrix of REAL st

( not b_{1} is empty-yielding & b_{1} is Conditional_Probability )
end;

cluster Relation-like non empty-yielding NAT -defined REAL * -valued Function-like V33() FinSequence-like FinSubsequence-like tabular V180() Conditional_Probability for FinSequence of REAL * ;

existence ex b

( not b

proof end;

theorem :: MATRPROB:59

for M being non empty-yielding Conditional_Probability Matrix of REAL

for i, j being Element of NAT st [i,j] in Indices M holds

M * (i,j) <= 1

for i, j being Element of NAT st [i,j] in Indices M holds

M * (i,j) <= 1

proof end;

theorem Th60: :: 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 being Element of NAT st i in dom M holds

Line (M,i) is non empty ProbFinS FinSequence of REAL )

( M is non empty-yielding Conditional_Probability Matrix of REAL iff for i being Element of NAT st i in dom M holds

Line (M,i) is non empty ProbFinS FinSequence of REAL )

proof end;

notation

let M be Matrix of REAL;

synonym Row_Marginal M for LineSum M;

synonym Column_Marginal M for ColSum M;

end;
synonym Row_Marginal M for LineSum M;

synonym Column_Marginal M for ColSum M;

registration

let M be non empty-yielding Joint_Probability Matrix of REAL;

coherence

( not Row_Marginal M is empty & Row_Marginal M is ProbFinS )

( not Column_Marginal M is empty & Column_Marginal M is ProbFinS )

end;
coherence

( not Row_Marginal M is empty & Row_Marginal M is ProbFinS )

proof end;

coherence ( not Column_Marginal M is empty & Column_Marginal M is ProbFinS )

proof end;

registration
end;

registration

let M be non empty-yielding Joint_Probability Matrix of REAL;

coherence

M @ is Joint_Probability by Th56;

end;
coherence

M @ is Joint_Probability by Th56;

theorem Th62: :: 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 )

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 )

proof end;

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 )

( P1 * P2 is non empty-yielding Conditional_Probability Matrix of REAL & len (P1 * P2) = len P1 & width (P1 * P2) = width P2 )

proof end;