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