:: 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
)
proof
end;
theorem
Th2
:
:: DYNKIN:2
for
n
being
Element
of
NAT
holds
n
is
finite
proof
end;
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
proof
end;
end;
theorem
Th3
:
:: 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
1
being
SetSequence
of
Omega
st
for
n
being
Element
of
NAT
holds
b
1
.
n
=
X
/\
(
f
.
n
)
proof
end;
uniqueness
for
b
1
,
b
2
being
SetSequence
of
Omega
st ( for
n
being
Element
of
NAT
holds
b
1
.
n
=
X
/\
(
f
.
n
)
) & ( for
n
being
Element
of
NAT
holds
b
2
.
n
=
X
/\
(
f
.
n
)
) holds
b
1
=
b
2
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
4
being
SetSequence
of
Omega
holds
(
b
4
=
seqIntersection
(
X
,
f
) iff for
n
being
Element
of
NAT
holds
b
4
.
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
attr
f
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
)
proof
end;
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
)
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
1
being
SetSequence
of
Omega
st
for
n
being
Nat
holds
b
1
.
n
=
disjointify
(
g
,
n
)
proof
end;
uniqueness
for
b
1
,
b
2
being
SetSequence
of
Omega
st ( for
n
being
Nat
holds
b
1
.
n
=
disjointify
(
g
,
n
) ) & ( for
n
being
Nat
holds
b
2
.
n
=
disjointify
(
g
,
n
) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def4
defines
disjointify
DYNKIN:def 4 :
for
Omega
being non
empty
set
for
g
,
b
3
being
SetSequence
of
Omega
holds
(
b
3
=
disjointify
g
iff for
n
being
Nat
holds
b
3
.
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
)
)
)
proof
end;
theorem
Th6
:
:: DYNKIN:6
for
Omega
being non
empty
set
for
f
being
SetSequence
of
Omega
holds
disjointify
f
is
V56
()
proof
end;
theorem
Th7
:
:: 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
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
()
proof
end;
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
()
proof
end;
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
)
)
proof
end;
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
&
f
is
V56
() holds
Union
f
in
it
) & ( for
X
being
Subset
of
Omega
st
X
in
it
holds
X
`
in
it
) &
{}
in
it
);
existence
ex
b
1
being
Subset-Family
of
Omega
st
( ( for
f
being
SetSequence
of
Omega
st
rng
f
c=
b
1
&
f
is
V56
() holds
Union
f
in
b
1
) & ( for
X
being
Subset
of
Omega
st
X
in
b
1
holds
X
`
in
b
1
) &
{}
in
b
1
)
proof
end;
end;
::
deftheorem
Def5
defines
Dynkin_System
DYNKIN:def 5 :
for
Omega
being non
empty
set
for
b
2
being
Subset-Family
of
Omega
holds
(
b
2
is
Dynkin_System
of
Omega
iff ( ( for
f
being
SetSequence
of
Omega
st
rng
f
c=
b
2
&
f
is
V56
() holds
Union
f
in
b
2
) & ( for
X
being
Subset
of
Omega
st
X
in
b
2
holds
X
`
in
b
2
) &
{}
in
b
2
) );
registration
let
Omega
be non
empty
set
;
cluster
->
non
empty
for
Dynkin_System
of
Omega
;
coherence
for
b
1
being
Dynkin_System
of
Omega
holds not
b
1
is
empty
by
Def5
;
end;
theorem
Th11
:
:: DYNKIN:11
for
Omega
being non
empty
set
holds
bool
Omega
is
Dynkin_System
of
Omega
proof
end;
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
proof
end;
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
&
D
is
intersection_stable
&
A
in
D
&
B
in
D
holds
A
\
B
in
D
proof
end;
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
&
D
is
intersection_stable
&
A
in
D
&
B
in
D
holds
A
\/
B
in
D
proof
end;
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
&
D
is
intersection_stable
holds
for
x
being
finite
set
st
x
c=
D
holds
union
x
in
D
proof
end;
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
&
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
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
&
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
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
proof
end;
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
proof
end;
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
&
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
1
being
Dynkin_System
of
Omega
st
(
E
c=
b
1
& ( for
D
being
Dynkin_System
of
Omega
st
E
c=
D
holds
b
1
c=
D
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Dynkin_System
of
Omega
st
E
c=
b
1
& ( for
D
being
Dynkin_System
of
Omega
st
E
c=
D
holds
b
1
c=
D
) &
E
c=
b
2
& ( for
D
being
Dynkin_System
of
Omega
st
E
c=
D
holds
b
2
c=
D
) holds
b
1
=
b
2
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
3
being
Dynkin_System
of
Omega
holds
(
b
3
=
generated_Dynkin_System
E
iff (
E
c=
b
3
& ( for
D
being
Dynkin_System
of
Omega
st
E
c=
D
holds
b
3
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
1
being
Subset-Family
of
Omega
st
for
A
being
Subset
of
Omega
holds
(
A
in
b
1
iff
A
/\
X
in
G
)
proof
end;
uniqueness
for
b
1
,
b
2
being
Subset-Family
of
Omega
st ( for
A
being
Subset
of
Omega
holds
(
A
in
b
1
iff
A
/\
X
in
G
) ) & ( for
A
being
Subset
of
Omega
holds
(
A
in
b
2
iff
A
/\
X
in
G
) ) holds
b
1
=
b
2
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
4
being
Subset-Family
of
Omega
holds
(
b
4
=
DynSys
(
X
,
G
) iff for
A
being
Subset
of
Omega
holds
(
A
in
b
4
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
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
&
Y
in
generated_Dynkin_System
E
&
E
is
intersection_stable
holds
X
/\
Y
in
generated_Dynkin_System
E
proof
end;
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
&
Y
in
generated_Dynkin_System
E
&
E
is
intersection_stable
holds
X
/\
Y
in
generated_Dynkin_System
E
proof
end;
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
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;