MESFUNC8: Egoroff's Theorem

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 sequence of 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

proof end;

theorem Th2: :: MESFUNC8:2

for X being non empty set
for F being SetSequence of X
for n being Nat holds
( (superior_setsequence F) . n = union (rng (F ^\ n)) & (inferior_setsequence F) . n = meet (rng (F ^\ n)) )

proof end;

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 sequence of S st
( G = inferior_setsequence F & M . (lim_inf F) = sup (rng (M * G)) )

proof end;

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 sequence of S st
( G = superior_setsequence F & M . (lim_sup F) = inf (rng (M * G)) )

proof end;

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 sequence of S st
( G = inferior_setsequence F & M . (lim F) = sup (rng (M * G)) )

proof end;

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 & M . (Union F) < +infty holds
ex G being sequence of S st
( G = superior_setsequence F & M . (lim F) = inf (rng (M * G)) ) by Th4;

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

proof end;

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) & ( for x being Element of X st x in dom it holds
it . x = inf (f # x) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines inf MESFUNC8:def 3 :

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) & ( for x being Element of X st x in dom it holds
it . x = sup (f # x) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines sup MESFUNC8:def 4 :

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) & ( for x being Element of X st x in dom (it . n) holds
(it . n) . x = (inferior_realsequence (f # x)) . n ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines inferior_realsequence MESFUNC8:def 5 :

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) & ( for x being Element of X st x in dom (it . n) holds
(it . n) . x = (superior_realsequence (f # x)) . n ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines superior_realsequence MESFUNC8:def 6 :

registration

let X, Y be set ;
let f be with_the_same_dom Functional_Sequence of X,Y;
let n be Nat;

cluster f ^\ n -> with_the_same_dom for Functional_Sequence of X,Y;

coherence

proof end;

end;

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) & ( for x being Element of X st x in dom it holds
it . x = lim_inf (f # x) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines lim_inf MESFUNC8:def 7 :

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) & ( for x being Element of X st x in dom it holds
it . x = lim_sup (f # x) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines lim_sup MESFUNC8:def 8 :

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 )

proof end;

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) & ( for x being Element of X st x in dom it holds
it . x = lim (f # x) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines lim MESFUNC8:def 9 :

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) & f # x is convergent holds
( (lim f) . x = (lim_sup f) . x & (lim f) . x = (lim_inf f) . x )

proof end;

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 st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r))

proof end;

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 st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds
meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))

proof end;

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 st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom ((f . n),r)) ) holds
for n being Nat holds (superior_setsequence F) . n = (dom (f . 0)) /\ (great_dom (((superior_realsequence f) . n),r))

proof end;

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 st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom ((f . n),r)) ) holds
for n being Nat holds (inferior_setsequence F) . n = (dom (f . 0)) /\ (great_eq_dom (((inferior_realsequence f) . n),r))

proof end;

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 & ( for n being Nat holds f . n is E -measurable ) holds
for n being Nat holds (superior_realsequence f) . n is E -measurable

proof end;

theorem Th20: :: MESFUNC8:20

proof end;

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 st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_eq_dom (((superior_realsequence f) . n),r)) ) holds
meet F = (dom (f . 0)) /\ (great_eq_dom ((lim_sup f),r))

proof end;

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 st ( for n being Nat holds F . n = (dom (f . 0)) /\ (great_dom (((inferior_realsequence f) . n),r)) ) holds
union (rng F) = (dom (f . 0)) /\ (great_dom ((lim_inf f),r))

proof end;

theorem Th23: :: MESFUNC8:23

proof end;

theorem :: MESFUNC8:24

proof end;

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 & ( for n being Nat holds f . n is E -measurable ) & ( for x being Element of X st x in E holds
f # x is convergent ) holds
lim f is E -measurable

proof end;

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 & ( for n being Nat holds f . n is E -measurable ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent & g . x = lim (f # x) ) ) holds
g is E -measurable

proof end;

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 & g . x = lim (f # x) ) ) holds
g is real-valued

proof end;

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 & dom (f . 0) = E & ( for n being Nat holds
( f . n is E -measurable & f . n is real-valued ) ) & dom g = E & ( for x being Element of X st x in E holds
( f # x is convergent_to_finite_number & g . x = lim (f # x) ) ) holds
for r, e being Real st 0 < r & 0 < e holds
ex H being Element of S ex N being Nat st
( H c= E & M . H < r & ( 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 ) )

proof end;

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 & ( for n being Nat holds f . n is E -measurable ) & M . E < +infty & ( for n being Nat ex L being Element of S st
( L c= E & M . (E \ L) = 0 & ( for x being Element of X st x in L holds
|.((f . n) . x).| < +infty ) ) ) & ex G being Element of S st
( G c= E & M . (E \ G) = 0 & ( for x being Element of X st x in E holds
f # x is convergent_to_finite_number ) & dom g = E & ( for x being Element of X st x in G holds
g . x = lim (f # x) ) ) holds
for e being Real st 0 < e holds
ex F being Element of S st
( F c= E & M . (E \ F) <= e & ( for p being Real 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 ) )

proof end;