:: Measurability of Extended Real Valued Functions
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received October 6, 2000
:: Copyright (c) 2000-2011 Association of Mizar Users

begin

definition

let X be non empty set ;
let f be PartFunc of X,ExtREAL;
:: original: real-valued
redefine attr f is real-valued means :Def1: :: MESFUNC2:def 1
for x being Element of X st x in dom f holds
|.(f . x).| < +infty ;
compatibility
( f is real-valued iff for x being Element of X st x in dom f holds
|.(f . x).| < +infty )

proof end;

end;

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

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 real-valued or g is real-valued ) 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 real-valued & g is real-valued & ( 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;

begin

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 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,(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 SigmaField of X
for f, g being PartFunc of X,ExtREAL
for A being Element of S st f is real-valued & g is real-valued & 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 :: MESFUNC2:10

canceled;

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 real-valued holds
r (#) f is real-valued

proof end;

theorem :: MESFUNC2:13

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 real-valued & g is real-valued & f is_measurable_on A & g is_measurable_on A & A c= dom g holds
f - g is_measurable_on A

proof end;

begin

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
ex b₁ being PartFunc of C,ExtREAL st
( dom b₁ = dom f & ( for x being Element of C st x in dom b₁ holds
b₁ . x = max ((f . x),0.) ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of C,ExtREAL st dom b₁ = dom f & ( for x being Element of C st x in dom b₁ holds
b₁ . x = max ((f . x),0.) ) & dom b₂ = dom f & ( for x being Element of C st x in dom b₂ holds
b₂ . x = max ((f . x),0.) ) holds
b₁ = b₂

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
ex b₁ being PartFunc of C,ExtREAL st
( dom b₁ = dom f & ( for x being Element of C st x in dom b₁ holds
b₁ . x = max ((- (f . x)),0.) ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of C,ExtREAL st dom b₁ = dom f & ( for x being Element of C st x in dom b₁ holds
b₁ . x = max ((- (f . x)),0.) ) & dom b₂ = dom f & ( for x being Element of C st x in dom b₂ holds
b₂ . x = max ((- (f . x)),0.) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines max+ MESFUNC2:def 2 :
for C being non empty set
for f, b₃ being PartFunc of C,ExtREAL holds
( b₃ = max+ f iff ( dom b₃ = dom f & ( for x being Element of C st x in dom b₃ holds
b₃ . x = max ((f . x),0.) ) ) );

:: deftheorem Def3 defines max- MESFUNC2:def 3 :
for C being non empty set
for f, b₃ being PartFunc of C,ExtREAL holds
( b₃ = max- f iff ( dom b₃ = dom f & ( for x being Element of C st x in dom b₃ holds
b₃ . x = max ((- (f . x)),0.) ) ) );

theorem Th14: :: MESFUNC2:14

for C being non empty set
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 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 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 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 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 (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 (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;

begin

theorem :: MESFUNC2:27

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

proof end;

theorem :: MESFUNC2:28

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

proof end;

theorem :: MESFUNC2:29

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

proof end;

begin

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

proof end;

end;

theorem :: MESFUNC2:30

canceled;

theorem :: MESFUNC2:31

for X being non empty set
for S being SigmaField of X
for A being Element of S holds chi (A,X) is real-valued

proof end;

theorem :: MESFUNC2:32

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

proof end;

begin

registration

let X be set ;
let S be SigmaField of X;
cluster Relation-like NAT -defined S -valued Function-like V30() FinSequence-like FinSubsequence-like disjoint_valued FinSequence of S;
existence
ex b₁ being FinSequence of S st b₁ is disjoint_valued

proof end;

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;

theorem Th33: :: MESFUNC2:33

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 = {} ) )

proof end;

theorem :: MESFUNC2:34

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

proof end;

definition

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

:: deftheorem Def5 defines is_simple_func_in MESFUNC2:def 5 :
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 real-valued & 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:35

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

proof end;

theorem :: MESFUNC2:36

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

proof end;

theorem :: MESFUNC2:37

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

proof end;