:: Integral of Measurable Function
:: by Noboru Endou and Yasunari Shidama
::
:: Received May 24, 2006
:: Copyright (c) 2006-2021 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, SUPINF_1, COMPLEX1, ARYTM_1, XXREAL_0, ARYTM_3,
MEASURE6, NAT_1, CARD_1, NEWTON, RELAT_1, REAL_1, SUBSET_1, INT_1,
PARTFUN1, FUNCT_1, SUPINF_2, XBOOLE_0, PROB_1, MESFUNC2, VALUED_0, RAT_1,
MESFUNC1, TARSKI, MEASURE1, VALUED_1, RFUNCT_3, FINSEQ_1, MESFUNC3,
CARD_3, ZFMISC_1, SEQ_2, ORDINAL2, XCMPLX_0, XXREAL_2, SEQFUNC, PBOOLE,
INTEGRA1, FINSET_1, MEMBERED, SETLIM_1, INTEGRA5, FUNCT_3, MESFUNC5,
FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, COMPLEX1, XXREAL_2, XXREAL_3, REAL_1, RELAT_1,
FUNCT_1, FINSEQ_1, RELSET_1, FINSET_1, PARTFUN1, FUNCT_2, INT_1, NAT_D,
RAT_1, MEMBERED, SUPINF_1, SUPINF_2, MEASURE1, EXTREAL1, NAT_1, MESFUNC1,
MESFUNC2, MESFUNC3, FINSEQOP, RFUNCT_3, PROB_1, MEASURE6, NEWTON,
SEQFUNC, SETLIM_1, VALUED_0;
constructors WELLORD2, REAL_1, SQUARE_1, NAT_D, FINSEQOP, LIMFUNC1, SEQFUNC,
NEWTON, RFUNCT_3, MEASURE6, EXTREAL1, MESFUNC1, BINARITH, MESFUNC2,
KURATO_0, MESFUNC3, SETLIM_1, SUPINF_1, RELSET_1, XREAL_0;
registrations SUBSET_1, ORDINAL1, RELSET_1, PARTFUN1, FINSET_1, NUMBERS,
XXREAL_0, XREAL_0, NAT_1, INT_1, RAT_1, MEMBERED, COMPLEX1, FINSEQ_1,
MEASURE1, VALUED_0, XXREAL_2, XXREAL_3, XCMPLX_0, NEWTON, EXTREAL1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin
theorem :: MESFUNC5:1
for x,y be R_eal holds |.x-y.| = |.y-x.|;
theorem :: MESFUNC5:2
for x,y be R_eal holds y-x <= |.x-y.|;
theorem :: MESFUNC5:3
for x,y be R_eal, e be Real st |.x-y.| < e & not ( x =
+infty & y = +infty or x = -infty & y = -infty ) holds x <> +infty & x <>
-infty & y <> +infty & y <>-infty;
theorem :: MESFUNC5:4
for n be Nat, p be ExtReal st 0 <= p & p < n
ex k be Nat st 1 <= k & k <= 2|^n*n & (k-1)/(2|^n) <= p & p < k/(2|^n);
theorem :: MESFUNC5:5
for n,k be Nat, p be ExtReal st k <= 2|^n*n & n <= p holds k/(2|^n) <= p;
theorem :: MESFUNC5:6
for x,y,k being ExtReal st 0 <= k holds k*max(x,y) = max
(k*x,k*y) & k*min(x,y) = min(k*x,k*y);
theorem :: MESFUNC5:7
for x,y,k being R_eal st k <= 0 holds k*min(x,y) = max(k*x,k*y) & k*
max(x,y) = min(k*x,k*y);
begin :: Lemmas for partial function of non empty set,extended real numbers
definition
let IT be set;
attr IT is nonpositive means
:: MESFUNC5:def 1
for x being R_eal holds x in IT implies x <= 0;
end;
definition
let R be Relation;
attr R is nonpositive means
:: MESFUNC5:def 2
rng R is nonpositive;
end;
theorem :: MESFUNC5:8
for X being set, F being PartFunc of X,ExtREAL holds F is
nonpositive iff for n being object holds F.n <= 0.;
theorem :: MESFUNC5:9
for X being set, F being PartFunc of X,ExtREAL st for n being
set st n in dom F holds F.n <= 0. holds F is nonpositive;
definition
let R be Relation;
attr R is without-infty means
:: MESFUNC5:def 3
not -infty in rng R;
attr R is without+infty means
:: MESFUNC5:def 4
not +infty in rng R;
end;
definition
let X be non empty set, f be PartFunc of X,ExtREAL;
redefine attr f is without-infty means
:: MESFUNC5:def 5
for x being object holds -infty < f.x;
redefine attr f is without+infty means
:: MESFUNC5:def 6
for x being object holds f.x < +infty;
end;
theorem :: MESFUNC5:10
for X be non empty set, f be PartFunc of X,ExtREAL holds (for x
be set st x in dom f holds -infty < f.x) iff f is without-infty;
theorem :: MESFUNC5:11
for X be non empty set, f be PartFunc of X,ExtREAL holds (for x
be set st x in dom f holds f.x < +infty) iff f is without+infty;
theorem :: MESFUNC5:12
for X be non empty set, f be PartFunc of X,ExtREAL st f is
nonnegative holds f is without-infty;
theorem :: MESFUNC5:13
for X be non empty set, f be PartFunc of X,ExtREAL st f is
nonpositive holds f is without+infty;
registration
let X be non empty set;
cluster nonnegative -> without-infty for PartFunc of X,ExtREAL;
cluster nonpositive -> without+infty for PartFunc of X,ExtREAL;
end;
theorem :: MESFUNC5:14
for X be non empty set, S be SigmaField of X, f be PartFunc of X
,ExtREAL st f is_simple_func_in S holds f is without+infty & f is without-infty
;
theorem :: MESFUNC5:15
for X be non empty set, Y be set, f be PartFunc of X,ExtREAL st
f is nonnegative holds f|Y is nonnegative;
theorem :: MESFUNC5:16
for X be non empty set, f,g be PartFunc of X,ExtREAL st f is
without-infty & g is without-infty holds dom(f+g)=dom f /\ dom g;
theorem :: MESFUNC5:17
for X be non empty set, f,g be PartFunc of X,ExtREAL st f is
without-infty & g is without+infty holds dom(f-g)=dom f /\ dom g;
theorem :: MESFUNC5:18
for X be non empty set, S be SigmaField of X, f,g be PartFunc of
X,ExtREAL, F be Function of RAT,S, r be Real,
A be Element of S st f is
without-infty & g is without-infty & (for p be Rational holds F.p = A /\
less_dom(f,p) /\
(A /\ less_dom(g, (r-(p qua Complex)))))
holds A /\ less_dom(f+g,r) = union rng F;
definition
let X be non empty set;
let f be PartFunc of X,REAL;
func R_EAL f -> PartFunc of X,ExtREAL equals
:: MESFUNC5:def 7
f;
end;
theorem :: MESFUNC5:19
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f,g be PartFunc of X,ExtREAL st f is nonnegative & g is nonnegative holds
f+g is nonnegative;
theorem :: MESFUNC5:20
for X be non empty set, f be PartFunc of X,ExtREAL,c be Real st
f is nonnegative holds (0 <= c implies c(#)f is nonnegative) & (c <= 0 implies
c(#)f is nonpositive);
theorem :: MESFUNC5:21
for X be non empty set, f,g be PartFunc of X,ExtREAL st (for x
be set st x in dom f /\ dom g holds g.x <= f.x & -infty < g.x & f.x < +infty)
holds f-g is nonnegative;
theorem :: MESFUNC5:22
for X be non empty set, f,g be PartFunc of X,ExtREAL st f is
nonnegative & g is nonnegative holds dom(f+g)=dom f /\ dom g & f+g is
nonnegative;
theorem :: MESFUNC5:23
for X be non empty set, f,g,h be PartFunc of X,ExtREAL st f is
nonnegative & g is nonnegative & h is nonnegative holds dom(f+g+h) = dom f /\
dom g /\ dom h & f+g+h is nonnegative & for x be set st x in dom f /\ dom g /\
dom h holds (f+g+h).x=f.x+g.x+h.x;
theorem :: MESFUNC5:24
for X be non empty set, f,g being PartFunc of X,ExtREAL st f is
without-infty & g is without-infty holds 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 :: MESFUNC5:25
for X being non empty set, f,g being PartFunc of X,ExtREAL st f
is without-infty & f is without+infty & g is without-infty & g is without+infty
holds max+(f+g) + max- f + max- g = max-(f+g) + max+ f + max+ g;
theorem :: MESFUNC5:26
for C being non empty set, f being PartFunc of C,ExtREAL, c be
Real st 0 <= c holds max+(c(#)f) = c(#)max+f & max-(c(#)f) = c(#)max-f;
theorem :: MESFUNC5:27
for C being non empty set, f being PartFunc of C,ExtREAL, c be
Real st 0 <= c holds max+((-c)(#)f) = c(#)max-f & max-((-c)(#)f) = c(#)max+f;
theorem :: MESFUNC5:28
for X be non empty set, f be PartFunc of X,ExtREAL, A be set
holds max+(f|A)=max+f|A & max-(f|A)=max-f|A;
theorem :: MESFUNC5:29
for X be non empty set, f,g be PartFunc of X,ExtREAL, B be set
st B c= dom(f+g) holds dom((f+g)|B) =B & dom(f|B+g|B)=B & (f+g)|B = f|B+g|B;
theorem :: MESFUNC5:30
for X be non empty set, f be PartFunc of X,ExtREAL, a be R_eal
holds eq_dom(f,a) = f"{a};
begin :: Lemmas for measurable function and simple valued function
theorem :: MESFUNC5:31
for X be non empty set, S be SigmaField of X, f,g be PartFunc of
X,ExtREAL, A be Element of S st f is without-infty & g is without-infty & f
is A-measurable & g is A-measurable holds f+g is A-measurable;
theorem :: MESFUNC5:32
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL st f is_simple_func_in S & dom f = {} holds ex F be
Finite_Sep_Sequence of S, a,x be FinSequence of ExtREAL st F,a
are_Re-presentation_of f & a.1 = 0 & (for n be Nat st 2 <= n & n in dom a holds
0 < a.n & a.n < +infty) & dom x = dom F & (for n be Nat st n in dom x holds x.n
= a.n*(M*F).n) & Sum x = 0;
theorem :: MESFUNC5:33
for X be non empty set, S be SigmaField of X,
f be PartFunc of X ,ExtREAL, A be Element of S,
r,s be Real st f is A-measurable & A c= dom f
holds A /\ great_eq_dom(f, r) /\ less_dom(f, s) in S;
theorem :: MESFUNC5:34
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL, A be Element of S st f is_simple_func_in S
holds f|A is_simple_func_in S;
theorem :: MESFUNC5:35
for X be non empty set, S be SigmaField of X, A be Element of S,
F be Finite_Sep_Sequence of S, G be FinSequence st dom F = dom G & (for n be
Nat st n in dom F holds G.n = F.n /\ A) holds G is Finite_Sep_Sequence of S;
theorem :: MESFUNC5:36
for X be non empty set, S be SigmaField of X, f be PartFunc of X
,ExtREAL, A be Element of S, F,G be Finite_Sep_Sequence of S, a be FinSequence
of ExtREAL st dom F = dom G & (for n be Nat st n in dom F holds G.n = F.n /\ A)
& F,a are_Re-presentation_of f holds G,a are_Re-presentation_of f|A;
theorem :: MESFUNC5:37
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL st f is_simple_func_in S holds dom f is
Element of S;
theorem :: MESFUNC5:38
for X be non empty set, S be SigmaField of X, f,g be PartFunc of
X,ExtREAL st f is_simple_func_in S & g is_simple_func_in S holds f+g
is_simple_func_in S;
theorem :: MESFUNC5:39
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL,c be Real st f is_simple_func_in S holds c(#)f
is_simple_func_in S;
theorem :: MESFUNC5:40
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f,g be PartFunc of X,ExtREAL st f is_simple_func_in S & g
is_simple_func_in S &
(for x be object st x in dom(f-g) holds g.x <= f.x) holds f-g is nonnegative;
theorem :: MESFUNC5:41
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, A be Element of S, c be R_eal st c <> +infty & c <> -infty holds ex f be
PartFunc of X,ExtREAL st f is_simple_func_in S & dom f = A &
for x be object st x in A holds f.x=c;
theorem :: MESFUNC5:42
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL, B,BF be Element of S st f is B-measurable
& BF = dom f /\ B holds f|B is BF-measurable;
theorem :: MESFUNC5:43
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, A be Element of S, f,g being PartFunc of X,ExtREAL st A c= dom f & f
is A-measurable & g is A-measurable & f is without-infty & g is
without-infty holds max+(f+g) + max-f is A-measurable;
theorem :: MESFUNC5:44
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, A be Element of S, f,g being PartFunc of X,ExtREAL st A c= dom f /\ dom g
& f is A-measurable & g is A-measurable & f is without-infty & g is
without-infty holds max-(f+g) + max+f is A-measurable;
theorem :: MESFUNC5:45
for X be non empty set, S being SigmaField of X, M being
sigma_Measure of S, A being set st A in S holds 0 <= M.A;
theorem :: MESFUNC5:46
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f,g be PartFunc of X,ExtREAL st (ex E1 be Element of S st E1=dom f & f
is E1-measurable) & (ex E2 be Element of S st E2=dom g & g is E2-measurable
) & f"{+infty} in S & f"{-infty} in S & g"{+infty} in S & g"{-infty} in S
holds dom(f+g) in S;
theorem :: MESFUNC5:47
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f,g be PartFunc of X,ExtREAL st (ex E1 be Element of S st E1=dom f & f
is E1-measurable) & (ex E2 be Element of S st E2=dom g & g is E2-measurable
) holds ex E be Element of S st E=dom(f+g) & (f+g) is E-measurable;
theorem :: MESFUNC5:48
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL, A,B be Element of S st dom f = A holds f
is B-measurable iff f is (A/\B)-measurable;
theorem :: MESFUNC5:49
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL st ( ex A be Element of S st dom f = A ) for c
be Real, B be Element of S st f is B-measurable holds c(#)f is B-measurable;
begin :: Sequence of extended real numbers
definition
mode ExtREAL_sequence is sequence of ExtREAL;
end;
definition
let seq be ExtREAL_sequence;
attr seq is convergent_to_finite_number means
:: MESFUNC5:def 8
ex g be Real st
for p be Real st 0
R_eal means
:: MESFUNC5:def 12
( ex g be Real st it = g & (for p
be Real st 0
+infty & (for n be Nat
holds L.n <= K) holds sup rng L < +infty;
theorem :: MESFUNC5:59
for L be ExtREAL_sequence st L is without-infty holds sup rng L
<> +infty iff ex K be Real st 0 ExtREAL_sequence means
:: MESFUNC5:def 13
for n be Nat holds it.n = (H.n).x;
end;
definition
let D1,D2 be set, F be sequence of PFuncs(D1,D2), n be Nat;
redefine func F.n -> PartFunc of D1,D2;
end;
theorem :: MESFUNC5:64
for X be non empty set, S be SigmaField of X, f be PartFunc of X,ExtREAL
st (ex A be Element of S st A = dom f & f is A-measurable)
& f qua ext-real-valued Function is nonnegative
ex F be Functional_Sequence of X,ExtREAL st (for n be Nat
holds F.n is_simple_func_in S & dom(F.n) = dom f) & (for n be Nat holds F.n is
nonnegative) & (for n,m be Nat st n <=m holds for x be Element of X st x in dom
f holds (F.n).x <= (F.m).x ) & for x be Element of X st x in dom f holds (F#x)
is convergent & lim(F#x) = f.x;
begin :: Integral of non negative simple valued function
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,ExtREAL;
func integral'(M,f) -> Element of ExtREAL equals
:: MESFUNC5:def 14
integral(M,f)
if dom f <> {} otherwise 0.;
end;
theorem :: MESFUNC5:65
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f,g be PartFunc of X,ExtREAL st f is_simple_func_in S & g
is_simple_func_in S & f is nonnegative & g is nonnegative holds dom(f+g) = dom
f /\ dom g & integral'(M,f+g) = integral'(M,f|dom(f+g)) + integral'(M,g|dom(f+g
));
theorem :: MESFUNC5:66
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL,c be Real st f is_simple_func_in S & f is
nonnegative & 0 <= c holds integral'(M,c(#)f) = (c)*integral'(M,f);
theorem :: MESFUNC5:67
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL, A,B be Element of S st f is_simple_func_in S
& f is nonnegative & A misses B holds integral'(M,f|(A\/B)) = integral'(M,f|A)
+ integral'(M,f|B);
theorem :: MESFUNC5:68
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative
holds 0 <= integral'(M,f);
theorem :: MESFUNC5:69
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f,g be PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative
& g is_simple_func_in S & g is nonnegative &
(for x be object st x in dom(f-g)
holds g.x <= f.x) holds dom (f-g) = dom f /\ dom g & integral'(M,f|dom(f-g))=
integral'(M,f-g)+integral'(M,g|dom(f-g));
theorem :: MESFUNC5:70
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f,g be PartFunc of X,ExtREAL st f is_simple_func_in S & g
is_simple_func_in S & f is nonnegative & g is nonnegative &
(for x be object st x
in dom(f-g) holds g.x <= f.x) holds integral'(M,g|dom(f-g)) <= integral'(M,f|
dom(f-g));
theorem :: MESFUNC5:71
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL, c be R_eal st 0 <= c & f is_simple_func_in S
& (for x be object st x in dom f holds f.x=c)
holds integral'(M,f) = c*(M.(dom f));
theorem :: MESFUNC5:72
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative
holds integral'(M,f|eq_dom(f,0)) = 0;
theorem :: MESFUNC5:73
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, B be Element of S, f be PartFunc of X,ExtREAL st f is_simple_func_in S &
M.B=0 & f is nonnegative holds integral'(M,f|B) = 0;
theorem :: MESFUNC5:74
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, g be PartFunc of X,ExtREAL, F be Functional_Sequence of X,ExtREAL, L be
ExtREAL_sequence st g is_simple_func_in S &
(for x be object st x in dom g holds 0 < g.x) &
(for n be Nat holds F.n is_simple_func_in S) & (for n be Nat holds dom
(F.n) = dom g) & (for n be Nat holds F.n is nonnegative) & (for n,m be Nat st n
<=m holds for x be Element of X st x in dom g holds (F.n).x <= (F.m).x ) & (for
x be Element of X st x in dom g holds (F#x) is convergent & g.x <= lim(F#x) ) &
(for n be Nat holds L.n = integral'(M,F.n)) holds L is convergent & integral'(M
,g) <= lim(L);
theorem :: MESFUNC5:75
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, g be PartFunc of X,ExtREAL, F be Functional_Sequence of X,ExtREAL st g
is_simple_func_in S & g is nonnegative & (for n be Nat holds F.n
is_simple_func_in S) & (for n be Nat holds dom(F.n) = dom g) & (for n be Nat
holds F.n is nonnegative) & (for n,m be Nat st n <=m holds for x be Element of
X st x in dom g holds (F.n).x <= (F.m).x ) & (for x be Element of X st x in dom
g holds (F#x) is convergent & g.x <= lim(F#x) ) holds ex G be ExtREAL_sequence
st (for n be Nat holds G.n = integral'(M,F.n)) & G is convergent & sup(rng G)=
lim (G) & integral'(M,g) <= lim(G);
theorem :: MESFUNC5:76
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, A be Element of S, F,G be Functional_Sequence of X,ExtREAL, K,L be
ExtREAL_sequence st (for n be Nat holds F.n is_simple_func_in S & dom(F.n)=A )
& (for n be Nat holds F.n is nonnegative) & (for n,m be Nat st n <=m holds for
x be Element of X st x in A holds (F.n).x <= (F.m).x ) & (for n be Nat holds G.
n is_simple_func_in S & dom(G.n)=A) & (for n be Nat holds G.n is nonnegative) &
(for n,m be Nat st n <=m holds for x be Element of X st x in A holds (G.n).x <=
(G.m).x ) & (for x be Element of X st x in A holds F#x is convergent & G#x is
convergent & lim(F#x) = lim(G#x)) & (for n be Nat holds K.n=integral'(M,F.n) &
L.n=integral'(M,G.n)) holds K is convergent & L is convergent & lim K = lim L
;
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,ExtREAL;
assume that
ex A be Element of S st A = dom f & f is A-measurable and
f is nonnegative;
func integral+(M,f) -> Element of ExtREAL means
:: MESFUNC5:def 15
ex F be
Functional_Sequence of X,ExtREAL, K be ExtREAL_sequence st (for n be Nat holds
F.n is_simple_func_in S & dom(F.n) = dom f) & (for n be Nat holds F.n is
nonnegative) & (for n,m be Nat st n <=m holds for x be Element of X st x in dom
f holds (F.n).x <= (F.m).x ) & (for x be Element of X st x in dom f holds F#x
is convergent & lim(F#x) = f.x) & (for n be Nat holds K.n=integral'(M,F.n)) & K
is convergent & it=lim K;
end;
theorem :: MESFUNC5:77
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative
holds integral+(M,f) =integral'(M,f);
theorem :: MESFUNC5:78
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f,g be PartFunc of X,ExtREAL st ( ex A be Element of S st A = dom f & f
is A-measurable ) & ( ex B be Element of S st B = dom g & g is B-measurable
) & f is nonnegative & g is nonnegative holds ex C be Element of S st C = dom
(f+g) & integral+(M,f+g) = integral+(M,f|C) + integral+(M,g|C);
theorem :: MESFUNC5:79
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL st (ex A be Element of S st A = dom f & f
is A-measurable) & f is nonnegative holds 0 <= integral+(M,f);
theorem :: MESFUNC5:80
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL, A be Element of S st (ex E be Element of S st
E = dom f & f is E-measurable ) & f is nonnegative holds 0<= integral+(M,f|A
);
theorem :: MESFUNC5:81
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL, A,B be Element of S st (ex E be Element of S
st E = dom f & f is E-measurable) & f is nonnegative & A misses B holds
integral+(M,f|(A\/B)) = integral+(M,f|A)+integral+(M,f|B);
theorem :: MESFUNC5:82
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL, A be Element of S st (ex E be Element of S st
E = dom f & f is E-measurable ) & f is nonnegative & M.A = 0 holds integral+
(M,f|A) = 0;
theorem :: MESFUNC5:83
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL, A,B be Element of S st (ex E be Element of S
st E = dom f & f is E-measurable ) & f is nonnegative & A c= B holds
integral+(M,f|A) <= integral+(M,f|B);
theorem :: MESFUNC5:84
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL, E,A be Element of S st f is nonnegative & E =
dom f & f is E-measurable & M.A =0 holds integral+(M,f|(E\A)) = integral+(M,
f);
theorem :: MESFUNC5:85
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f,g be PartFunc of X,ExtREAL st (ex E be Element of S st E = dom f & E=
dom g & f is E-measurable & g is E-measurable) & f is nonnegative & g is
nonnegative & (for x be Element of X st x in dom g holds g.x <= f.x) holds
integral+(M,g) <= integral+(M,f);
theorem :: MESFUNC5:86
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL, c be Real st 0 <= c & (ex A be Element of S
st A = dom f & f is A-measurable) & f is nonnegative holds integral+(M,c(#)f
) = c * integral+(M,f);
theorem :: MESFUNC5:87
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL st (ex A be Element of S st A = dom f & f
is A-measurable) & (for x be Element of X st x in dom f holds 0= f.x) holds
integral+(M,f) = 0;
begin :: Integral of measurable function
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,ExtREAL;
::$N Lebesgue Measure and Integration
::$N Integral of Measurable Function
func Integral(M,f) -> Element of ExtREAL equals
:: MESFUNC5:def 16
integral+(M,max+f)-integral+
(M,max-f);
end;
theorem :: MESFUNC5:88
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL st (ex A be Element of S st A = dom f & f
is A-measurable) & f is nonnegative holds Integral(M,f) =integral+(M,f);
theorem :: MESFUNC5:89
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative holds
Integral(M,f) = integral+(M,f) & Integral(M,f) = integral'(M,f);
theorem :: MESFUNC5:90
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL st (ex A be Element of S st A = dom f & f
is A-measurable) & f is nonnegative holds 0 <= Integral(M,f);
theorem :: MESFUNC5:91
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, A,B be Element of S st (ex E be Element of S st E =
dom f & f is E-measurable ) & f is nonnegative & A misses B holds Integral(M
,f|(A\/B)) = Integral(M,f|A)+Integral(M,f|B);
theorem :: MESFUNC5:92
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, A be Element of S st (ex E be Element of S st E =
dom f & f is E-measurable ) & f is nonnegative holds 0<= Integral(M,f|A);
theorem :: MESFUNC5:93
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, A,B be Element of S st (ex E be Element of S st E =
dom f & f is E-measurable ) & f is nonnegative & A c= B holds Integral(M,f|A
) <= Integral(M,f|B);
theorem :: MESFUNC5:94
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, A be Element of S st (ex E be Element of S st E =
dom f & f is E-measurable) & M.A = 0 holds Integral(M,f|A)=0;
theorem :: MESFUNC5:95
for X be non empty set, S be SigmaField of X, M be
sigma_Measure of S, f be PartFunc of X,ExtREAL, E,A be Element of S st E = dom
f & f is E-measurable & M.A =0 holds 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,ExtREAL;
pred f is_integrable_on M means
:: MESFUNC5:def 17
(ex A be Element of S st A = dom f &
f is A-measurable ) & integral+(M,max+ f) < +infty & integral+(M,max- f) <
+infty;
end;
theorem :: MESFUNC5:96
for X be non empty set, S be SigmaField of X, M be
sigma_Measure of S, f be PartFunc of X,ExtREAL st f is_integrable_on M holds 0
<= integral+(M,max+f) & 0 <= integral+(M,max-f) & -infty < Integral(M,f) &
Integral(M,f) < +infty;
theorem :: MESFUNC5:97
for X be non empty set, S be SigmaField of X, M be
sigma_Measure of S, f be PartFunc of X,ExtREAL, A be Element of S st f
is_integrable_on M holds integral+(M,max+(f|A)) <= integral+(M,max+ f) &
integral+(M,max-(f|A)) <= integral+(M,max- f) & f|A is_integrable_on M;
theorem :: MESFUNC5:98
for X be non empty set, S be SigmaField of X, M be
sigma_Measure of S, f be PartFunc of X,ExtREAL, A,B be Element of S st f
is_integrable_on M & A misses B holds Integral(M,f|(A\/B)) = Integral(M,f|A) +
Integral(M,f|B);
theorem :: MESFUNC5:99
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, A,B be Element of S st f is_integrable_on M & B = (
dom f)\A holds f|A is_integrable_on M & Integral(M,f) = Integral(M,f|A)+
Integral(M,f|B);
theorem :: MESFUNC5:100
for X be non empty set, S be SigmaField of X, M be
sigma_Measure of S, f be PartFunc of X,ExtREAL st (ex A be Element of S st A =
dom f & f is A-measurable ) holds f is_integrable_on M iff |.f.|
is_integrable_on M;
theorem :: MESFUNC5:101
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL st f is_integrable_on M holds |. Integral(M,f) .| <=
Integral(M,|.f.|);
theorem :: MESFUNC5:102
for X be non empty set, S be SigmaField of X, M be
sigma_Measure of S, f,g be PartFunc of X,ExtREAL st ( ex A be Element of S st A
= dom f & f is A-measurable ) & dom f = dom g & g is_integrable_on M & ( for
x be Element of X st x in dom f holds |.f.x .| <= g.x ) holds f
is_integrable_on M & Integral(M,|.f.|) <= Integral(M,g);
theorem :: MESFUNC5:103
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 & 0 <=
r & dom f <> {} & (for x be object st x in dom f holds f.x = r)
holds integral(M,f) = r * M.(dom f);
theorem :: MESFUNC5:104
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 & 0 <=
r & (for x be object st x in dom f holds f.x = r) holds integral'(M,f) = r
* M.(dom f);
theorem :: MESFUNC5:105
for X be non empty set, S be SigmaField of X, M be
sigma_Measure of S, f be PartFunc of X,ExtREAL st f is_integrable_on M holds f"
{+infty} in S & f"{-infty} in S & M.(f"{+infty})=0 & M.(f"{-infty})=0 & f"{
+infty} \/ f"{-infty} in S & M.(f"{+infty} \/ f"{-infty})=0;
theorem :: MESFUNC5:106
for X be non empty set, S be SigmaField of X, M be
sigma_Measure of S, f,g be PartFunc of X,ExtREAL st f is_integrable_on M & g
is_integrable_on M & f is nonnegative & g is nonnegative holds f+g
is_integrable_on M;
theorem :: MESFUNC5:107
for X be non empty set, S be SigmaField of X, M be
sigma_Measure of S, f,g be PartFunc of X,ExtREAL st f is_integrable_on M & g
is_integrable_on M holds dom (f+g) in S;
theorem :: MESFUNC5:108
for X be non empty set, S be SigmaField of X, M be
sigma_Measure of S, f,g be PartFunc of X,ExtREAL st f is_integrable_on M & g
is_integrable_on M holds f+g is_integrable_on M;
theorem :: MESFUNC5:109
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f,g be PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M
holds 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 :: MESFUNC5:110
for X be non empty set, S be SigmaField of X, M be
sigma_Measure of S, f be PartFunc of X,ExtREAL, c be Real st f is_integrable_on
M holds c(#)f is_integrable_on M & Integral(M,c(#)f) = c * 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,ExtREAL;
let B be Element of S;
func Integral_on(M,B,f) -> Element of ExtREAL equals
:: MESFUNC5:def 18
Integral(M,f|B);
end;
theorem :: MESFUNC5:111
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f,g be PartFunc of X,ExtREAL, B be Element of S st f is_integrable_on M & g
is_integrable_on M & B c= dom(f+g) holds f+g is_integrable_on M & Integral_on(M
,B,f+g) = Integral_on(M,B,f) + Integral_on(M,B,g);
theorem :: MESFUNC5:112
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, c be Real, B be Element of S st f is_integrable_on
M holds f|B is_integrable_on M & Integral_on(M,B,c(#)f) = c * Integral_on
(M,B,f);