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

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

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

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

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

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

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)) ) by Th4;

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)) ) by Th4;

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

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;

compatibility

( F is with_the_same_dom iff for n, m being Nat holds dom (F . n) = dom (F . m) );

end;
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 for n, m being Nat holds dom (F . n) = dom (F . m);

compatibility

( F is with_the_same_dom iff for n, m being Nat holds dom (F . n) = dom (F . m) );

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

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 ;

ex b_{1} being Functional_Sequence of X,Y st b_{1} is with_the_same_dom

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

proof end;

definition

let X be non empty set ;

let f be Functional_Sequence of X,ExtREAL;

ex b_{1} being PartFunc of X,ExtREAL st

( dom b_{1} = dom (f . 0) & ( for x being Element of X st x in dom b_{1} holds

b_{1} . x = inf (f # x) ) )

for b_{1}, b_{2} being PartFunc of X,ExtREAL st dom b_{1} = dom (f . 0) & ( for x being Element of X st x in dom b_{1} holds

b_{1} . x = inf (f # x) ) & dom b_{2} = dom (f . 0) & ( for x being Element of X st x in dom b_{2} holds

b_{2} . x = inf (f # x) ) holds

b_{1} = b_{2}

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

it . x = inf (f # x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines inf MESFUNC8:def 3 :

for X being non empty set

for f being Functional_Sequence of X,ExtREAL

for b_{3} being PartFunc of X,ExtREAL holds

( b_{3} = inf f iff ( dom b_{3} = dom (f . 0) & ( for x being Element of X st x in dom b_{3} holds

b_{3} . x = inf (f # x) ) ) );

for X being non empty set

for f being Functional_Sequence of X,ExtREAL

for b

( b

b

definition

let X be non empty set ;

let f be Functional_Sequence of X,ExtREAL;

ex b_{1} being PartFunc of X,ExtREAL st

( dom b_{1} = dom (f . 0) & ( for x being Element of X st x in dom b_{1} holds

b_{1} . x = sup (f # x) ) )

for b_{1}, b_{2} being PartFunc of X,ExtREAL st dom b_{1} = dom (f . 0) & ( for x being Element of X st x in dom b_{1} holds

b_{1} . x = sup (f # x) ) & dom b_{2} = dom (f . 0) & ( for x being Element of X st x in dom b_{2} holds

b_{2} . x = sup (f # x) ) holds

b_{1} = b_{2}

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

it . x = sup (f # x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines sup MESFUNC8:def 4 :

for X being non empty set

for f being Functional_Sequence of X,ExtREAL

for b_{3} being PartFunc of X,ExtREAL holds

( b_{3} = sup f iff ( dom b_{3} = dom (f . 0) & ( for x being Element of X st x in dom b_{3} holds

b_{3} . x = sup (f # x) ) ) );

for X being non empty set

for f being Functional_Sequence of X,ExtREAL

for b

( b

b

definition

let X be non empty set ;

let f be Functional_Sequence of X,ExtREAL;

ex b_{1} being with_the_same_dom Functional_Sequence of X,ExtREAL st

for n being Nat holds

( dom (b_{1} . n) = dom (f . 0) & ( for x being Element of X st x in dom (b_{1} . n) holds

(b_{1} . n) . x = (inferior_realsequence (f # x)) . n ) )

for b_{1}, b_{2} being with_the_same_dom Functional_Sequence of X,ExtREAL st ( for n being Nat holds

( dom (b_{1} . n) = dom (f . 0) & ( for x being Element of X st x in dom (b_{1} . n) holds

(b_{1} . n) . x = (inferior_realsequence (f # x)) . n ) ) ) & ( for n being Nat holds

( dom (b_{2} . n) = dom (f . 0) & ( for x being Element of X st x in dom (b_{2} . n) holds

(b_{2} . n) . x = (inferior_realsequence (f # x)) . n ) ) ) holds

b_{1} = b_{2}

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

ex b

for n being Nat holds

( dom (b

(b

proof end;

uniqueness for b

( dom (b

(b

( dom (b

(b

b

proof end;

:: deftheorem Def5 defines inferior_realsequence MESFUNC8:def 5 :

for X being non empty set

for f being Functional_Sequence of X,ExtREAL

for b_{3} being with_the_same_dom Functional_Sequence of X,ExtREAL holds

( b_{3} = inferior_realsequence f iff for n being Nat holds

( dom (b_{3} . n) = dom (f . 0) & ( for x being Element of X st x in dom (b_{3} . n) holds

(b_{3} . n) . x = (inferior_realsequence (f # x)) . n ) ) );

for X being non empty set

for f being Functional_Sequence of X,ExtREAL

for b

( b

( dom (b

(b

definition

let X be non empty set ;

let f be Functional_Sequence of X,ExtREAL;

ex b_{1} being with_the_same_dom Functional_Sequence of X,ExtREAL st

for n being Nat holds

( dom (b_{1} . n) = dom (f . 0) & ( for x being Element of X st x in dom (b_{1} . n) holds

(b_{1} . n) . x = (superior_realsequence (f # x)) . n ) )

for b_{1}, b_{2} being with_the_same_dom Functional_Sequence of X,ExtREAL st ( for n being Nat holds

( dom (b_{1} . n) = dom (f . 0) & ( for x being Element of X st x in dom (b_{1} . n) holds

(b_{1} . n) . x = (superior_realsequence (f # x)) . n ) ) ) & ( for n being Nat holds

( dom (b_{2} . n) = dom (f . 0) & ( for x being Element of X st x in dom (b_{2} . n) holds

(b_{2} . n) . x = (superior_realsequence (f # x)) . n ) ) ) holds

b_{1} = b_{2}

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

ex b

for n being Nat holds

( dom (b

(b

proof end;

uniqueness for b

( dom (b

(b

( dom (b

(b

b

proof end;

:: deftheorem Def6 defines superior_realsequence MESFUNC8:def 6 :

for X being non empty set

for f being Functional_Sequence of X,ExtREAL

for b_{3} being with_the_same_dom Functional_Sequence of X,ExtREAL holds

( b_{3} = superior_realsequence f iff for n being Nat holds

( dom (b_{3} . n) = dom (f . 0) & ( for x being Element of X st x in dom (b_{3} . n) holds

(b_{3} . n) . x = (superior_realsequence (f # x)) . n ) ) );

for X being non empty set

for f being Functional_Sequence of X,ExtREAL

for b

( b

( dom (b

(b

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)

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;

registration

let X, Y be set ;

let f be with_the_same_dom Functional_Sequence of X,Y;

let n be Element of NAT ;

coherence

for b_{1} being Functional_Sequence of X,Y st b_{1} = f ^\ n holds

b_{1} is with_the_same_dom

end;
let f be with_the_same_dom Functional_Sequence of X,Y;

let n be Element of NAT ;

coherence

for b

b

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

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)

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)

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;

ex b_{1} being PartFunc of X,ExtREAL st

( dom b_{1} = dom (f . 0) & ( for x being Element of X st x in dom b_{1} holds

b_{1} . x = lim_inf (f # x) ) )

for b_{1}, b_{2} being PartFunc of X,ExtREAL st dom b_{1} = dom (f . 0) & ( for x being Element of X st x in dom b_{1} holds

b_{1} . x = lim_inf (f # x) ) & dom b_{2} = dom (f . 0) & ( for x being Element of X st x in dom b_{2} holds

b_{2} . x = lim_inf (f # x) ) holds

b_{1} = b_{2}

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

it . x = lim_inf (f # x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def7 defines lim_inf MESFUNC8:def 7 :

for X being non empty set

for f being Functional_Sequence of X,ExtREAL

for b_{3} being PartFunc of X,ExtREAL holds

( b_{3} = lim_inf f iff ( dom b_{3} = dom (f . 0) & ( for x being Element of X st x in dom b_{3} holds

b_{3} . x = lim_inf (f # x) ) ) );

for X being non empty set

for f being Functional_Sequence of X,ExtREAL

for b

( b

b

definition

let X be non empty set ;

let f be Functional_Sequence of X,ExtREAL;

ex b_{1} being PartFunc of X,ExtREAL st

( dom b_{1} = dom (f . 0) & ( for x being Element of X st x in dom b_{1} holds

b_{1} . x = lim_sup (f # x) ) )

for b_{1}, b_{2} being PartFunc of X,ExtREAL st dom b_{1} = dom (f . 0) & ( for x being Element of X st x in dom b_{1} holds

b_{1} . x = lim_sup (f # x) ) & dom b_{2} = dom (f . 0) & ( for x being Element of X st x in dom b_{2} holds

b_{2} . x = lim_sup (f # x) ) holds

b_{1} = b_{2}

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

it . x = lim_sup (f # x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def8 defines lim_sup MESFUNC8:def 8 :

for X being non empty set

for f being Functional_Sequence of X,ExtREAL

for b_{3} being PartFunc of X,ExtREAL holds

( b_{3} = lim_sup f iff ( dom b_{3} = dom (f . 0) & ( for x being Element of X st x in dom b_{3} holds

b_{3} . x = lim_sup (f # x) ) ) );

for X being non empty set

for f being Functional_Sequence of X,ExtREAL

for b

( b

b

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

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

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 )

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;

ex b_{1} being PartFunc of X,ExtREAL st

( dom b_{1} = dom (f . 0) & ( for x being Element of X st x in dom b_{1} holds

b_{1} . x = lim (f # x) ) )

for b_{1}, b_{2} being PartFunc of X,ExtREAL st dom b_{1} = dom (f . 0) & ( for x being Element of X st x in dom b_{1} holds

b_{1} . x = lim (f # x) ) & dom b_{2} = dom (f . 0) & ( for x being Element of X st x in dom b_{2} holds

b_{2} . x = lim (f # x) ) holds

b_{1} = b_{2}

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

it . x = lim (f # x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def9 defines lim MESFUNC8:def 9 :

for X being non empty set

for f being Functional_Sequence of X,ExtREAL

for b_{3} being PartFunc of X,ExtREAL holds

( b_{3} = lim f iff ( dom b_{3} = dom (f . 0) & ( for x being Element of X st x in dom b_{3} holds

b_{3} . x = lim (f # x) ) ) );

for X being non empty set

for f being Functional_Sequence of X,ExtREAL

for b

( b

b

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 )

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

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

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

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

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

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

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

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

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_measurable_on E ) holds

for n being Nat holds (superior_realsequence f) . n is_measurable_on E

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_measurable_on E ) holds

for n being Nat holds (superior_realsequence f) . n is_measurable_on E

proof end;

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

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_measurable_on E ) holds

for n being Nat holds (inferior_realsequence f) . n is_measurable_on E

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

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

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

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

proof end;

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

lim_sup f is_measurable_on E

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_measurable_on E ) holds

lim_sup f is_measurable_on E

proof end;

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

lim_inf f is_measurable_on E

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_measurable_on E ) holds

lim_inf f is_measurable_on E

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_measurable_on E ) & ( for x being Element of X st x in E holds

f # x is convergent ) holds

lim f is_measurable_on E

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_measurable_on E ) & ( for x being Element of X st x in E holds

f # x is convergent ) holds

lim f is_measurable_on E

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_measurable_on E ) & 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_measurable_on E

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_measurable_on E ) & 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_measurable_on E

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

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;

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 & dom (f . 0) = E & ( for n being Nat holds

( f . n is_measurable_on E & 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 number 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 ) )

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_measurable_on E & 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 number 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: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))

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

proof end;

:: 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 & ( for n being Nat holds f . n is_measurable_on E ) & 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 number st 0 < e holds

ex F being Element of S st

( F c= E & M . (E \ F) <= e & ( 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 ) )

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_measurable_on E ) & 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 number st 0 < e holds

ex F being Element of S st

( F c= E & M . (E \ F) <= e & ( 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 ) )

proof end;