:: MESFUNC2 semantic presentation

definition

let X be non empty set ;
let f be PartFunc of X, ExtREAL ;
pred f is_finite means :Def1: :: MESFUNC2:def 1
for x being Element of X st x in dom f holds
|.(f . x).| <' +infty ;

end;

:: deftheorem Def1 defines is_finite MESFUNC2:def 1 :

theorem :: MESFUNC2:1

for X being non empty set
for f being PartFunc of X, ExtREAL holds f = 1 (#) f

proof end;

theorem Th2: :: MESFUNC2:2

for X being non empty set
for f, g being PartFunc of X, ExtREAL st ( f is_finite or g is_finite ) 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 sigma_Field_Subset 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_finite & g is_finite & ( for p being Rational holds F . p = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) ) holds
A /\ (less_dom (f + g),(R_EAL r)) = union (rng F)

proof end;

theorem :: MESFUNC2:4

ex F being Function of NAT , RAT st
( F is one-to-one & dom F = NAT & rng F = RAT )

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

proof end;

theorem Th6: :: MESFUNC2:6

for X being non empty set
for r being Real
for S being sigma_Field_Subset 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,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p))))

proof end;

theorem Th7: :: MESFUNC2:7

for X being non empty set
for S being sigma_Field_Subset of X
for f, g being PartFunc of X, ExtREAL
for A being Element of S st f is_finite & g is_finite & f is_measurable_on A & g is_measurable_on A holds
f + g is_measurable_on A

proof end;

theorem :: MESFUNC2:8

canceled;

theorem Th9: :: MESFUNC2:9

for C being non empty set
for f1, f2 being PartFunc of C, ExtREAL holds f1 - f2 = f1 + (- f2)

proof end;

theorem Th10: :: MESFUNC2:10

for r being Real holds R_EAL (- r) = - (R_EAL r)

proof end;

theorem Th11: :: MESFUNC2:11

for C being non empty set
for f being PartFunc of C, ExtREAL holds - f = (- 1) (#) f

proof end;

theorem Th12: :: MESFUNC2:12

for C being non empty set
for f being PartFunc of C, ExtREAL
for r being Real st f is_finite holds
r (#) f is_finite

proof end;

theorem :: MESFUNC2:13

proof end;

definition

let C be non empty set ;
let f be PartFunc of C, ExtREAL ;
deffunc H₁( Element of C) -> Element of ExtREAL = max (f . $1),0. ;
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

proof end;

uniqueness

proof end;

deffunc H₂( Element of C) -> Element of ExtREAL = max (- (f . $1)),0. ;
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

proof end;

uniqueness

proof end;

end;

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

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

theorem Th14: :: MESFUNC2:14

for C being non empty set
for f being PartFunc of C, ExtREAL
for x being Element of C st x in dom f 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 x in dom f holds
0. <=' (max- f) . x

proof end;

theorem :: MESFUNC2:16

for C being non empty set
for f being PartFunc of C, ExtREAL holds max- f = max+ (- f)

proof end;

theorem Th17: :: MESFUNC2:17

for C being non empty set
for f being PartFunc of C, ExtREAL
for x being Element of C st x in dom f & 0. <' (max+ f) . x holds
(max- f) . x = 0.

proof end;

theorem :: MESFUNC2:18

for C being non empty set
for f being PartFunc of C, ExtREAL
for x being Element of C st x in dom f & 0. <' (max- f) . x holds
(max+ f) . x = 0.

proof end;

theorem Th19: :: MESFUNC2:19

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

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 holds
( ( (max+ f) . x = f . x or (max+ f) . x = 0. ) & ( (max- f) . x = - (f . x) or (max- f) . x = 0. ) )

proof end;

theorem Th21: :: MESFUNC2:21

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 = f . x holds
(max- f) . x = 0.

proof end;

theorem Th22: :: 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)

proof end;

theorem :: MESFUNC2:23

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 = - (f . x) holds
(max+ f) . x = 0.

proof end;

theorem :: MESFUNC2:24

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

proof end;

theorem :: MESFUNC2:25

for C being non empty set
for f being PartFunc of C, ExtREAL holds f = (max+ f) - (max- f)

proof end;

theorem :: MESFUNC2:26

for C being non empty set
for f being PartFunc of C, ExtREAL holds |.f.| = (max+ f) + (max- f)

proof end;

theorem :: MESFUNC2:27

for X being non empty set
for f being PartFunc of X, ExtREAL
for S being sigma_Field_Subset 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:28

for X being non empty set
for f being PartFunc of X, ExtREAL
for S being sigma_Field_Subset 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:29

for X being non empty set
for S being sigma_Field_Subset 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;

theorem Th30: :: MESFUNC2:30

for A, X being set holds rng (chi A,X) c= {0. ,1. }

proof end;

definition

let A, X be set ;
:: original: chi
redefine func chi A,X -> PartFunc of X, ExtREAL ;
coherence

proof end;

end;

theorem :: MESFUNC2:31

for X being non empty set
for S being sigma_Field_Subset of X
for A being Element of S holds chi A,X is_finite

proof end;

theorem :: MESFUNC2:32

for X being non empty set
for S being sigma_Field_Subset 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 sigma_Field_Subset of X;
cluster disjoint_valued FinSequence of S;
existence

proof end;

end;

definition

let X be set ;
let S be sigma_Field_Subset of X;
mode Finite_Sep_Sequence of S is disjoint_valued FinSequence of S;

end;

theorem Th33: :: MESFUNC2:33

for X being non empty set
for S being sigma_Field_Subset 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:34

for X being non empty set
for S being sigma_Field_Subset of X
for F being Function st F is Finite_Sep_Sequence of S holds
union (rng F) in S

proof end;

definition

let X be non empty set ;
let S be sigma_Field_Subset of X;
let f be PartFunc of X, ExtREAL ;
canceled;
pred f is_simple_func_in S means :Def5: :: MESFUNC2:def 5
( f is_finite & 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 ) ) );

end;

:: deftheorem MESFUNC2:def 4 :

:: deftheorem Def5 defines is_simple_func_in MESFUNC2:def 5 :

theorem :: MESFUNC2:35

for X being non empty set
for f being PartFunc of X, ExtREAL st f is_finite holds
rng f is Subset of REAL

proof end;

theorem :: MESFUNC2:36

for X being non empty set
for S being sigma_Field_Subset 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:37

for X being non empty set
for f being PartFunc of X, ExtREAL
for S being sigma_Field_Subset of X
for A being Element of S st f is_simple_func_in S holds
f is_measurable_on A

proof end;