:: Dynkin's Lemma in Measure Theory
:: by Franz Merkl
::
:: Received November 27, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users


begin

:: Preliminaries ::
theorem Th1: :: DYNKIN:1
for Omega being non empty set
for f being SetSequence of Omega
for x being set holds
( x in rng f iff ex n being Element of NAT st f . n = x )
proofend;

theorem Th2: :: DYNKIN:2
for n being Element of NAT holds n is finite
proofend;

registration
let n be Element of NAT ;
cluster Segm n ->  finite ;
coherence
 Segm n is finite by Th2;
end;

Lm1:  for X being non empty set
for a, b, c being Element of X holds (a,b) followed_by c is Function of NAT,X
;

definition
let Omega be non empty set ;
let a, b, c be Subset of Omega;
:: original:followed_by
redefine func(a,b) followed_by c ->  SetSequence of Omega;
coherence
 (a,b) followed_by c is SetSequence of Omega
proofend;
end;

theorem Th3: :: DYNKIN:3
for a, b being set holds Union ((a,b) followed_by {}) = a \/ b
proofend;

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 :Def1: :: DYNKIN:def 1
 for n being Element of NAT holds it . n = X /\ (f . n);
existence
 ex b1 being SetSequence of Omega st
for n being Element of NAT holds b1 . n = X /\ (f . n)
proofend;
uniqueness
 for b1, b2 being SetSequence of Omega st ( for n being Element of NAT holds b1 . n = X /\ (f . n) ) & ( for n being Element of NAT holds b2 . n = X /\ (f . n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines seqIntersection DYNKIN:def_1_:_
 for Omega being non empty set
for f being SetSequence of Omega
for X being Subset of Omega
for b4 being SetSequence of Omega holds
( b4 = seqIntersection (X,f) iff for n being Element of NAT holds b4 . n = X /\ (f . n) );

begin

:: disjoint-valued functions and intersection ::
definition
let Omega be non empty set ;
let f be SetSequence of Omega;
:: original:disjoint_valued
redefine attrf is disjoint_valued  means :Def2: :: DYNKIN:def 2
 for n, m being Element of NAT st n < m holds
f . n misses f . m;
compatibility
 ( f is disjoint_valued iff for n, m being Element of NAT st n < m holds
f . n misses f . m )
proofend;
end;

:: deftheorem Def2 defines disjoint_valued DYNKIN:def_2_:_
 for Omega being non empty set
for f being SetSequence of Omega holds
( f is disjoint_valued iff for n, m being Element of NAT st n < m holds
f . n misses f . m );

theorem Th4: :: DYNKIN:4
for Y being non empty set
for x being set holds
( x c= meet Y iff for y being Element of Y holds x c= y )
proofend;

notation
let x be set ;
synonym  intersection_stable x for  cap-closed ;
end;

definition
let Omega be non empty set ;
let f be SetSequence of Omega;
let n be Nat;
func disjointify (f,n) ->  Subset of Omega equals :: DYNKIN:def 3
(f . n) \ (union (rng (f | n)));
coherence
 (f . n) \ (union (rng (f | n))) is Subset of Omega ;
end;

:: deftheorem  defines disjointify DYNKIN:def_3_:_
 for Omega being non empty set
for f being SetSequence of Omega
for n being Nat holds disjointify (f,n) = (f . n) \ (union (rng (f | n)));

definition
let Omega be non empty set ;
let g be SetSequence of Omega;
func disjointify g ->  SetSequence of Omega means :Def4: :: DYNKIN:def 4
 for n being Nat holds it . n = disjointify (g,n);
existence
 ex b1 being SetSequence of Omega st
for n being Nat holds b1 . n = disjointify (g,n)
proofend;
uniqueness
 for b1, b2 being SetSequence of Omega st ( for n being Nat holds b1 . n = disjointify (g,n) ) &amp; ( for n being Nat holds b2 . n = disjointify (g,n) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines disjointify DYNKIN:def_4_:_
 for Omega being non empty set
for g, b3 being SetSequence of Omega holds
( b3 = disjointify g iff for n being Nat holds b3 . n = disjointify (g,n) );

theorem Th5: :: DYNKIN:5
for Omega being non empty set
for f being SetSequence of Omega
for n being Nat holds (disjointify f) . n = (f . n) \ (union (rng (f | n)))
proofend;

theorem Th6: :: DYNKIN:6
for Omega being non empty set
for f being SetSequence of Omega holds disjointify f is V56()
proofend;

theorem Th7: :: DYNKIN:7
for Omega being non empty set
for f being SetSequence of Omega holds union (rng (disjointify f)) = union (rng f)
proofend;

theorem Th8: :: DYNKIN:8
for Omega being non empty set
for x, y being Subset of Omega st x misses y holds
(x,y) followed_by ({} Omega) is V56()
proofend;

theorem Th9: :: DYNKIN:9
for Omega being non empty set
for f being SetSequence of Omega st f is V56() holds
for X being Subset of Omega holds seqIntersection (X,f) is V56()
proofend;

theorem Th10: :: DYNKIN:10
for Omega being non empty set
for f being SetSequence of Omega
for X being Subset of Omega holds X /\ (Union f) = Union (seqIntersection (X,f))
proofend;

begin

:: Dynkin Systems:definition and closure properties ::
definition
let Omega be non empty set ;
mode Dynkin_System of Omega ->  Subset-Family of Omega means :Def5: :: DYNKIN:def 5
( ( for f being SetSequence of Omega st rng f c= it &amp; f is V56() holds
Union f in it ) &amp; ( for X being Subset of Omega st X in it holds
X ` in it ) &amp; {} in it );
existence
 ex b1 being Subset-Family of Omega st
( ( for f being SetSequence of Omega st rng f c= b1 &amp; f is V56() holds
Union f in b1 ) &amp; ( for X being Subset of Omega st X in b1 holds
X ` in b1 ) &amp; {} in b1 )
proofend;
end;

:: deftheorem Def5 defines Dynkin_System DYNKIN:def_5_:_
 for Omega being non empty set
for b2 being Subset-Family of Omega holds
( b2 is Dynkin_System of Omega iff ( ( for f being SetSequence of Omega st rng f c= b2 &amp; f is V56() holds
Union f in b2 ) &amp; ( for X being Subset of Omega st X in b2 holds
X ` in b2 ) &amp; {} in b2 ) );

registration
let Omega be non empty set ;
cluster  ->  non empty for Dynkin_System of Omega;
coherence
 for b1 being Dynkin_System of Omega holds not b1 is empty by Def5;
end;

theorem Th11: :: DYNKIN:11
for Omega being non empty set holds bool Omega is Dynkin_System of Omega
proofend;

theorem Th12: :: DYNKIN:12
for F, Omega being non empty set st ( for Y being set st Y in F holds
Y is Dynkin_System of Omega ) holds
meet F is Dynkin_System of Omega
proofend;

theorem Th13: :: DYNKIN:13
for Omega being non empty set
for A, B being Subset of Omega
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega &amp; D is intersection_stable &amp; A in D &amp; B in D holds
A \ B in D
proofend;

theorem Th14: :: DYNKIN:14
for Omega being non empty set
for A, B being Subset of Omega
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega &amp; D is intersection_stable &amp; A in D &amp; B in D holds
A \/ B in D
proofend;

theorem Th15: :: DYNKIN:15
for Omega being non empty set
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega &amp; D is intersection_stable holds
for x being finite set st x c= D holds
union x in D
proofend;

theorem Th16: :: DYNKIN:16
for Omega being non empty set
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega &amp; D is intersection_stable holds
for f being SetSequence of Omega st rng f c= D holds
rng (disjointify f) c= D
proofend;

theorem Th17: :: DYNKIN:17
for Omega being non empty set
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega &amp; D is intersection_stable holds
for f being SetSequence of Omega st rng f c= D holds
union (rng f) in D
proofend;

theorem Th18: :: DYNKIN:18
for Omega being non empty set
for D being Dynkin_System of Omega
for x, y being Element of D st x misses y holds
x \/ y in D
proofend;

theorem Th19: :: DYNKIN:19
for Omega being non empty set
for D being Dynkin_System of Omega
for x, y being Element of D st x c= y holds
y \ x in D
proofend;

begin

:: Main steps for Dynkin's Lemma ::
theorem Th20: :: DYNKIN:20
for Omega being non empty set
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega &amp; D is intersection_stable holds
D is SigmaField of Omega
proofend;

definition
let Omega be non empty set ;
let E be Subset-Family of Omega;
func generated_Dynkin_System E ->  Dynkin_System of Omega means :Def6: :: DYNKIN:def 6
( E c= it &amp; ( for D being Dynkin_System of Omega st E c= D holds
it c= D ) );
existence
 ex b1 being Dynkin_System of Omega st
( E c= b1 &amp; ( for D being Dynkin_System of Omega st E c= D holds
b1 c= D ) )
proofend;
uniqueness
 for b1, b2 being Dynkin_System of Omega st E c= b1 &amp; ( for D being Dynkin_System of Omega st E c= D holds
b1 c= D ) &amp; E c= b2 &amp; ( for D being Dynkin_System of Omega st E c= D holds
b2 c= D ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines generated_Dynkin_System DYNKIN:def_6_:_
 for Omega being non empty set
for E being Subset-Family of Omega
for b3 being Dynkin_System of Omega holds
( b3 = generated_Dynkin_System E iff ( E c= b3 &amp; ( for D being Dynkin_System of Omega st E c= D holds
b3 c= D ) ) );

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 :Def7: :: DYNKIN:def 7
 for A being Subset of Omega holds
( A in it iff A /\ X in G );
existence
 ex b1 being Subset-Family of Omega st
for A being Subset of Omega holds
( A in b1 iff A /\ X in G )
proofend;
uniqueness
 for b1, b2 being Subset-Family of Omega st ( for A being Subset of Omega holds
( A in b1 iff A /\ X in G ) ) &amp; ( for A being Subset of Omega holds
( A in b2 iff A /\ X in G ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines DynSys DYNKIN:def_7_:_
 for Omega being non empty set
for G being set
for X being Subset of Omega
for b4 being Subset-Family of Omega holds
( b4 = DynSys (X,G) iff for A being Subset of Omega holds
( A in b4 iff A /\ X in G ) );

definition
let Omega be non empty set ;
let G be Dynkin_System of Omega;
let X be Element of G;
:: original:DynSys
redefine func DynSys (X,G) ->  Dynkin_System of Omega;
coherence
 DynSys (X,G) is Dynkin_System of Omega
proofend;
end;

theorem Th21: :: DYNKIN:21
for Omega being non empty set
for E being Subset-Family of Omega
for X, Y being Subset of Omega st X in E &amp; Y in generated_Dynkin_System E &amp; E is intersection_stable holds
X /\ Y in generated_Dynkin_System E
proofend;

theorem Th22: :: DYNKIN:22
for Omega being non empty set
for E being Subset-Family of Omega
for X, Y being Subset of Omega st X in generated_Dynkin_System E &amp; Y in generated_Dynkin_System E &amp; E is intersection_stable holds
X /\ Y in generated_Dynkin_System E
proofend;

theorem Th23: :: DYNKIN:23
for Omega being non empty set
for E being Subset-Family of Omega st E is intersection_stable holds
generated_Dynkin_System E is intersection_stable
proofend;

:: [WP: ] Dynkin_Lemma
theorem :: DYNKIN:24
for Omega being non empty set
for E being Subset-Family of Omega st E is intersection_stable holds
for D being Dynkin_System of Omega st E c= D holds
sigma E c= D
proofend;