:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama

::

:: Received October 6, 2000

:: Copyright (c) 2000-2016 Association of Mizar Users

definition

let X be non empty set ;

let f be PartFunc of X,ExtREAL;

( f is real-valued iff for x being Element of X st x in dom f holds

|.(f . x).| < +infty )

end;
let f be PartFunc of X,ExtREAL;

:: original: real-valued

redefine attr f is real-valued means :: MESFUNC2:def 1

for x being Element of X st x in dom f holds

|.(f . x).| < +infty ;

compatibility redefine attr f is real-valued means :: MESFUNC2:def 1

for x being Element of X st x in dom f holds

|.(f . x).| < +infty ;

( f is real-valued iff for x being Element of X st x in dom f holds

|.(f . x).| < +infty )

proof end;

:: deftheorem defines real-valued MESFUNC2:def 1 :

for X being non empty set

for f being PartFunc of X,ExtREAL holds

( f is real-valued iff for x being Element of X st x in dom f holds

|.(f . x).| < +infty );

for X being non empty set

for f being PartFunc of X,ExtREAL holds

( f is real-valued iff for x being Element of X st x in dom f holds

|.(f . x).| < +infty );

theorem Th2: :: MESFUNC2:2

for X being non empty set

for f, g being PartFunc of X,ExtREAL st ( not f is V82() or not g is V82() ) holds

( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) )

for f, g being PartFunc of X,ExtREAL st ( not f is V82() or not g is V82() ) holds

( dom (f + g) = (dom f) /\ (dom g) & dom (f - g) = (dom f) /\ (dom g) )

proof end;

theorem Th3: :: MESFUNC2:3

for X being non empty set

for S being SigmaField of X

for f, g being PartFunc of X,ExtREAL

for F being Function of RAT,S

for r being Real

for A being Element of S st f is V82() & g is V82() & ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds

A /\ (less_dom ((f + g),r)) = union (rng F)

for S being SigmaField of X

for f, g being PartFunc of X,ExtREAL

for F being Function of RAT,S

for r being Real

for A being Element of S st f is V82() & g is V82() & ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds

A /\ (less_dom ((f + g),r)) = union (rng F)

proof end;

theorem Th5: :: MESFUNC2:5

for X, Y, Z being non empty set

for F being Function of X,Z st X,Y are_equipotent holds

ex G being Function of Y,Z st rng F = rng G

for F being Function of X,Z st X,Y are_equipotent holds

ex G being Function of Y,Z st rng F = rng G

proof end;

theorem Th6: :: MESFUNC2:6

for X being non empty set

for r being Real

for S being SigmaField of X

for f, g being PartFunc of X,ExtREAL

for A being Element of S st f is_measurable_on A & g is_measurable_on A holds

ex F being Function of RAT,S st

for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p))))

for r being Real

for S being SigmaField of X

for f, g being PartFunc of X,ExtREAL

for A being Element of S st f is_measurable_on A & g is_measurable_on A holds

ex F being Function of RAT,S st

for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p))))

proof end;

theorem Th7: :: MESFUNC2:7

for X being non empty set

for S being SigmaField of X

for f, g being PartFunc of X,ExtREAL

for A being Element of S st f is V82() & g is V82() & f is_measurable_on A & g is_measurable_on A holds

f + g is_measurable_on A

for S being SigmaField of X

for f, g being PartFunc of X,ExtREAL

for A being Element of S st f is V82() & g is V82() & f is_measurable_on A & g is_measurable_on A holds

f + g is_measurable_on A

proof end;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

theorem Th10: :: MESFUNC2:10

for C being non empty set

for f being PartFunc of C,ExtREAL

for r being Real st f is V82() holds

r (#) f is V82()

for f being PartFunc of C,ExtREAL

for r being Real st f is V82() holds

r (#) f is V82()

proof end;

theorem :: MESFUNC2:11

for X being non empty set

for S being SigmaField of X

for f, g being PartFunc of X,ExtREAL

for A being Element of S st f is V82() & g is V82() & f is_measurable_on A & g is_measurable_on A & A c= dom g holds

f - g is_measurable_on A

for S being SigmaField of X

for f, g being PartFunc of X,ExtREAL

for A being Element of S st f is V82() & g is V82() & f is_measurable_on A & g is_measurable_on A & A c= dom g holds

f - g is_measurable_on A

proof end;

:: and their basic properties ::

definition

let C be non empty set ;

let f be PartFunc of C,ExtREAL;

deffunc H_{1}( Element of C) -> Element of ExtREAL = max ((f . $1),0.);

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

( dom b_{1} = dom f & ( for x being Element of C st x in dom b_{1} holds

b_{1} . x = max ((f . x),0.) ) )

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

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

b_{2} . x = max ((f . x),0.) ) holds

b_{1} = b_{2}
_{2}( Element of C) -> Element of ExtREAL = max ((- (f . $1)),0.);

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

( dom b_{1} = dom f & ( for x being Element of C st x in dom b_{1} holds

b_{1} . x = max ((- (f . x)),0.) ) )

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

b_{1} . x = max ((- (f . x)),0.) ) & dom b_{2} = dom f & ( for x being Element of C st x in dom b_{2} holds

b_{2} . x = max ((- (f . x)),0.) ) holds

b_{1} = b_{2}

end;
let f be PartFunc of C,ExtREAL;

deffunc H

func max+ f -> PartFunc of C,ExtREAL means :Def2: :: MESFUNC2:def 2

( dom it = dom f & ( for x being Element of C st x in dom it holds

it . x = max ((f . x),0.) ) );

existence ( dom it = dom f & ( for x being Element of C st x in dom it holds

it . x = max ((f . x),0.) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

deffunc H
func max- f -> PartFunc of C,ExtREAL means :Def3: :: MESFUNC2:def 3

( dom it = dom f & ( for x being Element of C st x in dom it holds

it . x = max ((- (f . x)),0.) ) );

existence ( dom it = dom f & ( for x being Element of C st x in dom it holds

it . x = max ((- (f . x)),0.) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines max+ MESFUNC2:def 2 :

for C being non empty set

for f, b_{3} being PartFunc of C,ExtREAL holds

( b_{3} = max+ f iff ( dom b_{3} = dom f & ( for x being Element of C st x in dom b_{3} holds

b_{3} . x = max ((f . x),0.) ) ) );

for C being non empty set

for f, b

( b

b

:: deftheorem Def3 defines max- MESFUNC2:def 3 :

for C being non empty set

for f, b_{3} being PartFunc of C,ExtREAL holds

( b_{3} = max- f iff ( dom b_{3} = dom f & ( for x being Element of C st x in dom b_{3} holds

b_{3} . x = max ((- (f . x)),0.) ) ) );

for C being non empty set

for f, b

( b

b

theorem Th12: :: MESFUNC2:12

for C being non empty set

for f being PartFunc of C,ExtREAL

for x being Element of C holds 0. <= (max+ f) . x

for f being PartFunc of C,ExtREAL

for x being Element of C holds 0. <= (max+ f) . x

proof end;

theorem Th13: :: MESFUNC2:13

for C being non empty set

for f being PartFunc of C,ExtREAL

for x being Element of C holds 0. <= (max- f) . x

for f being PartFunc of C,ExtREAL

for x being Element of C holds 0. <= (max- f) . x

proof end;

theorem Th15: :: MESFUNC2:15

for C being non empty set

for f being PartFunc of C,ExtREAL

for x being Element of C st 0. < (max+ f) . x holds

(max- f) . x = 0.

for f being PartFunc of C,ExtREAL

for x being Element of C st 0. < (max+ f) . x holds

(max- f) . x = 0.

proof end;

theorem :: MESFUNC2:16

for C being non empty set

for f being PartFunc of C,ExtREAL

for x being Element of C st 0. < (max- f) . x holds

(max+ f) . x = 0.

for f being PartFunc of C,ExtREAL

for x being Element of C st 0. < (max- f) . x holds

(max+ f) . x = 0.

proof end;

theorem Th17: :: MESFUNC2:17

for C being non empty set

for f being PartFunc of C,ExtREAL holds

( dom f = dom ((max+ f) - (max- f)) & dom f = dom ((max+ f) + (max- f)) )

for f being PartFunc of C,ExtREAL holds

( dom f = dom ((max+ f) - (max- f)) & dom f = dom ((max+ f) + (max- f)) )

proof end;

theorem Th18: :: MESFUNC2:18

for C being non empty set

for f being PartFunc of C,ExtREAL

for x being Element of C holds

( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) )

for f being PartFunc of C,ExtREAL

for x being Element of C holds

( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) )

proof end;

theorem Th19: :: MESFUNC2:19

for C being non empty set

for f being PartFunc of C,ExtREAL

for x being Element of C st (max+ f) . x = f . x holds

(max- f) . x = 0.

for f being PartFunc of C,ExtREAL

for x being Element of C st (max+ f) . x = f . x holds

(max- f) . x = 0.

proof end;

theorem Th20: :: MESFUNC2:20

for C being non empty set

for f being PartFunc of C,ExtREAL

for x being Element of C st x in dom f & (max+ f) . x = 0. holds

(max- f) . x = - (f . x)

for f being PartFunc of C,ExtREAL

for x being Element of C st x in dom f & (max+ f) . x = 0. holds

(max- f) . x = - (f . x)

proof end;

theorem :: MESFUNC2:21

for C being non empty set

for f being PartFunc of C,ExtREAL

for x being Element of C st (max- f) . x = - (f . x) holds

(max+ f) . x = 0.

for f being PartFunc of C,ExtREAL

for x being Element of C st (max- f) . x = - (f . x) holds

(max+ f) . x = 0.

proof end;

theorem :: MESFUNC2:22

for C being non empty set

for f being PartFunc of C,ExtREAL

for x being Element of C st x in dom f & (max- f) . x = 0. holds

(max+ f) . x = f . x

for f being PartFunc of C,ExtREAL

for x being Element of C st x in dom f & (max- f) . x = 0. holds

(max+ f) . x = f . x

proof end;

theorem :: MESFUNC2:25

for X being non empty set

for f being PartFunc of X,ExtREAL

for S being SigmaField of X

for A being Element of S st f is_measurable_on A holds

max+ f is_measurable_on A

for f being PartFunc of X,ExtREAL

for S being SigmaField of X

for A being Element of S st f is_measurable_on A holds

max+ f is_measurable_on A

proof end;

theorem :: MESFUNC2:26

for X being non empty set

for f being PartFunc of X,ExtREAL

for S being SigmaField of X

for A being Element of S st f is_measurable_on A & A c= dom f holds

max- f is_measurable_on A

for f being PartFunc of X,ExtREAL

for S being SigmaField of X

for A being Element of S st f is_measurable_on A & A c= dom f holds

max- f is_measurable_on A

proof end;

theorem :: MESFUNC2:27

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,ExtREAL

for A being Element of S st f is_measurable_on A & A c= dom f holds

|.f.| is_measurable_on A

for S being SigmaField of X

for f being PartFunc of X,ExtREAL

for A being Element of S st f is_measurable_on A & A c= dom f holds

|.f.| is_measurable_on A

proof end;

definition

let A, X be set ;

:: original: chi

redefine func chi (A,X) -> PartFunc of X,ExtREAL;

coherence

chi (A,X) is PartFunc of X,ExtREAL

end;
:: original: chi

redefine func chi (A,X) -> PartFunc of X,ExtREAL;

coherence

chi (A,X) is PartFunc of X,ExtREAL

proof end;

theorem :: MESFUNC2:28

for X being non empty set

for S being SigmaField of X

for A being Element of S holds chi (A,X) is V82()

for S being SigmaField of X

for A being Element of S holds chi (A,X) is V82()

proof end;

theorem :: MESFUNC2:29

for X being non empty set

for S being SigmaField of X

for A, B being Element of S holds chi (A,X) is_measurable_on B

for S being SigmaField of X

for A, B being Element of S holds chi (A,X) is_measurable_on B

proof end;

registration

let X be set ;

let S be SigmaField of X;

ex b_{1} being FinSequence of S st b_{1} is disjoint_valued

end;
let S be SigmaField of X;

cluster Relation-like NAT -defined S -valued Function-like V44() FinSequence-like FinSubsequence-like disjoint_valued for FinSequence of S;

existence ex b

proof end;

definition

let X be set ;

let S be SigmaField of X;

mode Finite_Sep_Sequence of S is disjoint_valued FinSequence of S;

end;
let S be SigmaField of X;

mode Finite_Sep_Sequence of S is disjoint_valued FinSequence of S;

theorem Th30: :: MESFUNC2:30

for X being non empty set

for S being SigmaField of X

for F being Function st F is Finite_Sep_Sequence of S holds

ex G being Sep_Sequence of S st

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

F . n = G . n ) & ( for m being Nat st not m in dom F holds

G . m = {} ) )

for S being SigmaField of X

for F being Function st F is Finite_Sep_Sequence of S holds

ex G being Sep_Sequence of S st

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

F . n = G . n ) & ( for m being Nat st not m in dom F holds

G . m = {} ) )

proof end;

theorem :: MESFUNC2:31

for X being non empty set

for S being SigmaField of X

for F being Function st F is Finite_Sep_Sequence of S holds

union (rng F) in S

for S being SigmaField of X

for F being Function st F is Finite_Sep_Sequence of S holds

union (rng F) in S

proof end;

:: deftheorem defines is_simple_func_in MESFUNC2:def 4 :

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,ExtREAL holds

( f is_simple_func_in S iff ( f is V82() & 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,ExtREAL holds

( f is_simple_func_in S iff ( f is V82() & 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 ) ) ) );

theorem :: MESFUNC2:32

theorem :: MESFUNC2:33

for X being non empty set

for S being SigmaField of X

for n being Nat

for F being Relation st F is Finite_Sep_Sequence of S holds

F | (Seg n) is Finite_Sep_Sequence of S

for S being SigmaField of X

for n being Nat

for F being Relation st F is Finite_Sep_Sequence of S holds

F | (Seg n) is Finite_Sep_Sequence of S

proof end;

theorem :: MESFUNC2:34

for X being non empty set

for f being PartFunc of X,ExtREAL

for S being SigmaField of X

for A being Element of S st f is_simple_func_in S holds

f is_measurable_on A

for f being PartFunc of X,ExtREAL

for S being SigmaField of X

for A being Element of S st f is_simple_func_in S holds

f is_measurable_on A

proof end;