:: The Measurability of Complex-Valued Functional Sequences
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received December 16, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users
begin
definition
let
X
be non
empty
set
;
let
f
be
Functional_Sequence
of
X
,
REAL
;
func
R_EAL
f
->
Functional_Sequence
of
X
,
ExtREAL
equals
:: MESFUN7C:def 1
f
;
coherence
f
is
Functional_Sequence
of
X
,
ExtREAL
proof
end;
end;
::
deftheorem
defines
R_EAL
MESFUN7C:def 1 :
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
REAL
holds
R_EAL
f
=
f
;
theorem
Th1
:
:: MESFUN7C:1
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
REAL
for
x
being
Element
of
X
holds
f
#
x
=
(
R_EAL
f
)
#
x
proof
end;
registration
let
X
be non
empty
set
;
let
f
be
Function
of
X
,
REAL
;
cluster
R_EAL
f
->
total
;
coherence
R_EAL
f
is
total
;
end;
definition
let
X
be non
empty
set
;
let
f
be
Functional_Sequence
of
X
,
REAL
;
func
inf
f
->
PartFunc
of
X
,
ExtREAL
equals
:: MESFUN7C:def 2
inf
(
R_EAL
f
)
;
coherence
inf
(
R_EAL
f
)
is
PartFunc
of
X
,
ExtREAL
;
end;
::
deftheorem
defines
inf
MESFUN7C:def 2 :
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
REAL
holds
inf
f
=
inf
(
R_EAL
f
)
;
theorem
Th2
:
:: MESFUN7C:2
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
REAL
for
x
being
Element
of
X
st
x
in
dom
(
inf
f
)
holds
(
inf
f
)
.
x
=
inf
(
rng
(
R_EAL
(
f
#
x
)
)
)
proof
end;
definition
let
X
be non
empty
set
;
let
f
be
Functional_Sequence
of
X
,
REAL
;
func
sup
f
->
PartFunc
of
X
,
ExtREAL
equals
:: MESFUN7C:def 3
sup
(
R_EAL
f
)
;
coherence
sup
(
R_EAL
f
)
is
PartFunc
of
X
,
ExtREAL
;
end;
::
deftheorem
defines
sup
MESFUN7C:def 3 :
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
REAL
holds
sup
f
=
sup
(
R_EAL
f
)
;
theorem
Th3
:
:: MESFUN7C:3
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
REAL
for
x
being
Element
of
X
st
x
in
dom
(
sup
f
)
holds
(
sup
f
)
.
x
=
sup
(
rng
(
R_EAL
(
f
#
x
)
)
)
proof
end;
definition
let
X
be non
empty
set
;
let
f
be
Functional_Sequence
of
X
,
REAL
;
func
inferior_realsequence
f
->
with_the_same_dom
Functional_Sequence
of
X
,
ExtREAL
equals
:: MESFUN7C:def 4
inferior_realsequence
(
R_EAL
f
)
;
coherence
inferior_realsequence
(
R_EAL
f
)
is
with_the_same_dom
Functional_Sequence
of
X
,
ExtREAL
;
end;
::
deftheorem
defines
inferior_realsequence
MESFUN7C:def 4 :
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
REAL
holds
inferior_realsequence
f
=
inferior_realsequence
(
R_EAL
f
)
;
theorem
Th4
:
:: MESFUN7C:4
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
REAL
for
n
being
Nat
holds
(
dom
(
(
inferior_realsequence
f
)
.
n
)
=
dom
(
f
.
0
)
& ( for
x
being
Element
of
X
st
x
in
dom
(
(
inferior_realsequence
f
)
.
n
)
holds
(
(
inferior_realsequence
f
)
.
n
)
.
x
=
(
inferior_realsequence
(
R_EAL
(
f
#
x
)
)
)
.
n
) )
proof
end;
definition
let
X
be non
empty
set
;
let
f
be
Functional_Sequence
of
X
,
REAL
;
func
superior_realsequence
f
->
with_the_same_dom
Functional_Sequence
of
X
,
ExtREAL
equals
:: MESFUN7C:def 5
superior_realsequence
(
R_EAL
f
)
;
coherence
superior_realsequence
(
R_EAL
f
)
is
with_the_same_dom
Functional_Sequence
of
X
,
ExtREAL
;
end;
::
deftheorem
defines
superior_realsequence
MESFUN7C:def 5 :
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
REAL
holds
superior_realsequence
f
=
superior_realsequence
(
R_EAL
f
)
;
theorem
Th5
:
:: MESFUN7C:5
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
REAL
for
n
being
Nat
holds
(
dom
(
(
superior_realsequence
f
)
.
n
)
=
dom
(
f
.
0
)
& ( for
x
being
Element
of
X
st
x
in
dom
(
(
superior_realsequence
f
)
.
n
)
holds
(
(
superior_realsequence
f
)
.
n
)
.
x
=
(
superior_realsequence
(
R_EAL
(
f
#
x
)
)
)
.
n
) )
proof
end;
theorem
:: MESFUN7C:6
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
REAL
for
x
being
Element
of
X
st
x
in
dom
(
f
.
0
)
holds
(
inferior_realsequence
f
)
#
x
=
inferior_realsequence
(
R_EAL
(
f
#
x
)
)
proof
end;
registration
let
X
be non
empty
set
;
let
f
be
with_the_same_dom
Functional_Sequence
of
X
,
REAL
;
cluster
R_EAL
f
->
with_the_same_dom
;
coherence
R_EAL
f
is
with_the_same_dom
proof
end;
end;
theorem
Th7
:
:: MESFUN7C:7
for
X
being non
empty
set
for
f
being
with_the_same_dom
Functional_Sequence
of
X
,
REAL
for
S
being
SigmaField
of
X
for
E
being
Element
of
S
for
n
being
Nat
st
f
.
n
is_measurable_on
E
holds
(
R_EAL
f
)
.
n
is_measurable_on
E
proof
end;
theorem
:: MESFUN7C:8
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
REAL
for
n
being
Nat
holds
(
R_EAL
f
)
^\
n
=
R_EAL
(
f
^\
n
)
;
theorem
:: MESFUN7C:9
for
X
being non
empty
set
for
f
being
with_the_same_dom
Functional_Sequence
of
X
,
REAL
for
n
being
Nat
holds
(
inferior_realsequence
f
)
.
n
=
inf
(
f
^\
n
)
proof
end;
theorem
:: MESFUN7C:10
for
X
being non
empty
set
for
f
being
with_the_same_dom
Functional_Sequence
of
X
,
REAL
for
n
being
Nat
holds
(
superior_realsequence
f
)
.
n
=
sup
(
f
^\
n
)
proof
end;
theorem
Th11
:
:: MESFUN7C:11
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
REAL
for
x
being
Element
of
X
st
x
in
dom
(
f
.
0
)
holds
(
superior_realsequence
f
)
#
x
=
superior_realsequence
(
R_EAL
(
f
#
x
)
)
proof
end;
definition
let
X
be non
empty
set
;
let
f
be
Functional_Sequence
of
X
,
REAL
;
func
lim_inf
f
->
PartFunc
of
X
,
ExtREAL
equals
:: MESFUN7C:def 6
lim_inf
(
R_EAL
f
)
;
coherence
lim_inf
(
R_EAL
f
)
is
PartFunc
of
X
,
ExtREAL
;
end;
::
deftheorem
defines
lim_inf
MESFUN7C:def 6 :
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
REAL
holds
lim_inf
f
=
lim_inf
(
R_EAL
f
)
;
theorem
Th12
:
:: MESFUN7C:12
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
REAL
for
x
being
Element
of
X
st
x
in
dom
(
lim_inf
f
)
holds
(
lim_inf
f
)
.
x
=
lim_inf
(
R_EAL
(
f
#
x
)
)
proof
end;
definition
let
X
be non
empty
set
;
let
f
be
Functional_Sequence
of
X
,
REAL
;
func
lim_sup
f
->
PartFunc
of
X
,
ExtREAL
equals
:: MESFUN7C:def 7
lim_sup
(
R_EAL
f
)
;
coherence
lim_sup
(
R_EAL
f
)
is
PartFunc
of
X
,
ExtREAL
;
end;
::
deftheorem
defines
lim_sup
MESFUN7C:def 7 :
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
REAL
holds
lim_sup
f
=
lim_sup
(
R_EAL
f
)
;
theorem
Th13
:
:: MESFUN7C:13
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
REAL
for
x
being
Element
of
X
st
x
in
dom
(
lim_sup
f
)
holds
(
lim_sup
f
)
.
x
=
lim_sup
(
R_EAL
(
f
#
x
)
)
proof
end;
definition
let
X
be non
empty
set
;
let
f
be
Functional_Sequence
of
X
,
REAL
;
func
lim
f
->
PartFunc
of
X
,
ExtREAL
equals
:: MESFUN7C:def 8
lim
(
R_EAL
f
)
;
coherence
lim
(
R_EAL
f
)
is
PartFunc
of
X
,
ExtREAL
;
end;
::
deftheorem
defines
lim
MESFUN7C:def 8 :
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
REAL
holds
lim
f
=
lim
(
R_EAL
f
)
;
theorem
Th14
:
:: MESFUN7C:14
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
REAL
for
x
being
Element
of
X
st
x
in
dom
(
lim
f
)
holds
(
lim
f
)
.
x
=
lim
(
R_EAL
(
f
#
x
)
)
proof
end;
theorem
Th15
:
:: MESFUN7C:15
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
REAL
for
x
being
Element
of
X
st
x
in
dom
(
lim
f
)
&
f
#
x
is
convergent
holds
(
(
lim
f
)
.
x
=
(
lim_sup
f
)
.
x
&
(
lim
f
)
.
x
=
(
lim_inf
f
)
.
x
)
proof
end;
theorem
:: MESFUN7C:16
for
X
being non
empty
set
for
S
being
SigmaField
of
X
for
f
being
with_the_same_dom
Functional_Sequence
of
X
,
REAL
for
F
being
SetSequence
of
S
for
r
being
real
number
st ( for
n
being
Nat
holds
F
.
n
=
(
dom
(
f
.
0
)
)
/\
(
great_dom
(
(
f
.
n
)
,
r
)
)
) holds
union
(
rng
F
)
=
(
dom
(
f
.
0
)
)
/\
(
great_dom
(
(
sup
f
)
,
r
)
)
proof
end;
theorem
:: MESFUN7C:17
for
X
being non
empty
set
for
S
being
SigmaField
of
X
for
f
being
with_the_same_dom
Functional_Sequence
of
X
,
REAL
for
F
being
SetSequence
of
S
for
r
being
real
number
st ( for
n
being
Nat
holds
F
.
n
=
(
dom
(
f
.
0
)
)
/\
(
great_eq_dom
(
(
f
.
n
)
,
r
)
)
) holds
meet
(
rng
F
)
=
(
dom
(
f
.
0
)
)
/\
(
great_eq_dom
(
(
inf
f
)
,
r
)
)
proof
end;
theorem
Th18
:
:: MESFUN7C:18
for
X
being non
empty
set
for
S
being
SigmaField
of
X
for
f
being
with_the_same_dom
Functional_Sequence
of
X
,
REAL
for
E
being
Element
of
S
st
dom
(
f
.
0
)
=
E
& ( for
n
being
Nat
holds
f
.
n
is_measurable_on
E
) holds
lim_sup
f
is_measurable_on
E
proof
end;
theorem
:: MESFUN7C:19
for
X
being non
empty
set
for
S
being
SigmaField
of
X
for
f
being
with_the_same_dom
Functional_Sequence
of
X
,
REAL
for
E
being
Element
of
S
st
dom
(
f
.
0
)
=
E
& ( for
n
being
Nat
holds
f
.
n
is_measurable_on
E
) holds
lim_inf
f
is_measurable_on
E
proof
end;
theorem
:: MESFUN7C:20
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
REAL
for
x
being
Element
of
X
st
x
in
dom
(
f
.
0
)
&
f
#
x
is
convergent
holds
(
superior_realsequence
f
)
#
x
is
bounded_below
proof
end;
theorem
Th21
:
:: MESFUN7C:21
for
X
being non
empty
set
for
S
being
SigmaField
of
X
for
f
being
with_the_same_dom
Functional_Sequence
of
X
,
REAL
for
E
being
Element
of
S
st
dom
(
f
.
0
)
=
E
& ( for
n
being
Nat
holds
f
.
n
is_measurable_on
E
) & ( for
x
being
Element
of
X
st
x
in
E
holds
f
#
x
is
convergent
) holds
lim
f
is_measurable_on
E
proof
end;
theorem
Th22
:
:: MESFUN7C:22
for
X
being non
empty
set
for
S
being
SigmaField
of
X
for
f
being
with_the_same_dom
Functional_Sequence
of
X
,
REAL
for
g
being
PartFunc
of
X
,
ExtREAL
for
E
being
Element
of
S
st
dom
(
f
.
0
)
=
E
& ( for
n
being
Nat
holds
f
.
n
is_measurable_on
E
) &
dom
g
=
E
& ( for
x
being
Element
of
X
st
x
in
E
holds
(
f
#
x
is
convergent
&
g
.
x
=
lim
(
f
#
x
)
) ) holds
g
is_measurable_on
E
proof
end;
begin
definition
let
X
be non
empty
set
;
let
H
be
Functional_Sequence
of
X
,
COMPLEX
;
let
x
be
Element
of
X
;
func
H
#
x
->
Complex_Sequence
means
:
Def9
:
:: MESFUN7C:def 9
for
n
being
Nat
holds
it
.
n
=
(
H
.
n
)
.
x
;
existence
ex
b
1
being
Complex_Sequence
st
for
n
being
Nat
holds
b
1
.
n
=
(
H
.
n
)
.
x
proof
end;
uniqueness
for
b
1
,
b
2
being
Complex_Sequence
st ( for
n
being
Nat
holds
b
1
.
n
=
(
H
.
n
)
.
x
) & ( for
n
being
Nat
holds
b
2
.
n
=
(
H
.
n
)
.
x
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def9
defines
#
MESFUN7C:def 9 :
for
X
being non
empty
set
for
H
being
Functional_Sequence
of
X
,
COMPLEX
for
x
being
Element
of
X
for
b
4
being
Complex_Sequence
holds
(
b
4
=
H
#
x
iff for
n
being
Nat
holds
b
4
.
n
=
(
H
.
n
)
.
x
);
definition
let
X
be non
empty
set
;
let
f
be
Functional_Sequence
of
X
,
COMPLEX
;
func
lim
f
->
PartFunc
of
X
,
COMPLEX
means
:
Def10
:
:: MESFUN7C:def 10
(
dom
it
=
dom
(
f
.
0
)
& ( for
x
being
Element
of
X
st
x
in
dom
it
holds
it
.
x
=
lim
(
f
#
x
)
) );
existence
ex
b
1
being
PartFunc
of
X
,
COMPLEX
st
(
dom
b
1
=
dom
(
f
.
0
)
& ( for
x
being
Element
of
X
st
x
in
dom
b
1
holds
b
1
.
x
=
lim
(
f
#
x
)
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
PartFunc
of
X
,
COMPLEX
st
dom
b
1
=
dom
(
f
.
0
)
& ( for
x
being
Element
of
X
st
x
in
dom
b
1
holds
b
1
.
x
=
lim
(
f
#
x
)
) &
dom
b
2
=
dom
(
f
.
0
)
& ( for
x
being
Element
of
X
st
x
in
dom
b
2
holds
b
2
.
x
=
lim
(
f
#
x
)
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def10
defines
lim
MESFUN7C:def 10 :
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
COMPLEX
for
b
3
being
PartFunc
of
X
,
COMPLEX
holds
(
b
3
=
lim
f
iff (
dom
b
3
=
dom
(
f
.
0
)
& ( for
x
being
Element
of
X
st
x
in
dom
b
3
holds
b
3
.
x
=
lim
(
f
#
x
)
) ) );
definition
let
X
be non
empty
set
;
let
f
be
Functional_Sequence
of
X
,
COMPLEX
;
func
Re
f
->
Functional_Sequence
of
X
,
REAL
means
:
Def11
:
:: MESFUN7C:def 11
for
n
being
Nat
holds
(
dom
(
it
.
n
)
=
dom
(
f
.
n
)
& ( for
x
being
Element
of
X
st
x
in
dom
(
it
.
n
)
holds
(
it
.
n
)
.
x
=
(
Re
(
f
#
x
)
)
.
n
) );
existence
ex
b
1
being
Functional_Sequence
of
X
,
REAL
st
for
n
being
Nat
holds
(
dom
(
b
1
.
n
)
=
dom
(
f
.
n
)
& ( for
x
being
Element
of
X
st
x
in
dom
(
b
1
.
n
)
holds
(
b
1
.
n
)
.
x
=
(
Re
(
f
#
x
)
)
.
n
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Functional_Sequence
of
X
,
REAL
st ( for
n
being
Nat
holds
(
dom
(
b
1
.
n
)
=
dom
(
f
.
n
)
& ( for
x
being
Element
of
X
st
x
in
dom
(
b
1
.
n
)
holds
(
b
1
.
n
)
.
x
=
(
Re
(
f
#
x
)
)
.
n
) ) ) & ( for
n
being
Nat
holds
(
dom
(
b
2
.
n
)
=
dom
(
f
.
n
)
& ( for
x
being
Element
of
X
st
x
in
dom
(
b
2
.
n
)
holds
(
b
2
.
n
)
.
x
=
(
Re
(
f
#
x
)
)
.
n
) ) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def11
defines
Re
MESFUN7C:def 11 :
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
COMPLEX
for
b
3
being
Functional_Sequence
of
X
,
REAL
holds
(
b
3
=
Re
f
iff for
n
being
Nat
holds
(
dom
(
b
3
.
n
)
=
dom
(
f
.
n
)
& ( for
x
being
Element
of
X
st
x
in
dom
(
b
3
.
n
)
holds
(
b
3
.
n
)
.
x
=
(
Re
(
f
#
x
)
)
.
n
) ) );
registration
let
X
be non
empty
set
;
let
f
be
with_the_same_dom
Functional_Sequence
of
X
,
COMPLEX
;
cluster
Re
f
->
with_the_same_dom
;
correctness
coherence
Re
f
is
with_the_same_dom
;
proof
end;
end;
definition
let
X
be non
empty
set
;
let
f
be
Functional_Sequence
of
X
,
COMPLEX
;
func
Im
f
->
Functional_Sequence
of
X
,
REAL
means
:
Def12
:
:: MESFUN7C:def 12
for
n
being
Nat
holds
(
dom
(
it
.
n
)
=
dom
(
f
.
n
)
& ( for
x
being
Element
of
X
st
x
in
dom
(
it
.
n
)
holds
(
it
.
n
)
.
x
=
(
Im
(
f
#
x
)
)
.
n
) );
existence
ex
b
1
being
Functional_Sequence
of
X
,
REAL
st
for
n
being
Nat
holds
(
dom
(
b
1
.
n
)
=
dom
(
f
.
n
)
& ( for
x
being
Element
of
X
st
x
in
dom
(
b
1
.
n
)
holds
(
b
1
.
n
)
.
x
=
(
Im
(
f
#
x
)
)
.
n
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
Functional_Sequence
of
X
,
REAL
st ( for
n
being
Nat
holds
(
dom
(
b
1
.
n
)
=
dom
(
f
.
n
)
& ( for
x
being
Element
of
X
st
x
in
dom
(
b
1
.
n
)
holds
(
b
1
.
n
)
.
x
=
(
Im
(
f
#
x
)
)
.
n
) ) ) & ( for
n
being
Nat
holds
(
dom
(
b
2
.
n
)
=
dom
(
f
.
n
)
& ( for
x
being
Element
of
X
st
x
in
dom
(
b
2
.
n
)
holds
(
b
2
.
n
)
.
x
=
(
Im
(
f
#
x
)
)
.
n
) ) ) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def12
defines
Im
MESFUN7C:def 12 :
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
COMPLEX
for
b
3
being
Functional_Sequence
of
X
,
REAL
holds
(
b
3
=
Im
f
iff for
n
being
Nat
holds
(
dom
(
b
3
.
n
)
=
dom
(
f
.
n
)
& ( for
x
being
Element
of
X
st
x
in
dom
(
b
3
.
n
)
holds
(
b
3
.
n
)
.
x
=
(
Im
(
f
#
x
)
)
.
n
) ) );
registration
let
X
be non
empty
set
;
let
f
be
with_the_same_dom
Functional_Sequence
of
X
,
COMPLEX
;
cluster
Im
f
->
with_the_same_dom
;
correctness
coherence
Im
f
is
with_the_same_dom
;
proof
end;
end;
theorem
Th23
:
:: MESFUN7C:23
for
X
being non
empty
set
for
f
being
with_the_same_dom
Functional_Sequence
of
X
,
COMPLEX
for
x
being
Element
of
X
st
x
in
dom
(
f
.
0
)
holds
(
(
Re
f
)
#
x
=
Re
(
f
#
x
)
&
(
Im
f
)
#
x
=
Im
(
f
#
x
)
)
proof
end;
theorem
Th24
:
:: MESFUN7C:24
for
X
being non
empty
set
for
f
being
Functional_Sequence
of
X
,
COMPLEX
for
n
being
Nat
holds
(
(
Re
f
)
.
n
=
Re
(
f
.
n
)
&
(
Im
f
)
.
n
=
Im
(
f
.
n
)
)
proof
end;
theorem
Th25
:
:: MESFUN7C:25
for
X
being non
empty
set
for
f
being
with_the_same_dom
Functional_Sequence
of
X
,
COMPLEX
st ( for
x
being
Element
of
X
st
x
in
dom
(
f
.
0
)
holds
f
#
x
is
convergent
) holds
(
lim
(
Re
f
)
=
Re
(
lim
f
)
&
lim
(
Im
f
)
=
Im
(
lim
f
)
)
proof
end;
theorem
:: MESFUN7C:26
for
X
being non
empty
set
for
S
being
SigmaField
of
X
for
f
being
with_the_same_dom
Functional_Sequence
of
X
,
COMPLEX
for
E
being
Element
of
S
st
dom
(
f
.
0
)
=
E
& ( for
n
being
Nat
holds
f
.
n
is_measurable_on
E
) & ( for
x
being
Element
of
X
st
x
in
E
holds
f
#
x
is
convergent
) holds
lim
f
is_measurable_on
E
proof
end;
theorem
:: MESFUN7C:27
for
X
being non
empty
set
for
S
being
SigmaField
of
X
for
f
being
with_the_same_dom
Functional_Sequence
of
X
,
COMPLEX
for
g
being
PartFunc
of
X
,
COMPLEX
for
E
being
Element
of
S
st
dom
(
f
.
0
)
=
E
& ( for
n
being
Nat
holds
f
.
n
is_measurable_on
E
) &
dom
g
=
E
& ( for
x
being
Element
of
X
st
x
in
E
holds
(
f
#
x
is
convergent
&
g
.
x
=
lim
(
f
#
x
)
) ) holds
g
is_measurable_on
E
proof
end;
begin
theorem
:: MESFUN7C:28
for
X
being non
empty
set
for
Y
being
set
for
f
being
PartFunc
of
X
,
COMPLEX
for
r
being
Real
holds
(
r
(#)
f
)
|
Y
=
r
(#)
(
f
|
Y
)
proof
end;
Lm1
:
for
X
being non
empty
set
for
f
being
PartFunc
of
X
,
COMPLEX
holds
|.
f
.|
is
nonnegative
proof
end;
theorem
:: MESFUN7C:29
for
X
being non
empty
set
for
S
being
SigmaField
of
X
for
f
being
PartFunc
of
X
,
COMPLEX
for
k
being
real
number
for
E
being
Element
of
S
st
0
<=
k
&
E
c=
dom
f
&
f
is_measurable_on
E
holds
|.
f
.|
to_power
k
is_measurable_on
E
proof
end;
theorem
Th30
:
:: MESFUN7C:30
for
X
being non
empty
set
for
f
,
g
being
PartFunc
of
X
,
REAL
holds
(
R_EAL
f
)
(#)
(
R_EAL
g
)
=
R_EAL
(
f
(#)
g
)
proof
end;
theorem
Th31
:
:: MESFUN7C:31
for
X
being non
empty
set
for
S
being
SigmaField
of
X
for
E
being
Element
of
S
for
f
,
g
being
PartFunc
of
X
,
REAL
st
(
dom
f
)
/\
(
dom
g
)
=
E
&
f
is_measurable_on
E
&
g
is_measurable_on
E
holds
f
(#)
g
is_measurable_on
E
proof
end;
theorem
Th32
:
:: MESFUN7C:32
for
X
being non
empty
set
for
f
,
g
being
PartFunc
of
X
,
COMPLEX
holds
(
Re
(
f
(#)
g
)
=
(
(
Re
f
)
(#)
(
Re
g
)
)
-
(
(
Im
f
)
(#)
(
Im
g
)
)
&
Im
(
f
(#)
g
)
=
(
(
Im
f
)
(#)
(
Re
g
)
)
+
(
(
Re
f
)
(#)
(
Im
g
)
)
)
proof
end;
theorem
:: MESFUN7C:33
for
X
being non
empty
set
for
S
being
SigmaField
of
X
for
f
,
g
being
PartFunc
of
X
,
COMPLEX
for
E
being
Element
of
S
st
(
dom
f
)
/\
(
dom
g
)
=
E
&
f
is_measurable_on
E
&
g
is_measurable_on
E
holds
f
(#)
g
is_measurable_on
E
proof
end;
theorem
Th34
:
:: MESFUN7C:34
for
X
being non
empty
set
for
S
being
SigmaField
of
X
for
M
being
sigma_Measure
of
S
for
f
,
g
being
PartFunc
of
X
,
REAL
st ex
E
being
Element
of
S
st
(
E
=
dom
f
&
E
=
dom
g
&
f
is_measurable_on
E
&
g
is_measurable_on
E
) &
f
is
nonnegative
&
g
is
nonnegative
& ( for
x
being
Element
of
X
st
x
in
dom
g
holds
g
.
x
<=
f
.
x
) holds
Integral
(
M
,
g
)
<=
Integral
(
M
,
f
)
proof
end;
theorem
Th35
:
:: MESFUN7C:35
for
X
being non
empty
set
for
S
being
SigmaField
of
X
for
M
being
sigma_Measure
of
S
for
f
being
PartFunc
of
X
,
COMPLEX
st
f
is_integrable_on
M
holds
( ex
A
being
Element
of
S
st
(
A
=
dom
f
&
f
is_measurable_on
A
) &
|.
f
.|
is_integrable_on
M
)
proof
end;
theorem
:: MESFUN7C:36
for
X
being non
empty
set
for
S
being
SigmaField
of
X
for
M
being
sigma_Measure
of
S
for
f
being
PartFunc
of
X
,
COMPLEX
st
f
is_integrable_on
M
holds
ex
F
being
Function
of
NAT
,
S
st
( ( for
n
being
Nat
holds
F
.
n
=
(
dom
f
)
/\
(
great_eq_dom
(
|.
f
.|
,
(
R_EAL
(
1
/
(
n
+
1
)
)
)
)
)
) &
(
dom
f
)
\
(
eq_dom
(
|.
f
.|
,
0
)
)
=
union
(
rng
F
)
& ( for
n
being
Nat
holds
(
F
.
n
in
S
&
M
.
(
F
.
n
)
<
+infty
) ) )
proof
end;
theorem
Th37
:
:: MESFUN7C:37
for
X
being non
empty
set
for
f
being
PartFunc
of
X
,
COMPLEX
for
A
being
set
holds
|.
f
.|
|
A
=
|.
(
f
|
A
)
.|
proof
end;
theorem
Th38
:
:: MESFUN7C:38
for
X
being non
empty
set
for
f
,
g
being
PartFunc
of
X
,
COMPLEX
holds
(
dom
(
|.
f
.|
+
|.
g
.|
)
=
(
dom
f
)
/\
(
dom
g
)
&
dom
|.
(
f
+
g
)
.|
c=
dom
|.
f
.|
)
proof
end;
theorem
Th39
:
:: MESFUN7C:39
for
X
being non
empty
set
for
f
,
g
being
PartFunc
of
X
,
COMPLEX
holds
(
|.
f
.|
|
(
dom
|.
(
f
+
g
)
.|
)
)
+
(
|.
g
.|
|
(
dom
|.
(
f
+
g
)
.|
)
)
=
(
|.
f
.|
+
|.
g
.|
)
|
(
dom
|.
(
f
+
g
)
.|
)
proof
end;
theorem
Th40
:
:: MESFUN7C:40
for
X
being non
empty
set
for
f
,
g
being
PartFunc
of
X
,
COMPLEX
for
x
being
set
st
x
in
dom
|.
(
f
+
g
)
.|
holds
|.
(
f
+
g
)
.|
.
x
<=
(
|.
f
.|
+
|.
g
.|
)
.
x
proof
end;
theorem
Th41
:
:: MESFUN7C:41
for
X
being non
empty
set
for
f
,
g
being
PartFunc
of
X
,
REAL
st ( for
x
being
set
st
x
in
dom
f
holds
f
.
x
<=
g
.
x
) holds
g
-
f
is
nonnegative
proof
end;
theorem
:: MESFUN7C:42
for
X
being non
empty
set
for
S
being
SigmaField
of
X
for
M
being
sigma_Measure
of
S
for
f
,
g
being
PartFunc
of
X
,
COMPLEX
st
f
is_integrable_on
M
&
g
is_integrable_on
M
holds
ex
E
being
Element
of
S
st
(
E
=
dom
(
f
+
g
)
&
Integral
(
M
,
(
|.
(
f
+
g
)
.|
|
E
)
)
<=
(
Integral
(
M
,
(
|.
f
.|
|
E
)
)
)
+
(
Integral
(
M
,
(
|.
g
.|
|
E
)
)
)
)
proof
end;
begin
definition
let
X
be non
empty
set
;
let
S
be
SigmaField
of
X
;
let
f
be
PartFunc
of
X
,
COMPLEX
;
pred
f
is_simple_func_in
S
means
:
Def13
:
:: MESFUN7C:def 13
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
Def13
defines
is_simple_func_in
MESFUN7C:def 13 :
for
X
being non
empty
set
for
S
being
SigmaField
of
X
for
f
being
PartFunc
of
X
,
COMPLEX
holds
(
f
is_simple_func_in
S
iff 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
) ) );
definition
let
X
be non
empty
set
;
let
S
be
SigmaField
of
X
;
let
f
be
PartFunc
of
X
,
REAL
;
let
F
be
Finite_Sep_Sequence
of
S
;
let
a
be
FinSequence
of
REAL
;
pred
F
,
a
are_Re-presentation_of
f
means
:
Def14
:
:: MESFUN7C:def 14
(
dom
f
=
union
(
rng
F
)
&
dom
F
=
dom
a
& ( for
n
being
Nat
st
n
in
dom
F
holds
for
x
being
set
st
x
in
F
.
n
holds
f
.
x
=
a
.
n
) );
end;
::
deftheorem
Def14
defines
are_Re-presentation_of
MESFUN7C:def 14 :
for
X
being non
empty
set
for
S
being
SigmaField
of
X
for
f
being
PartFunc
of
X
,
REAL
for
F
being
Finite_Sep_Sequence
of
S
for
a
being
FinSequence
of
REAL
holds
(
F
,
a
are_Re-presentation_of
f
iff (
dom
f
=
union
(
rng
F
)
&
dom
F
=
dom
a
& ( for
n
being
Nat
st
n
in
dom
F
holds
for
x
being
set
st
x
in
F
.
n
holds
f
.
x
=
a
.
n
) ) );
definition
let
X
be non
empty
set
;
let
S
be
SigmaField
of
X
;
let
f
be
PartFunc
of
X
,
COMPLEX
;
let
F
be
Finite_Sep_Sequence
of
S
;
let
a
be
FinSequence
of
COMPLEX
;
pred
F
,
a
are_Re-presentation_of
f
means
:
Def15
:
:: MESFUN7C:def 15
(
dom
f
=
union
(
rng
F
)
&
dom
F
=
dom
a
& ( for
n
being
Nat
st
n
in
dom
F
holds
for
x
being
set
st
x
in
F
.
n
holds
f
.
x
=
a
.
n
) );
end;
::
deftheorem
Def15
defines
are_Re-presentation_of
MESFUN7C:def 15 :
for
X
being non
empty
set
for
S
being
SigmaField
of
X
for
f
being
PartFunc
of
X
,
COMPLEX
for
F
being
Finite_Sep_Sequence
of
S
for
a
being
FinSequence
of
COMPLEX
holds
(
F
,
a
are_Re-presentation_of
f
iff (
dom
f
=
union
(
rng
F
)
&
dom
F
=
dom
a
& ( for
n
being
Nat
st
n
in
dom
F
holds
for
x
being
set
st
x
in
F
.
n
holds
f
.
x
=
a
.
n
) ) );
theorem
:: MESFUN7C:43
for
X
being non
empty
set
for
S
being
SigmaField
of
X
for
f
being
PartFunc
of
X
,
COMPLEX
holds
(
f
is_simple_func_in
S
iff (
Re
f
is_simple_func_in
S
&
Im
f
is_simple_func_in
S
) )
proof
end;
theorem
Th44
:
:: MESFUN7C:44
for
X
being non
empty
set
for
S
being
SigmaField
of
X
for
f
being
PartFunc
of
X
,
COMPLEX
st
f
is_simple_func_in
S
holds
ex
F
being
Finite_Sep_Sequence
of
S
ex
a
being
FinSequence
of
COMPLEX
st
(
dom
f
=
union
(
rng
F
)
&
dom
F
=
dom
a
& ( for
n
being
Nat
st
n
in
dom
F
holds
for
x
being
set
st
x
in
F
.
n
holds
f
.
x
=
a
.
n
) )
proof
end;
theorem
Th45
:
:: MESFUN7C:45
for
X
being non
empty
set
for
S
being
SigmaField
of
X
for
f
being
PartFunc
of
X
,
COMPLEX
holds
(
f
is_simple_func_in
S
iff ex
F
being
Finite_Sep_Sequence
of
S
ex
a
being
FinSequence
of
COMPLEX
st
F
,
a
are_Re-presentation_of
f
)
proof
end;
theorem
Th46
:
:: MESFUN7C:46
for
c
being
FinSequence
of
COMPLEX
for
n
being
Nat
st
n
in
dom
(
Re
c
)
holds
(
Re
c
)
.
n
=
Re
(
c
.
n
)
proof
end;
theorem
Th47
:
:: MESFUN7C:47
for
c
being
FinSequence
of
COMPLEX
for
n
being
Nat
st
n
in
dom
(
Im
c
)
holds
(
Im
c
)
.
n
=
Im
(
c
.
n
)
proof
end;
theorem
Th48
:
:: MESFUN7C:48
for
X
being non
empty
set
for
S
being
SigmaField
of
X
for
f
being
PartFunc
of
X
,
COMPLEX
for
F
being
Finite_Sep_Sequence
of
S
for
a
being
FinSequence
of
COMPLEX
holds
(
F
,
a
are_Re-presentation_of
f
iff (
F
,
Re
a
are_Re-presentation_of
Re
f
&
F
,
Im
a
are_Re-presentation_of
Im
f
) )
proof
end;
theorem
:: MESFUN7C:49
for
X
being non
empty
set
for
S
being
SigmaField
of
X
for
f
being
PartFunc
of
X
,
COMPLEX
holds
(
f
is_simple_func_in
S
iff ex
F
being
Finite_Sep_Sequence
of
S
ex
c
being
FinSequence
of
COMPLEX
st
(
dom
f
=
union
(
rng
F
)
&
dom
F
=
dom
c
& ( for
n
being
Nat
st
n
in
dom
F
holds
for
x
being
set
st
x
in
F
.
n
holds
(
Re
f
)
.
x
=
(
Re
c
)
.
n
) & ( for
n
being
Nat
st
n
in
dom
F
holds
for
x
being
set
st
x
in
F
.
n
holds
(
Im
f
)
.
x
=
(
Im
c
)
.
n
) ) )
proof
end;