:: Measurability of Extended Real Valued Functions
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received October 6, 2000
:: 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 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 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;

cluster Relation-like NAT -defined S -valued Function-like V44() FinSequence-like FinSubsequence-like disjoint_valued for 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 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;