PROB_3: Set Sequences and Monotone Class

:: Set Sequences and Monotone Class
:: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received August 12, 2005
:: Copyright (c) 2005-2011 Association of Mizar Users

begin

Lm1: for t, p, s being real number st 0 < s & t <= p holds
( t < p + s & t - s < p )

proof end;

theorem Th1: :: PROB_3:1

for f being FinSequence holds not 0 in dom f

proof end;

theorem Th2: :: PROB_3:2

for n being Nat
for f being FinSequence holds
( n in dom f iff ( n <> 0 & n <= len f ) )

proof end;

theorem Th3: :: PROB_3:3

for g being real number
for f being Real_Sequence st ex k being Nat st
for n being Nat st k <= n holds
f . n = g holds
( f is convergent & lim f = g )

proof end;

theorem Th4: :: PROB_3:4

for n being Nat
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds (P * ASeq) . n >= 0

proof end;

theorem Th5: :: PROB_3:5

for n being Nat
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq, BSeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq . n c= BSeq . n holds
(P * ASeq) . n <= (P * BSeq) . n

proof end;

theorem Th6: :: PROB_3:6

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq is non-descending holds
P * ASeq is non-decreasing

proof end;

theorem Th7: :: PROB_3:7

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq is non-ascending holds
P * ASeq is non-increasing

proof end;

theorem Th8: :: PROB_3:8

for X being set
for A1 being SetSequence of X ex S being SetSequence of X st
( S . 0 = A1 . 0 & ( for n being Nat holds S . (n + 1) = (S . n) /\ (A1 . (n + 1)) ) )

proof end;

theorem Th9: :: PROB_3:9

for X being set
for A1 being SetSequence of X ex S being SetSequence of X st
( S . 0 = A1 . 0 & ( for n being Nat holds S . (n + 1) = (S . n) \/ (A1 . (n + 1)) ) )

proof end;

definition

let X be set ;
let A1 be SetSequence of X;
func Partial_Intersection A1 -> SetSequence of X means :Def1: :: PROB_3:def 1
( it . 0 = A1 . 0 & ( for n being Nat holds it . (n + 1) = (it . n) /\ (A1 . (n + 1)) ) );
existence by Th8;
uniqueness

proof end;

end;

:: deftheorem Def1 defines Partial_Intersection PROB_3:def 1 :

definition

let X be set ;
let A1 be SetSequence of X;
func Partial_Union A1 -> SetSequence of X means :Def2: :: PROB_3:def 2
( it . 0 = A1 . 0 & ( for n being Nat holds it . (n + 1) = (it . n) \/ (A1 . (n + 1)) ) );
existence by Th9;
uniqueness

proof end;

end;

:: deftheorem Def2 defines Partial_Union PROB_3:def 2 :

theorem Th10: :: PROB_3:10

for n being Nat
for X being set
for A1 being SetSequence of X holds (Partial_Intersection A1) . n c= A1 . n

proof end;

theorem Th11: :: PROB_3:11

for n being Nat
for X being set
for A1 being SetSequence of X holds A1 . n c= (Partial_Union A1) . n

proof end;

theorem Th12: :: PROB_3:12

for X being set
for A1 being SetSequence of X holds Partial_Intersection A1 is non-ascending

proof end;

theorem Th13: :: PROB_3:13

for X being set
for A1 being SetSequence of X holds Partial_Union A1 is non-descending

proof end;

theorem Th14: :: PROB_3:14

for n being Nat
for X, x being set
for A1 being SetSequence of X holds
( x in (Partial_Intersection A1) . n iff for k being Nat st k <= n holds
x in A1 . k )

proof end;

theorem Th15: :: PROB_3:15

for n being Nat
for X, x being set
for A1 being SetSequence of X holds
( x in (Partial_Union A1) . n iff ex k being Nat st
( k <= n & x in A1 . k ) )

proof end;

theorem Th16: :: PROB_3:16

for X being set
for A1 being SetSequence of X holds Intersection (Partial_Intersection A1) = Intersection A1

proof end;

theorem Th17: :: PROB_3:17

for X being set
for A1 being SetSequence of X holds Union (Partial_Union A1) = Union A1

proof end;

theorem Th18: :: PROB_3:18

for X being set
for A1 being SetSequence of X ex A2 being SetSequence of X st
( A2 . 0 = A1 . 0 & ( for n being Nat holds A2 . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) )

proof end;

definition

let X be set ;
let A1 be SetSequence of X;
func Partial_Diff_Union A1 -> SetSequence of X means :Def3: :: PROB_3:def 3
( it . 0 = A1 . 0 & ( for n being Nat holds it . (n + 1) = (A1 . (n + 1)) \ ((Partial_Union A1) . n) ) );
existence by Th18;
uniqueness

proof end;

end;

:: deftheorem Def3 defines Partial_Diff_Union PROB_3:def 3 :

theorem Th19: :: PROB_3:19

for n being Nat
for X, x being set
for A1 being SetSequence of X holds
( x in (Partial_Diff_Union A1) . n iff ( x in A1 . n & ( for k being Nat st k < n holds
not x in A1 . k ) ) )

proof end;

theorem Th20: :: PROB_3:20

for n being Nat
for X being set
for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= A1 . n

proof end;

theorem Th21: :: PROB_3:21

for n being Nat
for X being set
for A1 being SetSequence of X holds (Partial_Diff_Union A1) . n c= (Partial_Union A1) . n

proof end;

theorem Th22: :: PROB_3:22

for X being set
for A1 being SetSequence of X holds Partial_Union (Partial_Diff_Union A1) = Partial_Union A1

proof end;

theorem Th23: :: PROB_3:23

for X being set
for A1 being SetSequence of X holds Union (Partial_Diff_Union A1) = Union A1

proof end;

definition

let X be set ;
let A1 be SetSequence of X;
:: original: disjoint_valued
redefine attr A1 is disjoint_valued means :Def4: :: PROB_3:def 4
for m, n being Nat st m <> n holds
A1 . m misses A1 . n;
compatibility

proof end;

end;

:: deftheorem Def4 defines disjoint_valued PROB_3:def 4 :

theorem Th24: :: PROB_3:24

for X being set
for A1 being SetSequence of X holds Partial_Diff_Union A1 is disjoint_valued

proof end;

definition

let X be set ;
let Si be SigmaField of X;
let XSeq be SetSequence of Si;
func @Partial_Intersection XSeq -> SetSequence of Si equals :: PROB_3:def 5
Partial_Intersection XSeq;
coherence

proof end;

end;

:: deftheorem defines @Partial_Intersection PROB_3:def 5 :

definition

let X be set ;
let Si be SigmaField of X;
let XSeq be SetSequence of Si;
func @Partial_Union XSeq -> SetSequence of Si equals :: PROB_3:def 6
Partial_Union XSeq;
coherence

proof end;

end;

:: deftheorem defines @Partial_Union PROB_3:def 6 :

definition

let X be set ;
let Si be SigmaField of X;
let XSeq be SetSequence of Si;
func @Partial_Diff_Union XSeq -> SetSequence of Si equals :: PROB_3:def 7
Partial_Diff_Union XSeq;
coherence

proof end;

end;

:: deftheorem defines @Partial_Diff_Union PROB_3:def 7 :

theorem :: PROB_3:25

for X being set
for Si being SigmaField of X
for YSeq, XSeq being SetSequence of Si st YSeq = @Partial_Intersection XSeq holds
( YSeq . 0 = XSeq . 0 & ( for n being Nat holds YSeq . (n + 1) = (YSeq . n) /\ (XSeq . (n + 1)) ) ) by Def1;

theorem :: PROB_3:26

for X being set
for Si being SigmaField of X
for YSeq, XSeq being SetSequence of Si st YSeq = @Partial_Union XSeq holds
( YSeq . 0 = XSeq . 0 & ( for n being Nat holds YSeq . (n + 1) = (YSeq . n) \/ (XSeq . (n + 1)) ) ) by Def2;

theorem :: PROB_3:27

for n being Nat
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds (@Partial_Intersection XSeq) . n c= XSeq . n by Th10;

theorem :: PROB_3:28

for n being Nat
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds XSeq . n c= (@Partial_Union XSeq) . n by Th11;

theorem :: PROB_3:29

for n being Nat
for X, x being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds
( x in (@Partial_Intersection XSeq) . n iff for k being Nat st k <= n holds
x in XSeq . k ) by Th14;

theorem :: PROB_3:30

for n being Nat
for X, x being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds
( x in (@Partial_Union XSeq) . n iff ex k being Nat st
( k <= n & x in XSeq . k ) ) by Th15;

theorem :: PROB_3:31

for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds @Partial_Intersection XSeq is non-ascending by Th12;

theorem :: PROB_3:32

for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds @Partial_Union XSeq is non-descending by Th13;

theorem :: PROB_3:33

for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds Intersection (@Partial_Intersection XSeq) = Intersection XSeq by Th16;

theorem :: PROB_3:34

for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds Union (@Partial_Union XSeq) = Union XSeq by Th17;

theorem :: PROB_3:35

for X being set
for Si being SigmaField of X
for YSeq, XSeq being SetSequence of Si st YSeq = @Partial_Diff_Union XSeq holds
( YSeq . 0 = XSeq . 0 & ( for n being Nat holds YSeq . (n + 1) = (XSeq . (n + 1)) \ ((@Partial_Union XSeq) . n) ) ) by Def3;

theorem :: PROB_3:36

for n being Nat
for X, x being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds
( x in (@Partial_Diff_Union XSeq) . n iff ( x in XSeq . n & ( for k being Nat st k < n holds
not x in XSeq . k ) ) ) by Th19;

theorem :: PROB_3:37

for n being Nat
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds (@Partial_Diff_Union XSeq) . n c= XSeq . n by Th20;

theorem :: PROB_3:38

for n being Nat
for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds (@Partial_Diff_Union XSeq) . n c= (@Partial_Union XSeq) . n by Th21;

theorem :: PROB_3:39

for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds @Partial_Union (@Partial_Diff_Union XSeq) = @Partial_Union XSeq by Th22;

theorem :: PROB_3:40

for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds Union (@Partial_Diff_Union XSeq) = Union XSeq by Th23;

theorem :: PROB_3:41

for X being set
for Si being SigmaField of X
for XSeq being SetSequence of Si holds @Partial_Diff_Union XSeq is disjoint_valued by Th24;

theorem Th42: :: PROB_3:42

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds P * (@Partial_Union ASeq) is non-decreasing

proof end;

theorem :: PROB_3:43

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds P * (@Partial_Intersection ASeq) is non-increasing

proof end;

theorem :: PROB_3:44

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds Partial_Sums (P * ASeq) is non-decreasing

proof end;

theorem Th45: :: PROB_3:45

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds (P * (@Partial_Union ASeq)) . 0 = (Partial_Sums (P * ASeq)) . 0

proof end;

theorem Th46: :: PROB_3:46

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma holds
( P * (@Partial_Union ASeq) is convergent & lim (P * (@Partial_Union ASeq)) = upper_bound (P * (@Partial_Union ASeq)) & lim (P * (@Partial_Union ASeq)) = P . (Union ASeq) )

proof end;

theorem Th47: :: PROB_3:47

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma st ASeq is disjoint_valued holds
for n, m being Nat st n < m holds
(@Partial_Union ASeq) . n misses ASeq . m

proof end;

theorem Th48: :: PROB_3:48

for n being Nat
for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq is disjoint_valued holds
(P * (@Partial_Union ASeq)) . n = (Partial_Sums (P * ASeq)) . n

proof end;

theorem Th49: :: PROB_3:49

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq is disjoint_valued holds
P * (@Partial_Union ASeq) = Partial_Sums (P * ASeq)

proof end;

theorem Th50: :: PROB_3:50

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq is disjoint_valued holds
( Partial_Sums (P * ASeq) is convergent & lim (Partial_Sums (P * ASeq)) = upper_bound (Partial_Sums (P * ASeq)) & lim (Partial_Sums (P * ASeq)) = P . (Union ASeq) )

proof end;

theorem Th51: :: PROB_3:51

for Omega being non empty set
for Sigma being SigmaField of Omega
for ASeq being SetSequence of Sigma
for P being Probability of Sigma st ASeq is disjoint_valued holds
P . (Union ASeq) = Sum (P * ASeq)

proof end;

definition

let X be set ;
let F1 be FinSequence of bool X;
let n be Nat;
:: original: .
redefine func F1 . n -> Subset of X;
coherence

proof end;

end;

theorem Th52: :: PROB_3:52

for X being set ex F1 being FinSequence of bool X st
for k being Nat st k in dom F1 holds
F1 . k = X

proof end;

theorem :: PROB_3:53

for X being set
for F1 being FinSequence of bool X holds union (rng F1) is Subset of X ;

definition

let X be set ;
let F1 be FinSequence of bool X;
:: original: Union
redefine func Union F1 -> Subset of X;
coherence

proof end;

end;

theorem Th54: :: PROB_3:54

for X, x being set
for F1 being FinSequence of bool X holds
( x in Union F1 iff ex k being Nat st
( k in dom F1 & x in F1 . k ) )

proof end;

definition

let X be set ;
let F1 be FinSequence of bool X;
func Complement F1 -> FinSequence of bool X means :Def8: :: PROB_3:def 8
( len it = len F1 & ( for n being Nat st n in dom it holds
it . n = (F1 . n) ` ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines Complement PROB_3:def 8 :

definition

let X be set ;
let F1 be FinSequence of bool X;
func Intersection F1 -> Subset of X equals :Def9: :: PROB_3:def 9
(Union (Complement F1)) ` if F1 <> {}
otherwise {} ;
coherence by SUBSET_1:4;
consistency ;

end;

:: deftheorem Def9 defines Intersection PROB_3:def 9 :

theorem Th55: :: PROB_3:55

for X being set
for F1 being FinSequence of bool X holds dom (Complement F1) = dom F1

proof end;

theorem Th56: :: PROB_3:56

for X, x being set
for F1 being FinSequence of bool X st F1 <> {} holds
( x in Intersection F1 iff for k being Nat st k in dom F1 holds
x in F1 . k )

proof end;

theorem Th57: :: PROB_3:57

for X, x being set
for F1 being FinSequence of bool X st F1 <> {} holds
( x in meet (rng F1) iff for n being Nat st n in dom F1 holds
x in F1 . n )

proof end;

theorem :: PROB_3:58

for X being set
for F1 being FinSequence of bool X holds Intersection F1 = meet (rng F1)

proof end;

theorem Th59: :: PROB_3:59

for X being set
for F1 being FinSequence of bool X ex A1 being SetSequence of X st
( ( for k being Nat st k in dom F1 holds
A1 . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds
A1 . k = {} ) )

proof end;

theorem Th60: :: PROB_3:60

for X being set
for F1 being FinSequence of bool X
for A1 being SetSequence of X st ( for k being Nat st k in dom F1 holds
A1 . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds
A1 . k = {} ) holds
( A1 . 0 = {} & Union A1 = Union F1 )

proof end;

definition

let X be set ;
let Si be SigmaField of X;
mode FinSequence of Si -> FinSequence of bool X means :Def10: :: PROB_3:def 10
for k being Nat st k in dom it holds
it . k in Si;
existence

proof end;

end;

:: deftheorem Def10 defines FinSequence PROB_3:def 10 :

definition

let X be set ;
let Si be SigmaField of X;
let FSi be FinSequence of Si;
let n be Nat;
:: original: .
redefine func FSi . n -> Event of Si;
coherence

proof end;

end;

theorem Th61: :: PROB_3:61

for X being set
for Si being SigmaField of X
for FSi being FinSequence of Si ex ASeq being SetSequence of Si st
( ( for k being Nat st k in dom FSi holds
ASeq . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds
ASeq . k = {} ) )

proof end;

theorem Th62: :: PROB_3:62

for X being set
for Si being SigmaField of X
for FSi being FinSequence of Si holds Union FSi in Si

proof end;

definition

let X be set ;
let S be SigmaField of X;
let F be FinSequence of S;
func @Complement F -> FinSequence of S equals :: PROB_3:def 11
Complement F;
coherence

proof end;

end;

:: deftheorem defines @Complement PROB_3:def 11 :

theorem :: PROB_3:63

for X being set
for Si being SigmaField of X
for FSi being FinSequence of Si holds Intersection FSi in Si

proof end;

theorem Th64: :: PROB_3:64

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for FSeq being FinSequence of Sigma holds dom (P * FSeq) = dom FSeq

proof end;

theorem Th65: :: PROB_3:65

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for FSeq being FinSequence of Sigma holds P * FSeq is FinSequence of REAL

proof end;

definition

let Omega be non empty set ;
let Sigma be SigmaField of Omega;
let FSeq be FinSequence of Sigma;
let P be Probability of Sigma;
:: original: *
redefine func P * FSeq -> FinSequence of REAL ;
coherence by Th65;

end;

theorem Th66: :: PROB_3:66

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for FSeq being FinSequence of Sigma holds len (P * FSeq) = len FSeq

proof end;

theorem Th67: :: PROB_3:67

for RFin being FinSequence of REAL st len RFin = 0 holds
Sum RFin = 0

proof end;

theorem Th68: :: PROB_3:68

for RFin being FinSequence of REAL st len RFin >= 1 holds
ex f being Real_Sequence st
( f . 1 = RFin . 1 & ( for n being Nat st 0 <> n & n < len RFin holds
f . (n + 1) = (f . n) + (RFin . (n + 1)) ) & Sum RFin = f . (len RFin) )

proof end;

theorem Th69: :: PROB_3:69

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for FSeq being FinSequence of Sigma
for ASeq being SetSequence of Sigma st ( for k being Nat st k in dom FSeq holds
ASeq . k = FSeq . k ) & ( for k being Nat st not k in dom FSeq holds
ASeq . k = {} ) holds
( Partial_Sums (P * ASeq) is convergent & Sum (P * ASeq) = (Partial_Sums (P * ASeq)) . (len FSeq) & P . (Union ASeq) <= Sum (P * ASeq) & Sum (P * FSeq) = Sum (P * ASeq) )

proof end;

theorem :: PROB_3:70

for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for FSeq being FinSequence of Sigma holds
( P . (Union FSeq) <= Sum (P * FSeq) & ( FSeq is disjoint_valued implies P . (Union FSeq) = Sum (P * FSeq) ) )

proof end;

definition

let X be set ;
let IT be Subset-Family of X;
attr IT is non-decreasing-closed means :Def12: :: PROB_3:def 12
for A1 being SetSequence of X st A1 is non-descending & rng A1 c= IT holds
Union A1 in IT;
attr IT is non-increasing-closed means :Def13: :: PROB_3:def 13
for A1 being SetSequence of X st A1 is non-ascending & rng A1 c= IT holds
Intersection A1 in IT;

end;

:: deftheorem Def12 defines non-decreasing-closed PROB_3:def 12 :

:: deftheorem Def13 defines non-increasing-closed PROB_3:def 13 :

theorem Th71: :: PROB_3:71

for X being set
for IT being Subset-Family of X holds
( IT is non-decreasing-closed iff for A1 being SetSequence of X st A1 is non-descending & rng A1 c= IT holds
lim A1 in IT )

proof end;

theorem Th72: :: PROB_3:72

for X being set
for IT being Subset-Family of X holds
( IT is non-increasing-closed iff for A1 being SetSequence of X st A1 is non-ascending & rng A1 c= IT holds
lim A1 in IT )

proof end;

theorem Th73: :: PROB_3:73

for X being set holds
( bool X is non-decreasing-closed & bool X is non-increasing-closed )

proof end;

registration

let X be set ;
cluster non-decreasing-closed non-increasing-closed Element of K10(K10(X));
existence

proof end;

end;

definition

let X be set ;
mode MonotoneClass of X is non-decreasing-closed non-increasing-closed Subset-Family of X;

end;

theorem Th74: :: PROB_3:74

for Z, X being set holds
( Z is MonotoneClass of X iff ( Z c= bool X & ( for A1 being SetSequence of X st A1 is monotone & rng A1 c= Z holds
lim A1 in Z ) ) )

proof end;

theorem Th75: :: PROB_3:75

for X being set
for F being Field_Subset of X holds
( F is SigmaField of X iff F is MonotoneClass of X )

proof end;

theorem :: PROB_3:76

for Omega being non empty set holds bool Omega is MonotoneClass of Omega by Th73;

theorem Th77: :: PROB_3:77

for Omega being non empty set
for X being Subset-Family of Omega ex Y being MonotoneClass of Omega st
( X c= Y & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
Y c= Z ) )

proof end;

definition

canceled;
let Omega be non empty set ;
let X be Subset-Family of Omega;
func monotoneclass X -> MonotoneClass of Omega means :Def15: :: PROB_3:def 15
( X c= it & ( for Z being set st X c= Z & Z is MonotoneClass of Omega holds
it c= Z ) );
existence by Th77;
uniqueness

proof end;

end;

:: deftheorem PROB_3:def 14 :

:: deftheorem Def15 defines monotoneclass PROB_3:def 15 :

theorem Th78: :: PROB_3:78

for Omega being non empty set
for Z being Field_Subset of Omega holds monotoneclass Z is Field_Subset of Omega

proof end;

theorem :: PROB_3:79

for Omega being non empty set
for Z being Field_Subset of Omega holds sigma Z = monotoneclass Z

proof end;