:: by Keiko Narita , Noboru Endou and Yasunari Shidama

::

:: Received December 16, 2008

:: Copyright (c) 2008-2012 Association of Mizar Users

begin

definition

let X be non empty set ;

let f be Functional_Sequence of X,REAL;

coherence

f is Functional_Sequence of X,ExtREAL

end;
let f be Functional_Sequence of X,REAL;

coherence

f is Functional_Sequence of X,ExtREAL

proof end;

:: deftheorem defines R_EAL MESFUN7C:def 1 :

for X being non empty set

for f being Functional_Sequence of X,REAL holds R_EAL f = f;

for X being non empty set

for f being Functional_Sequence of X,REAL holds R_EAL f = f;

theorem Th1: :: MESFUN7C:1

for X being non empty set

for f being Functional_Sequence of X,REAL

for x being Element of X holds f # x = (R_EAL f) # x

for f being Functional_Sequence of X,REAL

for x being Element of X holds f # x = (R_EAL f) # x

proof end;

definition

let X be non empty set ;

let f be Functional_Sequence of X,REAL;

coherence

inf (R_EAL f) is PartFunc of X,ExtREAL ;

end;
let f be Functional_Sequence of X,REAL;

coherence

inf (R_EAL f) is PartFunc of X,ExtREAL ;

:: deftheorem defines inf MESFUN7C:def 2 :

for X being non empty set

for f being Functional_Sequence of X,REAL holds inf f = inf (R_EAL f);

for X being non empty set

for f being Functional_Sequence of X,REAL holds inf f = inf (R_EAL f);

theorem Th2: :: MESFUN7C:2

for X being non empty set

for f being Functional_Sequence of X,REAL

for x being Element of X st x in dom (inf f) holds

(inf f) . x = inf (rng (R_EAL (f # x)))

for f being Functional_Sequence of X,REAL

for x being Element of X st x in dom (inf f) holds

(inf f) . x = inf (rng (R_EAL (f # x)))

proof end;

definition

let X be non empty set ;

let f be Functional_Sequence of X,REAL;

coherence

sup (R_EAL f) is PartFunc of X,ExtREAL ;

end;
let f be Functional_Sequence of X,REAL;

coherence

sup (R_EAL f) is PartFunc of X,ExtREAL ;

:: deftheorem defines sup MESFUN7C:def 3 :

for X being non empty set

for f being Functional_Sequence of X,REAL holds sup f = sup (R_EAL f);

for X being non empty set

for f being Functional_Sequence of X,REAL holds sup f = sup (R_EAL f);

theorem Th3: :: MESFUN7C:3

for X being non empty set

for f being Functional_Sequence of X,REAL

for x being Element of X st x in dom (sup f) holds

(sup f) . x = sup (rng (R_EAL (f # x)))

for f being Functional_Sequence of X,REAL

for x being Element of X st x in dom (sup f) holds

(sup f) . x = sup (rng (R_EAL (f # x)))

proof end;

definition

let X be non empty set ;

let f be Functional_Sequence of X,REAL;

inferior_realsequence (R_EAL f) is with_the_same_dom Functional_Sequence of X,ExtREAL ;

end;
let f be Functional_Sequence of X,REAL;

func inferior_realsequence f -> with_the_same_dom Functional_Sequence of X,ExtREAL equals :: MESFUN7C:def 4

inferior_realsequence (R_EAL f);

coherence inferior_realsequence (R_EAL f);

inferior_realsequence (R_EAL f) is with_the_same_dom Functional_Sequence of X,ExtREAL ;

:: deftheorem defines inferior_realsequence MESFUN7C:def 4 :

for X being non empty set

for f being Functional_Sequence of X,REAL holds inferior_realsequence f = inferior_realsequence (R_EAL f);

for X being non empty set

for f being Functional_Sequence of X,REAL holds inferior_realsequence f = inferior_realsequence (R_EAL f);

theorem Th4: :: MESFUN7C:4

for X being non empty set

for f being Functional_Sequence of X,REAL

for n being Nat holds

( dom ((inferior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((inferior_realsequence f) . n) holds

((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n ) )

for f being Functional_Sequence of X,REAL

for n being Nat holds

( dom ((inferior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((inferior_realsequence f) . n) holds

((inferior_realsequence f) . n) . x = (inferior_realsequence (R_EAL (f # x))) . n ) )

proof end;

definition

let X be non empty set ;

let f be Functional_Sequence of X,REAL;

superior_realsequence (R_EAL f) is with_the_same_dom Functional_Sequence of X,ExtREAL ;

end;
let f be Functional_Sequence of X,REAL;

func superior_realsequence f -> with_the_same_dom Functional_Sequence of X,ExtREAL equals :: MESFUN7C:def 5

superior_realsequence (R_EAL f);

coherence superior_realsequence (R_EAL f);

superior_realsequence (R_EAL f) is with_the_same_dom Functional_Sequence of X,ExtREAL ;

:: deftheorem defines superior_realsequence MESFUN7C:def 5 :

for X being non empty set

for f being Functional_Sequence of X,REAL holds superior_realsequence f = superior_realsequence (R_EAL f);

for X being non empty set

for f being Functional_Sequence of X,REAL holds superior_realsequence f = superior_realsequence (R_EAL f);

theorem Th5: :: MESFUN7C:5

for X being non empty set

for f being Functional_Sequence of X,REAL

for n being Nat holds

( dom ((superior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((superior_realsequence f) . n) holds

((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n ) )

for f being Functional_Sequence of X,REAL

for n being Nat holds

( dom ((superior_realsequence f) . n) = dom (f . 0) & ( for x being Element of X st x in dom ((superior_realsequence f) . n) holds

((superior_realsequence f) . n) . x = (superior_realsequence (R_EAL (f # x))) . n ) )

proof end;

theorem :: MESFUN7C:6

for X being non empty set

for f being Functional_Sequence of X,REAL

for x being Element of X st x in dom (f . 0) holds

(inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x))

for f being Functional_Sequence of X,REAL

for x being Element of X st x in dom (f . 0) holds

(inferior_realsequence f) # x = inferior_realsequence (R_EAL (f # x))

proof end;

registration

let X be non empty set ;

let f be with_the_same_dom Functional_Sequence of X,REAL;

coherence

R_EAL f is with_the_same_dom

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

coherence

R_EAL f is with_the_same_dom

proof end;

theorem Th7: :: MESFUN7C:7

for X being non empty set

for f being with_the_same_dom Functional_Sequence of X,REAL

for S being SigmaField of X

for E being Element of S

for n being Nat st f . n is_measurable_on E holds

(R_EAL f) . n is_measurable_on E

for f being with_the_same_dom Functional_Sequence of X,REAL

for S being SigmaField of X

for E being Element of S

for n being Nat st f . n is_measurable_on E holds

(R_EAL f) . n is_measurable_on E

proof end;

theorem :: MESFUN7C:8

theorem :: MESFUN7C:9

for X being non empty set

for f being with_the_same_dom Functional_Sequence of X,REAL

for n being Nat holds (inferior_realsequence f) . n = inf (f ^\ n)

for f being with_the_same_dom Functional_Sequence of X,REAL

for n being Nat holds (inferior_realsequence f) . n = inf (f ^\ n)

proof end;

theorem :: MESFUN7C:10

for X being non empty set

for f being with_the_same_dom Functional_Sequence of X,REAL

for n being Nat holds (superior_realsequence f) . n = sup (f ^\ n)

for f being with_the_same_dom Functional_Sequence of X,REAL

for n being Nat holds (superior_realsequence f) . n = sup (f ^\ n)

proof end;

theorem Th11: :: MESFUN7C:11

for X being non empty set

for f being Functional_Sequence of X,REAL

for x being Element of X st x in dom (f . 0) holds

(superior_realsequence f) # x = superior_realsequence (R_EAL (f # x))

for f being Functional_Sequence of X,REAL

for x being Element of X st x in dom (f . 0) holds

(superior_realsequence f) # x = superior_realsequence (R_EAL (f # x))

proof end;

definition

let X be non empty set ;

let f be Functional_Sequence of X,REAL;

coherence

lim_inf (R_EAL f) is PartFunc of X,ExtREAL ;

end;
let f be Functional_Sequence of X,REAL;

coherence

lim_inf (R_EAL f) is PartFunc of X,ExtREAL ;

:: deftheorem defines lim_inf MESFUN7C:def 6 :

for X being non empty set

for f being Functional_Sequence of X,REAL holds lim_inf f = lim_inf (R_EAL f);

for X being non empty set

for f being Functional_Sequence of X,REAL holds lim_inf f = lim_inf (R_EAL f);

theorem Th12: :: MESFUN7C:12

for X being non empty set

for f being Functional_Sequence of X,REAL

for x being Element of X st x in dom (lim_inf f) holds

(lim_inf f) . x = lim_inf (R_EAL (f # x))

for f being Functional_Sequence of X,REAL

for x being Element of X st x in dom (lim_inf f) holds

(lim_inf f) . x = lim_inf (R_EAL (f # x))

proof end;

definition

let X be non empty set ;

let f be Functional_Sequence of X,REAL;

coherence

lim_sup (R_EAL f) is PartFunc of X,ExtREAL ;

end;
let f be Functional_Sequence of X,REAL;

coherence

lim_sup (R_EAL f) is PartFunc of X,ExtREAL ;

:: deftheorem defines lim_sup MESFUN7C:def 7 :

for X being non empty set

for f being Functional_Sequence of X,REAL holds lim_sup f = lim_sup (R_EAL f);

for X being non empty set

for f being Functional_Sequence of X,REAL holds lim_sup f = lim_sup (R_EAL f);

theorem Th13: :: MESFUN7C:13

for X being non empty set

for f being Functional_Sequence of X,REAL

for x being Element of X st x in dom (lim_sup f) holds

(lim_sup f) . x = lim_sup (R_EAL (f # x))

for f being Functional_Sequence of X,REAL

for x being Element of X st x in dom (lim_sup f) holds

(lim_sup f) . x = lim_sup (R_EAL (f # x))

proof end;

definition

let X be non empty set ;

let f be Functional_Sequence of X,REAL;

coherence

lim (R_EAL f) is PartFunc of X,ExtREAL ;

end;
let f be Functional_Sequence of X,REAL;

coherence

lim (R_EAL f) is PartFunc of X,ExtREAL ;

:: deftheorem defines lim MESFUN7C:def 8 :

for X being non empty set

for f being Functional_Sequence of X,REAL holds lim f = lim (R_EAL f);

for X being non empty set

for f being Functional_Sequence of X,REAL holds lim f = lim (R_EAL f);

theorem Th14: :: MESFUN7C:14

for X being non empty set

for f being Functional_Sequence of X,REAL

for x being Element of X st x in dom (lim f) holds

(lim f) . x = lim (R_EAL (f # x))

for f being Functional_Sequence of X,REAL

for x being Element of X st x in dom (lim f) holds

(lim f) . x = lim (R_EAL (f # x))

proof end;

theorem Th15: :: MESFUN7C:15

for X being non empty set

for f being Functional_Sequence of X,REAL

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,REAL

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

for X being non empty set

for S being SigmaField of X

for f being with_the_same_dom Functional_Sequence of X,REAL

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

union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r))

for S being SigmaField of X

for f being with_the_same_dom Functional_Sequence of X,REAL

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

union (rng F) = (dom (f . 0)) /\ (great_dom ((sup f),r))

proof end;

theorem :: MESFUN7C:17

for X being non empty set

for S being SigmaField of X

for f being with_the_same_dom Functional_Sequence of X,REAL

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

meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))

for S being SigmaField of X

for f being with_the_same_dom Functional_Sequence of X,REAL

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

meet (rng F) = (dom (f . 0)) /\ (great_eq_dom ((inf f),r))

proof end;

theorem Th18: :: MESFUN7C:18

for X being non empty set

for S being SigmaField of X

for f being with_the_same_dom Functional_Sequence of X,REAL

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,REAL

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

for X being non empty set

for S being SigmaField of X

for f being with_the_same_dom Functional_Sequence of X,REAL

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,REAL

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

for X being non empty set

for f being Functional_Sequence of X,REAL

for x being Element of X st x in dom (f . 0) & f # x is convergent holds

(superior_realsequence f) # x is bounded_below

for f being Functional_Sequence of X,REAL

for x being Element of X st x in dom (f . 0) & f # x is convergent holds

(superior_realsequence f) # x is bounded_below

proof end;

theorem Th21: :: MESFUN7C:21

for X being non empty set

for S being SigmaField of X

for f being with_the_same_dom Functional_Sequence of X,REAL

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,REAL

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 Th22: :: MESFUN7C:22

for X being non empty set

for S being SigmaField of X

for f being with_the_same_dom Functional_Sequence of X,REAL

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,REAL

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;

begin

definition

let X be non empty set ;

let H be Functional_Sequence of X,COMPLEX;

let x be Element of X;

ex b_{1} being Complex_Sequence st

for n being Nat holds b_{1} . n = (H . n) . x

for b_{1}, b_{2} being Complex_Sequence st ( for n being Nat holds b_{1} . n = (H . n) . x ) & ( for n being Nat holds b_{2} . n = (H . n) . x ) holds

b_{1} = b_{2}

end;
let H be Functional_Sequence of X,COMPLEX;

let x be Element of X;

func H # x -> Complex_Sequence means :Def9: :: MESFUN7C:def 9

for n being Nat holds it . n = (H . n) . x;

existence for n being Nat holds it . n = (H . n) . x;

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def9 defines # MESFUN7C:def 9 :

for X being non empty set

for H being Functional_Sequence of X,COMPLEX

for x being Element of X

for b_{4} being Complex_Sequence holds

( b_{4} = H # x iff for n being Nat holds b_{4} . n = (H . n) . x );

for X being non empty set

for H being Functional_Sequence of X,COMPLEX

for x being Element of X

for b

( b

definition

let X be non empty set ;

let f be Functional_Sequence of X,COMPLEX;

ex b_{1} being PartFunc of X,COMPLEX 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,COMPLEX 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,COMPLEX;

func lim f -> PartFunc of X,COMPLEX means :Def10: :: MESFUN7C: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 ( 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 Def10 defines lim MESFUN7C:def 10 :

for X being non empty set

for f being Functional_Sequence of X,COMPLEX

for b_{3} being PartFunc of X,COMPLEX 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,COMPLEX

for b

( b

b

definition

let X be non empty set ;

let f be Functional_Sequence of X,COMPLEX;

ex b_{1} being Functional_Sequence of X,REAL st

for n being Nat holds

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

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

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

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

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

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

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

b_{1} = b_{2}

end;
let f be Functional_Sequence of X,COMPLEX;

func Re f -> Functional_Sequence of X,REAL means :Def11: :: MESFUN7C:def 11

for n being Nat holds

( dom (it . n) = dom (f . n) & ( for x being Element of X st x in dom (it . n) holds

(it . n) . x = (Re (f # x)) . n ) );

existence for n being Nat holds

( dom (it . n) = dom (f . n) & ( for x being Element of X st x in dom (it . n) holds

(it . n) . x = (Re (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 Def11 defines Re MESFUN7C:def 11 :

for X being non empty set

for f being Functional_Sequence of X,COMPLEX

for b_{3} being Functional_Sequence of X,REAL holds

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

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

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

for X being non empty set

for f being Functional_Sequence of X,COMPLEX

for b

( b

( dom (b

(b

registration

let X be non empty set ;

let f be with_the_same_dom Functional_Sequence of X,COMPLEX;

correctness

coherence

Re f is with_the_same_dom ;

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

correctness

coherence

Re f is with_the_same_dom ;

proof end;

definition

let X be non empty set ;

let f be Functional_Sequence of X,COMPLEX;

ex b_{1} being Functional_Sequence of X,REAL st

for n being Nat holds

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

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

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

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

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

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

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

b_{1} = b_{2}

end;
let f be Functional_Sequence of X,COMPLEX;

func Im f -> Functional_Sequence of X,REAL means :Def12: :: MESFUN7C:def 12

for n being Nat holds

( dom (it . n) = dom (f . n) & ( for x being Element of X st x in dom (it . n) holds

(it . n) . x = (Im (f # x)) . n ) );

existence for n being Nat holds

( dom (it . n) = dom (f . n) & ( for x being Element of X st x in dom (it . n) holds

(it . n) . x = (Im (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 Def12 defines Im MESFUN7C:def 12 :

for X being non empty set

for f being Functional_Sequence of X,COMPLEX

for b_{3} being Functional_Sequence of X,REAL holds

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

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

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

for X being non empty set

for f being Functional_Sequence of X,COMPLEX

for b

( b

( dom (b

(b

registration

let X be non empty set ;

let f be with_the_same_dom Functional_Sequence of X,COMPLEX;

correctness

coherence

Im f is with_the_same_dom ;

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

correctness

coherence

Im f is with_the_same_dom ;

proof end;

theorem Th23: :: MESFUN7C:23

for X being non empty set

for f being with_the_same_dom Functional_Sequence of X,COMPLEX

for x being Element of X st x in dom (f . 0) holds

( (Re f) # x = Re (f # x) & (Im f) # x = Im (f # x) )

for f being with_the_same_dom Functional_Sequence of X,COMPLEX

for x being Element of X st x in dom (f . 0) holds

( (Re f) # x = Re (f # x) & (Im f) # x = Im (f # x) )

proof end;

theorem Th24: :: MESFUN7C:24

for X being non empty set

for f being Functional_Sequence of X,COMPLEX

for n being Nat holds

( (Re f) . n = Re (f . n) & (Im f) . n = Im (f . n) )

for f being Functional_Sequence of X,COMPLEX

for n being Nat holds

( (Re f) . n = Re (f . n) & (Im f) . n = Im (f . n) )

proof end;

theorem Th25: :: MESFUN7C:25

for X being non empty set

for f being with_the_same_dom Functional_Sequence of X,COMPLEX st ( for x being Element of X st x in dom (f . 0) holds

f # x is convergent ) holds

( lim (Re f) = Re (lim f) & lim (Im f) = Im (lim f) )

for f being with_the_same_dom Functional_Sequence of X,COMPLEX st ( for x being Element of X st x in dom (f . 0) holds

f # x is convergent ) holds

( lim (Re f) = Re (lim f) & lim (Im f) = Im (lim f) )

proof end;

theorem :: MESFUN7C:26

for X being non empty set

for S being SigmaField of X

for f being with_the_same_dom Functional_Sequence of X,COMPLEX

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,COMPLEX

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

for X being non empty set

for S being SigmaField of X

for f being with_the_same_dom Functional_Sequence of X,COMPLEX

for g being PartFunc of X,COMPLEX

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,COMPLEX

for g being PartFunc of X,COMPLEX

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;

begin

theorem :: MESFUN7C:28

for X being non empty set

for Y being set

for f being PartFunc of X,COMPLEX

for r being Real holds (r (#) f) | Y = r (#) (f | Y)

for Y being set

for f being PartFunc of X,COMPLEX

for r being Real holds (r (#) f) | Y = r (#) (f | Y)

proof end;

Lm1: for X being non empty set

for f being PartFunc of X,COMPLEX holds |.f.| is nonnegative

proof end;

theorem :: MESFUN7C:29

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for k being real number

for E being Element of S st 0 <= k & E c= dom f & f is_measurable_on E holds

|.f.| to_power k is_measurable_on E

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for k being real number

for E being Element of S st 0 <= k & E c= dom f & f is_measurable_on E holds

|.f.| to_power k is_measurable_on E

proof end;

theorem Th30: :: MESFUN7C:30

for X being non empty set

for f, g being PartFunc of X,REAL holds (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g)

for f, g being PartFunc of X,REAL holds (R_EAL f) (#) (R_EAL g) = R_EAL (f (#) g)

proof end;

theorem Th31: :: MESFUN7C:31

for X being non empty set

for S being SigmaField of X

for E being Element of S

for f, g being PartFunc of X,REAL st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds

f (#) g is_measurable_on E

for S being SigmaField of X

for E being Element of S

for f, g being PartFunc of X,REAL st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds

f (#) g is_measurable_on E

proof end;

theorem Th32: :: MESFUN7C:32

for X being non empty set

for f, g being PartFunc of X,COMPLEX holds

( Re (f (#) g) = ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) & Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) )

for f, g being PartFunc of X,COMPLEX holds

( Re (f (#) g) = ((Re f) (#) (Re g)) - ((Im f) (#) (Im g)) & Im (f (#) g) = ((Im f) (#) (Re g)) + ((Re f) (#) (Im g)) )

proof end;

theorem :: MESFUN7C:33

for X being non empty set

for S being SigmaField of X

for f, g being PartFunc of X,COMPLEX

for E being Element of S st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds

f (#) g is_measurable_on E

for S being SigmaField of X

for f, g being PartFunc of X,COMPLEX

for E being Element of S st (dom f) /\ (dom g) = E & f is_measurable_on E & g is_measurable_on E holds

f (#) g is_measurable_on E

proof end;

theorem Th34: :: MESFUN7C:34

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,REAL st ex E being Element of S st

( E = dom f & E = dom g & f is_measurable_on E & g is_measurable_on E ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds

g . x <= f . x ) holds

Integral (M,g) <= Integral (M,f)

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,REAL st ex E being Element of S st

( E = dom f & E = dom g & f is_measurable_on E & g is_measurable_on E ) & f is nonnegative & g is nonnegative & ( for x being Element of X st x in dom g holds

g . x <= f . x ) holds

Integral (M,g) <= Integral (M,f)

proof end;

theorem Th35: :: MESFUN7C:35

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,COMPLEX st f is_integrable_on M holds

( ex A being Element of S st

( A = dom f & f is_measurable_on A ) & |.f.| is_integrable_on M )

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,COMPLEX st f is_integrable_on M holds

( ex A being Element of S st

( A = dom f & f is_measurable_on A ) & |.f.| is_integrable_on M )

proof end;

theorem :: MESFUN7C:36

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,COMPLEX st f is_integrable_on M holds

ex F being Function of NAT,S st

( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (|.f.|,0)) = union (rng F) & ( for n being Nat holds

( F . n in S & M . (F . n) < +infty ) ) )

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,COMPLEX st f is_integrable_on M holds

ex F being Function of NAT,S st

( ( for n being Nat holds F . n = (dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (n + 1))))) ) & (dom f) \ (eq_dom (|.f.|,0)) = union (rng F) & ( for n being Nat holds

( F . n in S & M . (F . n) < +infty ) ) )

proof end;

theorem Th37: :: MESFUN7C:37

for X being non empty set

for f being PartFunc of X,COMPLEX

for A being set holds |.f.| | A = |.(f | A).|

for f being PartFunc of X,COMPLEX

for A being set holds |.f.| | A = |.(f | A).|

proof end;

theorem Th38: :: MESFUN7C:38

for X being non empty set

for f, g being PartFunc of X,COMPLEX holds

( dom (|.f.| + |.g.|) = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| )

for f, g being PartFunc of X,COMPLEX holds

( dom (|.f.| + |.g.|) = (dom f) /\ (dom g) & dom |.(f + g).| c= dom |.f.| )

proof end;

theorem Th39: :: MESFUN7C:39

for X being non empty set

for f, g being PartFunc of X,COMPLEX holds (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|)

for f, g being PartFunc of X,COMPLEX holds (|.f.| | (dom |.(f + g).|)) + (|.g.| | (dom |.(f + g).|)) = (|.f.| + |.g.|) | (dom |.(f + g).|)

proof end;

theorem Th40: :: MESFUN7C:40

for X being non empty set

for f, g being PartFunc of X,COMPLEX

for x being set st x in dom |.(f + g).| holds

|.(f + g).| . x <= (|.f.| + |.g.|) . x

for f, g being PartFunc of X,COMPLEX

for x being set st x in dom |.(f + g).| holds

|.(f + g).| . x <= (|.f.| + |.g.|) . x

proof end;

theorem Th41: :: MESFUN7C:41

for X being non empty set

for f, g being PartFunc of X,REAL st ( for x being set st x in dom f holds

f . x <= g . x ) holds

g - f is nonnegative

for f, g being PartFunc of X,REAL st ( for x being set st x in dom f holds

f . x <= g . x ) holds

g - f is nonnegative

proof end;

theorem :: MESFUN7C:42

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds

ex E being Element of S st

( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )

for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,COMPLEX st f is_integrable_on M & g is_integrable_on M holds

ex E being Element of S st

( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )

proof end;

begin

:: deftheorem Def13 defines is_simple_func_in MESFUN7C:def 13 :

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,COMPLEX holds

( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S st

( dom f = union (rng F) & ( for n being Nat

for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

f . x = f . y ) ) );

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,COMPLEX holds

( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S st

( dom f = union (rng F) & ( for n being Nat

for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

f . x = f . y ) ) );

definition

let X be non empty set ;

let S be SigmaField of X;

let f be PartFunc of X,REAL;

let F be Finite_Sep_Sequence of S;

let a be FinSequence of REAL ;

end;
let S be SigmaField of X;

let f be PartFunc of X,REAL;

let F be Finite_Sep_Sequence of S;

let a be FinSequence of REAL ;

:: deftheorem Def14 defines are_Re-presentation_of MESFUN7C:def 14 :

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,REAL

for F being Finite_Sep_Sequence of S

for a being FinSequence of REAL holds

( F,a are_Re-presentation_of f iff ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

f . x = a . n ) ) );

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,REAL

for F being Finite_Sep_Sequence of S

for a being FinSequence of REAL holds

( F,a are_Re-presentation_of f iff ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

f . x = a . n ) ) );

definition

let X be non empty set ;

let S be SigmaField of X;

let f be PartFunc of X,COMPLEX;

let F be Finite_Sep_Sequence of S;

let a be FinSequence of COMPLEX ;

end;
let S be SigmaField of X;

let f be PartFunc of X,COMPLEX;

let F be Finite_Sep_Sequence of S;

let a be FinSequence of COMPLEX ;

:: deftheorem Def15 defines are_Re-presentation_of MESFUN7C:def 15 :

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for F being Finite_Sep_Sequence of S

for a being FinSequence of COMPLEX holds

( F,a are_Re-presentation_of f iff ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

f . x = a . n ) ) );

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for F being Finite_Sep_Sequence of S

for a being FinSequence of COMPLEX holds

( F,a are_Re-presentation_of f iff ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

f . x = a . n ) ) );

theorem :: MESFUN7C:43

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,COMPLEX holds

( f is_simple_func_in S iff ( Re f is_simple_func_in S & Im f is_simple_func_in S ) )

for S being SigmaField of X

for f being PartFunc of X,COMPLEX holds

( f is_simple_func_in S iff ( Re f is_simple_func_in S & Im f is_simple_func_in S ) )

proof end;

theorem Th44: :: MESFUN7C:44

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,COMPLEX st f is_simple_func_in S holds

ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st

( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

f . x = a . n ) )

for S being SigmaField of X

for f being PartFunc of X,COMPLEX st f is_simple_func_in S holds

ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st

( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

f . x = a . n ) )

proof end;

theorem Th45: :: MESFUN7C:45

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,COMPLEX holds

( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f )

for S being SigmaField of X

for f being PartFunc of X,COMPLEX holds

( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f )

proof end;

theorem Th48: :: MESFUN7C:48

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for F being Finite_Sep_Sequence of S

for a being FinSequence of COMPLEX holds

( F,a are_Re-presentation_of f iff ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) )

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for F being Finite_Sep_Sequence of S

for a being FinSequence of COMPLEX holds

( F,a are_Re-presentation_of f iff ( F, Re a are_Re-presentation_of Re f & F, Im a are_Re-presentation_of Im f ) )

proof end;

theorem :: MESFUN7C:49

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,COMPLEX holds

( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st

( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Im f) . x = (Im c) . n ) ) )

for S being SigmaField of X

for f being PartFunc of X,COMPLEX holds

( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st

( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

(Im f) . x = (Im c) . n ) ) )

proof end;