:: MESFUNC8 semantic presentation

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 natural number holds { x where x is Element of X : for k being natural number 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 Element of 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 Function of NAT ,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 Function of NAT ,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 Function of NAT ,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 Function of NAT ,S st
( G = superior_setsequence F & M . (lim F) = inf (rng (M * G)) )

proof end;

definition

let X, Y be set ;
let F be Functional_Sequence of X,Y;
attr F 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 :

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 natural number holds dom (F . n) = dom (F . m);
correctness

proof end;

end;

:: deftheorem Def2 defines with_the_same_dom MESFUNC8:def 2 :

registration

let X, Y be set ;
cluster with_the_same_dom Functional_Sequence of X,Y;
existence

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

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)

proof end;

definition

let X, Y be set ;
:: original: Functional_Sequence
redefine mode Functional_Sequence of X,Y -> Function of NAT , PFuncs X,Y;
coherence

proof end;

end;

definition

let X, Y be set ;
let f be Functional_Sequence of X,Y;
let n be Element of NAT ;
func f ^\ n -> Functional_Sequence of X,Y equals :: MESFUNC8:def 7
f ^\ n;
correctness

proof end;

end;

:: deftheorem defines ^\ MESFUNC8:def 7 :

registration

let X, Y be set ;
let f be with_the_same_dom Functional_Sequence of X,Y;
let n be Element of NAT ;
cluster f ^\ n -> with_the_same_dom ;
coherence

proof end;

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)

proof end;

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)

proof end;

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)

proof 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 :Def8: :: MESFUNC8:def 8
( 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 Def8 defines lim_inf MESFUNC8:def 8 :

definition

let X be non empty set ;
let f be Functional_Sequence of X, ExtREAL ;
func lim_sup 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_sup (f # x) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines lim_sup MESFUNC8:def 9 :

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)) & (lim_inf f) . x = sup ((inferior_realsequence f) # x) & (lim_inf f) . x = (sup (inferior_realsequence f)) . x ) ) & lim_inf f = sup (inferior_realsequence f) )

proof end;

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)) & (lim_sup f) . x = inf ((superior_realsequence f) # x) & (lim_sup f) . x = (inf (superior_realsequence f)) . x ) ) & lim_sup f = inf (superior_realsequence f) )

proof end;

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 :Def10: :: MESFUNC8:def 10
( 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 Def10 defines lim MESFUNC8:def 10 :

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 number st ( for n being natural number 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))

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