1. The Measurability of Real-Valued Functions
FORMALIZED MATHEMATICS
Volume14,Number4,Pages143–152
University of Bia l ystok,2006
Integral of Real-Valued
Measurable Function1
Yasunari Shidama Shinshu University Nagano,Japan
Noboru Endou
Gifu National College of Technology
Gifu,Japan
Summary.Based on[16],authors formalized the integral of an extended real valued measurable function in[12]before.However,the integral argued in
[12]cannot be applied to real-valued functions unconditionally.Therefore,in this
article we have formalized the integral of a real-value function.
MML identi?er:MESFUNC6,version:7.8.034.75.958
The papers[25],[11],[26],[1],[23],[24],[17],[18],[8],[27],[10],[2],[19],[7],[20],
[6],[9],[3],[4],[5],[13],[14],[15],[22],[21],and[12]provide the terminology
and notation for this paper.
1.The Measurability of Real-V alued Functions
For simplicity,we follow the rules:X denotes a non empty set,Y denotes a set,S denotes aσ-?eld of subsets of X,F denotes a function from N into S,f,
g denote partial functions from X to R,A,B denote elements of S,r,s denote
real numbers,a denotes a real number,and n denotes a natural number.
Let X be a non empty set,let f be a partial function from X to R,and let a be a real number.The functor LE-dom(f,a)yields a subset of X and is de?ned as follows:
(Def.1)LE-dom(f,a)=LE-dom(R(a)).
The following three propositions are true:
(1)|R(|f|).
144yasunari shidama and noboru endou
(2)Let X be a non empty set,S be aσ-?eld of subsets of X,M be a
σ-measure on S,f be a partial function from X to
R(f),
R(f),
R(f),
R(f),
),then Y∩
n+1 GTE-dom(f,r)= rng F.
(9)If for every n holds F(n)=Y∩LE-dom(f,r+1
),then Y∩
n+1 LE-dom(f,r)= rng F.
(11)If for every n holds F(n)=Y∩GTE-dom(f,r+1
integral of real-valued (145)
Let X be a non empty set,let S be aσ-?eld of subsets of X,let f be a partial function from X to R,and let A be an element of S.We say that f is measurable on A if and only if:
(Def.6)
R(r f)=r
R(f)is?nite.
(23)R(f)+R(f?g)=R(g)and dom
R(f)∩dom R(f?g)=dom R(g)and dom R(f?g)=dom f∩dom g.
(24)For every function F from Q into S such that for every p holds F(p)=
A∩LE-dom(f,p)∩(A∩LE-dom(g,r?p))holds A∩LE-dom(f+g,r)=
rng F.
146yasunari shidama and noboru endou
(25)Suppose f is measurable on A and g is measurable on A.Then there
exists a function F from Q into S such that for every rational number p holds F(p)=A∩LE-dom(f,p)∩(A∩LE-dom(g,r?p)).
(26)If f is measurable on A and g is measurable on A,then f+g is measurable
on A.
(27)R(g)=R(?g).
(28)?R((?1)f)and?R(?f).
(29)If f is measurable on A and g is measurable on A and A?dom g,then
f?g is measurable on A.
3.Basic Properties of Real-V alued Functions,max+f and max?f
In the sequel X denotes a non empty set,f denotes a partial function from X to R,and r denotes a real number.
Next we state a number of propositions:
(30)max+(R(f))=max?(f).
(31)For every element x of X holds0≤(max+(f))(x).
(32)For every element x of X holds0≤(max?(f))(x).
(33)max?(f)=max+(?f).
(34)For every set x such that x∈dom f and0<(max+(f))(x)holds
(max?(f))(x)=0.
(35)For every set x such that x∈dom f and0<(max?(f))(x)holds
(max+(f))(x)=0.
(36)dom f=dom(max+(f)?max?(f))and dom f=dom(max+(f)+
max?(f)).
(37)For every set x such that x∈dom f holds(max+(f))(x)=f(x)or
(max+(f))(x)=0but(max?(f))(x)=?f(x)or(max?(f))(x)=0. (38)For every set x such that x∈dom f and(max+(f))(x)=f(x)holds
(max?(f))(x)=0.
(39)For every set x such that x∈dom f and(max+(f))(x)=0holds
(max?(f))(x)=?f(x).
(40)For every set x such that x∈dom f and(max?(f))(x)=?f(x)holds
(max+(f))(x)=0.
(41)For every set x such that x∈dom f and(max?(f))(x)=0holds
(max+(f))(x)=f(x).
(42)f=max+(f)?max?(f).
(43)|r|=|
R(|f|)=|
integral of real-valued (147)
(45)|f|=max+(f)+max?(f).
4.The Measurability of max+f,max?f and|f|
In the sequel X denotes a non empty set,S denotes aσ-?eld of subsets of X,f denotes a partial function from X to R,and A denotes an element of S.
The following propositions are true:
(46)If f is measurable on A,then max+(f)is measurable on A.
(47)If f is measurable on A and A?dom f,then max?(f)is measurable on
A.
(48)If f is measurable on A and A?dom f,then|f|is measurable on A.
5.The Definition and the Measurability of a Real-V alued Simple
Function
For simplicity,we adopt the following rules:X is a non empty set,Y is a set,S is aσ-?eld of subsets of X,f,g,h are partial functions from X to R,A is an element of S,and r is a real number.
Let us consider X,S,f.We say that f is simple function in S if and only if the condition(Def.7)is satis?ed.
(Def.7)There exists a?nite sequence F of separated subsets of S such that
(i)dom f= rng F,and
(ii)for every natural number n and for all elements x,y of X such that n∈dom F and x∈F(n)and y∈F(n)holds f(x)=f(y).
Next we state a number of propositions:
(49)f is simple function in S i?
148yasunari shidama and noboru endou
(58)If for every set x such that x∈dom f∩dom g holds g(x)≤f(x),then
f?g is non-negative.
(59)If f is non-negative and g is non-negative and h is non-negative,then
f+g+h is non-negative.
(60)For every set x such that x∈dom(f+g+h)holds(f+g+h)(x)=
f(x)+g(x)+h(x).
(61)max+(f)is non-negative and max?(f)is non-negative.
(62)(i)dom(max+(f+g)+max?(f))=dom f∩dom g,
(ii)dom(max?(f+g)+max+(f))=dom f∩dom g,
(iii)dom(max+(f+g)+max?(f)+max?(g))=dom f∩dom g,
(iv)dom(max?(f+g)+max+(f)+max+(g))=dom f∩dom g,
(v)max+(f+g)+max?(f)is non-negative,and
(vi)max?(f+g)+max+(f)is non-negative.
(63)max+(f+g)+max?(f)+max?(g)=max?(f+g)+max+(f)+max+(g).
(64)If0≤r,then max+(r f)=r max+(f)and max?(r f)=r max?(f).
(65)If0≤r,then max+((?r)f)=r max?(f)and max?((?r)f)=
r max+(f).
(66)max+(f?Y)=max+(f)?Y and max?(f?Y)=max?(f)?Y.
(67)If Y?dom(f+g),then dom((f+g)?Y)=Y and dom(f?Y+g?Y)=Y
and(f+g)?Y=f?Y+g?Y.
(68)EQ-dom(f,r)=f?1({r}).
6.Lemmas for a Real-V alued Measurable Function and a Simple
Function
For simplicity,we use the following convention:X is a non empty set,S is aσ-?eld of subsets of X,f,g are partial functions from X to R,A,B are elements of S,and r,s are real numbers.
We now state a number of propositions:
(69)If f is measurable on A and A?dom f,then A∩GTE-dom(f,r)∩
LE-dom(f,s)is measurable on S.
(70)If f is simple function in S,then f?A is simple function in S.
(71)If f is simple function in S,then dom f is an element of S.
(72)If f is simple function in S and g is simple function in S,then f+g is
simple function in S.
(73)If f is simple function in S,then r f is simple function in S.
(74)If for every set x such that x∈dom(f?g)holds g(x)≤f(x),then f?g
is non-negative.
integral of real-valued (149)
(75)There exists a partial function f from X to R such that f is simple
function in S and dom f=A and for every set x such that x∈A holds
f(x)=r.
(76)If f is measurable on B and A=dom f∩B,then f?B is measurable on
A.
(77)If A?dom f and f is measurable on A and g is measurable on A,then
max+(f+g)+max?(f)is measurable on A.
(78)If A?dom f∩dom g and f is measurable on A and g is measurable on
A,then max?(f+g)+max+(f)is measurable on A.
(79)If dom f∈S and dom g∈S,then dom(f+g)∈S.
(80)If dom f=A,then f is measurable on B i?f is measurable on A∩B.
(81)Given an element A of S such that dom f=A.Let c be a real number
and B be an element of S.If f is measurable on B,then c f is measurable
on B.
7.The Integral of a Real-V alued Function
For simplicity,we follow the rules:X is a non empty set,S is aσ-?eld of subsets of X,M is aσ-measure on S,f,g are partial functions from X to R,r
is a real number,and E,A,B are elements of S.
Let X be a non empty set,let S be aσ-?eld of subsets of X,let M be
aσ-measure on S,and let f be a partial function from X to R.The functor f d M yields an element of
R(f)d M.
The following propositions are true:
(82)If there exists an element A of S such that A=dom f and f is measur-
able on A and f is non-negative,then f d M= +
R(f)d M and f d M= ′
150yasunari shidama and noboru endou
(88)If there exists an element E of S such that E=dom f and f is measur-
able on E and M(A)=0,then f?A d M=0.
(89)If E=dom f and f is measurable on E and M(A)=0,then f?(E\
A)d M= f d M.
Let X be a non empty set,let S be aσ-?eld of subsets of X,let M be a σ-measure on S,and let f be a partial function from X to R.We say that f is integrable on M if and only if:
(Def.9)
R(r)·M(dom f).
(98)Suppose f is integrable on M and g is integrable on M and f is non-
negative and g is non-negative.Then f+g is integrable on M.
(99)If f is integrable on M and g is integrable on M,then dom(f+g)∈S.
(100)If f is integrable on M and g is integrable on M,then f+g is integrable on M.
(101)Suppose f is integrable on M and g is integrable on M.Then there exists an element E of S such that E=dom f∩dom g and f+g d M=
f?E d M+ g?E d M.
(102)If f is integrable on M,then r f is integrable on M and r f d M=
integral of real-valued (151)
element of S.The functor B f d M yielding an element of
R(r)· B f d M.
References
[1]Grzegorz Bancerek.The ordinal numbers.Formalized Mathematics,1(1):91–96,1990.
[2]Grzegorz Bancerek and Krzysztof Hryniewiecki.Segments of natural numbers and?nite
sequences.Formalized Mathematics,1(1):107–114,1990.
[3]J′o zef Bia l as.In?mum and supremum of the set of real numbers.Measure theory.For-
malized Mathematics,2(1):163–171,1991.
[4]J′o zef Bia l as.Series of positive real numbers.Measure theory.Formalized Mathematics,
2(1):173–183,1991.
[5]J′o zef Bia l as.Theσ-additive measure theory.Formalized Mathematics,2(2):263–270,
1991.
[6]J′o zef Bia l as.Some properties of the intervals.Formalized Mathematics,5(1):21–26,1996.
[7]Czes l aw Byli′n ski.The complex numbers.Formalized Mathematics,1(3):507–513,1990.
[8]Czes l aw Byli′n ski.Functions and their basic properties.Formalized Mathematics,1(1):55–
65,1990.
[9]Czes l aw Byli′n ski.Functions from a set to a set.Formalized Mathematics,1(1):153–164,
1990.
[10]Czes l aw Byli′n ski.Partial functions.Formalized Mathematics,1(2):357–367,1990.
[11]Czes l aw Byli′n ski.Some basic properties of sets.Formalized Mathematics,1(1):47–53,
1990.
[12]Noboru Endou and Yasunari Shidama.Integral of measurable function.Formalized Math-
ematics,14(2):53–70,2006.
[13]Noboru Endou,Katsumi Wasaki,and Yasunari Shidama.Basic properties of extended
real numbers.Formalized Mathematics,9(3):491–494,2001.
[14]Noboru Endou,Katsumi Wasaki,and Yasunari Shidama.De?nitions and basic properties
of measurable functions.Formalized Mathematics,9(3):495–500,2001.
[15]Noboru Endou,Katsumi Wasaki,and Yasunari Shidama.The measurability of extended
real valued functions.Formalized Mathematics,9(3):525–529,2001.
[16]P.R.Halmos.Measure Theory.Springer-Verlag,1987.
[17]Krzysztof Hryniewiecki.Basic properties of real numbers.Formalized Mathematics,
1(1):35–40,1990.
[18]Andrzej Kondracki.Basic properties of rational numbers.Formalized Mathematics,
1(5):841–845,1990.
[19]Jaros l aw Kotowicz.Real sequences and basic operations on them.Formalized Mathemat-
ics,1(2):269–272,1990.
[20]Jaros l aw Kotowicz and Yuji Sakai.Properties of partial functions from a domain to the
set of real numbers.Formalized Mathematics,3(2):279–288,1992.
[21]Andrzej N?e dzusiak.σ-?elds and probability.Formalized Mathematics,1(2):401–407,1990.
[22]Beata Padlewska.Families of sets.Formalized Mathematics,1(1):147–152,1990.
[23]Andrzej Trybulec.Subsets of complex numbers.To appear in Formalized Mathematics.
[24]Andrzej Trybulec.Domains and their Cartesian products.Formalized Mathematics,
1(1):115–122,1990.
[25]Andrzej Trybulec.Tarski Grothendieck set theory.Formalized Mathematics,1(1):9–11,
1990.
[26]Zinaida Trybulec.Properties of subsets.Formalized Mathematics,1(1):67–71,1990.
152yasunari shidama and noboru endou
[27]Edmund Woronowicz.Relations de?ned on sets.Formalized Mathematics,1(1):181–186,
1990.
Received October27,2006