:: Egoroff's Theorem
:: by Noboru Endou , Yasunari Shidama and Keiko Narita
::
:: Received October 30, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users


begin

theorem Th1: :: MESFUNC8:1
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for F being Function of NAT,S
for n being Nat holds  {  x where x is Element of X : for k being Nat st n <= k holds
x in F . k  }  is Element of S
proofend;

theorem Th2: :: MESFUNC8:2
for X being non empty set
for F being SetSequence of X
for n being Element of NAT holds
( (superior_setsequence F) . n = union (rng (F ^\ n)) &amp; (inferior_setsequence F) . n = meet (rng (F ^\ n)) )
proofend;

theorem Th3: :: MESFUNC8:3
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for F being SetSequence of S ex G being Function of NAT,S st
( G = inferior_setsequence F &amp; M . (lim_inf F) = sup (rng (M * G)) )
proofend;

theorem Th4: :: MESFUNC8:4
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for F being SetSequence of S st M . (Union F) < +infty holds
ex G being Function of NAT,S st
( G = superior_setsequence F &amp; M . (lim_sup F) = inf (rng (M * G)) )
proofend;

theorem :: MESFUNC8:5
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for F being SetSequence of S st F is convergent holds
ex G being Function of NAT,S st
( G = inferior_setsequence F &amp; M . (lim F) = sup (rng (M * G)) )
proofend;

theorem :: MESFUNC8:6
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for F being SetSequence of S st F is convergent &amp; M . (Union F) < +infty holds
ex G being Function of NAT,S st
( G = superior_setsequence F &amp; M . (lim F) = inf (rng (M * G)) ) by Th4;

definition
let X, Y be set ;
let F be Functional_Sequence of X,Y;
attrF is with_the_same_dom  means :Def1: :: MESFUNC8:def 1
 rng F is with_common_domain ;
end;

:: deftheorem Def1 defines with_the_same_dom MESFUNC8:def_1_:_
 for X, Y being set
for F being Functional_Sequence of X,Y holds
( F is with_the_same_dom iff rng F is with_common_domain );

definition
let X, Y be set ;
let F be Functional_Sequence of X,Y;
redefine attr F is with_the_same_dom  means :Def2: :: MESFUNC8:def 2
 for n, m being Nat holds dom (F . n) = dom (F . m);
correctness
compatibility
( F is with_the_same_dom iff for n, m being Nat holds dom (F . n) = dom (F . m) );
proofend;
end;

:: deftheorem Def2 defines with_the_same_dom MESFUNC8:def_2_:_
 for X, Y being set
for F being Functional_Sequence of X,Y holds
( F is with_the_same_dom iff for n, m being Nat holds dom (F . n) = dom (F . m) );

registration
let X, Y be set ;
cluster non empty Relation-like NAT -defined PFuncs (X,Y) -valued Function-like total V30( NAT , PFuncs (X,Y)) with_the_same_dom for Element of bool [:NAT,(PFuncs (X,Y)):];
existence
 ex b1 being Functional_Sequence of X,Y st b1 is with_the_same_dom
proofend;
end;

definition
let X be non empty set ;
let f be Functional_Sequence of X,ExtREAL;
func inf f ->  PartFunc of X,ExtREAL means :Def3: :: MESFUNC8:def 3
( dom it = dom (f . 0) &amp; ( for x being Element of X st x in dom it holds
it . x = inf (f # x) ) );
existence
 ex b1 being PartFunc of X,ExtREAL st
( dom b1 = dom (f . 0) &amp; ( for x being Element of X st x in dom b1 holds
b1 . x = inf (f # x) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of X,ExtREAL st dom b1 = dom (f . 0) &amp; ( for x being Element of X st x in dom b1 holds
b1 . x = inf (f # x) ) &amp; dom b2 = dom (f . 0) &amp; ( for x being Element of X st x in dom b2 holds
b2 . x = inf (f # x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines inf MESFUNC8:def_3_:_
 for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for b3 being PartFunc of X,ExtREAL holds
( b3 = inf f iff ( dom b3 = dom (f . 0) &amp; ( for x being Element of X st x in dom b3 holds
b3 . x = inf (f # x) ) ) );

definition
let X be non empty set ;
let f be Functional_Sequence of X,ExtREAL;
func sup f ->  PartFunc of X,ExtREAL means :Def4: :: MESFUNC8:def 4
( dom it = dom (f . 0) &amp; ( for x being Element of X st x in dom it holds
it . x = sup (f # x) ) );
existence
 ex b1 being PartFunc of X,ExtREAL st
( dom b1 = dom (f . 0) &amp; ( for x being Element of X st x in dom b1 holds
b1 . x = sup (f # x) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of X,ExtREAL st dom b1 = dom (f . 0) &amp; ( for x being Element of X st x in dom b1 holds
b1 . x = sup (f # x) ) &amp; dom b2 = dom (f . 0) &amp; ( for x being Element of X st x in dom b2 holds
b2 . x = sup (f # x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines sup MESFUNC8:def_4_:_
 for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for b3 being PartFunc of X,ExtREAL holds
( b3 = sup f iff ( dom b3 = dom (f . 0) &amp; ( for x being Element of X st x in dom b3 holds
b3 . x = sup (f # x) ) ) );

definition
let X be non empty set ;
let f be Functional_Sequence of X,ExtREAL;
func inferior_realsequence f ->  with_the_same_dom Functional_Sequence of X,ExtREAL means :Def5: :: MESFUNC8:def 5
 for n being Nat holds
( dom (it . n) = dom (f . 0) &amp; ( for x being Element of X st x in dom (it . n) holds
(it . n) . x = (inferior_realsequence (f # x)) . n ) );
existence
 ex b1 being with_the_same_dom Functional_Sequence of X,ExtREAL st
for n being Nat holds
( dom (b1 . n) = dom (f . 0) &amp; ( for x being Element of X st x in dom (b1 . n) holds
(b1 . n) . x = (inferior_realsequence (f # x)) . n ) )
proofend;
uniqueness
 for b1, b2 being with_the_same_dom Functional_Sequence of X,ExtREAL st ( for n being Nat holds
( dom (b1 . n) = dom (f . 0) &amp; ( for x being Element of X st x in dom (b1 . n) holds
(b1 . n) . x = (inferior_realsequence (f # x)) . n ) ) ) &amp; ( for n being Nat holds
( dom (b2 . n) = dom (f . 0) &amp; ( for x being Element of X st x in dom (b2 . n) holds
(b2 . n) . x = (inferior_realsequence (f # x)) . n ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines inferior_realsequence MESFUNC8:def_5_:_
 for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for b3 being with_the_same_dom Functional_Sequence of X,ExtREAL holds
( b3 = inferior_realsequence f iff for n being Nat holds
( dom (b3 . n) = dom (f . 0) &amp; ( for x being Element of X st x in dom (b3 . n) holds
(b3 . n) . x = (inferior_realsequence (f # x)) . n ) ) );

definition
let X be non empty set ;
let f be Functional_Sequence of X,ExtREAL;
func superior_realsequence f ->  with_the_same_dom Functional_Sequence of X,ExtREAL means :Def6: :: MESFUNC8:def 6
 for n being Nat holds
( dom (it . n) = dom (f . 0) &amp; ( for x being Element of X st x in dom (it . n) holds
(it . n) . x = (superior_realsequence (f # x)) . n ) );
existence
 ex b1 being with_the_same_dom Functional_Sequence of X,ExtREAL st
for n being Nat holds
( dom (b1 . n) = dom (f . 0) &amp; ( for x being Element of X st x in dom (b1 . n) holds
(b1 . n) . x = (superior_realsequence (f # x)) . n ) )
proofend;
uniqueness
 for b1, b2 being with_the_same_dom Functional_Sequence of X,ExtREAL st ( for n being Nat holds
( dom (b1 . n) = dom (f . 0) &amp; ( for x being Element of X st x in dom (b1 . n) holds
(b1 . n) . x = (superior_realsequence (f # x)) . n ) ) ) &amp; ( for n being Nat holds
( dom (b2 . n) = dom (f . 0) &amp; ( for x being Element of X st x in dom (b2 . n) holds
(b2 . n) . x = (superior_realsequence (f # x)) . n ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines superior_realsequence MESFUNC8:def_6_:_
 for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for b3 being with_the_same_dom Functional_Sequence of X,ExtREAL holds
( b3 = superior_realsequence f iff for n being Nat holds
( dom (b3 . n) = dom (f . 0) &amp; ( for x being Element of X st x in dom (b3 . n) holds
(b3 . n) . x = (superior_realsequence (f # x)) . n ) ) );

theorem Th7: :: MESFUNC8:7
for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for x being Element of X st x in dom (f . 0) holds
(inferior_realsequence f) # x = inferior_realsequence (f # x)
proofend;

registration
let X, Y be set ;
let f be with_the_same_dom Functional_Sequence of X,Y;
let n be Element of NAT ;
clusterf ^\ n ->  with_the_same_dom for Functional_Sequence of X,Y;
coherence
 for b1 being Functional_Sequence of X,Y st b1 = f ^\ n holds
b1 is with_the_same_dom
proofend;
end;

theorem Th8: :: MESFUNC8:8
for X being non empty set
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for n being Element of NAT holds (inferior_realsequence f) . n = inf (f ^\ n)
proofend;

theorem Th9: :: MESFUNC8:9
for X being non empty set
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for n being Element of NAT holds (superior_realsequence f) . n = sup (f ^\ n)
proofend;

theorem Th10: :: MESFUNC8:10
for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for x being Element of X st x in dom (f . 0) holds
(superior_realsequence f) # x = superior_realsequence (f # x)
proofend;

definition
let X be non empty set ;
let f be Functional_Sequence of X,ExtREAL;
func lim_inf f ->  PartFunc of X,ExtREAL means :Def7: :: MESFUNC8:def 7
( dom it = dom (f . 0) &amp; ( for x being Element of X st x in dom it holds
it . x = lim_inf (f # x) ) );
existence
 ex b1 being PartFunc of X,ExtREAL st
( dom b1 = dom (f . 0) &amp; ( for x being Element of X st x in dom b1 holds
b1 . x = lim_inf (f # x) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of X,ExtREAL st dom b1 = dom (f . 0) &amp; ( for x being Element of X st x in dom b1 holds
b1 . x = lim_inf (f # x) ) &amp; dom b2 = dom (f . 0) &amp; ( for x being Element of X st x in dom b2 holds
b2 . x = lim_inf (f # x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines lim_inf MESFUNC8:def_7_:_
 for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for b3 being PartFunc of X,ExtREAL holds
( b3 = lim_inf f iff ( dom b3 = dom (f . 0) &amp; ( for x being Element of X st x in dom b3 holds
b3 . x = lim_inf (f # x) ) ) );

definition
let X be non empty set ;
let f be Functional_Sequence of X,ExtREAL;
func lim_sup f ->  PartFunc of X,ExtREAL means :Def8: :: MESFUNC8:def 8
( dom it = dom (f . 0) &amp; ( for x being Element of X st x in dom it holds
it . x = lim_sup (f # x) ) );
existence
 ex b1 being PartFunc of X,ExtREAL st
( dom b1 = dom (f . 0) &amp; ( for x being Element of X st x in dom b1 holds
b1 . x = lim_sup (f # x) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of X,ExtREAL st dom b1 = dom (f . 0) &amp; ( for x being Element of X st x in dom b1 holds
b1 . x = lim_sup (f # x) ) &amp; dom b2 = dom (f . 0) &amp; ( for x being Element of X st x in dom b2 holds
b2 . x = lim_sup (f # x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines lim_sup MESFUNC8:def_8_:_
 for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for b3 being PartFunc of X,ExtREAL holds
( b3 = lim_sup f iff ( dom b3 = dom (f . 0) &amp; ( for x being Element of X st x in dom b3 holds
b3 . x = lim_sup (f # x) ) ) );

theorem Th11: :: MESFUNC8:11
for X being non empty set
for f being Functional_Sequence of X,ExtREAL holds
( ( for x being Element of X st x in dom (lim_inf f) holds
( (lim_inf f) . x = sup (inferior_realsequence (f # x)) &amp; (lim_inf f) . x = sup ((inferior_realsequence f) # x) &amp; (lim_inf f) . x = (sup (inferior_realsequence f)) . x ) ) &amp; lim_inf f = sup (inferior_realsequence f) )
proofend;

theorem Th12: :: MESFUNC8:12
for X being non empty set
for f being Functional_Sequence of X,ExtREAL holds
( ( for x being Element of X st x in dom (lim_sup f) holds
( (lim_sup f) . x = inf (superior_realsequence (f # x)) &amp; (lim_sup f) . x = inf ((superior_realsequence f) # x) &amp; (lim_sup f) . x = (inf (superior_realsequence f)) . x ) ) &amp; lim_sup f = inf (superior_realsequence f) )
proofend;

theorem :: MESFUNC8:13
for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for x being Element of X st x in dom (f . 0) holds
( f # x is convergent iff (lim_sup f) . x = (lim_inf f) . x )
proofend;

definition
let X be non empty set ;
let f be Functional_Sequence of X,ExtREAL;
func lim f ->  PartFunc of X,ExtREAL means :Def9: :: MESFUNC8:def 9
( dom it = dom (f . 0) &amp; ( for x being Element of X st x in dom it holds
it . x = lim (f # x) ) );
existence
 ex b1 being PartFunc of X,ExtREAL st
( dom b1 = dom (f . 0) &amp; ( for x being Element of X st x in dom b1 holds
b1 . x = lim (f # x) ) )
proofend;
uniqueness
 for b1, b2 being PartFunc of X,ExtREAL st dom b1 = dom (f . 0) &amp; ( for x being Element of X st x in dom b1 holds
b1 . x = lim (f # x) ) &amp; dom b2 = dom (f . 0) &amp; ( for x being Element of X st x in dom b2 holds
b2 . x = lim (f # x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines lim MESFUNC8:def_9_:_
 for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for b3 being PartFunc of X,ExtREAL holds
( b3 = lim f iff ( dom b3 = dom (f . 0) &amp; ( for x being Element of X st x in dom b3 holds
b3 . x = lim (f # x) ) ) );

theorem Th14: :: MESFUNC8:14
for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for x being Element of X st x in dom (lim f) &amp; f # x is convergent holds
( (lim f) . x = (lim_sup f) . x &amp; (lim f) . x = (lim_inf f) . x )
proofend;

theorem Th15: :: MESFUNC8:15
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),(R_EAL r)))
proofend;

theorem Th16: :: MESFUNC8:16
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) holds
meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),(R_EAL r)))
proofend;

theorem Th17: :: MESFUNC8:17
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),(R_EAL r))) ) holds
for n being Nat holds (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),(R_EAL r)))
proofend;

theorem Th18: :: MESFUNC8:18
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),(R_EAL r))) ) holds
for n being Nat holds (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),(R_EAL r)))
proofend;

theorem Th19: :: MESFUNC8:19
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for E being Element of S st dom (f . 0) = E &amp; ( for n being Nat holds f . n is_measurable_on E ) holds
for n being Nat holds (superior_realsequence f) . n is_measurable_on E
proofend;

theorem Th20: :: MESFUNC8:20
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for E being Element of S st dom (f . 0) = E &amp; ( for n being Nat holds f . n is_measurable_on E ) holds
for n being Nat holds (inferior_realsequence f) . n is_measurable_on E
proofend;

theorem Th21: :: MESFUNC8:21
for X being non empty set
for S being SigmaField of X
for f being Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom (((superior_realsequence f) . n),(R_EAL r))) ) holds
meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),(R_EAL r)))
proofend;

theorem Th22: :: MESFUNC8:22
for X being non empty set
for S being SigmaField of X
for f being Functional_Sequence of X,ExtREAL
for F being SetSequence of S
for r being real number st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom (((inferior_realsequence f) . n),(R_EAL r))) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((lim_inf f),(R_EAL r)))
proofend;

theorem Th23: :: MESFUNC8:23
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for E being Element of S st dom (f . 0) = E &amp; ( for n being Nat holds f . n is_measurable_on E ) holds
lim_sup f is_measurable_on E
proofend;

theorem :: MESFUNC8:24
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for E being Element of S st dom (f . 0) = E &amp; ( for n being Nat holds f . n is_measurable_on E ) holds
lim_inf f is_measurable_on E
proofend;

theorem Th25: :: MESFUNC8:25
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for E being Element of S st dom (f . 0) = E &amp; ( for n being Nat holds f . n is_measurable_on E ) &amp; ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is_measurable_on E
proofend;

theorem Th26: :: MESFUNC8:26
for X being non empty set
for S being SigmaField of X
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for g being PartFunc of X,ExtREAL
for E being Element of S st dom (f . 0) = E &amp; ( for n being Nat holds f . n is_measurable_on E ) &amp; dom g = E &amp; ( for x being Element of X st x in E holds
( f # x is convergent &amp; g . x = lim (f # x) ) ) holds
g is_measurable_on E
proofend;

theorem Th27: :: MESFUNC8:27
for X being non empty set
for f being Functional_Sequence of X,ExtREAL
for g being PartFunc of X,ExtREAL st ( for x being Element of X st x in dom g holds
( f # x is convergent_to_finite_number &amp; g . x = lim (f # x) ) ) holds
g is real-valued
proofend;

begin

theorem Th28: :: MESFUNC8:28
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for g being PartFunc of X,ExtREAL
for E being Element of S st M . E < +infty &amp; dom (f . 0) = E &amp; ( for n being Nat holds
( f . n is_measurable_on E &amp; f . n is real-valued ) ) &amp; dom g = E &amp; ( for x being Element of X st x in E holds
( f # x is convergent_to_finite_number &amp; g . x = lim (f # x) ) ) holds
for r, e being real number st 0 < r &amp; 0 < e holds
ex H being Element of S ex N being Nat st
( H c= E &amp; M . H < r &amp; ( for k being Nat st N < k holds
for x being Element of X st x in E \ H holds
|.(((f . k) . x) - (g . x)).| < e ) )
proofend;

theorem :: MESFUNC8:29
for X, Y being non empty set
for E being set
for F, G being Function of X,Y st ( for x being Element of X holds G . x = E \ (F . x) ) holds
union (rng G) = E \ (meet (rng F))
proofend;

:: [WP: ] Egorov's_theorem
theorem :: MESFUNC8:30
for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being with_the_same_dom Functional_Sequence of X,ExtREAL
for g being PartFunc of X,ExtREAL
for E being Element of S st dom (f . 0) = E &amp; ( for n being Nat holds f . n is_measurable_on E ) &amp; M . E < +infty &amp; ( for n being Nat ex L being Element of S st
( L c= E &amp; M . (E \ L) = 0 &amp; ( for x being Element of X st x in L holds
|.((f . n) . x).| < +infty ) ) ) &amp; ex G being Element of S st
( G c= E &amp; M . (E \ G) = 0 &amp; ( for x being Element of X st x in E holds
f # x is convergent_to_finite_number ) &amp; dom g = E &amp; ( for x being Element of X st x in G holds
g . x = lim (f # x) ) ) holds
for e being real number st 0 < e holds
ex F being Element of S st
( F c= E &amp; M . (E \ F) <= e &amp; ( for p being real number st 0 < p holds
ex N being Nat st
for n being Nat st N < n holds
for x being Element of X st x in F holds
|.(((f . n) . x) - (g . x)).| < p ) )
proofend;