:: Dynkin's Lemma in Measure Theory :: by Franz Merkl :: :: Received November 27, 2000 :: Copyright (c) 2000-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 XBOOLE_0, PROB_1, SUBSET_1, SETFAM_1, NUMBERS, RELAT_1, FUNCT_1, FINSET_1, ARYTM_3, CARD_1, FUNCT_7, CARD_3, TARSKI, ZFMISC_1, PROB_2, XXREAL_0, NAT_1, EQREL_1, DYNKIN, FINSUB_1; notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, FINSET_1, CARD_1, ORDINAL1, NUMBERS, SETFAM_1, RELAT_1, FUNCT_1, FUNCT_2, XCMPLX_0, NAT_1, FUNCT_7, CARD_3, PROB_1, FINSUB_1, PROB_2, XXREAL_0; constructors SETFAM_1, FINSUB_1, NAT_1, PROB_2, XREAL_0, FUNCT_7, ENUMSET1, RELSET_1; registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, FINSET_1, XREAL_0, FUNCT_7, CARD_1; 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-Family of Omega, n,m for Element of 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; 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; ::$CT theorem :: DYNKIN:3 for a,b being set holds Union (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 1 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 2 n Subset of Omega equals :: DYNKIN:def 3 f.n \ union rng (f|n); end; definition let Omega be non empty set; let g be SetSequence of Omega; func disjointify(g) -> SetSequence of Omega means :: DYNKIN:def 4 for n being Nat holds it.n=disjointify(g,n); end; theorem :: DYNKIN:5 for n being Nat holds (disjointify(f)).n=f.n \ union rng(f|n); theorem :: DYNKIN:6 for f being SetSequence of Omega holds disjointify(f) is disjoint_valued; theorem :: DYNKIN:7 for f being SetSequence of Omega holds union rng disjointify(f) = union rng f ; theorem :: DYNKIN:8 for x,y being Subset of Omega st x misses y holds (x,y) followed_by {} Omega is disjoint_valued; theorem :: DYNKIN:9 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:10 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-Family of Omega means :: DYNKIN:def 5 (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; registration let Omega; cluster -> non empty for Dynkin_System of Omega; end; theorem :: DYNKIN:11 bool Omega is Dynkin_System of Omega; theorem :: DYNKIN:12 (for Y st Y in F holds Y is Dynkin_System of Omega) implies meet F is Dynkin_System of Omega; theorem :: DYNKIN:13 D is Dynkin_System of Omega & D is intersection_stable implies ( A in D & B in D implies A\B in D); theorem :: DYNKIN:14 D is Dynkin_System of Omega & D is intersection_stable implies ( A in D & B in D implies A \/ B in D); theorem :: DYNKIN:15 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:16 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:17 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:18 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:19 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:20 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-Family of Omega; func generated_Dynkin_System(E) -> Dynkin_System of Omega means :: DYNKIN:def 6 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-Family of Omega means :: DYNKIN:def 7 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:21 for E being Subset-Family of 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:22 for E being Subset-Family of 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:23 for E being Subset-Family of Omega st E is intersection_stable holds generated_Dynkin_System(E) is intersection_stable; ::$N Dynkin Lemma theorem :: DYNKIN:24 for E being Subset-Family of Omega st E is intersection_stable for D being Dynkin_System of Omega st E c= D holds sigma(E) c= D;