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

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;

registration
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

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

definition

let Omega be non empty set ;

let f be SetSequence of Omega;

let X be Subset of Omega;

ex b_{1} being SetSequence of Omega st

for n being Element of NAT holds b_{1} . n = X /\ (f . n)

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}

end;
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 for n being Element of NAT holds it . n = X /\ (f . n);

ex b

for n being Element of NAT holds b

proof end;

uniqueness for b

b

proof 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) );

for Omega being non empty set

for f being SetSequence of Omega

for X being Subset of Omega

for b

( b

begin

:: disjoint-valued functions and intersection ::

definition

let Omega be non empty set ;

let f be SetSequence of Omega;

( f is disjoint_valued iff for n, m being Element of NAT st n < m holds

f . n misses f . m )

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

( f is disjoint_valued iff for n, m being Element of NAT st n < m holds

f . n misses f . m )

proof 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 );

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 )

for x being set holds

( x c= meet Y iff for y being Element of Y holds x c= y )

proof end;

definition

let Omega be non empty set ;

let f be SetSequence of Omega;

let n be Nat;

coherence

(f . n) \ (union (rng (f | n))) is Subset of Omega ;

end;
let f be SetSequence of Omega;

let n be Nat;

coherence

(f . n) \ (union (rng (f | n))) is Subset of Omega ;

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

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;

ex b_{1} being SetSequence of Omega st

for n being Nat holds b_{1} . n = disjointify (g,n)

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}

end;
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 for n being Nat holds it . n = disjointify (g,n);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof 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) );

for Omega being non empty set

for g, b

( b

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

for f being SetSequence of Omega

for n being Nat holds (disjointify f) . n = (f . n) \ (union (rng (f | n)))

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)

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

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

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

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 ;

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

end;
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 ( ( 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 );

ex b

( ( for f being SetSequence of Omega st rng f c= b

Union f in b

X ` in b

proof 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} ) );

for Omega being non empty set

for b

( b

Union f in b

X ` in b

registration

let Omega be non empty set ;

coherence

for b_{1} being Dynkin_System of Omega holds not b_{1} is empty
by Def5;

end;
coherence

for b

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

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

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

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

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

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

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

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

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

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;

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

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}

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

it c= D ) );

ex b

( E c= b

b

proof end;

uniqueness for b

b

b

b

proof 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 ) ) );

for Omega being non empty set

for E being Subset-Family of Omega

for b

( b

b

definition

let Omega be non empty set ;

let G be set ;

let X be Subset of Omega;

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 )

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}

end;
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 for A being Subset of Omega holds

( A in it iff A /\ X in G );

ex b

for A being Subset of Omega holds

( A in b

proof end;

uniqueness for b

( A in b

( A in b

b

proof 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 ) );

for Omega being non empty set

for G being set

for X being Subset of Omega

for b

( b

( A in b

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

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

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

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

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

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

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;