Journal of Formalized Mathematics
Volume 12, 2000
University of Bialystok
Copyright (c) 2000 Association of Mizar Users

### Dynkin's Lemma in Measure Theory

by
Franz Merkl

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