:: Integral of Real-valued Measurable Function
:: by Yasunari Shidama and Noboru Endou
::
:: Received October 27, 2006
:: Copyright (c) 2006-2026 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, SUPINF_2, COMPLEX1, XXREAL_0,
VALUED_0, RFUNCT_3, MEASURE6, FUNCT_2, SUPINF_1, MEASURE1, EXTREAL1,
MESFUNC1,
VALUED_1, 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, VALUED_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, SUPINF_2, MESFUNC5;
equalities XBOOLE_0, RFUNCT_3, FINSEQ_1, MESFUNC5, VALUED_1, XXREAL_3;
expansions TARSKI, XBOOLE_0, SUPINF_2, MESFUNC5;
theorems MEASURE1, TARSKI, PARTFUN1, FUNCT_1, NAT_1, SUPINF_2, EXTREAL1,
MESFUNC1, FINSEQ_1, ABSVALUE, PROB_1, XBOOLE_0, XBOOLE_1, MESFUNC2,
MESFUNC3, XREAL_1, ZFMISC_1, MESFUNC5, XXREAL_0, RFUNCT_3, FUZZY_2,
FINSUB_1, NAT_2, FINSEQ_3, FINSEQ_2, NAT_D, VALUED_1, XXREAL_3, RELAT_1,
XREAL_0;
schemes FINSEQ_1, PARTFUN1;
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 Th1:
|. R_EAL f .| = R_EAL abs f
proof
A1: now
let x be Element of X;
assume x in dom |. R_EAL f .|;
then (|. R_EAL f .|).x = |. (R_EAL f).x .| by MESFUNC1:def 10;
then (|. R_EAL f .|).x = |.f.x qua Complex.| by EXTREAL1:12;
then (|. R_EAL f .|).x = |.f.|.x
by VALUED_1:18;
hence (|. R_EAL f .|).x = (R_EAL abs f).x;
end;
dom |. R_EAL f .| = dom R_EAL f by MESFUNC1:def 10
.= dom abs f by VALUED_1:def 11;
hence thesis by A1,PARTFUN1:5;
end;
theorem Th2:
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
proof
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 r be Real;
assume that
A1: dom f in S and
A2: for x be object st x in dom f holds f.x = r;
reconsider Df = dom f as Element of S by A1;
A3: 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)
proof
set F = <*Df*>;
A4: dom F = Seg 1 by FINSEQ_1:38;
A5: now
let i,j be Nat;
assume that
A6: i in dom F and
A7: j in dom F & i <> j;
i = 1 by A4,A6,FINSEQ_1:2,TARSKI:def 1;
hence F.i misses F.j by A4,A7,FINSEQ_1:2,TARSKI:def 1;
end;
A8: for n be Nat st n in dom F holds F.n = Df
proof
let n be Nat;
assume n in dom F;
then n = 1 by A4,FINSEQ_1:2,TARSKI:def 1;
hence thesis by FINSEQ_1:40;
end;
reconsider F as Finite_Sep_Sequence of S by A5,MESFUNC3:4;
take F;
F = <* F.1 *> by FINSEQ_1:40;
then
A9: rng F = {F.1} by FINSEQ_1:38;
1 in Seg 1;
then F.1 = Df by A4,A8;
hence dom f = union rng F by A9,ZFMISC_1:25;
hereby
let n be Nat, x,y be Element of X;
assume that
A10: n in dom F and
A11: x in F.n and
A12: y in F.n;
A13: F.n = Df by A8,A10;
then f.x = r by A2,A11;
hence f.x = f.y by A2,A12,A13;
end;
end;
now
let x be Element of X;
A14: r in REAL by XREAL_0:def 1;
assume x in dom f;
then
A15: f.x = r by A2;
then -infty < f.x by XXREAL_0:12,A14;
then
A16: -(+infty) < f.x by XXREAL_3:def 3;
f.x < +infty by A15,XXREAL_0:9,A14;
hence |. f.x .| < +infty by A16,EXTREAL1:22;
end;
then f is real-valued by MESFUNC2:def 1;
hence thesis by A3,MESFUNC2:def 4;
end;
theorem
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
proof
let x be set;
(ex y being Real st y=f.x & y < a) iff f.x < a;
hence thesis by MESFUNC1:def 11;
end;
theorem
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
proof
let x be set;
(ex y being Real st y=f.x & y <= a) iff f.x <= a;
hence thesis by MESFUNC1:def 12;
end;
theorem
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
proof
let x be set;
(ex y being Real st y=f.x & r < y) iff r < f.x;
hence thesis by MESFUNC1:def 13;
end;
theorem
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
proof
let x be set;
(ex y being Real st y=f.x & r <= y) iff r <= f.x;
hence thesis by MESFUNC1:def 14;
end;
theorem
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
proof
let x be set;
(ex y being Real st y=f.x & r = y) iff r = f.x;
hence thesis by MESFUNC1:def 15;
end;
theorem
(for n holds F.n = Y /\ great_dom(f,r-1/(n+1))) implies Y /\
great_eq_dom(f,r) = meet rng F
proof
assume for n holds F.n = Y /\ great_dom(f,r-1/(n+1));
then
for n be Element of NAT holds F.n = Y /\ great_dom(R_EAL f,(r-1/(n+
1)));
then Y /\ great_eq_dom(f,r) = meet rng F by MESFUNC1:19;
hence thesis;
end;
theorem
(for n holds F.n = Y /\ less_dom(f,(r+1/(n+1)))) implies Y /\
less_eq_dom(f,r) = meet rng F
proof
assume for n holds F.n = Y /\ less_dom(f,r+1/(n+1));
then
for n be Element of NAT holds F.n =Y /\ less_dom(R_EAL f,(r+1/(n+1) ));
then Y /\ less_eq_dom(f,r) = meet rng F by MESFUNC1:20;
hence thesis;
end;
theorem
(for n holds F.n = Y /\ less_eq_dom(f,r-1/(n+1))) implies Y /\
less_dom(f,r) = union rng F
proof
assume for n holds F.n = Y /\ less_eq_dom(f,r-1/(n+1));
then
for n be Element of NAT holds F.n =Y /\ less_eq_dom(R_EAL f,(r-1/(n
+1)));
then Y /\ less_dom(f,r) = union rng F by MESFUNC1:21;
hence thesis;
end;
theorem
(for n holds F.n = Y /\ great_eq_dom(f,r+1/(n+1))) implies Y /\
great_dom(f,r) = union rng F
proof
assume for n holds F.n = Y /\ great_eq_dom(f,r+1/(n+1));
then
for n be Element of NAT holds F.n =Y /\ great_eq_dom(R_EAL f,(r+1/(
n+1)));
then Y /\ great_dom(f,r) = union rng F by MESFUNC1:22;
hence thesis;
end;
definition
let X be non empty set;
let S be SigmaField of X;
let A be Element of S;
let f be PartFunc of X,REAL;
attr f is A-measurable means
R_EAL f is A-measurable;
end;
theorem Th12:
f is A-measurable iff for r being Real holds A /\
less_dom(f,r) in S by MESFUNC1:def 16;
theorem Th13:
A c= dom f implies (f is A-measurable iff for r being Real
holds A /\ great_eq_dom(f,r) in S) by MESFUNC1:27;
theorem
f is A-measurable iff for r being Real holds A /\
less_eq_dom(f,r) in S by MESFUNC1:28;
theorem
A c= dom f implies (f is A-measurable iff for r being Real
holds A /\ great_dom(f,r) in S ) by MESFUNC1:29;
theorem
B c= A & f is A-measurable implies f is B-measurable
by MESFUNC1:30;
theorem
f is A-measurable & f is B-measurable implies f is (A\/B)-measurable
by MESFUNC1:31;
theorem
f is A-measurable & A c= dom f implies A /\ great_dom(f,r) /\
less_dom(f,s) in S by MESFUNC1:32;
theorem
f is A-measurable & g is A-measurable & A c= dom g implies A /\
less_dom(f,r) /\ great_dom(g,r) in S
by MESFUNC1:36;
theorem Th20:
R_EAL(r(#)f)=r(#)R_EAL f
proof
dom(R_EAL(r(#)f)) = dom(R_EAL f) by VALUED_1:def 5;
then
A1: dom(R_EAL(r(#)f)) = dom(r(#)R_EAL f) by MESFUNC1:def 6;
now
let x be object;
reconsider rr= r as R_eal by XXREAL_0:def 1;
assume
A2: x in dom R_EAL(r(#)f);
then (R_EAL(r(#)f)).x = r*(f.x) by VALUED_1:def 5;
then (R_EAL(r(#)f)).x = rr * f.x by EXTREAL1:1;
hence (R_EAL(r(#)f)).x = (r(#)R_EAL f).x by A1,A2,MESFUNC1:def 6;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th21:
f is A-measurable & A c= dom f implies r(#)f is A-measurable
proof
assume that
A1: f is A-measurable and
A2: A c= dom f;
R_EAL f is A-measurable by A1;
then r(#)R_EAL f is A-measurable by A2,MESFUNC1:37;
then R_EAL(r(#)f) is A-measurable by Th20;
hence thesis;
end;
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
R_EAL f is real-valued;
theorem Th23:
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
proof
dom(R_EAL f - R_EAL g) = dom(R_EAL f) /\ dom(R_EAL g) by MESFUNC2:2;
then
A1: dom(R_EAL f - R_EAL g) = dom(f-g) by VALUED_1:12;
A2: now
let x be object;
assume
A3: x in dom(R_EAL f - R_EAL g);
then (R_EAL f - R_EAL g).x =(R_EAL f).x - (R_EAL g).x by MESFUNC1:def 4
.=f.x - g.x by SUPINF_2:3;
hence (R_EAL f - R_EAL g).x =(f-g).x by A1,A3,VALUED_1:13;
end;
dom(R_EAL f + R_EAL g) = dom(R_EAL f) /\ dom(R_EAL g) by MESFUNC2:2;
then
A4: dom(R_EAL f + R_EAL g) = dom(f+g) by VALUED_1:def 1;
now
let x be object;
assume
A5: x in dom(R_EAL f + R_EAL g);
then (R_EAL f + R_EAL g).x =(R_EAL f).x + (R_EAL g).x by MESFUNC1:def 3
.=f.x + g.x by SUPINF_2:1;
hence (R_EAL f + R_EAL g).x = (f+g).x by A4,A5,VALUED_1:def 1;
end;
hence thesis by A4,A1,A2,FUNCT_1:2,MESFUNC2:2;
end;
theorem
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
proof
let F be Function of RAT,S;
assume for p holds F.p = (A /\ less_dom(f,p)) /\ (A /\ less_dom(g,r-p));
then for p holds F.p = (A /\ less_dom(R_EAL f,p)) /\ (A /\ less_dom(
R_EAL g,r-p));
then
A1: A /\ less_dom(R_EAL f + R_EAL g,r) = union rng F by MESFUNC2:3;
R_EAL f + R_EAL g = R_EAL(f+g) by Th23;
hence thesis by A1;
end;
theorem
f is A-measurable & g is A-measurable 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))
by MESFUNC2:6;
theorem Th26:
f is A-measurable & g is A-measurable implies f+g is A-measurable
proof
assume f is A-measurable & g is A-measurable;
then R_EAL f is A-measurable & R_EAL g is A-measurable;
then R_EAL f + R_EAL g is A-measurable by MESFUNC2:7;
then R_EAL(f+g) is A-measurable by Th23;
hence thesis;
end;
theorem
R_EAL f - R_EAL g = R_EAL f + R_EAL -g
proof
R_EAL f - R_EAL g = R_EAL(f-g) by Th23
.=R_EAL(f + -g);
hence thesis by Th23;
end;
theorem Th28:
-R_EAL f = R_EAL((-1)(#)f) & -R_EAL f = R_EAL -f
proof
-R_EAL f = (-1)(#)R_EAL f by MESFUNC2:9;
hence thesis by Th20;
end;
theorem
f is A-measurable & g is A-measurable & A c= dom g implies
f-g is A-measurable
proof
assume that
A1: f is A-measurable and
A2: g is A-measurable and
A3: A c= dom g;
R_EAL g is A-measurable by A2;
then (-1)(#)R_EAL g is A-measurable by A3,MESFUNC1:37;
then -R_EAL g is A-measurable by MESFUNC2:9;
then
A4: R_EAL -g is A-measurable by Th28;
R_EAL f is A-measurable by A1;
then R_EAL f + R_EAL -g is A-measurable by A4,MESFUNC2:7;
then R_EAL(f-g) is A-measurable by Th23;
hence thesis;
end;
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 Th30:
max+(R_EAL f) = max+f & max-(R_EAL f) = max-f
proof
A1: dom max+(R_EAL f) = dom R_EAL f by MESFUNC2:def 2
.= dom max+f by RFUNCT_3:def 10;
now
let x be object;
assume
A2: x in dom max+(R_EAL f);
then (max+(R_EAL f)).x = max+(f.x) by MESFUNC2:def 2;
hence (max+(R_EAL f)).x = (max+f).x by A1,A2,RFUNCT_3:def 10;
end;
hence max+(R_EAL f) = max+f by A1,FUNCT_1:2;
A3: dom max-(R_EAL f) = dom R_EAL f by MESFUNC2:def 3
.=dom max-f by RFUNCT_3:def 11;
now
let x be object;
assume
A4: x in dom max-(R_EAL f);
(max-(R_EAL f)).x = max(-(((R_EAL f).x)),0.) by MESFUNC2:def 3,A4;
then (max-(R_EAL f)).x = max-(f.x) by SUPINF_2:2;
hence (max-(R_EAL f)).x = (max-f).x by A3,A4,RFUNCT_3:def 11;
end;
hence thesis by A3,FUNCT_1:2;
end;
theorem
for x being Element of X holds 0 <= (max+f).x
proof
let x be Element of X;
0. <= (max+(R_EAL f)).x by MESFUNC2:12;
hence thesis by Th30;
end;
theorem
for x being Element of X holds 0 <= (max-f).x
proof
let x be Element of X;
0. <= (max-(R_EAL f)).x by MESFUNC2:13;
hence thesis by Th30;
end;
theorem
max-f = max+(-f)
proof
max-f = max-(R_EAL f) by Th30;
then max-f = max+(-R_EAL f) by MESFUNC2:14;
then max-f = max+(R_EAL -f) by Th28;
hence thesis by Th30;
end;
theorem
for x being set st x in dom f & 0 < max+f.x holds max-f.x = 0
proof
let x be set;
assume that
A1: x in dom f and
A2: 0 < max+(f).x;
0. < (max+(R_EAL(f))).x by A2,Th30;
then max-(R_EAL(f)).x = 0. by A1,MESFUNC2:15;
hence thesis by Th30;
end;
theorem
for x being set st x in dom f & 0 < max-f.x holds max+f.x = 0
proof
let x be set;
assume that
A1: x in dom f and
A2: 0 < max-f.x;
0. < (max-(R_EAL f)).x by A2,Th30;
then max+(R_EAL f).x = 0. by A1,MESFUNC2:16;
hence thesis by Th30;
end;
theorem
dom f = dom (max+f - max-f) & dom f = dom (max+f + max-f)
proof
dom f = dom (max+(R_EAL f)-max-(R_EAL f)) by MESFUNC2:17;
then dom f = dom (R_EAL(max+f)-max-(R_EAL f)) by Th30;
then dom f = dom (R_EAL(max+f)-R_EAL(max-f)) by Th30;
then dom f = dom (R_EAL(max+f - max-f)) by Th23;
hence dom f =dom (max+f - max-f);
dom f = dom (max+(R_EAL f)+max-(R_EAL f)) by MESFUNC2:17;
then dom f = dom (R_EAL(max+f)+max-(R_EAL f)) by Th30;
then dom f = dom (R_EAL(max+f)+R_EAL(max-f)) by Th30;
then dom f = dom (R_EAL(max+f + max-f)) by Th23;
hence thesis;
end;
theorem
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)
proof
let x be set;
assume
A1: x in dom f;
then max+(R_EAL f).x = (R_EAL f).x or max+(R_EAL f).x = 0. by MESFUNC2:18;
hence max+f.x = f.x or max+f.x = 0 by Th30;
A2: max+(R_EAL f) = max+f & max-(R_EAL f) = max-f by Th30;
max-(R_EAL f).x = -((R_EAL f).x) or max-(R_EAL f).x = 0. by A1,MESFUNC2:18;
hence thesis by A2,SUPINF_2:2;
end;
theorem
for x being set st x in dom f & max+f.x = f.x holds max-f.x = 0
proof
let x be set;
assume that
A1: x in dom f and
A2: max+f.x =f.x;
f.x = max+(R_EAL f).x by A2,Th30;
then max-(R_EAL f).x = 0. by A1,MESFUNC2:19;
hence thesis by Th30;
end;
theorem
for x being set st x in dom f & max+f.x = 0 holds max-f.x = -(f.x)
proof
let x be set;
assume that
A1: x in dom f and
A2: max+f.x =0;
0 = max+(R_EAL f).x by A2,Th30;
then max-(R_EAL f).x =-((R_EAL f).x) by A1,MESFUNC2:20;
then max-f.x =-((R_EAL f).x) by Th30;
hence thesis by SUPINF_2:2;
end;
theorem
for x being set st x in dom f & max-f.x = -(f.x) holds max+f.x = 0
proof
let x be set;
assume that
A1: x in dom f and
A2: max-f.x = -(f.x);
-(f.x) = max-(R_EAL f).x by A2,Th30;
then -((R_EAL f).x) = max-(R_EAL f).x by SUPINF_2:2;
then max+(R_EAL f).x =0. by A1,MESFUNC2:21;
hence thesis by Th30;
end;
theorem
for x being set st x in dom f & max-f.x = 0 holds max+f.x = f.x
proof
let x be set;
assume that
A1: x in dom f and
A2: max-f.x =0;
0 = max-(R_EAL f).x by A2,Th30;
then max+(R_EAL f).x = (R_EAL f).x by A1,MESFUNC2:22;
hence thesis by Th30;
end;
theorem
f = max+f - max-f
proof
f = max+(R_EAL f)-max-(R_EAL f) by MESFUNC2:23;
then f = R_EAL(max+f)-max-(R_EAL f) by Th30;
then f = R_EAL(max+f)-R_EAL(max-f) by Th30;
then f = R_EAL(max+f - max-f) by Th23;
hence thesis;
end;
theorem Th43:
|.r qua Complex.| = |. r .|
proof
reconsider rr=r as Real;
per cases;
suppose
A1: 0 <= r;
then |. r .| = r by EXTREAL1:def 1;
hence thesis by A1,ABSVALUE:def 1;
end;
suppose
A2: r < 0;
then |. r .| =-(r qua ExtReal) by EXTREAL1:def 1;
then |. rr .| =-rr;
hence thesis by A2,ABSVALUE:def 1;
end;
end;
theorem Th44:
R_EAL(abs f) =|.R_EAL f.|
proof
A1: dom R_EAL(abs f) = dom f by VALUED_1:def 11
.= dom(|. R_EAL f .|) by MESFUNC1:def 10;
now
let x be object;
reconsider fx=f.x as Real;
(R_EAL(abs f)).x = |.fx qua Complex.| by VALUED_1:18;
then
A2: (R_EAL(abs f)).x = |.f.x.| by Th43;
assume x in dom R_EAL(abs f);
hence (R_EAL(abs f)).x =( |. R_EAL f .| ).x by A1,A2,MESFUNC1:def 10;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem
abs f = max+f + max-f
proof
abs f = R_EAL(abs f);
then abs f = |. R_EAL f .| by Th44;
then abs f = max+(R_EAL f) + max-(R_EAL f) by MESFUNC2:24;
then abs f = R_EAL(max+f)+max-(R_EAL f) by Th30;
then abs f = R_EAL(max+f)+R_EAL(max-f) by Th30;
then abs f = R_EAL(max+f + max-f) by Th23;
hence thesis;
end;
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 Th46:
f is A-measurable implies max+f is A-measurable
proof
assume f is A-measurable;
then R_EAL f is A-measurable;
then max+(R_EAL f) is A-measurable by MESFUNC2:25;
then R_EAL(max+f) is A-measurable by Th30;
hence thesis;
end;
theorem Th47:
f is A-measurable & A c= dom f implies max-f is A-measurable
proof
assume that
A1: f is A-measurable and
A2: A c= dom f;
R_EAL f is A-measurable by A1;
then max-(R_EAL f) is A-measurable by A2,MESFUNC2:26;
then R_EAL(max-f) is A-measurable by Th30;
hence thesis;
end;
theorem
f is A-measurable & A c= dom f implies abs f is A-measurable
proof
assume that
A1: f is A-measurable and
A2: A c= dom f;
R_EAL f is A-measurable by A1;
then |.R_EAL f.| is A-measurable by A2,MESFUNC2:27;
then R_EAL(abs f) is A-measurable by Th44;
hence thesis;
end;
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
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 Th49:
f is_simple_func_in S iff R_EAL f is_simple_func_in S by MESFUNC2:def 4;
theorem
f is_simple_func_in S implies f is A-measurable by Th49,MESFUNC2:34;
theorem Th51:
for X being set, f being PartFunc of X,REAL holds f is
nonnegative iff for x being object holds 0 <= f.x
proof
let X be set, f be PartFunc of X,REAL;
hereby
assume f is nonnegative;
then
A1: rng f is nonnegative;
hereby
let x be object;
now
assume x in dom f;
then
A2: f.x in rng f by FUNCT_1:def 3;
thus 0 <= f.x by A1,A2;
end;
hence 0 <= f.x by FUNCT_1:def 2;
end;
end;
assume
A3: for x being object holds 0 <= f.x;
let y be ExtReal;
assume y in rng f;
then ex x being object st x in dom f & y = f.x by FUNCT_1:def 3;
hence thesis by A3;
end;
theorem Th52:
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
proof
let X be set, f be PartFunc of X,REAL such that
A1: for x being object st x in dom f holds 0 <= f.x;
let y be ExtReal;
assume y in rng f;
then ex x being object st x in dom f & y = f.x by FUNCT_1:def 3;
hence thesis by A1;
end;
theorem
for X being set, f being PartFunc of X,REAL holds f is nonpositive iff
for x being set holds f.x <= 0
proof
let X be set, f be PartFunc of X,REAL;
hereby
assume f is nonpositive;
then
A1: rng f is nonpositive;
hereby
let x be set;
now
assume x in dom f;
then
A2: f.x in rng f by FUNCT_1:def 3;
thus f.x <= 0 by A1,A2;
end;
hence f.x <= 0 by FUNCT_1:def 2;
end;
end;
assume
A3: for x being set holds f.x <= 0;
let y be R_eal;
assume y in rng f;
then ex x being object st x in dom f & y = f.x by FUNCT_1:def 3;
hence thesis by A3;
end;
theorem Th54:
(for x being object st x in dom f holds f.x <= 0) implies f is nonpositive
proof
assume
A1: for x being object st x in dom f holds f.x <= 0;
let y be R_eal;
assume y in rng f;
then ex x being object st x in dom f & y = f.x by FUNCT_1:def 3;
hence thesis by A1;
end;
theorem
f is nonnegative implies f|Y is nonnegative
proof
assume f is nonnegative;
then
A1: rng f is nonnegative;
now
let y be ExtReal;
assume y in rng(f|Y);
then consider x be object such that
A2: x in dom(f|Y) and
A3: (f|Y).x = y by FUNCT_1:def 3;
x in dom f /\ Y by A2,RELAT_1:61;
then
A4: x in dom f by XBOOLE_0:def 4;
(f|Y).x = f.x by A2,FUNCT_1:47;
then (f|Y).x in rng f by A4,FUNCT_1:3;
hence 0. <= y by A1,A3;
end;
then rng(f|Y) is nonnegative;
hence thesis;
end;
theorem Th56:
f is nonnegative & g is nonnegative implies f+g is nonnegative
proof
assume that
A1: f is nonnegative and
A2: g is nonnegative;
for x be object st x in dom(f+g) holds 0 <= (f+g).x
proof
let x be object such that
A3: x in dom(f+g);
0 <= f.x by A1,Th51;
then
A4: g.x <= f.x + g.x by XREAL_1:31;
0 <= g.x by A2,Th51;
hence thesis by A3,A4,VALUED_1:def 1;
end;
hence thesis by Th52;
end;
theorem
f is nonnegative implies (0 <= r implies r(#)f is nonnegative) & (r <=
0 implies r(#)f is nonpositive)
proof
assume
A1: f is nonnegative;
hereby
assume
A2: 0 <= r;
now
let x be object such that
A3: x in dom(r(#)f);
0 <= f.x by A1,Th51;
then 0*r <= r*f.x by A2;
hence 0 <= (r(#)f).x by A3,VALUED_1:def 5;
end;
hence r(#)f is nonnegative by Th52;
end;
assume
A4: r <= 0;
now
let x be object such that
A5: x in dom(r(#)f);
0 <= f.x by A1,Th51;
then r*f.x <= r*0 by A4;
hence (r(#)f).x <= 0 by A5,VALUED_1:def 5;
end;
hence thesis by Th54;
end;
theorem Th58:
(for x be set st x in dom f /\ dom g holds g.x <= f.x) implies f
-g is nonnegative
proof
assume
A1: for x be set st x in dom f /\ dom g holds g.x <= f.x;
now
let x be object such that
A2: x in dom(f-g);
dom(f-g) = dom f /\ dom g by VALUED_1:12;
then 0 <= f.x - g.x by A1,A2,XREAL_1:48;
hence 0 <= (f-g).x by A2,VALUED_1:13;
end;
hence thesis by Th52;
end;
theorem
f is nonnegative & g is nonnegative & h is nonnegative implies f+g+h
is nonnegative
proof
assume that
A1: f is nonnegative & g is nonnegative and
A2: h is nonnegative;
f+g is nonnegative by A1,Th56;
hence thesis by A2,Th56;
end;
theorem Th60:
for x be object st x in dom(f+g+h) holds (f+g+h).x=f.x+g.x+h.x
proof
let x be object;
assume
A1: x in dom(f+g+h);
dom(f+g+h) = dom(f+g) /\ dom h by VALUED_1:def 1;
then x in dom(f+g) by A1,XBOOLE_0:def 4;
then f.x + g.x + h.x = (f+g).x + h.x by VALUED_1:def 1;
hence thesis by A1,VALUED_1:def 1;
end;
theorem
max+f is nonnegative & max-f is nonnegative
proof
for x be object st x in dom max+f holds 0 <= max+f.x by RFUNCT_3:37;
hence max+f is nonnegative by Th52;
for x be object st x in dom max-f holds 0 <= max-f.x by RFUNCT_3:40;
hence thesis by Th52;
end;
theorem Th62:
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
proof
A1: dom max-f = dom f & dom(max+(f+g) + max-f) = dom max+(f+g) /\ dom max-f
by RFUNCT_3:def 11,VALUED_1:def 1;
A2: dom max+f = dom f & dom(max-(f+g) + max+f) = dom max-(f+g) /\ dom max+f
by RFUNCT_3:def 10,VALUED_1:def 1;
A3: dom(f+g) = dom f /\ dom g by VALUED_1:def 1;
then
A4: dom(max-(f+g)) = dom f /\ dom g by RFUNCT_3:def 11;
dom(max+(f+g)) = dom f /\ dom g by A3,RFUNCT_3:def 10;
then
A5: dom(max+(f+g) + max-f) = dom g /\ (dom f /\ dom f) by A1,XBOOLE_1:16;
hence dom(max+(f+g) + max-f) = dom f /\ dom g & dom(max-(f+g) + max+f) = dom
f /\ dom g by A4,A2,XBOOLE_1:16;
dom max-g = dom g by RFUNCT_3:def 11;
then dom(max+(f+g) + max-f + max-g) = dom f /\ dom g /\ dom g by A5,
VALUED_1:def 1
.= dom f /\ (dom g /\ dom g) by XBOOLE_1:16;
hence dom(max+(f+g) + max-f + max-g) = dom f /\ dom g;
dom max+g = dom g & dom(max-(f+g) + max+f) = dom g /\ (dom f /\ dom f)
by A4,A2,RFUNCT_3:def 10,XBOOLE_1:16;
then dom(max-(f+g) + max+ f + max+ g) = dom f /\ dom g /\ dom g by
VALUED_1:def 1;
then dom(max-(f+g) + max+f + max+g) = dom f /\ (dom g /\ dom g) by
XBOOLE_1:16;
hence dom(max-(f+g) + max+f + max+g) = dom f /\ dom g;
now
let x be object;
assume
A6: x in dom(max+(f+g) + max-f);
then 0 <= max+(f+g).x & 0 <= max-f.x by RFUNCT_3:37,40;
then 0+0 <= max+(f+g).x + max-f.x;
hence 0 <= (max+(f+g) + max-f).x by A6,VALUED_1:def 1;
end;
hence max+(f+g) + max-f is nonnegative by Th52;
now
let x be object;
assume
A7: x in dom(max-(f+g) + max+f);
then 0 <= max-(f+g).x & 0 <= max+f.x by RFUNCT_3:37,40;
then 0+0 <= max-(f+g).x + max+f.x;
hence 0 <= (max-(f+g) + max+f).x by A7,VALUED_1:def 1;
end;
hence thesis by Th52;
end;
theorem
max+(f+g) + max-f + max-g = max-(f+g) + max+f + max+g
proof
A1: dom(max+(f+g))= dom (f+g) by RFUNCT_3:def 10;
A2: dom max+g = dom g by RFUNCT_3:def 10;
A3: dom max+f = dom f by RFUNCT_3:def 10;
A4: dom max-f = dom f by RFUNCT_3:def 11;
A5: dom max-g = dom g by RFUNCT_3:def 11;
A6: dom(max+(f+g) + max-f + max-g) = dom(max+(f+g) + max-f) /\ dom max-g by
VALUED_1:def 1
.= dom(f+g) /\ dom f /\ dom g by A1,A4,A5,VALUED_1:def 1;
then
A7: dom(max+(f+g) + max-f + max-g) = dom(f+g) /\ (dom f /\ dom g) by
XBOOLE_1:16;
A8: dom(max-(f+g))= dom (f+g) by RFUNCT_3:def 11;
A9: for x be object st x in dom(max+(f+g) + max-f + max-g) holds (max+(f+g) +
max-f + max-g).x = (max-(f+g) + max+f + max+g).x
proof
let x be object;
assume
A10: x in dom(max+(f+g) + max-f + max-g);
then
A11: x in dom g by A6,XBOOLE_0:def 4;
then
A12: (max+g).x = max+(g .x) by A2,RFUNCT_3:def 10;
A13: (max-g).x = max-(g.x) by A5,A11,RFUNCT_3:def 11;
A14: dom(f+g) = dom f /\ dom g by VALUED_1:def 1;
then
A15: max+(f+g).x = max+((f+g).x) by A1,A7,A10,RFUNCT_3:def 10
.= max((f.x+g.x),0) by A7,A10,A14,VALUED_1:def 1;
A16: x in dom f by A7,A10,A14,XBOOLE_0:def 4;
then
A17: (max+f).x = max+(f.x) by A3,RFUNCT_3:def 10;
A18: max-(f+g).x = max-((f+g).x) by A8,A7,A10,A14,RFUNCT_3:def 11
.= max(-(f.x+g.x),0) by A7,A10,A14,VALUED_1:def 1;
A19: (max-f).x = max-(f.x) by A4,A16,RFUNCT_3:def 11;
A20: now
assume
A21: 0 <= f.x;
then
A22: max-f.x =0 by A19,XXREAL_0:def 10;
A23: now
assume
A24: g.x < 0;
then
A25: (max-g).x= -g.x by A13,XXREAL_0:def 10;
A26: (max+g).x = 0 by A12,A24,XXREAL_0:def 10;
A27: now
assume
A28: f.x + g.x < 0;
then (max-(f+g)).x = -(f.x + g.x) by A18,XXREAL_0:def 10;
then (max-(f+g)).x + (max+f).x + (max+g).x
= -(f.x + (g.x qua Real)) +f.x + 0
by A17,A21,A26,XXREAL_0:def 10;
hence
(max+(f+g)).x + (max-f).x + (max-g).x =(max-(f+g)).x + (max+f).
x + (max+g).x by A15,A22,A25,A28,XXREAL_0:def 10;
end;
now
assume 0 <= f.x + g.x;
then
(max-(f+g)).x=0 & (max+(f+g)).x + (max-f).x + (max-g).x
=f.x+ (g.x qua Real) + 0 + -(g.x qua Real)
by A15,A18,A22,A25,XXREAL_0:def 10;
hence
(max+(f+g)).x+ (max-f).x + (max-g).x =(max-(f+g)).x + (max+f).x
+ (max+g).x by A17,A21,A26,XXREAL_0:def 10;
end;
hence
(max+(f+g)).x+ (max-f).x + (max-g).x =(max-(f+g)).x + (max+f).x +
(max+g).x by A27;
end;
now
assume
A29: 0 <= g.x;
then (max-g).x=0 by A13,XXREAL_0:def 10;
then
A30: (max+(f+g)).x + (max-f).x + (max-g).x = f.x + g.x by A15,A21,A22,A29,
XXREAL_0:def 10;
(max-(f+g)).x=0 & (max+g).x = g.x by A18,A12,A21,A29,XXREAL_0:def 10;
hence (max+(f+g)).x + (max-f).x + (max-g).x =(max-(f+g)).x + (max+f).x
+ (max+g).x by A17,A21,A30,XXREAL_0:def 10;
end;
hence (max+(f+g)).x + (max-f).x + (max-g).x =(max-(f+g)).x + (max+f).x +
(max+g).x by A23;
end;
A31: now
assume
A32: f.x < 0;
then
A33: (max-f).x = -f.x by A19,XXREAL_0:def 10;
A34: now
assume
A35: 0 <= g.x;
then
A36: (max-g).x = 0 by A13,XXREAL_0:def 10;
A37: (max+g).x = g.x by A12,A35,XXREAL_0:def 10;
A38: now
assume
A39: f.x + g.x < 0;
then (max-(f+g)).x = -(f.x + g.x) by A18,XXREAL_0:def 10;
then (max-(f+g)).x + (max+f).x + (max+g).x
= -(f.x + (g.x qua Real)) + 0 + g.x
by A17,A32,A37,XXREAL_0:def 10
.=-f.x + (-g.x +g.x);
hence
(max+(f+g)).x + (max-f).x + (max-g).x =(max-(f+g)).x + (max+f).
x + (max+g).x by A15,A33,A36,A39,XXREAL_0:def 10;
end;
now
assume 0 <= f.x + g.x;
then (max-(f+g)).x = 0 & (max+(f+g)).x + (max-f).x + (max-g).x
=f.x + (g.x qua Real) + -(f.x qua Real) + 0
by A15,A18,A33,A36,XXREAL_0:def 10;
hence
(max+(f+g)).x + (max-f).x + (max-g).x =(max-(f+g)).x + (max+f).
x + (max+g).x by A17,A32,A37,XXREAL_0:def 10;
end;
hence (max+(f+g)).x + (max-f).x + (max-g).x =(max-(f+g)).x + (max+f).x
+ (max+g).x by A38;
end;
now
assume
A40: g.x < 0;
then (max-(f+g)).x=-(f.x + g.x) & (max+g).x = 0 by A18,A12,A32,
XXREAL_0:def 10;
then
A41: (max-(f+g)).x + (max+f).x + (max+g).x
= -(f.x + (g.x qua Real)) + 0 + 0 by A17,A32
,XXREAL_0:def 10;
(max-g).x=-g.x by A13,A40,XXREAL_0:def 10;
then
(max+(f+g)).x+ (max-f).x + (max-g).x
= 0 + -(f.x qua Real) + -(g.x qua Real)
by A15,A32,A33
,A40,XXREAL_0:def 10;
hence
(max+(f+g)).x+ (max-f).x + (max-g).x =(max-(f+g)).x + (max+f).x +
(max+g).x by A41;
end;
hence (max+(f+g)).x + (max-f).x + (max-g).x =(max-(f+g)).x + (max+f).x +
(max+g).x by A34;
end;
x in dom f /\ dom g by A10,Th62;
then x in dom(max-(f+g) + max+f + max+g) by Th62;
then (max-(f+g)+ max+f + max+g).x =(max-(f+g)).x +(max+f).x +(max+g).x by
Th60;
hence thesis by A10,A20,A31,Th60;
end;
dom(max+(f+g) + max-f + max-g) = dom f /\ dom g by Th62;
then dom(max+(f+g) + max-f + max-g) = dom(max-(f+g) + max+f + max+g) by Th62;
hence thesis by A9,FUNCT_1:2;
end;
theorem
0 <= r implies max+(r(#)f) = r(#)max+f & max-(r(#)f) = r(#)max-f
proof
assume
A1: 0 <= r;
A2: dom max+(r(#)f) = dom(r(#)f) by RFUNCT_3:def 10
.= dom f by VALUED_1:def 5
.= dom max+f by RFUNCT_3:def 10
.= dom(r(#)max+f) by VALUED_1:def 5;
reconsider rr=r as Real;
for x be Element of X st x in dom max+(r(#)f) holds (max+(r(#)f)).x = (r
(#)max+f).x
proof
let x be Element of X;
assume
A3: x in dom max+(r(#)f);
then
A4: x in dom(r(#)f) by RFUNCT_3:def 10;
then x in dom f by VALUED_1:def 5;
then
A5: x in dom max+ f by RFUNCT_3:def 10;
A6: (max+(r(#)f)).x = max+((r(#)f).x) by A3,RFUNCT_3:def 10
.= max(r*f.x,0) by A4,VALUED_1:def 5;
(r(#)max+f).x = r * max+f.x by A2,A3,VALUED_1:def 5
.= rr * max+(f.x) by A5,RFUNCT_3:def 10
.= max(rr * f.x,rr * 0) by A1,FUZZY_2:41;
hence thesis by A6;
end;
hence max+(r(#)f) = r(#)max+f by A2,PARTFUN1:5;
A7: dom(max-(r(#)f)) = dom(r(#)f) by RFUNCT_3:def 11
.= dom f by VALUED_1:def 5
.= dom max-f by RFUNCT_3:def 11
.= dom(r(#)max-f) by VALUED_1:def 5;
for x be Element of X st x in dom max-(r(#)f) holds (max-(r(#)f)).x = (
r(#)max-f).x
proof
let x be Element of X;
assume
A8: x in dom max-(r(#)f);
then
A9: x in dom(r(#)f) by RFUNCT_3:def 11;
then x in dom f by VALUED_1:def 5;
then
A10: x in dom max- f by RFUNCT_3:def 11;
A11: (max-(r(#)f)).x = max-((r(#)f).x) by A8,RFUNCT_3:def 11
.= max(-(r*f.x),0) by A9,VALUED_1:def 5;
(r(#)max-f).x = r * max-f.x by A7,A8,VALUED_1:def 5
.= rr * max-(f.x) by A10,RFUNCT_3:def 11
.= max(rr*(-(f.x qua Real)qua Real),rr*0 )
by A1,FUZZY_2:41
.= max(-(r)*f.x,r*0);
hence thesis by A11;
end;
hence thesis by A7,PARTFUN1:5;
end;
theorem
0 <= r implies max+((-r)(#)f) = r(#)max-f & max-((-r)(#)f) = r(#)max+f
proof
assume
A1: 0 <= r;
A2: dom max+((-r)(#)f) = dom((-r)(#)f) by RFUNCT_3:def 10;
then dom max+((-r)(#)f) = dom f by VALUED_1:def 5;
then
A3: dom max+((-r)(#)f) = dom max-f by RFUNCT_3:def 11;
then
A4: dom max+((-r)(#)f) = dom(r(#)max-f) by VALUED_1:def 5;
reconsider rr=r as Real;
for x be Element of X st x in dom max+((-r)(#)f) holds max+((-r)(#)f).x
= (r(#)max-f).x
proof
let x be Element of X;
assume
A5: x in dom max+((-r)(#)f);
then
A6: (max+((-r)(#)f)).x = max+(((-r)(#)f).x) by RFUNCT_3:def 10
.= max((-r)*f.x,0) by A2,A5,VALUED_1:def 5;
(r(#)max-f).x = r * max-f.x by A4,A5,VALUED_1:def 5
.= rr * max-(f.x) by A3,A5,RFUNCT_3:def 11
.= max(rr * (-(f.x qua Real)qua Real),rr * 0)
by A1,FUZZY_2:41;
hence thesis by A6;
end;
hence max+((-r)(#)f) = r(#)max-f by A4,PARTFUN1:5;
A7: dom max-((-r)(#)f) = dom((-r)(#)f) by RFUNCT_3:def 11;
then dom max-((-r)(#)f) = dom f by VALUED_1:def 5;
then
A8: dom max-((-r)(#)f) = dom max+f by RFUNCT_3:def 10;
then
A9: dom max-((-r)(#)f) = dom(r(#) max+ f) by VALUED_1:def 5;
for x be Element of X st x in dom max-((-r)(#)f) holds max-((-r)(#)f).x
= (r(#)max+f).x
proof
let x be Element of X;
assume
A10: x in dom max-((-r)(#)f);
then
A11: max-((-r)(#)f).x = max-(((-r)(#)f).x) by RFUNCT_3:def 11
.= max(-((-r))*f.x,0) by A7,A10,VALUED_1:def 5;
(r(#)max+f).x = r * max+f.x by A9,A10,VALUED_1:def 5
.= rr * max+(f.x) by A8,A10,RFUNCT_3:def 10
.= max(rr*f.x,rr*0) by A1,FUZZY_2:41;
hence thesis by A11;
end;
hence thesis by A9,PARTFUN1:5;
end;
theorem
max+(f|Y)=max+f|Y & max-(f|Y)=max-f|Y
proof
A1: dom max+(f|Y) = dom(f|Y) by RFUNCT_3:def 10
.= dom f /\ Y by RELAT_1:61
.= dom max+f /\ Y by RFUNCT_3:def 10
.= dom(max+f|Y) by RELAT_1:61;
for x being Element of X st x in dom max+(f|Y) holds (max+(f|Y)).x = (
max+f|Y).x
proof
let x be Element of X;
assume
A2: x in dom max+(f|Y);
then
A3: x in dom max+f /\ Y by A1,RELAT_1:61;
then
A4: x in Y by XBOOLE_0:def 4;
A5: x in dom max+f by A3,XBOOLE_0:def 4;
A6: (max+(f|Y)).x = max+((f|Y).x) by A2,RFUNCT_3:def 10
.= max(f.x,0) by A4,FUNCT_1:49;
(max+f|Y).x = (max+f).x by A1,A2,FUNCT_1:47
.= max+(f.x) by A5,RFUNCT_3:def 10;
hence thesis by A6;
end;
hence max+(f|Y) = max+f|Y by A1,PARTFUN1:5;
A7: dom max-(f|Y) = dom(f|Y) by RFUNCT_3:def 11
.= dom f /\ Y by RELAT_1:61
.= dom max-f /\ Y by RFUNCT_3:def 11
.= dom(max-f|Y) by RELAT_1:61;
for x being Element of X st x in dom max-(f|Y) holds (max-(f|Y)).x = (
max-f|Y).x
proof
let x be Element of X;
assume
A8: x in dom max-(f|Y);
then
A9: x in dom max-f /\ Y by A7,RELAT_1:61;
then
A10: x in Y by XBOOLE_0:def 4;
A11: x in dom max-f by A9,XBOOLE_0:def 4;
A12: (max-(f|Y)).x = max-((f|Y).x) by A8,RFUNCT_3:def 11
.= max(-f.x,0) by A10,FUNCT_1:49;
(max-f|Y).x = (max-f).x by A7,A8,FUNCT_1:47
.= max-(f.x) by A11,RFUNCT_3:def 11;
hence thesis by A12;
end;
hence thesis by A7,PARTFUN1:5;
end;
theorem
Y c= dom(f+g) implies dom((f+g)|Y) = Y & dom(f|Y+g|Y)=Y & (f+g)|Y = f|Y +g|Y
proof
assume
A1: Y c= dom(f+g);
dom(f|Y) /\ dom(g|Y) = dom f /\ Y /\ dom(g|Y) by RELAT_1:61
.= dom f /\ Y /\ (dom g /\ Y) by RELAT_1:61
.= dom f /\ Y /\ dom g /\ Y by XBOOLE_1:16
.= dom f /\ dom g /\ Y /\ Y by XBOOLE_1:16
.= dom f /\ dom g /\ (Y /\ Y) by XBOOLE_1:16;
then
A2: dom(f|Y+g|Y) = dom f /\ dom g /\ Y by VALUED_1:def 1
.= dom(f+g) /\ Y by VALUED_1:def 1
.= Y by A1,XBOOLE_1:28;
A3: dom(f+g) = dom f /\ dom g by VALUED_1:def 1;
dom(g|Y) = dom g /\ Y by RELAT_1:61;
then
A4: dom(g|Y) = Y by A1,A3,XBOOLE_1:18,28;
A5: dom((f+g)|Y) =dom(f+g) /\ Y by RELAT_1:61;
then
A6: dom((f+g)|Y) = Y by A1,XBOOLE_1:28;
dom(f|Y) = dom f /\ Y by RELAT_1:61;
then
A7: dom(f|Y) = Y by A1,A3,XBOOLE_1:18,28;
now
let x be object;
assume
A8: x in dom((f+g)|Y);
hence ((f+g)|Y).x = (f+g).x by FUNCT_1:47
.=f.x+g.x by A1,A6,A8,VALUED_1:def 1
.=(f|Y).x + g.x by A6,A7,A8,FUNCT_1:47
.=(f|Y).x + (g|Y).x by A6,A4,A8,FUNCT_1:47
.= ((f|Y)+(g|Y)).x by A6,A2,A8,VALUED_1:def 1;
end;
hence thesis by A1,A5,A2,FUNCT_1:2,XBOOLE_1:28;
end;
theorem
eq_dom(f,r) = f"{r}
proof
now
let x be object;
assume
A1: x in f"{r};
then f.x in {r} by FUNCT_1:def 7;
then
A2: (R_EAL f).x = r by TARSKI:def 1;
x in dom f by A1,FUNCT_1:def 7;
hence x in eq_dom(f,r) by A2,MESFUNC1:def 15;
end;
then
A3: f"{r} c= eq_dom(f,r);
now
let x be object;
assume
A4: x in eq_dom(f,r);
then r = f.x by MESFUNC1:def 15;
then
A5: f.x in {r} by TARSKI:def 1;
x in dom f by A4,MESFUNC1:def 15;
hence x in f"{r} by A5,FUNCT_1:def 7;
end;
then eq_dom(f,r) c= f"{r};
hence thesis by A3;
end;
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
f is A-measurable & A c= dom f implies A /\ great_eq_dom(f,r) /\
less_dom(f,s) in S
proof
assume that
A1: f is A-measurable and
A2: A c= dom f;
R_EAL f is A-measurable by A1;
then
A3: A /\ less_dom(R_EAL f,s) in S by MESFUNC1:def 16;
A4: A /\ great_eq_dom(f,r) /\ (A /\ less_dom(f,s)) = A /\ great_eq_dom(f,r)
/\ A /\ less_dom(f,s) by XBOOLE_1:16
.= great_eq_dom(f,r) /\ (A/\A) /\ less_dom(f,s) by XBOOLE_1:16;
A /\ great_eq_dom(f,r) in S by A1,A2,Th13;
hence thesis by A3,A4,FINSUB_1:def 2;
end;
theorem Th70:
f is_simple_func_in S implies f|A is_simple_func_in S
proof
assume f is_simple_func_in S;
then consider F be Finite_Sep_Sequence of S such that
A1: dom f = union rng F and
A2: for n be 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;
deffunc FA(Nat) = F.$1 /\ A;
consider G be FinSequence such that
A3: len G = len F & for n be Nat st n in dom G holds G.n = FA(n) from
FINSEQ_1:sch 2;
A4: rng G c= S
proof
let P be object;
assume P in rng G;
then consider k be object such that
A5: k in dom G and
A6: P = G.k by FUNCT_1:def 3;
reconsider k as Element of NAT by A5;
k in Seg len F by A3,A5,FINSEQ_1:def 3;
then k in dom F by FINSEQ_1:def 3;
then
A7: F.k in rng F by FUNCT_1:3;
G.k = F.k /\ A by A3,A5;
hence thesis by A6,A7,FINSUB_1:def 2;
end;
A8: dom G = Seg len F by A3,FINSEQ_1:def 3;
reconsider G as FinSequence of S by A4,FINSEQ_1:def 4;
for i,j be Nat st i in dom G & j in dom G & i <> j holds G.i misses G.j
proof
let i,j be Nat;
assume that
A9: i in dom G and
A10: j in dom G and
A11: i <> j;
j in Seg len F by A3,A10,FINSEQ_1:def 3;
then
A12: j in dom F by FINSEQ_1:def 3;
i in Seg len F by A3,A9,FINSEQ_1:def 3;
then i in dom F by FINSEQ_1:def 3;
then
A13: F.i misses F.j by A11,A12,MESFUNC3:4;
G.i = F.i /\ A & G.j = F.j /\ A by A3,A9,A10;
then G.i /\ G.j = F.i /\ A /\ F.j /\ A by XBOOLE_1:16
.= F.i /\ F.j /\ A /\ A by XBOOLE_1:16
.= {} /\ A /\ A by A13;
hence thesis;
end;
then reconsider G as Finite_Sep_Sequence of S by MESFUNC3:4;
for v be object st v in union rng G holds v in dom(f|A)
proof
let v be object;
assume v in union rng G;
then consider W be set such that
A14: v in W and
A15: W in rng G by TARSKI:def 4;
consider k be object such that
A16: k in dom G and
A17: W = G.k by A15,FUNCT_1:def 3;
reconsider k as Element of NAT by A16;
k in Seg(len F) by A3,A16,FINSEQ_1:def 3;
then k in dom F by FINSEQ_1:def 3;
then
A18: F.k in rng F by FUNCT_1:3;
A19: G.k = F.k /\ A by A3,A16;
then v in F.k by A14,A17,XBOOLE_0:def 4;
then
A20: v in union rng F by A18,TARSKI:def 4;
v in A by A14,A17,A19,XBOOLE_0:def 4;
then v in dom f /\ A by A1,A20,XBOOLE_0:def 4;
hence thesis by RELAT_1:61;
end;
then
A21: union rng G c= dom(f|A);
for v be object st v in dom(f|A) holds v in union rng G
proof
let v be object;
assume v in dom(f|A);
then
A22: v in dom f /\ A by RELAT_1:61;
then
A23: v in A by XBOOLE_0:def 4;
v in dom f by A22,XBOOLE_0:def 4;
then consider W be set such that
A24: v in W and
A25: W in rng F by A1,TARSKI:def 4;
consider k be object such that
A26: k in dom F and
A27: W = F.k by A25,FUNCT_1:def 3;
reconsider k as Element of NAT by A26;
A28: k in Seg len F by A26,FINSEQ_1:def 3;
then k in dom G by A3,FINSEQ_1:def 3;
then
A29: G.k in rng G by FUNCT_1:3;
G.k = F.k /\ A by A3,A8,A28;
then v in G.k by A23,A24,A27,XBOOLE_0:def 4;
hence thesis by A29,TARSKI:def 4;
end;
then dom(f|A) c= union rng G;
then
A30: dom(f|A) = union rng G by A21;
for n be Nat, x,y be Element of X st n in dom G & x in G.n & y in G.n
holds (f|A).x = (f|A).y
proof
let n be Nat;
let x,y be Element of X;
assume that
A31: n in dom G and
A32: x in G.n and
A33: y in G.n;
n in Seg(len F) by A3,A31,FINSEQ_1:def 3;
then
A34: n in dom F by FINSEQ_1:def 3;
G.n = F.n /\ A by A3,A31;
then x in F.n & y in F.n by A32,A33,XBOOLE_0:def 4;
then
A35: f.x = f.y by A2,A34;
A36: G.n in rng G by A31,FUNCT_1:3;
then x in dom(f|A) by A30,A32,TARSKI:def 4;
then
A37: (f|A).x = f.y by A35,FUNCT_1:47;
y in dom(f|A) by A30,A33,A36,TARSKI:def 4;
hence thesis by A37,FUNCT_1:47;
end;
hence thesis by A30;
end;
theorem Th71:
f is_simple_func_in S implies dom f is Element of S
by MESFUNC2:31;
Lm1: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,
g be PartFunc of X,REAL st f is_simple_func_in S & dom f <> {} & g
is_simple_func_in S & dom g = dom f holds f+g is_simple_func_in S & dom(f+g) <>
{}
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g
be PartFunc of X,REAL such that
A1: f is_simple_func_in S and
A2: dom f <> {} and
A3: g is_simple_func_in S and
A4: dom g = dom f;
R_EAL f is_simple_func_in S by A1,Th49;
then consider
F be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL such
that
A5: F,a are_Re-presentation_of R_EAL f by MESFUNC3:12;
set la = len F;
A6: dom f = union rng F by A5,MESFUNC3:def 1;
R_EAL g is_simple_func_in S by A3,Th49;
then consider
G be Finite_Sep_Sequence of S, b be FinSequence of ExtREAL such
that
A7: G,b are_Re-presentation_of R_EAL g by MESFUNC3:12;
set lb = len G;
A8: dom(f+g) = dom f /\ dom g by VALUED_1:def 1;
deffunc FG1(Nat) = F.(($1-'1) div lb + 1) /\ G.(($1-'1) mod lb + 1);
consider FG be FinSequence such that
A9: len FG = la*lb and
A10: for k be Nat st k in dom FG holds FG.k=FG1(k) from FINSEQ_1:sch 2;
A11: dom FG = Seg(la*lb) by A9,FINSEQ_1:def 3;
now
reconsider la9=la,lb9=lb as Nat;
let k be Nat;
set i=(k-'1) div lb + 1;
set j=(k-'1) mod lb + 1;
assume
A12: k in dom FG;
then
A13: k in Seg(la*lb) by A9,FINSEQ_1:def 3;
then
A14: k <= la*lb by FINSEQ_1:1;
then (k -' 1) <= (la*lb -' 1) by NAT_D:42;
then
A15: (k -' 1) div lb <= (la*lb -' 1) div lb by NAT_2:24;
1 <= k by A13,FINSEQ_1:1;
then
A16: lb9 divides (la9*lb9) & 1 <= la*lb by A14,NAT_D:def 3,XXREAL_0:2;
A17: lb <> 0 by A13,A14,FINSEQ_1:1;
then lb >= 0+1 by NAT_1:13;
then ((la9*lb9) -' 1) div lb9 = ((la9*lb9) div lb9) - 1 by A16,NAT_2:15;
then (k -' 1) div lb + 1 <= la*lb div lb by A15,XREAL_1:19;
then i >= 0+1 & i <= la by A17,NAT_D:18,XREAL_1:6;
then i in Seg la;
then i in dom F by FINSEQ_1:def 3;
then
A18: F.i in rng F by FUNCT_1:3;
(k -' 1) mod lb < lb by A17,NAT_D:1;
then j >= 0+1 & j <= lb by NAT_1:13;
then j in dom G by FINSEQ_3:25;
then G.j in rng G by FUNCT_1:3;
then F.i /\ G.j in S by A18,MEASURE1:34;
hence FG.k in S by A10,A12;
end;
then reconsider FG as FinSequence of S by FINSEQ_2:12;
for k,l be Nat st k in dom FG & l in dom FG & k <> l holds FG.k misses FG. l
proof
reconsider la9=la,lb9=lb as Nat;
let k,l be Nat;
assume that
A19: k in dom FG and
A20: l in dom FG and
A21: k <> l;
set j=(k-'1) mod lb + 1;
set i=(k-'1) div lb + 1;
A22: FG.k = F.i /\ G.j by A10,A19;
set m=(l-'1) mod lb + 1;
set n=(l-'1) div lb + 1;
A23: k in Seg(la*lb) by A9,A19,FINSEQ_1:def 3;
then
A24: 1 <= k by FINSEQ_1:1;
then
A25: lb <> 0 by A23,FINSEQ_1:1;
then (k -' 1) mod lb < lb by NAT_D:1;
then j >= 0+1 & j <= lb by NAT_1:13;
then
A26: j in dom G by FINSEQ_3:25;
A27: k <= la*lb by A23,FINSEQ_1:1;
then
A28: lb9 divides (la9*lb9) & 1 <= la*lb by A24,NAT_D:def 3,XXREAL_0:2;
lb >= 0+1 by A25,NAT_1:13;
then
A29: ((la9*lb9) -' 1) div lb9 = ((la9*lb9) div lb9) - 1 by A28,NAT_2:15;
A30: l in Seg (la*lb) by A9,A20,FINSEQ_1:def 3;
then
A31: 1 <= l by FINSEQ_1:1;
A32: now
(l-'1)+1=(n-1)*lb+(m-1)+1 by A25,NAT_D:2;
then
A33: l - 1 + 1 = (n-1)*lb+m by A31,XREAL_1:233;
(k-'1)+1=(i-1)*lb+(j-1)+1 by A25,NAT_D:2;
then
A34: k - 1 + 1 = (i-1)*lb + j by A24,XREAL_1:233;
assume i=n & j=m;
hence contradiction by A21,A34,A33;
end;
(k -' 1) <= (la*lb -' 1) by A27,NAT_D:42;
then (k -' 1) div lb <= (la*lb div lb) - 1 by A29,NAT_2:24;
then (k -' 1) div lb + 1 <= la*lb div lb by XREAL_1:19;
then i >= 0+1 & i <= la by A25,NAT_D:18,XREAL_1:6;
then i in Seg la;
then
A35: i in dom F by FINSEQ_1:def 3;
(l -' 1) mod lb < lb by A25,NAT_D:1;
then m >= 0+1 & m <= lb by NAT_1:13;
then
A36: m in dom G by FINSEQ_3:25;
l <= la*lb by A30,FINSEQ_1:1;
then (l -' 1) <= (la*lb -' 1) by NAT_D:42;
then (l -' 1) div lb <= (la*lb div lb) - 1 by A29,NAT_2:24;
then (l -' 1) div lb + 1 <= la*lb div lb by XREAL_1:19;
then n >= 0+1 & n <= la by A25,NAT_D:18,XREAL_1:6;
then n in Seg la;
then
A37: n in dom F by FINSEQ_1:def 3;
per cases by A32;
suppose
A38: i <> n;
FG.k /\ FG.l= F.i /\ G.j /\ (F.n /\ G.m) by A10,A20,A22;
then FG.k /\ FG.l= F.i /\ (G.j /\ (F.n /\ G.m)) by XBOOLE_1:16;
then FG.k /\ FG.l= F.i /\ (F.n /\ (G.j /\ G.m)) by XBOOLE_1:16;
then
A39: FG.k /\ FG.l= F.i /\ F.n /\ (G.j /\ G.m) by XBOOLE_1:16;
F.i misses F.n by A35,A37,A38,MESFUNC3:4;
then FG.k /\ FG.l= {} /\ (G.j /\ G.m) by A39;
hence thesis;
end;
suppose
A40: j <> m;
FG.k /\ FG.l= F.i /\ G.j /\ (F.n /\ G.m) by A10,A20,A22;
then FG.k /\ FG.l= F.i /\ (G.j /\ (F.n /\ G.m)) by XBOOLE_1:16;
then FG.k /\ FG.l= F.i /\ (F.n /\ (G.j /\ G.m)) by XBOOLE_1:16;
then
A41: FG.k /\ FG.l= F.i /\ F.n /\ (G.j /\ G.m) by XBOOLE_1:16;
G.j misses G.m by A26,A36,A40,MESFUNC3:4;
then FG.k /\ FG.l= F.i /\ F.n /\ {} by A41;
hence thesis;
end;
end;
then reconsider FG as Finite_Sep_Sequence of S by MESFUNC3:4;
A42: dom g = union rng G by A7,MESFUNC3:def 1;
A43: dom f = union rng FG
proof
now
let z be object;
assume
A44: z in dom f;
then consider Y be set such that
A45: z in Y and
A46: Y in rng F by A6,TARSKI:def 4;
consider i be Nat such that
A47: i in dom F and
A48: Y = F.i by A46,FINSEQ_2:10;
A49: i in Seg len F by A47,FINSEQ_1:def 3;
then 1 <= i by FINSEQ_1:1;
then consider i9 be Nat such that
A50: i = 1 + (i9 qua Complex) by NAT_1:10;
consider Z be set such that
A51: z in Z and
A52: Z in rng G by A4,A42,A44,TARSKI:def 4;
consider j be Nat such that
A53: j in dom G and
A54: Z = G.j by A52,FINSEQ_2:10;
A55: j in Seg len G by A53,FINSEQ_1:def 3;
then
A56: 1 <= j by FINSEQ_1:1;
then consider j9 be Nat such that
A57: j = 1 + (j9 qua Complex) by NAT_1:10;
A58: j <= lb by A55,FINSEQ_1:1;
then
A59: j9 < lb by A57,NAT_1:13;
reconsider k=(i-1)*lb+j as Nat by A50;
A60: k >= 0 + j by A50,XREAL_1:6;
then
A61: k -' 1 = k - 1 by A56,XREAL_1:233,XXREAL_0:2
.= i9*lb + j9 by A50,A57;
then
A62: i = (k-'1) div lb +1 by A50,A59,NAT_D:def 1;
i <= la by A49,FINSEQ_1:1;
then i-1 <= la-1 by XREAL_1:9;
then (i-1)*lb <= (la - 1)*lb by XREAL_1:64;
then
A63: k <= (la - 1) * lb + j by XREAL_1:6;
(la - 1) * lb + j <= (la - 1) * lb + lb by A58,XREAL_1:6;
then
A64: k <= la*lb by A63,XXREAL_0:2;
k >= 1 by A56,A60,XXREAL_0:2;
then
A65: k in Seg (la*lb) by A64;
then k in dom FG by A9,FINSEQ_1:def 3;
then
A66: FG.k in rng FG by FUNCT_1:def 3;
A67: j = (k-'1) mod lb +1 by A57,A61,A59,NAT_D:def 2;
z in F.i /\ G.j by A45,A48,A51,A54,XBOOLE_0:def 4;
then z in FG.k by A10,A11,A62,A67,A65;
hence z in union rng FG by A66,TARSKI:def 4;
end;
hence dom f c= union rng FG;
reconsider la9=la,lb9=lb as Nat;
let z be object;
assume z in union rng FG;
then consider Y be set such that
A68: z in Y and
A69: Y in rng FG by TARSKI:def 4;
consider k be Nat such that
A70: k in dom FG and
A71: Y = FG.k by A69,FINSEQ_2:10;
set j=(k-'1) mod lb +1;
set i=(k-'1) div lb +1;
A72: k in Seg len FG by A70,FINSEQ_1:def 3;
then
A73: k <= la*lb by A9,FINSEQ_1:1;
then
A74: lb <> 0 by A72,FINSEQ_1:1;
then
A75: lb >= 0+1 by NAT_1:13;
1 <= k by A72,FINSEQ_1:1;
then lb9 divides (la9*lb9) & 1 <= la*lb by A73,NAT_D:def 3,XXREAL_0:2;
then
A76: ((la9*lb9) -' 1) div lb9 = ((la9*lb9) div lb9) - 1 by A75,NAT_2:15;
(k -' 1) <= (la*lb -' 1) by A73,NAT_D:42;
then (k -' 1) div lb <= (la*lb div lb) - 1 by A76,NAT_2:24;
then
A77: i <= la*lb div lb by XREAL_1:19;
i >= 0+1 & la*lb div lb = la by A74,NAT_D:18,XREAL_1:6;
then i in Seg la by A77;
then i in dom F by FINSEQ_1:def 3;
then
A78: F.i in rng F by FUNCT_1:def 3;
FG.k=F.i /\ G.j by A10,A70;
then z in F.i by A68,A71,XBOOLE_0:def 4;
hence thesis by A6,A78,TARSKI:def 4;
end;
for k being Nat,x,y being Element of X st k in dom FG & x in FG.k & y
in FG.k holds (f+g).x = (f+g).y
proof
reconsider la9=la,lb9=lb as Nat;
let k be Nat;
let x,y be Element of X;
assume that
A79: k in dom FG and
A80: x in FG.k and
A81: y in FG.k;
set i=(k-'1) div lb + 1;
set j=(k-'1) mod lb + 1;
A82: k in Seg len FG by A79,FINSEQ_1:def 3;
then
A83: k <= la*lb by A9,FINSEQ_1:1;
then
A84: (k -' 1) <= (la*lb -' 1) by NAT_D:42;
A85: lb <> 0 by A82,A83,FINSEQ_1:1;
then (k -' 1) mod lb < lb by NAT_D:1;
then j >= 0+1 & j <= lb by NAT_1:13;
then j in Seg lb;
then
A86: j in dom G by FINSEQ_1:def 3;
1 <= k by A82,FINSEQ_1:1;
then
A87: lb9 divides (la9*lb9) & 1 <= la*lb by A83,NAT_D:def 3,XXREAL_0:2;
lb >= 0+1 by A85,NAT_1:13;
then ((la9*lb9) -' 1) div lb9 = ((la9*lb9) div lb9) - 1 by A87,NAT_2:15;
then (k -' 1) div lb <= (la*lb div lb) - 1 by A84,NAT_2:24;
then (k -' 1) div lb + 1 <= la*lb div lb by XREAL_1:19;
then i >= 0+1 & i <= la by A85,NAT_D:18,XREAL_1:6;
then i in Seg la;
then
A88: i in dom F by FINSEQ_1:def 3;
A89: FG.k = F.( (k-'1) div lb + 1 ) /\ G.( (k-'1) mod lb + 1 ) by A10,A79;
then x in G.j by A80,XBOOLE_0:def 4;
then
A90: g.x = b.j by A7,A86,MESFUNC3:def 1;
y in G.j by A81,A89,XBOOLE_0:def 4;
then
A91: g.y = b.j by A7,A86,MESFUNC3:def 1;
x in F.i by A80,A89,XBOOLE_0:def 4;
then f.x = a.i by A5,A88,MESFUNC3:def 1;
then
A92: f.x + g.x = a.i + b.j by A90,SUPINF_2:1;
y in F.i by A81,A89,XBOOLE_0:def 4;
then
A93: f.y = a.i by A5,A88,MESFUNC3:def 1;
A94: FG.k in rng FG by A79,FUNCT_1:def 3;
then x in dom (f+g) by A4,A43,A8,A80,TARSKI:def 4;
then (f+g).x= a.i+b.j by A92,VALUED_1:def 1;
then
A95: (f+g).x= f.y+g.y by A93,A91,SUPINF_2:1;
y in dom(f+g) by A4,A43,A8,A81,A94,TARSKI:def 4;
hence thesis by A95,VALUED_1:def 1;
end;
hence f+g is_simple_func_in S by A4,A43,A8;
thus thesis by A2,A4,A8;
end;
theorem
f is_simple_func_in S & g is_simple_func_in S implies f+g is_simple_func_in S
proof
assume
A1: f is_simple_func_in S & g is_simple_func_in S;
per cases;
suppose
A2: dom(f+g) = {};
ex F being Finite_Sep_Sequence of S st (dom(f+g) = 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+g
).x = (f+g).y)
proof
reconsider EMPTY = {} as Element of S by PROB_1:4;
set F = <*EMPTY*>;
A3: dom F = Seg 1 by FINSEQ_1:38;
A4: now
let i,j be Nat;
assume that
A5: i in dom F and
A6: j in dom F & i <> j;
i = 1 by A3,A5,FINSEQ_1:2,TARSKI:def 1;
hence F.i misses F.j by A3,A6,FINSEQ_1:2,TARSKI:def 1;
end;
A7: for n be Nat st n in dom F holds F.n = EMPTY
proof
let n be Nat;
assume n in dom F;
then n = 1 by A3,FINSEQ_1:2,TARSKI:def 1;
hence thesis by FINSEQ_1:40;
end;
reconsider F as Finite_Sep_Sequence of S by A4,MESFUNC3:4;
take F;
union rng F = union bool {} by FINSEQ_1:39,ZFMISC_1:1;
hence dom(f+g) = union rng F by A2;
thus thesis by A7;
end;
hence thesis;
end;
suppose
A8: dom(f+g) <> {};
A9: dom(f+g) = dom f /\ dom g by VALUED_1:def 1;
dom f is Element of S & dom g is Element of S by A1,Th71;
then dom(f+g) in S by A9,FINSUB_1:def 2;
then
A10: f|dom(f+g) is_simple_func_in S & g|dom(f+g) is_simple_func_in S by A1,Th70
;
dom(f|dom(f+g)) = dom f /\ dom(f+g) by RELAT_1:61;
then
A11: dom(f|dom(f+g)) = dom f /\ dom f /\ dom g by A9,XBOOLE_1:16;
dom(g|dom(f+g)) = dom g /\ dom(f+g) by RELAT_1:61;
then
A12: dom(g|dom(f+g)) = dom g /\ dom g /\ dom f by A9,XBOOLE_1:16;
then
A13: dom(g|dom(f+g)) = dom(f+g) by VALUED_1:def 1;
A14: dom(f|dom(f+g) + g|dom(f+g)) = dom(f|dom(f+g)) /\ dom(g|dom(f+g))
by VALUED_1:def 1
.= dom(f+g) by A11,A12,VALUED_1:def 1;
A15: for x be Element of X st x in dom(f|dom(f+g) + g|dom(f+g)) holds (f|
dom(f+g) + g|dom(f+g)).x = (f+g).x
proof
let x be Element of X;
assume
A16: x in dom(f|dom(f+g) + g|dom(f+g));
then (f|dom(f+g) + g|dom(f+g)).x = (f|dom(f+g)).x + (g|dom(f+g)).x
by VALUED_1:def 1
.= f.x + (g|dom(f+g)).x by A14,A16,FUNCT_1:49
.= f.x + g.x by A14,A16,FUNCT_1:49;
hence thesis by A14,A16,VALUED_1:def 1;
end;
dom(f|dom(f+g)) = dom(f+g) by A11,VALUED_1:def 1;
then f|dom(f+g) + g|dom(f+g) is_simple_func_in S by A8,A10,A13,Lm1;
hence thesis by A14,A15,PARTFUN1:5;
end;
end;
theorem
f is_simple_func_in S implies r(#)f is_simple_func_in S
proof
set g = r(#)f;
assume f is_simple_func_in S;
then consider G be Finite_Sep_Sequence of S such that
A1: dom f = union rng G and
A2: for n be Nat, x,y be Element of X st n in dom G & x in G.n & y in G.
n holds f.x = f.y;
A3: dom g = dom f by VALUED_1:def 5;
now
let n be Nat;
let x,y be Element of X;
assume that
A4: n in dom G and
A5: x in G.n and
A6: y in G.n;
A7: G.n in rng G by A4,FUNCT_1:3;
then y in dom g by A3,A1,A6,TARSKI:def 4;
then
A8: g.y = r*f.y by VALUED_1:def 5;
x in dom g by A3,A1,A5,A7,TARSKI:def 4;
then g.x = r*f.x by VALUED_1:def 5;
hence g.x = g.y by A2,A4,A5,A6,A8;
end;
hence thesis by A3,A1;
end;
theorem
(for x be set st x in dom(f-g) holds g.x <= f.x) implies f-g is nonnegative
proof
A1: dom (f-g) = dom f /\ dom g by VALUED_1:12;
assume for x be set st x in dom(f-g) holds g.x <= f.x;
hence thesis by A1,Th58;
end;
theorem
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
proof
defpred P[object] means $1 in A;
deffunc F(object) = r;
A1: for x be object st P[x] holds F(x) in REAL by XREAL_0:def 1;
consider f be PartFunc of X,REAL such that
A2: (for x be object holds x in dom f iff x in X & P[x]) &
for x be object st
x in dom f holds f.x = F(x) from PARTFUN1:sch 3(A1);
take f;
A3: A c= dom f
by A2;
A4: dom f c= A
by A2;
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)
proof
set F = <* dom f *>;
A5: rng F = {dom f} by FINSEQ_1:38;
then rng F = {A} by A4,A3,XBOOLE_0:def 10;
then reconsider F as FinSequence of S by FINSEQ_1:def 4;
now
let i,j be Nat such that
A6: i in dom F and
A7: j in dom F & i <> j;
A8: dom F = Seg 1 by FINSEQ_1:38;
then i = 1 by A6,FINSEQ_1:2,TARSKI:def 1;
hence F.i misses F.j by A7,A8,FINSEQ_1:2,TARSKI:def 1;
end;
then reconsider F as Finite_Sep_Sequence of S by MESFUNC3:4;
take F;
thus dom f = union rng F by A5,ZFMISC_1:25;
hereby
let n be Nat;
let x,y be Element of X;
assume that
A9: n in dom F and
A10: x in F.n and
A11: y in F.n;
dom F = Seg 1 by FINSEQ_1:38;
then
A12: n = 1 by A9,FINSEQ_1:2,TARSKI:def 1;
then x in dom f by A10,FINSEQ_1:40;
then
A13: f.x = r by A2;
y in dom f by A11,A12,FINSEQ_1:40;
hence f.x = f.y by A2,A13;
end;
end;
hence f is_simple_func_in S;
thus dom f = A by A4,A3;
thus thesis by A2;
end;
theorem
f is B-measurable & A = dom f /\ B implies f|B is A-measurable
proof
assume that
A1: f is B-measurable and
A2: A = dom f /\ B;
A3: R_EAL f is B-measurable by A1;
now
let r be Real;
now
let x be object;
x in dom(f|B) & f|B.x < r iff x in dom f /\ B & f|B.x <
r by RELAT_1:61;
then
A4: x in A & x in less_dom(f|B,r) iff x in B & x in dom f & (f|B).x <
r by A2,MESFUNC1:def 11,XBOOLE_0:def 4;
x in B & x in dom f implies (f.x < r iff (f|B).x < r) by
FUNCT_1:49;
then x in A /\ less_dom(f|B,r) iff x in B & x in less_dom(f,r) by A4,
MESFUNC1:def 11,XBOOLE_0:def 4;
hence x in A /\ less_dom(f|B,r) iff x in B /\ less_dom(f,r) by
XBOOLE_0:def 4;
end;
then A /\ less_dom(f|B,r) c= B /\ less_dom(f,r) & B /\ less_dom(f,r) c= A
/\ less_dom(f|B,r);
then A /\ less_dom(f|B,r) = B /\ less_dom(f,r);
then A /\ less_dom(f|B,r) in S by A3,MESFUNC1:def 16;
hence A /\ less_dom(f|B,r) in S;
end;
hence thesis by Th12;
end;
theorem
A c= dom f & f is A-measurable & g is A-measurable implies max+(
f+g) + max-f is A-measurable
proof
assume that
A1: A c= dom f and
A2: f is A-measurable and
A3: g is A-measurable;
f+g is A-measurable by A2,A3,Th26;
then
A4: max+(f+g) is A-measurable by Th46;
max-f is A-measurable by A1,A2,Th47;
hence thesis by A4,Th26;
end;
theorem
A c= dom f /\ dom g & f is A-measurable & g is A-measurable
implies max-(f+g) + max+f is A-measurable
proof
assume that
A1: A c= dom f /\ dom g and
A2: f is A-measurable and
A3: g is A-measurable;
A4: max+ f is A-measurable by A2,Th46;
A5: dom(f+g) = dom f /\ dom g by VALUED_1:def 1;
f+g is A-measurable by A2,A3,Th26;
then max-(f+g) is A-measurable by A1,A5,Th47;
hence thesis by A4,Th26;
end;
theorem
dom f in S & dom g in S implies dom(f+g) in S
proof
assume dom f in S & dom g in S;
then reconsider E1 = dom f, E2 = dom g as Element of S;
dom(f+g) = E1 /\ E2 by VALUED_1:def 1;
hence thesis;
end;
theorem Th80:
dom f = A implies (f is B-measurable iff f is (A/\B)-measurable)
proof
assume
A1: dom f = A;
A2: now
let r be Real;
now
let x be object;
x in A /\ less_dom(f,r) iff x in A & x in less_dom(f,r) by XBOOLE_0:def 4
;
hence x in A /\ less_dom(f,r) iff x in less_dom(f,r) by A1,
MESFUNC1:def 11;
end;
then
A /\ less_dom(f,r) c= less_dom(f,r) & less_dom(f,r) c= A /\ less_dom(f
,r);
hence A /\ less_dom(f,r) = less_dom(f,r);
end;
hereby
assume
A3: f is B-measurable;
now
let r be Real;
A /\ B /\ less_dom(f,r) = B /\ (A /\ less_dom(f,r)) by XBOOLE_1:16
.= B /\ less_dom(f,r) by A2;
hence A/\B/\less_dom(f,r) in S by A3,Th12;
end;
hence f is (A/\B)-measurable by Th12;
end;
assume
A4: f is (A/\B)-measurable;
now
let r be Real;
A /\ B /\ less_dom(f,r) = B /\ (A /\ less_dom(f,r)) by XBOOLE_1:16
.=B /\ less_dom(f,r) by A2;
hence B /\ less_dom(f,r) in S by A4,Th12;
end;
hence thesis by Th12;
end;
theorem
( ex A be Element of S st dom f = A ) implies for c be Real, B be
Element of S st f is B-measurable holds c(#)f is B-measurable
proof
assume ex A be Element of S st A = dom f;
then consider A be Element of S such that
A1: A = dom f;
let c be Real, B be Element of S;
assume f is B-measurable;
then f is (A/\B)-measurable by A1,Th80;
then
A2: c(#)f is (A/\B)-measurable by A1,Th21,XBOOLE_1:17;
dom(c(#)f) = A by A1,VALUED_1:def 5;
hence thesis by A2,Th80;
end;
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
Integral(M,R_EAL f);
coherence;
end;
theorem Th82:
(ex A be Element of S st A = dom f & f is A-measurable) & f
is nonnegative implies Integral(M,f) = integral+(M,R_EAL f)
by MESFUNC5:88;
theorem
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)
proof
assume that
A1: f is_simple_func_in S and
A2: f is nonnegative;
A3: R_EAL f is_simple_func_in S by A1,Th49;
then reconsider A=dom(R_EAL f) as Element of S by MESFUNC5:37;
R_EAL f is A-measurable by A3,MESFUNC2:34;
then f is A-measurable;
hence Integral(M,f) = integral+(M,R_EAL f) by A2,Th82;
hence thesis by A2,A3,MESFUNC5:77;
end;
theorem
(ex A be Element of S st A = dom f & f is A-measurable) & f is
nonnegative implies 0 <= Integral(M,f)
by MESFUNC5:90;
theorem
(ex E be Element of S st E = dom f & f is E-measurable) & f is
nonnegative & A misses B implies Integral(M,f|(A\/B)) = Integral(M,f|A)+
Integral(M,f|B)
by MESFUNC5:91;
theorem
(ex E be Element of S st E = dom f & f is E-measurable) & f is
nonnegative implies 0<= Integral(M,f|A)
by MESFUNC5:92;
theorem
(ex E be Element of S st E = dom f & f is E-measurable ) & f is
nonnegative & A c= B implies Integral(M,f|A) <= Integral(M,f|B)
by MESFUNC5:93;
theorem
(ex E be Element of S st E = dom f & f is E-measurable) & M.A = 0
implies Integral(M,f|A)=0
by MESFUNC5:94;
theorem
E = dom f & f is E-measurable & M.A =0 implies Integral(M,f|(E\A))
= Integral(M,f)
by MESFUNC5:95;
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
R_EAL f is_integrable_on M;
end;
theorem
f is_integrable_on M implies -infty < Integral(M,f) & Integral(M,f) < +infty
by MESFUNC5:96;
theorem
f is_integrable_on M implies f|A is_integrable_on M
by MESFUNC5:97;
theorem
f is_integrable_on M & A misses B implies Integral(M,f|(A\/B)) =
Integral(M,f|A) + Integral(M,f|B)
by MESFUNC5:98;
theorem
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)
by MESFUNC5:99;
theorem
(ex A be Element of S st A = dom f & f is A-measurable ) implies (f
is_integrable_on M iff abs f is_integrable_on M)
proof
assume ex A be Element of S st A = dom f & f is A-measurable;
then consider A be Element of S such that
A1: A = dom f and
A2: f is A-measurable;
R_EAL f is A-measurable by A2;
then R_EAL f is_integrable_on M iff |. R_EAL f .| is_integrable_on M by A1,
MESFUNC5:100;
then f is_integrable_on M iff R_EAL abs f is_integrable_on M by Th1;
hence thesis;
end;
theorem
f is_integrable_on M implies |. Integral(M,f).| <= Integral(M,abs f)
proof
assume f is_integrable_on M;
then R_EAL f is_integrable_on M;
then |. Integral(M,f) .| <= Integral(M,|. R_EAL f .|) by MESFUNC5:101;
hence thesis by Th1;
end;
theorem
( 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 qua Complex.| <= g.x ) implies
f is_integrable_on M & Integral(M,abs f) <= Integral(M,g)
proof
assume that
A1: ex A be Element of S st A = dom f & f is A-measurable and
A2: dom f = dom g and
A3: g is_integrable_on M and
A4: for x be Element of X st x in dom f holds |.f.x qua Complex.| <= g.x;
A5: R_EAL g is_integrable_on M by A3;
A6: now
let x be Element of X;
A7: |.f.x qua Complex.| = |. (R_EAL f).x .| by EXTREAL1:12;
assume x in dom R_EAL f;
hence |. (R_EAL f).x .| <= (R_EAL g).x by A4,A7;
end;
consider A be Element of S such that
A8: A = dom f and
A9: f is A-measurable by A1;
R_EAL f is A-measurable by A9;
then R_EAL f is_integrable_on M & Integral(M,|.(R_EAL f).|) <= Integral(M,
R_EAL g ) by A2,A8,A5,A6,MESFUNC5:102;
hence thesis by Th1;
end;
theorem
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)
proof
assume that
A1: dom f in S and
A2: 0 <= r and
A3: for x be object st x in dom f holds f.x = r;
A4: for x be object st x in dom R_EAL f holds 0. <= (R_EAL f).x by A2,A3;
reconsider A = dom R_EAL f as Element of S by A1;
A5: R_EAL f is A-measurable by A3,Th2,MESFUNC2:34;
r * M.(dom R_EAL f) = integral'(M,R_EAL f) & R_EAL f
is_simple_func_in S by A1,A2,A3,Th2,MESFUNC5:104;
then integral+(M,R_EAL f) = r * M.(dom R_EAL f) by A4,MESFUNC5:77
,SUPINF_2:52;
hence thesis by A4,A5,MESFUNC5:88,SUPINF_2:52;
end;
theorem
f is_integrable_on M & g is_integrable_on M & f is nonnegative & g is
nonnegative implies f+g is_integrable_on M
proof
assume that
A1: f is_integrable_on M & g is_integrable_on M and
A2: f is nonnegative & g is nonnegative;
R_EAL f is_integrable_on M & R_EAL g is_integrable_on M by A1;
then R_EAL f + R_EAL g is_integrable_on M by A2,MESFUNC5:106;
then R_EAL(f+g) is_integrable_on M by Th23;
hence thesis;
end;
theorem
f is_integrable_on M & g is_integrable_on M implies dom (f+g) in S
proof
assume f is_integrable_on M & g is_integrable_on M;
then R_EAL f is_integrable_on M & R_EAL g is_integrable_on M;
then dom((R_EAL f)+(R_EAL g)) in S by MESFUNC5:107;
then dom(R_EAL(f+g)) in S by Th23;
hence thesis;
end;
theorem
f is_integrable_on M & g is_integrable_on M implies f+g is_integrable_on M
proof
assume f is_integrable_on M & g is_integrable_on M;
then R_EAL f is_integrable_on M & R_EAL g is_integrable_on M;
then R_EAL f + R_EAL g is_integrable_on M by MESFUNC5:108;
then R_EAL(f+g) is_integrable_on M by Th23;
hence thesis;
end;
theorem
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)
proof
assume f is_integrable_on M & g is_integrable_on M;
then R_EAL f is_integrable_on M & R_EAL g is_integrable_on M;
then consider E be Element of S such that
A1: E = dom(R_EAL f) /\ dom(R_EAL g) & Integral(M,R_EAL f + R_EAL g) =
Integral( M,(R_EAL f)|E) + Integral(M,(R_EAL g)|E) by MESFUNC5:109;
take E;
thus thesis by A1,Th23;
end;
theorem
f is_integrable_on M implies r(#)f is_integrable_on M & Integral(M,r
(#)f) = r * Integral(M,f)
proof
assume f is_integrable_on M;
then
A1: R_EAL f is_integrable_on M;
then r(#)(R_EAL f) is_integrable_on M by MESFUNC5:110;
then
A2: R_EAL(r(#)f) is_integrable_on M by Th20;
Integral(M,r(#)(R_EAL f)) = r * Integral(M,R_EAL f)
by A1,MESFUNC5:110;
hence thesis by A2,Th20;
end;
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
Integral(M,f|B);
coherence;
end;
theorem
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)
proof
assume that
A1: f is_integrable_on M & g is_integrable_on M and
A2: B c= dom(f+g);
A3: dom(f+g) = dom(R_EAL(f+g)) .= dom(R_EAL f + R_EAL g) by Th23;
A4: R_EAL f is_integrable_on M & R_EAL g is_integrable_on M by A1;
then R_EAL f + R_EAL g is_integrable_on M by A2,A3,MESFUNC5:111;
then
A5: R_EAL(f+g) is_integrable_on M by Th23;
Integral_on(M,B,R_EAL f + R_EAL g) = Integral_on(M,B,R_EAL f) +
Integral_on(M,B,R_EAL g) by A2,A4,A3,MESFUNC5:111;
hence thesis by A5,Th23;
end;
theorem
f is_integrable_on M implies f|B is_integrable_on M & Integral_on(M,B,
r(#)f) = r * Integral_on(M,B,f)
proof
assume f is_integrable_on M;
then
A1: R_EAL f is_integrable_on M;
then Integral_on(M,B,r(#)(R_EAL f)) = r * Integral_on(M,B,R_EAL f) by
MESFUNC5:112;
then
A2: Integral_on(M,B,R_EAL(r(#)f)) = r * Integral_on(M,B,R_EAL f) by Th20;
R_EAL(f|B) is_integrable_on M by A1,MESFUNC5:112;
hence thesis by A2;
end;