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

definition
let X be non empty set ;
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
( f is real-valued iff for x being Element of X st x in dom f holds
|.(f . x).| < +infty )
proof end;
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 );

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 ( 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)
proof end;

theorem :: MESFUNC2:4
ex F being sequence of 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 A -measurable & g is A -measurable 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 A -measurable & g is A -measurable holds
f + g is A -measurable
proof end;

theorem Th8: :: MESFUNC2:8
for C being non empty set
for f1, f2 being PartFunc of C,ExtREAL holds f1 - f2 = f1 + (- f2)
proof end;

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

theorem Th9: :: MESFUNC2:9
for C being non empty set
for f being PartFunc of C,ExtREAL holds - f = (- 1) (#) f
proof end;

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()
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 A -measurable & g is A -measurable & A c= dom g holds
f - g is A -measurable
proof end;

:: and their basic properties ::
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 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
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
proof end;

theorem :: MESFUNC2:14
for C being non empty set
for f being PartFunc of C,ExtREAL holds max- f = max+ (- f)
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.
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.
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)) )
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. ) )
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.
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)
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.
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
proof end;

theorem :: MESFUNC2:23
for C being non empty set
for f being PartFunc of C,ExtREAL holds f = (max+ f) - (max- f)
proof end;

theorem :: MESFUNC2:24
for C being non empty set
for f being PartFunc of C,ExtREAL holds |.f.| = (max+ f) + (max- f)
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 A -measurable holds
max+ f is A -measurable
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 A -measurable & A c= dom f holds
max- f is A -measurable
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 A -measurable & A c= dom f holds
|.f.| is A -measurable
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
proof end;
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()
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 B -measurable
proof end;

registration
let X be set ;
let S be SigmaField of X;
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 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 = {} ) )
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
proof end;

definition
let X be non empty set ;
let S be SigmaField of X;
let f be PartFunc of X,ExtREAL;
pred f is_simple_func_in S means :: MESFUNC2:def 4
( 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 ) ) );
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 ) ) ) );

theorem :: MESFUNC2:32
for X being non empty set
for f being PartFunc of X,ExtREAL st f is V82() holds
rng f is Subset of REAL ;

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
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 A -measurable
proof end;