Volume 12, 2000

University of Bialystok

Copyright (c) 2000 Association of Mizar Users

### The abstract of the Mizar article:

### Dynkin's Lemma in Measure Theory

**by****Franz Merkl**- Received November 27, 2000
- MML identifier: DYNKIN

- [ Mizar article, MML identifier index ]

environ vocabulary PROB_1, RELAT_1, FUNCT_1, ALGSEQ_1, FINSET_1, BOOLE, FUNCOP_1, FUNCT_4, TARSKI, PROB_2, SETFAM_1, COHSP_1, SUBSET_1, DYNKIN; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FINSET_1, NUMBERS, XREAL_0, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, NAT_1, FUNCT_4, FUNCOP_1, ALGSEQ_1, PROB_1, COHSP_1, PROB_2; constructors ALGSEQ_1, NAT_1, FUNCT_4, COHSP_1, PROB_2, MEMBERED; clusters SUBSET_1, ARYTM_3, RELSET_1, FINSET_1, FUNCT_1, FUNCT_4, FUNCOP_1, MEMBERED, NUMBERS, ORDINAL2; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve Omega, F for non empty set, f for SetSequence of Omega, X,A,B for Subset of Omega, D for non empty Subset of bool Omega, k,n,m for Nat, h,x,y,z,u,v,Y,I for set; ::::::::::::::::::: :: Preliminaries :: ::::::::::::::::::: theorem :: DYNKIN:1 for f being SetSequence of Omega for x holds x in rng f iff ex n st f.n=x; theorem :: DYNKIN:2 for n holds PSeg(n) is finite; definition let n; cluster PSeg(n) -> finite; end; definition let a,b,c be set; func (a,b) followed_by c equals :: DYNKIN:def 1 (NAT --> c) +* ((0,1) --> (a,b)); end; definition let a,b,c be set; cluster (a,b) followed_by c -> Function-like Relation-like; end; definition let X be non empty set; let a,b,c be Element of X; redefine func (a,b) followed_by c -> Function of NAT, X; end; definition let Omega be non empty set; let a,b,c be Subset of Omega; redefine func (a,b) followed_by c -> SetSequence of Omega; end; canceled 2; theorem :: DYNKIN:5 for a,b,c being set holds ((a,b) followed_by c).0 = a & ((a,b) followed_by c).1 = b & for n st n <> 0 & n <> 1 holds ((a,b) followed_by c).n = c; theorem :: DYNKIN:6 for a,b being Subset of Omega holds union rng ((a,b) followed_by {}) = a \/ b; definition let Omega be non empty set; let f be SetSequence of Omega; let X be Subset of Omega; func seqIntersection(X,f) -> SetSequence of Omega means :: DYNKIN:def 2 for n holds it.n = X /\ f.n; end; begin :::::::::::::::::::::::::::::::::::::::::::::::: :: disjoint-valued functions and intersection :: :::::::::::::::::::::::::::::::::::::::::::::::: definition let Omega; let f; redefine attr f is disjoint_valued means :: DYNKIN:def 3 n<m implies f.n misses f.m; end; theorem :: DYNKIN:7 for Y being non empty set holds for x holds x c= meet Y iff for y being Element of Y holds x c= y; definition let x be set; redefine attr x is multiplicative; synonym x is intersection_stable; end; definition let Omega be non empty set; let f be SetSequence of Omega; let n be Element of NAT; canceled; func disjointify(f,n) -> Element of bool Omega equals :: DYNKIN:def 5 f.n \ union rng (f|PSeg(n)); end; definition let Omega be non empty set; let g be SetSequence of Omega; func disjointify(g) -> SetSequence of Omega means :: DYNKIN:def 6 for n holds it.n=disjointify(g,n); end; theorem :: DYNKIN:8 for n holds (disjointify(f)).n=f.n \ union rng(f|PSeg(n)); theorem :: DYNKIN:9 for f being SetSequence of Omega holds disjointify(f) is disjoint_valued; theorem :: DYNKIN:10 for f being SetSequence of Omega holds union rng disjointify(f) = union rng f; theorem :: DYNKIN:11 for x,y being Subset of Omega st x misses y holds (x,y) followed_by {} Omega is disjoint_valued; theorem :: DYNKIN:12 for f being SetSequence of Omega holds f is disjoint_valued implies for X being Subset of Omega holds seqIntersection(X,f) is disjoint_valued; theorem :: DYNKIN:13 for f being SetSequence of Omega for X being Subset of Omega holds X/\ Union f= Union seqIntersection(X,f); begin ::::::::::::::::::::::::::::::::::::::::::::::::::::::: :: Dynkin Systems:definition and closure properties :: ::::::::::::::::::::::::::::::::::::::::::::::::::::::: definition let Omega; mode Dynkin_System of Omega -> Subset of bool Omega means :: DYNKIN:def 7 (for f holds rng f c= it & f is disjoint_valued implies Union f in it) & (for X holds X in it implies X` in it) & {} in it; end; definition let Omega; cluster -> non empty Dynkin_System of Omega; end; theorem :: DYNKIN:14 bool Omega is Dynkin_System of Omega; theorem :: DYNKIN:15 (for Y st Y in F holds Y is Dynkin_System of Omega) implies meet F is Dynkin_System of Omega; theorem :: DYNKIN:16 D is Dynkin_System of Omega & D is intersection_stable implies (A in D & B in D implies A\B in D); theorem :: DYNKIN:17 D is Dynkin_System of Omega & D is intersection_stable implies (A in D & B in D implies A \/ B in D); theorem :: DYNKIN:18 D is Dynkin_System of Omega & D is intersection_stable implies for x being finite set holds x c= D implies union x in D; theorem :: DYNKIN:19 D is Dynkin_System of Omega & D is intersection_stable implies for f being SetSequence of Omega holds rng f c= D implies rng disjointify(f) c= D; theorem :: DYNKIN:20 D is Dynkin_System of Omega & D is intersection_stable implies for f being SetSequence of Omega holds rng f c= D implies union rng f in D; theorem :: DYNKIN:21 for D being Dynkin_System of Omega for x,y being Element of D holds x misses y implies x \/ y in D; theorem :: DYNKIN:22 for D being Dynkin_System of Omega for x,y being Element of D holds x c= y implies y\x in D; begin ::::::::::::::::::::::::::::::::::: :: Main steps for Dynkin's Lemma :: ::::::::::::::::::::::::::::::::::: theorem :: DYNKIN:23 D is Dynkin_System of Omega & D is intersection_stable implies D is SigmaField of Omega; definition let Omega be non empty set; let E be Subset of bool Omega; func generated_Dynkin_System(E) -> Dynkin_System of Omega means :: DYNKIN:def 8 E c= it & for D being Dynkin_System of Omega holds (E c= D implies it c= D); end; definition let Omega be non empty set; let G be set; let X be Subset of Omega; func DynSys(X,G) -> Subset of bool Omega means :: DYNKIN:def 9 for A being Subset of Omega holds A in it iff A /\ X in G; end; definition let Omega be non empty set; let G be Dynkin_System of Omega; let X be Element of G; redefine func DynSys(X,G) -> Dynkin_System of Omega; end; theorem :: DYNKIN:24 for E being Subset of bool Omega for X,Y being Subset of Omega holds X in E & Y in generated_Dynkin_System(E) & E is intersection_stable implies X/\ Y in generated_Dynkin_System(E); theorem :: DYNKIN:25 for E being Subset of bool Omega for X,Y being Subset of Omega holds X in generated_Dynkin_System(E) & Y in generated_Dynkin_System(E) & E is intersection_stable implies X/\ Y in generated_Dynkin_System(E); theorem :: DYNKIN:26 for E being Subset of bool Omega st E is intersection_stable holds generated_Dynkin_System(E) is intersection_stable; theorem :: DYNKIN:27 for E being Subset of bool Omega st E is intersection_stable for D being Dynkin_System of Omega st E c= D holds sigma(E) c= D;

Back to top