:: 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 H1( 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 b1 being PartFunc of C,ExtREAL st
( dom b1 = dom f & ( for x being Element of C st x in dom b1 holds
b1 . x = max ((f . x),0.) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of C,ExtREAL st dom b1 = dom f & ( for x being Element of C st x in dom b1 holds
b1 . x = max ((f . x),0.) ) & dom b2 = dom f & ( for x being Element of C st x in dom b2 holds
b2 . x = max ((f . x),0.) ) holds
b1 = b2
proof end;
deffunc H2( 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 b1 being PartFunc of C,ExtREAL st
( dom b1 = dom f & ( for x being Element of C st x in dom b1 holds
b1 . x = max ((- (f . x)),0.) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of C,ExtREAL st dom b1 = dom f & ( for x being Element of C st x in dom b1 holds
b1 . x = max ((- (f . x)),0.) ) & dom b2 = dom f & ( for x being Element of C st x in dom b2 holds
b2 . x = max ((- (f . x)),0.) ) holds
b1 = b2
proof end;
end;

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

:: deftheorem Def3 defines max- MESFUNC2:def 3 :
for C being non empty set
for f, b3 being PartFunc of C,ExtREAL holds
( b3 = max- f iff ( dom b3 = dom f & ( for x being Element of C st x in dom b3 holds
b3 . 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 b1 being FinSequence of S st b1 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;