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

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

proof end;

Lm1: for X being non empty set
for a, b, c being Element of X holds (a,b) followed_by c is sequence of 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

proof end;

end;

theorem :: DYNKIN:2

canceled;

::$CT

theorem Th2: :: DYNKIN:3

for a, b being set holds Union ((a,b) followed_by {}) = a \/ b

proof end;

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 b₁ being SetSequence of Omega st
for n being Element of NAT holds b₁ . n = X /\ (f . n)

proof end;

uniqueness
for b₁, b₂ being SetSequence of Omega st ( for n being Element of NAT holds b₁ . n = X /\ (f . n) ) & ( for n being Element of NAT holds b₂ . n = X /\ (f . n) ) holds
b₁ = b₂

proof end;

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 b₄ being SetSequence of Omega holds
( b₄ = seqIntersection (X,f) iff for n being Element of NAT holds b₄ . n = X /\ (f . n) );

:: disjoint-valued functions and intersection ::

definition

let Omega be non empty set ;
let f be SetSequence of Omega;

:: original: disjoint_valued
redefine attr f is disjoint_valued means :: 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 )

proof end;

end;

:: deftheorem 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 Th3: :: 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 )

proof end;

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 b₁ being SetSequence of Omega st
for n being Nat holds b₁ . n = disjointify (g,n)

proof end;

uniqueness
for b₁, b₂ being SetSequence of Omega st ( for n being Nat holds b₁ . n = disjointify (g,n) ) & ( for n being Nat holds b₂ . n = disjointify (g,n) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines disjointify DYNKIN:def 4 :
for Omega being non empty set
for g, b₃ being SetSequence of Omega holds
( b₃ = disjointify g iff for n being Nat holds b₃ . n = disjointify (g,n) );

theorem Th4: :: 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)))

proof end;

theorem Th5: :: DYNKIN:6

for Omega being non empty set
for f being SetSequence of Omega holds disjointify f is V62()

proof end;

theorem Th6: :: DYNKIN:7

for Omega being non empty set
for f being SetSequence of Omega holds union (rng (disjointify f)) = union (rng f)

proof end;

theorem Th7: :: 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 V62()

proof end;

theorem Th8: :: DYNKIN:9

for Omega being non empty set
for f being SetSequence of Omega st f is V62() holds
for X being Subset of Omega holds seqIntersection (X,f) is V62()

proof end;

theorem Th9: :: 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))

proof end;

:: 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 & f is V62() holds
Union f in it ) & ( for X being Subset of Omega st X in it holds
X ` in it ) & {} in it );

existence
ex b₁ being Subset-Family of Omega st
( ( for f being SetSequence of Omega st rng f c= b₁ & f is V62() holds
Union f in b₁ ) & ( for X being Subset of Omega st X in b₁ holds
X ` in b₁ ) & {} in b₁ )

proof end;

end;

:: deftheorem Def5 defines Dynkin_System DYNKIN:def 5 :
for Omega being non empty set
for b₂ being Subset-Family of Omega holds
( b₂ is Dynkin_System of Omega iff ( ( for f being SetSequence of Omega st rng f c= b₂ & f is V62() holds
Union f in b₂ ) & ( for X being Subset of Omega st X in b₂ holds
X ` in b₂ ) & {} in b₂ ) );

registration

let Omega be non empty set ;

cluster -> non empty for Dynkin_System of Omega;

coherence
for b₁ being Dynkin_System of Omega holds not b₁ is empty by Def5;

end;

theorem Th10: :: DYNKIN:11

for Omega being non empty set holds bool Omega is Dynkin_System of Omega

proof end;

theorem Th11: :: DYNKIN:12

for Omega, F 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

proof end;

theorem Th12: :: 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 & D is intersection_stable & A in D & B in D holds
A \ B in D

proof end;

theorem Th13: :: 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 & D is intersection_stable & A in D & B in D holds
A \/ B in D

proof end;

theorem Th14: :: DYNKIN:15

for Omega being non empty set
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
for x being finite set st x c= D holds
union x in D

proof end;

theorem Th15: :: DYNKIN:16

for Omega being non empty set
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
for f being SetSequence of Omega st rng f c= D holds
rng (disjointify f) c= D

proof end;

theorem Th16: :: DYNKIN:17

for Omega being non empty set
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
for f being SetSequence of Omega st rng f c= D holds
union (rng f) in D

proof end;

theorem Th17: :: 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

proof end;

theorem Th18: :: 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

proof end;

:: Main steps for Dynkin's Lemma ::

theorem Th19: :: DYNKIN:20

for Omega being non empty set
for D being non empty Subset-Family of Omega st D is Dynkin_System of Omega & D is intersection_stable holds
D is SigmaField of Omega

proof end;

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 & ( for D being Dynkin_System of Omega st E c= D holds
it c= D ) );

existence
ex b₁ being Dynkin_System of Omega st
( E c= b₁ & ( for D being Dynkin_System of Omega st E c= D holds
b₁ c= D ) )

proof end;

uniqueness
for b₁, b₂ being Dynkin_System of Omega st E c= b₁ & ( for D being Dynkin_System of Omega st E c= D holds
b₁ c= D ) & E c= b₂ & ( for D being Dynkin_System of Omega st E c= D holds
b₂ c= D ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines generated_Dynkin_System DYNKIN:def 6 :
for Omega being non empty set
for E being Subset-Family of Omega
for b₃ being Dynkin_System of Omega holds
( b₃ = generated_Dynkin_System E iff ( E c= b₃ & ( for D being Dynkin_System of Omega st E c= D holds
b₃ 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 b₁ being Subset-Family of Omega st
for A being Subset of Omega holds
( A in b₁ iff A /\ X in G )

proof end;

uniqueness
for b₁, b₂ being Subset-Family of Omega st ( for A being Subset of Omega holds
( A in b₁ iff A /\ X in G ) ) & ( for A being Subset of Omega holds
( A in b₂ iff A /\ X in G ) ) holds
b₁ = b₂

proof end;

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 b₄ being Subset-Family of Omega holds
( b₄ = DynSys (X,G) iff for A being Subset of Omega holds
( A in b₄ 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

proof end;

end;

theorem Th20: :: 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 & Y in generated_Dynkin_System E & E is intersection_stable holds
X /\ Y in generated_Dynkin_System E

proof end;

theorem Th21: :: 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 & Y in generated_Dynkin_System E & E is intersection_stable holds
X /\ Y in generated_Dynkin_System E

proof end;

theorem Th22: :: 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

proof end;

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

proof end;