:: Integral of Real-valued Measurable Function
:: by Yasunari Shidama and Noboru Endou
::
:: Received October 27, 2006
:: Copyright (c) 2006-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, PROB_1, FUNCT_1, PARTFUN1, SUBSET_1, REAL_1,
NAT_1, COMPLEX1, MEASURE6, RELAT_1, MEASURE1, MESFUNC2, TARSKI, FINSEQ_1,
XXREAL_0, ARYTM_3, ARYTM_1, VALUED_0, MESFUNC1, SETFAM_1, VALUED_1,
RAT_1, RFUNCT_3, SUPINF_2, CARD_1, SUPINF_1, MESFUNC5, MESFUNC3, INT_1,
ZFMISC_1, INTEGRA5, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_3,
XCMPLX_0, DOMAIN_1, XREAL_0, REAL_1, RAT_1, NAT_1, NAT_D, FUNCT_1,
RELSET_1, PARTFUN1, FINSEQ_1, VALUED_1, SUPINF_2, COMPLEX1, XXREAL_0,
VALUED_0, RFUNCT_3, MEASURE6, FUNCT_2, SUPINF_1, MEASURE1, EXTREAL1,
MESFUNC1, MESFUNC2, MESFUNC3, SETFAM_1, PROB_1, MESFUNC5;
constructors DOMAIN_1, REAL_1, SQUARE_1, NAT_D, MEASURE3, MEASURE6, EXTREAL1,
MESFUNC1, BINARITH, MESFUNC2, MESFUNC3, MESFUNC5, SUPINF_1, RELSET_1,
ABSVALUE, RFUNCT_3, FUNCT_4, SEQFUNC;
registrations SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, RAT_1, MEMBERED,
MEASURE1, VALUED_0, ORDINAL1, XXREAL_3;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin :: The Measurability of Real-valued Functions
reserve X for non empty set,
Y for set,
S for SigmaField of X,
F for sequence of S,
f,g for PartFunc of X,REAL,
A,B for Element of S,
r,s for Real,
a for Real,
n for Nat;
theorem :: MESFUNC6:1
|. R_EAL f .| = R_EAL abs f;
theorem :: MESFUNC6:2
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL, r be Real
st dom f in S & (for x be object st x in dom f holds f.x = r)
holds f is_simple_func_in S;
theorem :: MESFUNC6:3
for x be set holds x in less_dom(f,a) iff x in dom f &
ex y being Real st y=f.x & y < a;
theorem :: MESFUNC6:4
for x be set holds x in less_eq_dom(f,a) iff x in dom f &
ex y being Real st y=f.x & y <= a;
theorem :: MESFUNC6:5
for x be set holds x in great_dom(f,r) iff x in dom f &
ex y being Real st y=f.x & r < y;
theorem :: MESFUNC6:6
for x be set holds x in great_eq_dom(f,r) iff x in dom f &
ex y being Real st y=f.x & r <= y;
theorem :: MESFUNC6:7
for x be set holds x in eq_dom(f,r) iff x in dom f &
ex y being Real st y=f.x & r= y;
theorem :: MESFUNC6:8
(for n holds F.n = Y /\ great_dom(f,r-1/(n+1))) implies Y /\
great_eq_dom(f,r) = meet rng F;
theorem :: MESFUNC6:9
(for n holds F.n = Y /\ less_dom(f,(r+1/(n+1)))) implies Y /\
less_eq_dom(f,r) = meet rng F;
theorem :: MESFUNC6:10
(for n holds F.n = Y /\ less_eq_dom(f,r-1/(n+1))) implies Y /\
less_dom(f,r) = union rng F;
theorem :: MESFUNC6:11
(for n holds F.n = Y /\ great_eq_dom(f,r+1/(n+1))) implies Y /\
great_dom(f,r) = union rng F;
definition
let X be non empty set;
let S be SigmaField of X;
let f be PartFunc of X,REAL;
let A be Element of S;
pred f is_measurable_on A means
:: MESFUNC6:def 1
R_EAL f is_measurable_on A;
end;
theorem :: MESFUNC6:12
f is_measurable_on A iff for r being Real holds A /\
less_dom(f,r) in S;
theorem :: MESFUNC6:13
A c= dom f implies ( f is_measurable_on A iff for r being Real
holds A /\ great_eq_dom(f,r) in S );
theorem :: MESFUNC6:14
f is_measurable_on A iff for r being Real holds A /\
less_eq_dom(f,r) in S;
theorem :: MESFUNC6:15
A c= dom f implies ( f is_measurable_on A iff for r being Real
holds A /\ great_dom(f,r) in S );
theorem :: MESFUNC6:16
B c= A & f is_measurable_on A implies f is_measurable_on B;
theorem :: MESFUNC6:17
f is_measurable_on A & f is_measurable_on B implies f is_measurable_on
(A \/ B);
theorem :: MESFUNC6:18
f is_measurable_on A & A c= dom f implies A /\ great_dom(f,r) /\
less_dom(f,s) in S;
theorem :: MESFUNC6:19
f is_measurable_on A & g is_measurable_on A & A c= dom g implies A /\
less_dom(f,r) /\ great_dom(g,r) in S;
theorem :: MESFUNC6:20
R_EAL(r(#)f)=r(#)R_EAL f;
theorem :: MESFUNC6:21
f is_measurable_on A & A c= dom f implies r(#)f is_measurable_on A;
begin :: The Measurability of $f+g$ and $f-g$ for Real-valued Functions $f,g$
reserve X for non empty set,
S for SigmaField of X,
f,g for PartFunc of X,REAL ,
A for Element of S,
r for Real,
p for Rational;
theorem :: MESFUNC6:22
R_EAL f is real-valued;
theorem :: MESFUNC6:23
R_EAL(f+g)=R_EAL f + R_EAL g & R_EAL(f-g)=R_EAL f - R_EAL g &
dom(R_EAL(f+g))= dom(R_EAL f) /\ dom(R_EAL g) & dom(R_EAL(f-g))= dom(R_EAL f)
/\ dom(R_EAL g) & dom(R_EAL(f+g))= dom f /\ dom g & dom(R_EAL(f-g))= dom f /\
dom g;
theorem :: MESFUNC6:24
for F be Function of RAT,S st (for p holds F.p = (A/\less_dom(f,p)) /\
(A/\less_dom(g,r-p))) holds A /\ less_dom(f+g,r) = union rng F;
theorem :: MESFUNC6:25
f is_measurable_on A & g is_measurable_on A implies 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));
theorem :: MESFUNC6:26
f is_measurable_on A & g is_measurable_on A implies f+g is_measurable_on A;
theorem :: MESFUNC6:27
R_EAL f - R_EAL g = R_EAL f + R_EAL -g;
theorem :: MESFUNC6:28
-R_EAL f = R_EAL((-1)(#)f) & -R_EAL f = R_EAL -f;
theorem :: MESFUNC6:29
f is_measurable_on A & g is_measurable_on A & A c= dom g implies f-g
is_measurable_on A;
begin :: Basic Properties of Real-valued Functions, $\max_{+}f$ and $\max_{-}f$
reserve X for non empty set,
f,g for PartFunc of X,REAL,
r for Real ;
theorem :: MESFUNC6:30
max+(R_EAL f) = max+f & max-(R_EAL f) = max-f;
theorem :: MESFUNC6:31
for x being Element of X holds 0 <= (max+f).x;
theorem :: MESFUNC6:32
for x being Element of X holds 0 <= (max-f).x;
theorem :: MESFUNC6:33
max-f = max+(-f);
theorem :: MESFUNC6:34
for x being set st x in dom f & 0 < max+f.x holds max-f.x = 0;
theorem :: MESFUNC6:35
for x being set st x in dom f & 0 < max-f.x holds max+f.x = 0;
theorem :: MESFUNC6:36
dom f = dom (max+f - max-f) & dom f = dom (max+f + max-f);
theorem :: MESFUNC6:37
for x being set st x in dom f holds (max+f.x = f.x or max+f.x = 0) & (
max-f.x = -(f.x) or max-f.x = 0);
theorem :: MESFUNC6:38
for x being set st x in dom f & max+f.x = f.x holds max-f.x = 0;
theorem :: MESFUNC6:39
for x being set st x in dom f & max+f.x = 0 holds max-f.x = -(f.x);
theorem :: MESFUNC6:40
for x being set st x in dom f & max-f.x = -(f.x) holds max+f.x = 0;
theorem :: MESFUNC6:41
for x being set st x in dom f & max-f.x = 0 holds max+f.x = f.x;
theorem :: MESFUNC6:42
f = max+f - max-f;
theorem :: MESFUNC6:43
|.r qua Complex.| = |. r .|;
theorem :: MESFUNC6:44
R_EAL(abs f) =|.R_EAL f.|;
theorem :: MESFUNC6:45
abs f = max+f + max-f;
begin :: The Measurability of $\max_{+}f, \max_{-}f$ and $|f|$
reserve X for non empty set,
S for SigmaField of X,
f,g for PartFunc of X,REAL,
A for Element of S;
theorem :: MESFUNC6:46
f is_measurable_on A implies max+f is_measurable_on A;
theorem :: MESFUNC6:47
f is_measurable_on A & A c= dom f implies max-f is_measurable_on A;
theorem :: MESFUNC6:48
f is_measurable_on A & A c= dom f implies abs f is_measurable_on A;
begin :: The Definition and the Measurability of a Real-valued Simple Function
reserve X for non empty set,
Y for set,
S for SigmaField of X,
f,g,h for PartFunc of X,REAL,
A for Element of S,
r for Real;
definition
let X,S,f;
pred f is_simple_func_in S means
:: MESFUNC6:def 2
ex F being Finite_Sep_Sequence of S
st (dom f = union rng F & for n being Nat,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;
theorem :: MESFUNC6:49
f is_simple_func_in S iff R_EAL f is_simple_func_in S;
theorem :: MESFUNC6:50
f is_simple_func_in S implies f is_measurable_on A;
theorem :: MESFUNC6:51
for X being set, f being PartFunc of X,REAL holds f is
nonnegative iff for x being object holds 0 <= f.x;
theorem :: MESFUNC6:52
for X being set, f being PartFunc of X,REAL st for x being object
st x in dom f holds 0 <= f.x holds f is nonnegative;
theorem :: MESFUNC6:53
for X being set, f being PartFunc of X,REAL holds f is nonpositive iff
for x being set holds f.x <= 0;
theorem :: MESFUNC6:54
(for x being object st x in dom f holds f.x <= 0) implies f is nonpositive;
theorem :: MESFUNC6:55
f is nonnegative implies f|Y is nonnegative;
theorem :: MESFUNC6:56
f is nonnegative & g is nonnegative implies f+g is nonnegative;
theorem :: MESFUNC6:57
f is nonnegative implies (0 <= r implies r(#)f is nonnegative) & (r <=
0 implies r(#)f is nonpositive);
theorem :: MESFUNC6:58
(for x be set st x in dom f /\ dom g holds g.x <= f.x) implies f
-g is nonnegative;
theorem :: MESFUNC6:59
f is nonnegative & g is nonnegative & h is nonnegative implies f+g+h
is nonnegative;
theorem :: MESFUNC6:60
for x be object st x in dom(f+g+h) holds (f+g+h).x=f.x+g.x+h.x;
theorem :: MESFUNC6:61
max+f is nonnegative & max-f is nonnegative;
theorem :: MESFUNC6:62
dom(max+(f+g) + max-f) = dom f /\ dom g & dom(max-(f+g) + max+f)
= dom f /\ dom g & dom(max+(f+g) + max-f + max-g) = dom f /\ dom g & dom(max-(f
+g) + max+f + max+g) = dom f /\ dom g & max+(f+g) + max-f is nonnegative & max-
(f+g) + max+f is nonnegative;
theorem :: MESFUNC6:63
max+(f+g) + max-f + max-g = max-(f+g) + max+f + max+g;
theorem :: MESFUNC6:64
0 <= r implies max+(r(#)f) = r(#)max+f & max-(r(#)f) = r(#)max-f;
theorem :: MESFUNC6:65
0 <= r implies max+((-r)(#)f) = r(#)max-f & max-((-r)(#)f) = r(#)max+f;
theorem :: MESFUNC6:66
max+(f|Y)=max+f|Y & max-(f|Y)=max-f|Y;
theorem :: MESFUNC6:67
Y c= dom(f+g) implies dom((f+g)|Y) =Y & dom(f|Y+g|Y)=Y & (f+g)|Y = f|Y +g|Y;
theorem :: MESFUNC6:68
eq_dom(f,r) = f"{r};
begin :: Lemmas for a Real-valued Measurable Function and a Simple Function
reserve X for non empty set,
S for SigmaField of X,
f,g for PartFunc of X,REAL ,
A,B for Element of S,
r,s for Real;
theorem :: MESFUNC6:69
f is_measurable_on A & A c= dom f implies A /\ great_eq_dom(f,r) /\
less_dom(f,s) in S;
theorem :: MESFUNC6:70
f is_simple_func_in S implies f|A is_simple_func_in S;
theorem :: MESFUNC6:71
f is_simple_func_in S implies dom f is Element of S;
theorem :: MESFUNC6:72
f is_simple_func_in S & g is_simple_func_in S implies f+g is_simple_func_in S
;
theorem :: MESFUNC6:73
f is_simple_func_in S implies r(#)f is_simple_func_in S;
theorem :: MESFUNC6:74
(for x be set st x in dom(f-g) holds g.x <= f.x) implies f-g is nonnegative;
theorem :: MESFUNC6:75
ex f be PartFunc of X,REAL st f is_simple_func_in S & dom f = A & for
x be object st x in A holds f.x=r;
theorem :: MESFUNC6:76
f is_measurable_on B & A = dom f /\ B implies f|B is_measurable_on A;
theorem :: MESFUNC6:77
A c= dom f & f is_measurable_on A & g is_measurable_on A implies max+(
f+g) + max-f is_measurable_on A;
theorem :: MESFUNC6:78
A c= dom f /\ dom g & f is_measurable_on A & g is_measurable_on A
implies max-(f+g) + max+f is_measurable_on A;
theorem :: MESFUNC6:79
dom f in S & dom g in S implies dom(f+g) in S;
theorem :: MESFUNC6:80
dom f = A implies (f is_measurable_on B iff f is_measurable_on ( A/\B));
theorem :: MESFUNC6:81
( ex A be Element of S st dom f = A ) implies for c be Real, B be
Element of S st f is_measurable_on B holds c(#)f is_measurable_on B;
begin :: The Integral of a Real-valued Function
reserve X for non empty set,
S for SigmaField of X,
M for sigma_Measure of S,
f,g for PartFunc of X,REAL,
r for Real,
E,A,B for Element of S;
definition
let X be non empty set;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f be PartFunc of X,REAL;
func Integral(M,f) -> Element of ExtREAL equals
:: MESFUNC6:def 3
Integral(M,R_EAL f);
end;
theorem :: MESFUNC6:82
(ex A be Element of S st A = dom f & f is_measurable_on A) & f
is nonnegative implies Integral(M,f) = integral+(M,R_EAL f);
theorem :: MESFUNC6:83
f is_simple_func_in S & f is nonnegative implies Integral(M,f) =
integral+(M,R_EAL f) & Integral(M,f) = integral'(M,R_EAL f);
theorem :: MESFUNC6:84
(ex A be Element of S st A = dom f & f is_measurable_on A) & f is
nonnegative implies 0 <= Integral(M,f);
theorem :: MESFUNC6:85
(ex E be Element of S st E = dom f & f is_measurable_on E) & f is
nonnegative & A misses B implies Integral(M,f|(A\/B)) = Integral(M,f|A)+
Integral(M,f|B);
theorem :: MESFUNC6:86
(ex E be Element of S st E = dom f & f is_measurable_on E) & f is
nonnegative implies 0<= Integral(M,f|A);
theorem :: MESFUNC6:87
(ex E be Element of S st E = dom f & f is_measurable_on E ) & f is
nonnegative & A c= B implies Integral(M,f|A) <= Integral(M,f|B);
theorem :: MESFUNC6:88
(ex E be Element of S st E = dom f & f is_measurable_on E) & M.A = 0
implies Integral(M,f|A)=0;
theorem :: MESFUNC6:89
E = dom f & f is_measurable_on E & M.A =0 implies Integral(M,f|(E\A))
= Integral(M,f);
definition
let X be non empty set;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f be PartFunc of X,REAL;
pred f is_integrable_on M means
:: MESFUNC6:def 4
R_EAL f is_integrable_on M;
end;
theorem :: MESFUNC6:90
f is_integrable_on M implies -infty < Integral(M,f) & Integral(M,f) < +infty;
theorem :: MESFUNC6:91
f is_integrable_on M implies f|A is_integrable_on M;
theorem :: MESFUNC6:92
f is_integrable_on M & A misses B implies Integral(M,f|(A\/B)) =
Integral(M,f|A) + Integral(M,f|B);
theorem :: MESFUNC6:93
f is_integrable_on M & B = (dom f)\A implies f|A is_integrable_on M &
Integral(M,f) = Integral(M,f|A)+Integral(M,f|B);
theorem :: MESFUNC6:94
(ex A be Element of S st A = dom f & f is_measurable_on A ) implies (f
is_integrable_on M iff abs f is_integrable_on M);
theorem :: MESFUNC6:95
f is_integrable_on M implies |. Integral(M,f).| <= Integral(M,abs f);
theorem :: MESFUNC6:96
( ex A be Element of S st A = dom f & f is_measurable_on A ) & dom f =
dom g & g is_integrable_on M & ( for x be Element of X st x in dom f holds
|.f.x qua Complex.| <= g.x ) implies
f is_integrable_on M & Integral(M,abs f) <= Integral(M,g);
theorem :: MESFUNC6:97
dom f in S & 0 <= r & (for x be object st x in dom f holds f.x = r)
implies Integral(M,f) = r * M.(dom f);
theorem :: MESFUNC6:98
f is_integrable_on M & g is_integrable_on M & f is nonnegative & g is
nonnegative implies f+g is_integrable_on M;
theorem :: MESFUNC6:99
f is_integrable_on M & g is_integrable_on M implies dom (f+g) in S;
theorem :: MESFUNC6:100
f is_integrable_on M & g is_integrable_on M implies f+g is_integrable_on M;
theorem :: MESFUNC6:101
f is_integrable_on M & g is_integrable_on M implies ex E be Element of
S st E = dom f /\ dom g & Integral(M,f+g)=Integral(M,f|E)+Integral(M,g|E);
theorem :: MESFUNC6:102
f is_integrable_on M implies r(#)f is_integrable_on M & Integral(M,r
(#)f) = r * Integral(M,f);
definition
let X be non empty set;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f be PartFunc of X,REAL;
let B be Element of S;
func Integral_on(M,B,f) -> Element of ExtREAL equals
:: MESFUNC6:def 5
Integral(M,f|B);
end;
theorem :: MESFUNC6:103
f is_integrable_on M & g is_integrable_on M & B c= dom(f+g) implies f+
g is_integrable_on M & Integral_on(M,B,f+g) = Integral_on(M,B,f) + Integral_on(
M,B,g);
theorem :: MESFUNC6:104
f is_integrable_on M implies f|B is_integrable_on M & Integral_on(M,B,
r(#)f) = r * Integral_on(M,B,f);