:: Measurability of Extended Real Valued Functions
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received October 6, 2000
:: Copyright (c) 2000-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, SUBSET_1, PARTFUN1, PROB_1, FUNCT_1, RAT_1,
REAL_1, NAT_1, VALUED_0, RELAT_1, COMPLEX1, ARYTM_3, XXREAL_0, TARSKI,
VALUED_1, ARYTM_1, MESFUNC1, SUPINF_2, RFUNCT_3, CARD_1, FUNCT_3, PROB_2,
FINSEQ_1, FUNCOP_1, MEASURE1, SUPINF_1, ORDINAL4, MESFUNC2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_3, XCMPLX_0,
XREAL_0, VALUED_0, REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
NAT_1, WELLORD2, RAT_1, FINSEQ_1, PROB_1, XXREAL_0, SUPINF_1, FUNCOP_1,
SUPINF_2, FUNCT_3, PROB_2, MEASURE1, MEASURE2, MEASURE3, MEASURE6,
EXTREAL1, MESFUNC1;
constructors PARTFUN1, WELLORD2, FUNCT_3, FUNCOP_1, REAL_1, NAT_1, RAT_1,
FINSEQ_1, PROB_2, MEASURE3, MEASURE6, EXTREAL1, MESFUNC1, SUPINF_1,
RELSET_1, BINOP_2, NUMBERS;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, RAT_1, MEMBERED,
FINSEQ_1, MEASURE1, VALUED_0, FUNCT_2, CARD_1, XXREAL_3;
requirements NUMERALS, REAL, BOOLE, SUBSET;
definitions TARSKI, XBOOLE_0, VALUED_0;
equalities XBOOLE_0, XXREAL_3, ORDINAL1, SUPINF_2;
expansions TARSKI, XBOOLE_0, VALUED_0, MESFUNC1;
theorems MEASURE1, TARSKI, SUBSET_1, PARTFUN1, FUNCT_1, FUNCT_2, NAT_1,
SUPINF_2, WELLORD2, RAT_1, RELSET_1, EXTREAL1, MESFUNC1, ZFMISC_1,
FINSEQ_1, FINSEQ_3, FINSEQ_5, XREAL_0, PROB_2, FUNCT_3, XBOOLE_0,
XBOOLE_1, RELAT_1, FUNCOP_1, XREAL_1, FINSUB_1, PROB_1, XXREAL_0,
ORDINAL1, XXREAL_3;
schemes FUNCT_2, SEQ_1, NAT_1;
begin :: Finite Valued Function ::
reserve X for non empty set;
reserve e for set;
reserve x for Element of X;
reserve f,g for PartFunc of X,ExtREAL;
reserve S for SigmaField of X;
reserve F for Function of RAT,S;
reserve p,q for Rational;
reserve r for Real;
reserve n,m for Nat;
reserve A,B for Element of S;
definition
let X, f;
redefine attr f is real-valued means :: redefines real-valued (VALUED_0, redefinition) → real-valued (VALUED_0, definition)
for x st x in dom f holds |. f.x .| < +infty;
compatibility
proof
thus
f is real-valued implies for x st x in dom f holds |. f.x .| < +infty
proof
assume
A1: f is real-valued;
let x;
assume x in dom f;
then A2: f.x in rng f by FUNCT_1:3;
rng f c= REAL by A1;
hence thesis by A2,EXTREAL1:41;
end;
assume
A3: for x st x in dom f holds |. f.x .| < +infty;
let e be object;
assume
A4: e in dom f;
then reconsider x = e as Element of X;
|. f.x .| < +infty by A3,A4;
then f.x in REAL by EXTREAL1:41;
hence thesis;
end;
end;
theorem
f = 1(#)f
proof
A1: dom f = dom (1(#)f) by MESFUNC1:def 6;
for x st x in dom (1(#)f) holds f.x = (1(#)f).x
proof
let x;
assume x in dom(1(#)f);
then (1(#)f).x = (1) * f.x by MESFUNC1:def 6;
hence thesis by XXREAL_3:81;
end;
hence thesis by A1,PARTFUN1:5;
end;
theorem Th2:
f is real-valued or g is real-valued implies
dom (f+g) = dom f /\ dom g & dom (f-g) = dom f /\ dom g
proof
assume
A1: f is real-valued or g is real-valued;
now per cases by A1;
suppose
A2: f is real-valued;
then not +infty in rng f;
then A3: f"{+infty} = {} by FUNCT_1:72;
not -infty in rng f by A2;
then A4: f"{-infty} = {} by FUNCT_1:72;
then
A5: (f"{+infty} /\ g"{-infty}) \/ (f"{-infty} /\ g"{+infty}) = {} by A3;
A6: (f"{+infty} /\ g"{+infty}) \/ (f"{-infty} /\ g"{-infty}) = {} by A3,A4;
dom (f+g) = (dom f /\ dom g)\{} by A5,MESFUNC1:def 3;
hence thesis by A6,MESFUNC1:def 4;
end;
suppose
A7: g is real-valued;
then not +infty in rng g;
then A8: g"{+infty} = {} by FUNCT_1:72;
not -infty in rng g by A7;
then A9: g"{-infty} = {} by FUNCT_1:72;
then
A10: (f"{+infty} /\ g"{-infty}) \/ (f"{-infty} /\ g"{+infty}) = {} by A8;
A11: (f"{+infty} /\ g"{+infty}) \/ (f"{-infty} /\ g"{-infty}) = {} by A8,A9;
dom (f+g) = (dom f /\ dom g)\{} by A10,MESFUNC1:def 3;
hence thesis by A11,MESFUNC1:def 4;
end;
end;
hence thesis;
end;
theorem Th3:
for f,g,F,r,A st f is real-valued & g is real-valued &
(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,g,F,r,A;
assume that
A1: f is real-valued and
A2: g is real-valued and
A3: for p holds F.p = (A /\ less_dom(f, p)) /\ (A /\
less_dom(g, (r-p)));
A4: dom(f+g) = dom f /\ dom g by A1,Th2;
A5: A /\ less_dom(f+g, r) c= union (rng F)
proof
let x be object;
assume
A6: x in A /\ less_dom(f+g, r);
then A7: x in A by XBOOLE_0:def 4;
A8: x in less_dom(f+g, r) by A6,XBOOLE_0:def 4;
then A9: x in dom(f+g) by MESFUNC1:def 11;
A10: (f+g).x < r by A8,MESFUNC1:def 11;
reconsider x as Element of X by A6;
A11: f.x + g.x < r by A9,A10,MESFUNC1:def 3;
A12: x in dom f by A4,A9,XBOOLE_0:def 4;
A13: x in dom g by A4,A9,XBOOLE_0:def 4;
A14: |. f.x .| < +infty by A1,A12;
A15: |. g.x .| < +infty by A2,A13;
A16: -(+infty) < f.x by A14,EXTREAL1:21;
A17: f.x < +infty by A14,EXTREAL1:21;
A18: -(+infty) < g.x by A15,EXTREAL1:21;
A19: g.x < +infty by A15,EXTREAL1:21;
then A20: f.x < r - g.x by A11,A17,XXREAL_3:52;
A21: -infty < f.x by A16,XXREAL_3:23;
A22: -infty < g.x by A18,XXREAL_3:23;
reconsider f1 = f.x as Element of REAL by A17,A21,XXREAL_0:14;
reconsider g1 = g.x as Element of REAL by A19,A22,XXREAL_0:14;
reconsider rr = r as R_eal by XXREAL_0:def 1;
f1 < r - g1 by A20,SUPINF_2:3;
then consider p such that
A23: f1 < p and
A24: p < r - g1 by RAT_1:7;
A25: not r - p <= g1 by A24,XREAL_1:12;
A26: x in less_dom(f, p) by A12,A23,MESFUNC1:def 11;
A27: x in less_dom(g,(r-p)) by A13,A25,MESFUNC1:def 11;
A28: x in A /\ less_dom(f, p) by A7,A26,XBOOLE_0:def 4;
x in A /\ less_dom(g,(r-p)) by A7,A27,XBOOLE_0:def 4;
then A29: x in (A /\ less_dom(f, p))/\(A /\
less_dom(g,(r-p))) by A28,XBOOLE_0:def 4;
p in RAT by RAT_1:def 2;
then A30: p in dom F by FUNCT_2:def 1;
A31: x in F.p by A3,A29;
F.p in rng F by A30,FUNCT_1:def 3;
hence thesis by A31,TARSKI:def 4;
end;
union (rng F) c= A /\ less_dom(f+g, r)
proof
let x be object;
assume x in union (rng F);
then consider Y being set such that
A32: x in Y and
A33: Y in rng F by TARSKI:def 4;
consider p being object such that
A34: p in dom F and
A35: Y = F.p by A33,FUNCT_1:def 3;
reconsider p as Rational by A34;
A36: x in (A /\ less_dom(f, p))/\(A /\ less_dom(g, (r-p)))
by A3,A32,A35;
then A37: x in A /\ less_dom(f, p) by XBOOLE_0:def 4;
A38: x in A /\ less_dom(g, (r-p)) by A36,XBOOLE_0:def 4;
A39: x in A by A37,XBOOLE_0:def 4;
A40: x in less_dom(f, p) by A37,XBOOLE_0:def 4;
A41: x in less_dom(g, (r-p)) by A38,XBOOLE_0:def 4;
A42: x in dom f by A40,MESFUNC1:def 11;
A43: x in dom g by A41,MESFUNC1:def 11;
reconsider x as Element of X by A36;
A44: g.x < (r-p) by A41,MESFUNC1:def 11;
A45: |.f.x.| < +infty by A1,A42;
A46: |.g.x.| < +infty by A2,A43;
A47: -(+infty) < f.x by A45,EXTREAL1:21;
A48: -(+infty) < g.x by A46,EXTREAL1:21;
A49: -infty< f.x by A47,XXREAL_3:23;
A50: f.x< +infty by A45,EXTREAL1:21;
A51: -infty< g.x by A48,XXREAL_3:23;
A52: g.x< +infty by A46,EXTREAL1:21;
reconsider f1 = f.x as Element of REAL by A49,A50,XXREAL_0:14;
reconsider g1 = g.x as Element of REAL by A51,A52,XXREAL_0:14;
A53: f1 < p by A40,MESFUNC1:def 11;
p < r- g1 by A44,XREAL_1:12;
then f1 < r - g1 by A53,XXREAL_0:2;
then A54: f1 + g1 < r by XREAL_1:20;
A55: x in dom (f+g) by A4,A42,A43,XBOOLE_0:def 4;
then (f+g).x = f.x + g.x by MESFUNC1:def 3
.= f1+g1 by SUPINF_2:1;
then x in less_dom(f+g, r) by A54,A55,MESFUNC1:def 11;
hence thesis by A39,XBOOLE_0:def 4;
end;
hence thesis by A5;
end;
begin :: Measurability of f+g and f-g ::
theorem
ex F being sequence of RAT st F is one-to-one & dom F = NAT & rng F = RAT
proof
consider F being Function such that
A1: F is one-to-one and
A2: dom F = NAT & rng F = RAT by MESFUNC1:5,WELLORD2:def 4;
F is sequence of RAT by A2,FUNCT_2:2;
hence thesis by A1,A2;
end;
theorem Th5:
for X,Y,Z be non empty set, F be Function of X,Z st X,Y are_equipotent holds
ex G be Function of Y,Z st rng F = rng G
proof
let X,Y,Z be non empty set;
let F be Function of X,Z;
assume X,Y are_equipotent;
then consider H being Function such that
A1: H is one-to-one and
A2: dom H = Y and
A3: rng H = X by WELLORD2:def 4;
reconsider H as Function of Y,X by A2,A3,FUNCT_2:2;
reconsider G = F*H as Function of Y,Z;
A4: dom F = X by FUNCT_2:def 1;
A5: dom G = Y by FUNCT_2:def 1;
for z being Element of Z holds z in rng F implies z in rng G
proof
let z be Element of Z;
assume z in rng F;
then consider x be object such that
A6: x in dom F and
A7: z = F.x by FUNCT_1:def 3;
x in rng H by A3,A6;
then x in dom (H") by A1,FUNCT_1:32;
then (H").x in rng (H") by FUNCT_1:def 3;
then A8: (H").x in dom G by A1,A2,A5,FUNCT_1:33;
then G.((H").x) in rng G by FUNCT_1:def 3;
then F.(H.((H").x)) in rng G by A8,FUNCT_1:12;
hence thesis by A1,A3,A6,A7,FUNCT_1:35;
end;
then A9: rng F c= rng G;
for z being Element of Z holds z in rng G implies z in rng F
proof
let z be Element of Z;
assume z in rng G;
then consider y be object such that
A10: y in dom G and
A11: z = G.y by FUNCT_1:def 3;
y in rng (H") by A1,A2,A5,A10,FUNCT_1:33;
then consider x be object such that
A12: x in dom (H") and
A13: y = (H").x by FUNCT_1:def 3;
A14: x in rng H by A1,A12,FUNCT_1:33;
then A15: F.x in rng F by A4,FUNCT_1:def 3;
x = H.y by A1,A13,A14,FUNCT_1:32;
hence thesis by A10,A11,A15,FUNCT_1:12;
end;
then rng G c= rng F;
then rng F = rng G by A9;
hence thesis;
end;
theorem Th6:
for S,f,g,A st f is A-measurable & g is A-measurable holds
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)))
proof
let S,f,g,A;
assume
A1: f is A-measurable & g is A-measurable;
defpred P[object,object] means ex p st p = $1 &
$2 = (A /\ less_dom(f, p)) /\ (A /\ less_dom(g, (r-p)));
A2: for x1 being object st x1 in RAT
ex y1 being object st y1 in S & P[x1,y1]
proof
let x1 be object;
assume x1 in RAT;
then consider p such that
A3: p = x1;
A4: A
/\ less_dom(f, p) in S & A /\ less_dom(g, (r-p)) in S by A1;
take (A /\ less_dom(f, p)) /\ (A /\ less_dom(g, (r-p)));
thus thesis by A3,A4,FINSUB_1:def 2;
end;
consider G being Function of RAT,S such that
A5: for x1 being object st x1 in RAT holds P[x1,G.x1] from FUNCT_2:sch 1(A2);
A6: for p being Rational holds
G.p = (A /\ less_dom(f, p)) /\ (A /\ less_dom(g, (r-p)))
proof
let p be Rational;
p in RAT by RAT_1:def 2;
then ex q st q = p & G.p = (A /\ less_dom(f, q)) /\ (A /\
less_dom(g, (r-q))) by A5;
hence thesis;
end;
take G;
thus thesis by A6;
end;
theorem Th7:
for f,g,A st f is real-valued & g is real-valued & f is A-measurable &
g is A-measurable holds f+g is A-measurable
proof
let f,g,A;
assume that
A1: f is real-valued & g is real-valued and
A2: f is A-measurable & g is A-measurable;
for r be Real holds A /\ less_dom(f+g, r) in S
proof
let r be Real;
reconsider r as Real;
consider F being Function of RAT,S such that
A3: for p being Rational holds
F.p = (A /\ less_dom(f, p)) /\ (A /\ less_dom(g, (r-p)))
by A2,Th6;
consider G being sequence of S such that
A4: rng F = rng G by Th5,MESFUNC1:5;
A /\ less_dom(f+g, r) = union (rng G) by A1,A3,A4,Th3;
hence thesis;
end;
hence thesis;
end;
theorem Th8:
for C being non empty set, f1,f2 being PartFunc of C,ExtREAL holds
f1 - f2 = f1 + (-f2)
proof
let C be non empty set;
let f1,f2 be PartFunc of C,ExtREAL;
A1: dom (f1-f2)
=(dom f1 /\ dom f2)\((f1"{+infty}/\f2"{+infty}) \/ (f1"{-infty}/\
f2"{-infty})) by MESFUNC1:def 4;
for x being Element of C st x in f2"{+infty} holds x in (-f2)"{-infty}
proof
let x be Element of C;
assume
A2: x in f2"{+infty};
then A3: x in dom f2 by FUNCT_1:def 7;
A4: f2.x in {+infty} by A2,FUNCT_1:def 7;
A5: x in dom(-f2) by A3,MESFUNC1:def 7;
f2.x = +infty by A4,TARSKI:def 1;
then (-f2).x = -(+infty) by A5,MESFUNC1:def 7
.= -infty by XXREAL_3:def 3;
then (-f2).x in {-infty} by TARSKI:def 1;
hence thesis by A5,FUNCT_1:def 7;
end;
then A6: f2"{+infty} c= (-f2)"{-infty};
for x being Element of C st x in (-f2)"{-infty} holds x in f2"{+infty}
proof
let x be Element of C;
assume
A7: x in (-f2)"{-infty};
then A8: x in dom(-f2) by FUNCT_1:def 7;
A9: (-f2).x in {-infty} by A7,FUNCT_1:def 7;
A10: x in dom f2 by A8,MESFUNC1:def 7;
(-f2).x = -infty by A9,TARSKI:def 1;
then -infty = -(f2.x) by A8,MESFUNC1:def 7;
then f2.x in {+infty} by TARSKI:def 1,XXREAL_3:5;
hence thesis by A10,FUNCT_1:def 7;
end;
then (-f2)"{-infty} c= f2"{+infty};
then A11: f2"{+infty} = (-f2)"{-infty} by A6;
for x being Element of C st x in f2"{-infty} holds x in (-f2)"{+infty}
proof
let x be Element of C;
assume
A12: x in f2"{-infty};
then A13: x in dom f2 by FUNCT_1:def 7;
A14: f2.x in {-infty} by A12,FUNCT_1:def 7;
A15: x in dom(-f2) by A13,MESFUNC1:def 7;
f2.x = -infty by A14,TARSKI:def 1;
then (-f2).x = +infty by A15,MESFUNC1:def 7,XXREAL_3:5;
then (-f2).x in {+infty} by TARSKI:def 1;
hence thesis by A15,FUNCT_1:def 7;
end;
then A16: f2"{-infty} c= (-f2)"{+infty};
for x being Element of C st x in (-f2)"{+infty} holds x in f2"{-infty}
proof
let x be Element of C;
assume
A17: x in (-f2)"{+infty};
then A18: x in dom(-f2) by FUNCT_1:def 7;
A19: (-f2).x in {+infty} by A17,FUNCT_1:def 7;
A20: x in dom f2 by A18,MESFUNC1:def 7;
(-f2).x = +infty by A19,TARSKI:def 1;
then +infty = -(f2.x) by A18,MESFUNC1:def 7;
then f2.x = -(+infty)
.= -infty by XXREAL_3:def 3;
then f2.x in {-infty} by TARSKI:def 1;
hence thesis by A20,FUNCT_1:def 7;
end;
then (-f2)"{+infty} c= f2"{-infty};
then A21: f2"{-infty} = (-f2)"{+infty} by A16;
dom (f1+(-f2)) =(dom f1 /\ dom(-f2))\
((f1"{-infty}/\(-f2)"{+infty}) \/ (f1"{+infty}/\(-f2)"{-infty}))
by MESFUNC1:def 3
.=(dom f1 /\ dom f2)\
((f1"{-infty}/\f2"{-infty}) \/ (f1"{+infty}/\f2"{+infty}))
by A11,A21,MESFUNC1:def 7;
then A22: dom(f1-f2)=dom(f1+(-f2)) by MESFUNC1:def 4;
for
x being Element of C st x in dom(f1-f2) holds (f1-f2).x = (f1+(-f2)).x
proof
let x be Element of C;
assume
A23: x in dom(f1-f2);
dom(f1-f2) c= dom f1 /\ dom f2 by A1,XBOOLE_1:36;
then x in dom f2 by A23,XBOOLE_0:def 4;
then A24: x in dom (-f2) by MESFUNC1:def 7;
(f1-f2).x = f1.x - f2.x & (f1+(-f2)).x = f1.x + (-f2).x by A22,A23,
MESFUNC1:def 3,def 4;
hence thesis by A24,MESFUNC1:def 7;
end;
hence thesis by A22,PARTFUN1:5;
end;
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
theorem Th9:
for C being non empty set, f being PartFunc of C,ExtREAL holds -f = (-1)(#)f
proof
let C be non empty set;
let f be PartFunc of C,ExtREAL;
A1: dom (-f) = dom f by MESFUNC1:def 7;
A2: dom ((-1)(#)f) = dom f by MESFUNC1:def 6;
for x being Element of C st x in dom f holds (-f).x = ((-1)(#)f).x
proof
let x be Element of C;
assume
A3: x in dom f;
then
A4:((-1)(#) f).x=( -1)*(f.x) by A2,MESFUNC1:def 6;
((-1)(#)f).x = ((-jj)(#)f).x
.= (-( 1.))*(f.x) by SUPINF_2:2,A4
.= -( 1.)*(f.x) by XXREAL_3:92
.= -( 1)*(f.x)
.= -(f.x) by XXREAL_3:81;
hence thesis by A1,A3,MESFUNC1:def 7;
end;
hence thesis by A1,A2,PARTFUN1:5;
end;
theorem Th10:
for C being non empty set, f being PartFunc of C,ExtREAL, r be Real
st f is real-valued holds r(#)f is real-valued
proof
let C be non empty set;
let f be PartFunc of C,ExtREAL;
let r be Real;
assume
A1: f is real-valued;
for x being Element of C st x in dom(r(#)f) holds |.(r(#)f).x .| < +infty
proof
let x be Element of C;
assume
A2: x in dom(r(#)f);
then x in dom f by MESFUNC1:def 6;
then A3: |. f.x .| < +infty by A1;
then -(+infty) < f.x by EXTREAL1:21;
then A4: -infty < f.x by XXREAL_3:def 3;
f.x < +infty by A3,EXTREAL1:21;
then reconsider y = f.x as Element of REAL by A4,XXREAL_0:14;
reconsider yy = f.x as Element of ExtREAL;
reconsider ry = r*y as Element of REAL by XREAL_0:def 1;
A5: -infty < (ry) by XXREAL_0:12;
A6: (ry) < +infty by XXREAL_0:9;
A7: -infty < r * y by A5;
A8: r * y = r * yy by XXREAL_3:def 5
.= (r(#)f).x by A2,MESFUNC1:def 6;
then A9: -(+infty) < (r(#)f).x by A7,XXREAL_3:def 3;
(r(#)f).x < +infty by A6,A8;
hence thesis by A9,EXTREAL1:22;
end;
hence thesis;
end;
theorem
for f,g,A st f is real-valued & g is real-valued & f is A-measurable &
g is A-measurable & A c= dom g holds f-g is A-measurable
proof
let f,g,A;
assume that
A1: f is real-valued and
A2: g is real-valued and
A3: f is A-measurable and
A4: g is A-measurable & A c= dom g;
A5: (-1)(#)g is real-valued by A2,Th10;
A6: (-1)(#)g is A-measurable by A4,MESFUNC1:37;
A7: -g is real-valued by A5,Th9;
-g is A-measurable by A6,Th9;
then f+(-g) is A-measurable by A1,A3,A7,Th7;
hence thesis by Th8;
end;
begin ::definitions of extended real valued functions max+(f) and max-(f) ::
:: and their basic properties ::
definition
let C be non empty set, f be PartFunc of C,ExtREAL;
deffunc F(Element of C) = max(f.$1,0.);
func max+(f) -> PartFunc of C,ExtREAL means
:Def2:
dom it = dom f &
for x be Element of C st x in dom it holds it.x = max(f.x,0.);
existence
proof
defpred P[Element of C] means $1 in dom f;
consider F be PartFunc of C,ExtREAL such that
A1: for c being Element of C holds c in dom F iff P[c] and
A2: for c being Element of C st c in dom F holds F.c = F(c) from SEQ_1:sch 3;
take F;
thus dom F=dom f
proof
thus dom F c= dom f
by A1;
let x be object;
assume x in dom f;
hence thesis by A1;
end;
let c be Element of C;
assume c in dom F;
hence thesis by A2;
end;
uniqueness
proof
set X = dom f;
thus for F,G being PartFunc of C,ExtREAL st
(dom F=X & for c be Element of C st c in dom F holds F.c = F(c)) &
(dom G=X & for c be Element of C st c in dom G holds G.c = F(c))
holds F = G from SEQ_1:sch 4;
end;
deffunc F(Element of C) = max(-(f.$1),0.);
func max-(f) -> PartFunc of C,ExtREAL means
:Def3:
dom it = dom f &
for x be Element of C st x in dom it holds it.x = max(-(f.x),0.);
existence
proof
defpred P[Element of C] means $1 in dom f;
consider F be PartFunc of C,ExtREAL such that
A3: for c being Element of C holds c in dom F iff P[c] and
A4: for c being Element of C st c in dom F holds F.c = F(c) from SEQ_1:sch 3;
take F;
thus dom F=dom f
proof
thus dom F c= dom f
by A3;
let x be object;
assume x in dom f;
hence thesis by A3;
end;
let c be Element of C;
assume c in dom F;
hence thesis by A4;
end;
uniqueness
proof
set X = dom f;
thus for F,G being PartFunc of C,ExtREAL st
(dom F=X & for c be Element of C st c in dom F holds F.c = F(c)) &
(dom G=X & for c be Element of C st c in dom G holds G.c = F(c))
holds F = G from SEQ_1:sch 4;
end;
end;
theorem Th12:
for C being non empty set, f being PartFunc of C,ExtREAL,
x being Element of C holds 0. <= (max+(f)).x
proof
let C be non empty set;
let f be PartFunc of C,ExtREAL;
let x be Element of C;
A1: dom max+f = dom f by Def2;
per cases;
suppose
x in dom f;
then (max+(f).x) = max(f.x,0.) by A1,Def2;
hence thesis by XXREAL_0:25;
end;
suppose
not x in dom f;
hence thesis by A1,FUNCT_1:def 2;
end;
end;
theorem Th13:
for C being non empty set, f being PartFunc of C,ExtREAL,
x being Element of C holds 0. <= (max-(f)).x
proof
let C be non empty set;
let f be PartFunc of C,ExtREAL;
let x be Element of C;
A1: dom max-f = dom f by Def3;
per cases;
suppose
x in dom f;
then (max-(f).x) = max(-f.x,0.) by A1,Def3;
hence thesis by XXREAL_0:25;
end;
suppose
not x in dom f;
hence thesis by A1,FUNCT_1:def 2;
end;
end;
theorem
for C being non empty set, f being PartFunc of C,ExtREAL holds
max-(f) = max+(-f)
proof
let C be non empty set;
let f be PartFunc of C,ExtREAL;
A1: dom(max-(f)) = dom f by Def3
.= dom (-f) by MESFUNC1:def 7;
then A2: dom(max-(f)) = dom(max+(-f)) by Def2;
for
x being Element of C st x in dom(max-(f)) holds max-(f).x = max+(-f).x
proof
let x be Element of C;
assume
A3: x in dom (max-(f));
then max-
(f).x = max(-(f.x),0.) & -(f.x) = (-f).x by A1,Def3,MESFUNC1:def 7;
hence thesis by A2,A3,Def2;
end;
hence thesis by A2,PARTFUN1:5;
end;
theorem Th15:
for C being non empty set, f being PartFunc of C,ExtREAL, x being Element of C
st 0. < max+(f).x holds max-(f).x = 0.
proof
let C be non empty set;
let f be PartFunc of C,ExtREAL;
let x be Element of C;
A1: dom max+f = dom f by Def2;
per cases;
suppose
A2: x in dom f;
assume
A3: 0. < max+(f).x;
A4: x in dom(max+(f)) by A2,Def2;
A5: x in dom(max-(f)) by A2,Def3;
max+(f).x = max(f.x,0.) by A4,Def2;
then not (f.x <= 0. & 0. <= 0.) by A3,XXREAL_0:28;
then max(-(f.x),0.) = 0. by XXREAL_0:def 10;
hence thesis by A5,Def3;
end;
suppose
not x in dom f;
hence thesis by A1,FUNCT_1:def 2;
end;
end;
theorem
for C being non empty set, f being PartFunc of C,ExtREAL,
x being Element of C st 0. < max-(f).x holds max+(f).x = 0.
proof
let C be non empty set;
let f be PartFunc of C,ExtREAL;
let x be Element of C;
A1: dom max-f = dom f by Def3;
per cases;
suppose
A2: x in dom f;
assume
A3: 0. < max-(f).x;
A4: x in dom(max-(f)) by A2,Def3;
A5: x in dom(max+(f)) by A2,Def2;
max-(f).x = max(-(f.x),0.) by A4,Def3;
then -(-(f.x)) < -0. by A3,XXREAL_0:28;
then max(f.x,0.) = 0. by XXREAL_0:def 10;
hence thesis by A5,Def2;
end;
suppose
not x in dom f;
hence thesis by A1,FUNCT_1:def 2;
end;
end;
theorem Th17:
for C being non empty set, f being PartFunc of C,ExtREAL holds
dom f = dom (max+(f)-max-(f)) & dom f = dom (max+(f)+max-(f))
proof
let C be non empty set;
let f be PartFunc of C,ExtREAL;
A1: dom (max+(f)) = dom f & dom (max-(f)) = dom f by Def2,Def3;
(max+(f))"{+infty} misses (max-(f))"{+infty}
proof
assume not (max+(f))"{+infty} misses (max-(f))"{+infty};
then consider x1 being object such that
A2: x1 in (max+(f))"{+infty} and
A3: x1 in (max-(f))"{+infty} by XBOOLE_0:3;
reconsider x1 as Element of C by A2;
A4: max+(f).x1 in {+infty} by A2,FUNCT_1:def 7;
A5: max-(f).x1 in {+infty} by A3,FUNCT_1:def 7;
A6: max+(f).x1 = +infty by A4,TARSKI:def 1;
max-(f).x1 = +infty by A5,TARSKI:def 1;
hence contradiction by A6,Th15;
end;
then A7: (max+(f))"{+infty} /\ (max-(f))"{+infty} = {};
(max+(f))"{-infty} misses (max-(f))"{-infty}
proof
assume not (max+(f))"{-infty} misses (max-(f))"{-infty};
then consider x1 being object such that
A8: x1 in (max+(f))"{-infty} and x1 in (max-(f))"{-infty} by XBOOLE_0:3;
reconsider x1 as Element of C by A8;
max+(f).x1 in {-infty} by A8,FUNCT_1:def 7;
then max+(f).x1 = -infty by TARSKI:def 1;
hence contradiction by Th12;
end;
then A9: (max+(f))"{-infty} /\ (max-(f))"{-infty} = {};
(max+(f))"{+infty} misses (max-(f))"{-infty}
proof
assume not (max+(f))"{+infty} misses (max-(f))"{-infty};
then consider x1 being object such that
A10: x1 in (max+(f))"{+infty} and
A11: x1 in (max-(f))"{-infty} by XBOOLE_0:3;
reconsider x1 as Element of C by A10;
max-(f).x1 in {-infty} by A11,FUNCT_1:def 7;
then max-(f).x1 = -infty by TARSKI:def 1;
hence contradiction by Th13;
end;
then A12: (max+(f))"{+infty} /\ (max-(f))"{-infty} = {};
(max+(f))"{-infty} misses (max-(f))"{+infty}
proof
assume not (max+(f))"{-infty} misses (max-(f))"{+infty};
then consider x1 being object such that
A13: x1 in (max+(f))"{-infty} and x1 in (max-(f))"{+infty} by XBOOLE_0:3;
reconsider x1 as Element of C by A13;
max+(f).x1 in {-infty} by A13,FUNCT_1:def 7;
then max+(f).x1 = -infty by TARSKI:def 1;
hence contradiction by Th12;
end;
then A14: (max+(f))"{-infty} /\ (max-(f))"{+infty} = {};
dom (max+(f)-max-(f)) = (dom f /\ dom f)\({}\/{}) by A1,A7,A9,MESFUNC1:def 4;
hence thesis by A1,A12,A14,MESFUNC1:def 3;
end;
theorem Th18:
for C being non empty set, f being PartFunc of C,ExtREAL, x being Element of C
holds
(max+(f).x = f.x or max+(f).x = 0.) & (max-(f).x = -(f.x) or max-(f).x = 0.)
proof
let C be non empty set;
let f be PartFunc of C,ExtREAL;
let x be Element of C;
A1: dom max-f = dom f & dom max+f = dom f by Def2,Def3;
per cases;
suppose
A2: x in dom f;
then A3: x in dom(max+(f)) by Def2;
A4: x in dom(max-(f)) by A2,Def3;
A5: max+(f).x = max(f.x,0.) by A3,Def2;
max-(f).x = max(-(f.x),0.) by A4,Def3;
hence thesis by A5,XXREAL_0:16;
end;
suppose
not x in dom f;
hence thesis by A1,FUNCT_1:def 2;
end;
end;
theorem Th19:
for C being non empty set, f being PartFunc of C,ExtREAL, x being Element of C
st max+(f).x = f.x holds max-(f).x = 0.
proof
let C be non empty set;
let f be PartFunc of C,ExtREAL;
let x be Element of C;
A1: dom max-f = dom f by Def3;
per cases;
suppose
A2: x in dom f;
assume
A3: max+(f).x = f.x;
A4: x in dom(max+(f)) by A2,Def2;
A5: x in dom(max-(f)) by A2,Def3;
A6: max+(f).x = max(f.x,0.) by A4,Def2;
A7: max-(f).x = max(-(f.x),0.) by A5,Def3;
0. <= f.x by A3,A6,XXREAL_0:def 10;
hence thesis by A7,XXREAL_0:def 10;
end;
suppose
not x in dom f;
hence thesis by A1,FUNCT_1:def 2;
end;
end;
theorem Th20:
for C being non empty set, f being PartFunc of C,ExtREAL, x being Element of C
st x in dom f & max+(f).x = 0. holds max-(f).x = -(f.x)
proof
let C be non empty set;
let f be PartFunc of C,ExtREAL;
let x be Element of C;
assume that
A1: x in dom f and
A2: max+(f).x = 0.;
A3: x in dom(max+(f)) by A1,Def2;
A4: x in dom(max-(f)) by A1,Def3;
A5: max+(f).x = max(f.x,0.) by A3,Def2;
A6: max-(f).x = max(-(f.x),0.) by A4,Def3;
f.x <= 0. by A2,A5,XXREAL_0:def 10;
hence thesis by A6,XXREAL_0:def 10;
end;
theorem
for C being non empty set, f being PartFunc of C,ExtREAL,
x being Element of C st max-(f).x = -(f.x) holds max+(f).x = 0.
proof
let C be non empty set;
let f be PartFunc of C,ExtREAL;
let x be Element of C;
A1: dom max+f = dom f by Def2;
per cases;
suppose
A2: x in dom f;
assume
A3: max-(f).x = -(f.x);
A4: x in dom(max+(f)) by A2,Def2;
A5: x in dom(max-(f)) by A2,Def3;
A6: max+(f).x = max(f.x,0.) by A4,Def2;
max-(f).x = max(-(f.x),0.) by A5,Def3;
then -(-(f.x)) <= -0. by A3,XXREAL_0:def 10;
hence thesis by A6,XXREAL_0:def 10;
end;
suppose
not x in dom f;
hence thesis by A1,FUNCT_1:def 2;
end;
end;
theorem
for C being non empty set, f being PartFunc of C,ExtREAL,
x being Element of C st x in dom f & max-(f).x = 0. holds max+(f).x = f.x
proof
let C be non empty set;
let f be PartFunc of C,ExtREAL;
let x be Element of C;
assume that
A1: x in dom f and
A2: max-(f).x = 0.;
A3: x in dom(max+(f)) by A1,Def2;
A4: x in dom(max-(f)) by A1,Def3;
A5: max+(f).x = max(f.x,0.) by A3,Def2;
max-(f).x = max(-(f.x),0.) by A4,Def3;
then -0. <= -(-(f.x)) by A2,XXREAL_0:def 10;
hence thesis by A5,XXREAL_0:def 10;
end;
theorem
for C being non empty set, f being PartFunc of C,ExtREAL holds
f = max+(f) - max-(f)
proof
let C be non empty set;
let f be PartFunc of C,ExtREAL;
A1: dom f = dom(max+(f)-max-(f)) by Th17;
for x being Element of C st x in dom f holds f.x = (max+(f) - max-(f)).x
proof
let x be Element of C;
assume
A2: x in dom f;
then A3: (max+(f) - max-(f)).x = max+(f).x - max-(f).x by A1,MESFUNC1:def 4;
per cases by Th18;
suppose
A4: max+(f).x = f.x;
then max-(f).x = 0. by Th19;
then -max-(f).x = 0;
hence thesis by A3,A4,XXREAL_3:4;
end;
suppose
A5: max+(f).x = 0.;
then max-(f).x = -(f.x) by A2,Th20;
hence thesis by A3,A5,XXREAL_3:4;
end;
end;
hence thesis by A1,PARTFUN1:5;
end;
theorem
for C being non empty set, f being PartFunc of C,ExtREAL holds
|.f.| = max+(f) + max-(f)
proof
let C be non empty set;
let f be PartFunc of C,ExtREAL;
A1: dom f = dom(max+(f)+max-(f)) by Th17;
A2: dom f = dom |.f.| by MESFUNC1:def 10;
for x being Element of C st x in dom f holds
|.f.| .x = (max+(f) + max-(f)).x
proof
let x be Element of C;
assume
A3: x in dom f;
now per cases by Th18;
suppose
A4: max+(f).x = f.x;
then A5: max+(f).x + max-(f).x = f.x + 0. by Th19
.= f.x by XXREAL_3:4;
x in dom(max+(f)) by A3,Def2;
then max+(f).x = max(f.x,0.) by Def2;
then 0. <= f.x by A4,XXREAL_0:def 10;
then f.x = |. f.x .| by EXTREAL1:def 1
.= |.f.| .x by A2,A3,MESFUNC1:def 10;
hence thesis by A1,A3,A5,MESFUNC1:def 3;
end;
suppose
A6: max+(f).x = 0.;
then A7: max+(f).x + max-(f).x = 0. + -(f.x) by A3,Th20
.= -(f.x) by XXREAL_3:4;
x in dom(max+(f)) by A3,Def2;
then max+(f).x = max(f.x,0.) by Def2;
then f.x <= 0. by A6,XXREAL_0:def 10;
then -(f.x) = |. f.x .| by EXTREAL1:18
.= |.f.| .x by A2,A3,MESFUNC1:def 10;
hence thesis by A1,A3,A7,MESFUNC1:def 3;
end;
end;
hence thesis;
end;
hence thesis by A1,A2,PARTFUN1:5;
end;
begin :: Measurability of max+(f), max-(f) and |.f.|
theorem
f is A-measurable implies max+(f) is A-measurable
proof
assume
A1: f is A-measurable;
for r be Real holds A /\ less_dom(max+(f), r) in S
proof
let r be Real;
reconsider r as Real;
now per cases;
suppose
A2: 0 < r;
for x being object st x in less_dom(max+(f), r) holds
x in less_dom(f, r)
proof
let x be object;
assume
A3: x in less_dom(max+(f), r);
then A4: x in dom max+(f) by MESFUNC1:def 11;
A5: max+(f).x < r by A3,MESFUNC1:def 11;
reconsider x as Element of X by A3;
A6: max(f.x,0.) < r by A4,A5,Def2;
then A7: f.x <= r by XXREAL_0:30;
f.x <> r
proof
assume
A8: f.x = r;
then max(f.x,0.) = 0. by A6,XXREAL_0:16;
hence contradiction by A6,A8,XXREAL_0:def 10;
end;
then A9: f.x < r by A7,XXREAL_0:1;
x in dom f by A4,Def2;
hence thesis by A9,MESFUNC1:def 11;
end;
then A10: less_dom(max+(f), r) c= less_dom(f, r);
for x being object st x in less_dom(f, r) holds
x in less_dom(max+(f), r)
proof
let x be object;
assume
A11: x in less_dom(f, r);
then A12: x in dom f by MESFUNC1:def 11;
A13: f.x < r by A11,MESFUNC1:def 11;
reconsider x as Element of X by A11;
A14: x in dom (max+(f)) by A12,Def2;
now per cases;
suppose
0. <= f.x;
then max(f.x,0.) = f.x by XXREAL_0:def 10;
then max+(f).x = f.x by A14,Def2;
hence thesis by A13,A14,MESFUNC1:def 11;
end;
suppose
not 0. <= f.x;
then max(f.x,0.) = 0. by XXREAL_0:def 10;
then max+(f).x = 0. by A14,Def2;
hence thesis by A2,A14,MESFUNC1:def 11;
end;
end;
hence thesis;
end;
then
less_dom(f, r) c= less_dom(max+(f), r);
then less_dom
(max+(f), r) = less_dom(f, r) by A10;
hence thesis by A1;
end;
suppose
A15: r <= 0;
for x being Element of X holds not x in less_dom(max+(f), r)
proof
let x be Element of X;
assume
A16: x in less_dom(max+(f), r);
then A17: x in dom(max+(f)) by MESFUNC1:def 11;
A18: max+(f).x < r by A16,MESFUNC1:def 11;
max+(f).x = max(f.x,0.) by A17,Def2;
hence contradiction by A15,A18,XXREAL_0:25;
end;
then less_dom(max+(f), r) = {} by SUBSET_1:4;
hence thesis by PROB_1:4;
end;
end;
hence thesis;
end;
hence thesis;
end;
theorem
f is A-measurable & A c= dom f implies max-(f) is A-measurable
proof
assume
A1: f is A-measurable & A c= dom f;
for r be Real holds A /\ less_dom(max-(f), r) in S
proof
let r be Real;
reconsider r as Real;
now per cases;
suppose
A2: 0 < r;
(-1)(#)f is A-measurable by A1,MESFUNC1:37;
then A3: -f is A-measurable by Th9;
for x being object st x in less_dom(max-(f), r) holds
x in less_dom(-f, r)
proof
let x be object;
assume
A4: x in less_dom(max-(f), r);
then A5: x in dom max-(f) by MESFUNC1:def 11;
A6: max-(f).x < r by A4,MESFUNC1:def 11;
reconsider x as Element of X by A4;
A7: max(-(f.x),0.) < r by A5,A6,Def3;
then A8: -(f.x) <= r by XXREAL_0:30;
-(f.x) <> r
proof
assume
A9: -(f.x) = r;
then max(-(f.x),0.) = 0. by A7,XXREAL_0:16;
hence contradiction by A7,A9,XXREAL_0:def 10;
end;
then A10: -(f.x) < r by A8,XXREAL_0:1;
x in dom f by A5,Def3;
then A11: x in dom -f by MESFUNC1:def 7;
then (-f).x = -(f.x) by MESFUNC1:def 7;
hence thesis by A10,A11,MESFUNC1:def 11;
end;
then A12: less_dom(max-(f), r) c= less_dom(-f, r);
for x being object st x in less_dom(-f, r) holds
x in less_dom(max-(f), r)
proof
let x be object;
assume
A13: x in less_dom(-f, r);
then A14: x in dom -f by MESFUNC1:def 11;
A15: (-f).x < r by A13,MESFUNC1:def 11;
reconsider x as Element of X by A13;
x in dom f by A14,MESFUNC1:def 7;
then A16: x in dom (max-(f)) by Def3;
now per cases;
suppose
0. <= -(f.x);
then max(-(f.x),0.) = -(f.x) by XXREAL_0:def 10;
then max-(f).x = -(f.x) by A16,Def3
.= (-f).x by A14,MESFUNC1:def 7;
hence thesis by A15,A16,MESFUNC1:def 11;
end;
suppose
not 0. <= -(f.x);
then max(-(f.x),0.) = 0. by XXREAL_0:def 10;
then max-(f).x = 0. by A16,Def3;
hence thesis by A2,A16,MESFUNC1:def 11;
end;
end;
hence thesis;
end;
then
less_dom(-f, r) c= less_dom(max-(f), r);
then less_dom(max-(f), r) = less_dom(-f, r) by A12;
hence thesis by A3;
end;
suppose
A17: r <= 0;
for x being Element of X holds not x in less_dom(max-(f), r)
proof
let x be Element of X;
assume
A18: x in less_dom(max-(f), r);
then A19: x in dom(max-(f)) by MESFUNC1:def 11;
A20: max-(f).x < r by A18,MESFUNC1:def 11;
max-(f).x = max(-(f.x),0.) by A19,Def3;
hence contradiction by A17,A20,XXREAL_0:25;
end;
then less_dom(max-(f), r) = {} by SUBSET_1:4;
hence thesis by PROB_1:4;
end;
end;
hence thesis;
end;
hence thesis;
end;
theorem
for f,A st f is A-measurable & A c= dom f holds |.f.| is A-measurable
proof
let f,A;
assume
A1: f is A-measurable & A c= dom f;
for r be Real holds A /\ less_dom(|.f.|, r) in S
proof
let r be Real;
reconsider r as R_eal by XXREAL_0:def 1;
for x being object st x in less_dom(|.f.|, r) holds
x in less_dom(f, r) /\ great_dom(f, -r)
proof
let x be object;
assume
A2: x in less_dom(|.f.|, r);
then A3: x in dom |.f.| by MESFUNC1:def 11;
A4: |.f.| .x < r by A2,MESFUNC1:def 11;
reconsider x as Element of X by A2;
A5: x in dom f by A3,MESFUNC1:def 10;
A6: |. f.x .| < r by A3,A4,MESFUNC1:def 10;
then A7: -( r) < f.x by EXTREAL1:21;
A8: f.x < r by A6,EXTREAL1:21;
A9: x in less_dom(f, r) by A5,A8,MESFUNC1:def 11;
x in great_dom(f, -r) by A5,A7,MESFUNC1:def 13;
hence thesis by A9,XBOOLE_0:def 4;
end;
then
A10: less_dom(|.f.|, r) c= less_dom(f, r) /\ great_dom(f,
-r);
for x being object st x in less_dom(f, r) /\
great_dom(f, -r) holds x in less_dom(|.f.|, r)
proof
let x be object;
assume
A11: x in less_dom(f, r) /\ great_dom(f, -r);
then A12: x in less_dom(f, r) by XBOOLE_0:def 4;
A13: x in great_dom(f, -r) by A11,XBOOLE_0:def 4;
A14: x in dom f by A12,MESFUNC1:def 11;
A15: f.x < r by A12,MESFUNC1:def 11;
A16: -r < f.x by A13,MESFUNC1:def 13;
reconsider x as Element of X by A11;
A17: x in dom |.f.| by A14,MESFUNC1:def 10;
|. f.x .| < r by A15,A16,EXTREAL1:22;
then |.f.| .x < r by A17,MESFUNC1:def 10;
hence thesis by A17,MESFUNC1:def 11;
end;
then less_dom(f, r) /\ great_dom(f, -r) c= less_dom(|.f.|,
r);
then
A18: less_dom(|.f.|, r) = less_dom(f, r) /\ great_dom(f, -r) by
A10;
A /\ great_dom(f, -r) /\ less_dom(f, r) in S by A1,MESFUNC1:32;
hence thesis by A18,XBOOLE_1:16;
end;
hence thesis;
end;
begin
definition
let A,X be set;
redefine func chi(A,X) -> PartFunc of X,ExtREAL; :: redefines chi (FUNCT_3, definition)
coherence
proof
now
let x be object;
assume
A1: x in rng chi(A,X);
now per cases by A1,TARSKI:def 2;
suppose
x=0.;
hence x in ExtREAL;
end;
suppose
x=1.;
hence x in ExtREAL;
end;
end;
hence x in ExtREAL;
end;
then dom
chi(A,X) =X & rng chi(A,X) c= ExtREAL by FUNCT_3:def 3;
hence chi(A,X) is PartFunc of X,ExtREAL by RELSET_1:4;
end;
end;
theorem
chi(A,X) is real-valued
proof
for x st x in dom chi(A,X) holds |.chi(A,X).x.| < +infty
proof
let x;
assume x in dom chi(A,X);
per cases;
suppose
x in A;
then chi(A,X).x = 1. by FUNCT_3:def 3;
then |.chi(A,X).x.| = jj by EXTREAL1:def 1;
hence thesis by XXREAL_0:9;
end;
suppose
not x in A;
then chi(A,X).x = 0. by FUNCT_3:def 3;
hence thesis by EXTREAL1:def 1;
end;
end;
hence thesis;
end;
theorem
chi(A,X) is B-measurable
proof
for r be Real holds B /\ less_eq_dom(chi(A,X), r) in S
proof
let r be Real;
reconsider r as Real;
now per cases;
suppose
A1: r >= 1;
for x being object st x in X holds x in less_eq_dom(chi(A,X), r)
proof
let x be object;
assume
A2: x in X;
then A3: x in dom chi(A,X) by FUNCT_3:def 3;
reconsider x as Element of X by A2;
chi(A,X).x <= 1.
proof
now per cases;
suppose
x in A;
hence thesis by FUNCT_3:def 3;
end;
suppose
not x in A;
hence thesis by FUNCT_3:def 3;
end;
end;
hence thesis;
end;
then chi(A,X).x <= r by A1,XXREAL_0:2;
hence thesis by A3,MESFUNC1:def 12;
end;
then X c= less_eq_dom(chi(A,X), r);
then less_eq_dom(chi(A,X), r) = X;
then less_eq_dom(chi(A,X), r) in S by PROB_1:5;
hence thesis by FINSUB_1:def 2;
end;
suppose
A4: 0 <= r & r < 1;
for
x being object st x in less_eq_dom(chi(A,X), r) holds x in X\A
proof
let x be object;
assume
A5: x in less_eq_dom(chi(A,X), r);
then reconsider x as Element of X;
chi(A,X).x <= r by A5,MESFUNC1:def 12;
then not x in A by A4,FUNCT_3:def 3;
hence thesis by XBOOLE_0:def 5;
end;
then A6: less_eq_dom(chi(A,X), r) c= X\A;
for
x being object st x in X\A holds x in less_eq_dom(chi(A,X), r)
proof
let x be object;
assume
A7: x in X\A;
then A8: x in X;
A9: not x in A by A7,XBOOLE_0:def 5;
reconsider x as Element of X by A7;
A10: chi(A,X).x = 0. by A9,FUNCT_3:def 3;
x in dom chi(A,X) by A8,FUNCT_3:def 3;
hence thesis by A4,A10,MESFUNC1:def 12;
end;
then X\A c= less_eq_dom(chi(A,X), r);
then A11: less_eq_dom(chi(A,X), r) = X\A by A6;
X in S by PROB_1:5;
then less_eq_dom(chi(A,X), r) in S by A11,MEASURE1:6;
hence thesis by FINSUB_1:def 2;
end;
suppose
A12: r < 0;
for x holds not x in less_eq_dom(chi(A,X), r)
proof
assume ex x st x in less_eq_dom(chi(A,X), r);
then consider x such that
A13: x in less_eq_dom(chi(A,X), r);
0. <= chi(A,X).x
proof
now per cases;
suppose
x in A;
hence thesis by FUNCT_3:def 3;
end;
suppose
not x in A;
hence thesis by FUNCT_3:def 3;
end;
end;
hence thesis;
end;
hence contradiction by A12,A13,MESFUNC1:def 12;
end;
then less_eq_dom(chi(A,X), r) = {} by SUBSET_1:4;
hence thesis by PROB_1:4;
end;
end;
hence thesis;
end;
hence thesis by MESFUNC1:28;
end;
begin :: Definition and measurability of simple function
registration
let X be set;
let S be SigmaField of X;
cluster disjoint_valued for FinSequence of S;
existence
proof
reconsider A = {} as Element of S by PROB_1:4;
reconsider p = Seg 1 --> A as Function of Seg 1, S;
A1: dom p = Seg 1 by FUNCOP_1:13;
then reconsider p as FinSequence by FINSEQ_1:def 2;
rng p c= S by RELAT_1:def 19;
then reconsider p as FinSequence of S by FINSEQ_1:def 4;
A2: for n,m being object st n <> m holds p.n misses p.m
proof
let n,m be object;
assume n <> m;
p.n = {}
proof
per cases;
suppose
n in dom p;
hence thesis by A1,FUNCOP_1:7;
end;
suppose
not n in dom p;
hence thesis by FUNCT_1:def 2;
end;
end;
hence thesis;
end;
take p;
thus thesis by A2,PROB_2:def 2;
end;
end;
definition
let X be set;
let S be SigmaField of X;
mode Finite_Sep_Sequence of S is disjoint_valued FinSequence of S;
end;
theorem Th30:
for F being Function st F is Finite_Sep_Sequence of S holds
ex G being Sep_Sequence of S st union rng F = union rng G &
(for n st n in dom F holds F.n = G.n) &
for m st not m in dom F holds G.m = {}
proof
let F be Function;
defpred P[object,object] means
($1 in dom F implies F.$1 = $2) & (not $1 in dom F implies $2 = {});
assume
A1: F is Finite_Sep_Sequence of S;
A2: for x1 being object st x1 in NAT
ex y1 being object st y1 in S & P[x1,y1]
proof
let x1 be object;
assume x1 in NAT;
then reconsider x1 as Element of NAT;
per cases;
suppose
A3: x1 in dom F;
then A4: F.x1 in rng F by FUNCT_1:def 3;
A5: rng F c= S by A1,FINSEQ_1:def 4;
take F.x1;
thus thesis by A3,A4,A5;
end;
suppose
A6: not x1 in dom F;
take {};
thus thesis by A6,PROB_1:4;
end;
end;
consider G being sequence of S such that
A7: for x1 being object st x1 in NAT holds P[x1,G.x1] from FUNCT_2:sch 1(A2);
for n,m being object st n <> m holds G.n misses G.m
proof
let n,m be object;
assume
A8: n <> m;
per cases;
suppose
A9: n in NAT & m in NAT;
now per cases;
suppose
n in dom F & m in dom F;
then G.n = F.n & G.m = F.m by A7,A9;
hence thesis by A1,A8,PROB_2:def 2;
end;
suppose
A10: not n in dom F or not m in dom F;
now per cases by A10;
suppose
not n in dom F;
then G.n = {} by A7,A9;
hence thesis;
end;
suppose
not m in dom F;
then G.m = {} by A7,A9;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
suppose
not (n in NAT & m in NAT);
then not n in dom G or not m in dom G;
then G.n = {} or G.m = {} by FUNCT_1:def 2;
hence thesis;
end;
end;
then reconsider G as Sep_Sequence of S by PROB_2:def 2;
take G;
for x1 being object st x1 in union rng F holds x1 in union rng G
proof
let x1 be object;
assume x1 in union rng F;
then consider Y being set such that
A11: x1 in Y and
A12: Y in rng F by TARSKI:def 4;
consider k being object such that
A13: k in dom F and
A14: Y = F.k by A12,FUNCT_1:def 3;
dom F c= NAT by A1,RELAT_1:def 18;
then reconsider k as Element of NAT by A13;
A15: F.k = G.k by A7,A13;
G.k in rng G by FUNCT_2:4;
hence thesis by A11,A14,A15,TARSKI:def 4;
end;
then A16: union rng F c= union rng G;
for x1 being object st x1 in union rng G holds x1 in union rng F
proof
let x1 be object;
assume x1 in union rng G;
then consider Y being set such that
A17: x1 in Y and
A18: Y in rng G by TARSKI:def 4;
consider k being object such that
A19: k in dom G and
A20: Y = G.k by A18,FUNCT_1:def 3;
reconsider k as Element of NAT by A19;
A21: k in dom F by A7,A17,A20;
A22: F.k = G.k by A7,A17,A20;
F.k in rng F by A21,FUNCT_1:def 3;
hence thesis by A17,A20,A22,TARSKI:def 4;
end;
then union rng G c= union rng F;
hence union rng F = union rng G by A16;
hereby
let n;
n in NAT by ORDINAL1:def 12;
hence n in dom F implies F.n = G.n by A7;
end;
let m;
m in NAT by ORDINAL1:def 12;
hence thesis by A7;
end;
theorem
for F being Function st F is Finite_Sep_Sequence of S holds union rng F in S
proof
let F be Function;
assume F is Finite_Sep_Sequence of S;
then ex G being Sep_Sequence of S st union rng F = union rng G
&( for n st n in dom F holds F.n = G.n)& for m st not m in dom F holds G.m =
{} by Th30;
hence thesis;
end;
definition
let X be non empty set;
let S be SigmaField of X;
let f be PartFunc of X,ExtREAL;
pred f is_simple_func_in S means
f is real-valued &
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
f is real-valued implies rng f is Subset of REAL;
theorem
for F being Relation st F is Finite_Sep_Sequence of S holds
F|(Seg n) is Finite_Sep_Sequence of S
proof
let F be Relation;
assume
A1: F is Finite_Sep_Sequence of S;
then reconsider G = F|(Seg n) as FinSequence of S by FINSEQ_1:18;
reconsider F as FinSequence of S by A1;
for k,m being object st k <> m holds G.k misses G.m
proof
let k,m be object;
assume
A2: k <> m;
per cases;
suppose k in dom G & m in dom G;
then G.k = F.k & G.m = F.m by FUNCT_1:47;
hence thesis by A1,A2,PROB_2:def 2;
end;
suppose not (k in dom G & m in dom G);
then G.k = {} or G.m = {} by FUNCT_1:def 2;
hence thesis;
end;
end;
hence thesis by PROB_2:def 2;
end;
theorem
f is_simple_func_in S implies f is A-measurable
proof
assume
A1: f is_simple_func_in S;
then consider F being Finite_Sep_Sequence of S such that
A2: dom f = union rng F and
A3: 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;
reconsider F as FinSequence of S;
defpred P[Nat] means
$1 <= len F implies f|(union rng(F|(Seg($1)))) is A-measurable;
A4: P[0]
proof
assume
A5: 0 <= len F;
reconsider z = 0 as Nat;
reconsider G = F|Seg z as FinSequence of S by FINSEQ_1:18;
len G = 0 by A5,FINSEQ_1:17;
then G = {};
then A6: dom(f|union rng G) = dom f /\ {} by RELAT_1:38,61,ZFMISC_1:2
.= {};
for r be Real holds A /\ less_dom(f|union rng G, r) in S
proof
let r be Real;
for x1 being object st x1 in less_dom(f|union rng G, r) holds
x1 in dom(f|union rng G) by MESFUNC1:def 11;
then less_dom(f|union rng G, r)c=dom(f|union rng G);
then less_dom(f|union rng G, r) = {} by A6,XBOOLE_1:3;
hence thesis by PROB_1:4;
end;
hence thesis;
end;
A7: for m st P[m] holds P[m+1]
proof
let m;
assume
A8: m <= len F implies f|(union rng(F|(Seg m))) is A-measurable;
reconsider m as Element of NAT by ORDINAL1:def 12;
m+1 <= len F implies f|(union rng(F|(Seg(m+1)))) is A-measurable
proof
assume
A9: m+1 <= len F;
A10: m <= m+1 by NAT_1:11;
for r be Real holds
A /\ less_dom(f|union rng(F|(Seg(m+1))), r) in S
proof
let r be Real;
now per cases;
suppose
A11: F.(m+1) = {};
less_dom(f|union rng(F|(Seg m)), r)
= less_dom(f|union rng(F|(Seg(m+1))), r)
proof
reconsider G1 = F|(Seg m) as FinSequence of S by FINSEQ_1:18;
1 <= m+1 by NAT_1:11;
then m+1 in Seg len F by A9,FINSEQ_1:1;
then m+1 in dom F by FINSEQ_1:def 3;
then F|(Seg(m+1)) = G1^<*{}*> by A11,FINSEQ_5:10;
then rng (F|(Seg(m+1))) = rng G1 \/ rng <*{}*> by FINSEQ_1:31
.= rng G1 \/ {{}} by FINSEQ_1:39;
then union rng (F|(Seg(m+1))) = union rng G1 \/ union {{}} by
ZFMISC_1:78
.= union rng G1 \/ {} by ZFMISC_1:25
.= union rng G1;
hence thesis;
end;
hence thesis by A8,A9,A10,XXREAL_0:2;
end;
suppose
A12: F.(m+1) <> {};
reconsider G1 = F|(Seg m) as FinSequence of S by FINSEQ_1:18;
1 <= m+1 by NAT_1:11;
then m+1 in Seg len F by A9,FINSEQ_1:1;
then A13: m+1 in dom F by FINSEQ_1:def 3;
then A14: F.(m+1) in rng F by FUNCT_1:def 3;
then F.(m+1) in S;
then reconsider F1=F.(m+1) as Subset of X;
consider x such that
A15: x in F1 by A12,SUBSET_1:4;
F|(Seg(m+1)) = G1^<*(F.(m+1))*> by A13,FINSEQ_5:10;
then
rng (F|(Seg(m+1))) = rng G1 \/ rng <*(F.(m+1))*> by FINSEQ_1:31
.= rng G1 \/ {F.(m+1)} by FINSEQ_1:39;
then A16: union rng (F|(Seg(m+1))) = union rng G1 \/
union {F.(m+1)} by ZFMISC_1:78
.= union rng G1 \/ F.(m+1) by ZFMISC_1:25;
A17: x in dom f by A2,A14,A15,TARSKI:def 4;
f is real-valued by A1;
then A18: |. f.x .| < +infty by A17;
then -(+infty) < f.x by EXTREAL1:21;
then A19: -infty < f.x by XXREAL_3:def 3;
f.x < +infty by A18,EXTREAL1:21;
then reconsider r1 = f.x as Element of REAL by A19,XXREAL_0:14;
now per cases;
suppose
A20: r <= r1;
for
x1 being object st x1 in less_dom(f|union rng(F|(Seg(m+1)))
, r)
holds x1 in less_dom(f|union rng(F|(Seg m)), r)
proof
let x1 be object;
assume
A21: x1 in less_dom(f|union rng(F|(Seg(m+1))), r);
then A22: x1
in dom(f|union rng(F|(Seg(m+1)) )) by MESFUNC1:def 11;
then x1 in dom f /\ union rng(F|(Seg(m+1))) by RELAT_1:61;
then x1 in (dom f /\ union rng G1) \/ (dom f /\
F.(m+1)) by A16,XBOOLE_1:23;
then A23: x1
in dom f /\ union rng G1 or x1 in dom f /\ F.(m+1) by XBOOLE_0:def 3;
reconsider x1 as Element of X by A21;
A24: (f|union rng(F|(Seg(m+1)))).x1 < r
by A21,MESFUNC1:def 11;
A25: ( f|union rng(F|(Seg(m+1)))).x1 = f.x1 by A22,FUNCT_1:47;
set m1 = m+1;
not x1 in dom(f|F1)
proof
assume x1 in dom(f|F1);
then x1 in dom f /\ F1 by RELAT_1:61;
then x1 in F.m1 by XBOOLE_0:def 4;
hence contradiction by A3,A13,A15,A20,A24,A25;
end;
then A26: x1 in dom(f|union rng G1) by A23,RELAT_1:61;
then (
f|union rng(F|(Seg(m+1)))).x1 = (f|union rng G1).x1 by A25,FUNCT_1:47;
hence thesis by A24,A26,MESFUNC1:def 11;
end;
then
A27: less_dom(f|union rng(F|(Seg(m+1))), r)
c= less_dom(f|union rng(F|(Seg m)), r);
for
x1 being object st x1 in less_dom(f|union rng(F|(Seg m)), r)
holds x1 in less_dom(f|union rng(F|(Seg(m+1))), r)
proof
let x1 be object;
assume
A28: x1 in less_dom(f|union rng(F|(Seg m)), r);
then A29: x1 in dom(f|union rng(F|(Seg m))) by MESFUNC1:def 11;
then A30: x1 in dom f /\ union rng G1 by RELAT_1:61;
then A31: x1 in union rng G1 by XBOOLE_0:def 4;
A32: x1 in dom f by A30,XBOOLE_0:def 4;
x1 in union rng (F|(Seg(m+1))) by A16,A31,XBOOLE_0:def 3;
then x1
in dom f /\ union rng (F|(Seg(m+1))) by A32,XBOOLE_0:def 4;
then A33: x1
in dom(f|union rng(F|(Seg(m+1)) )) by RELAT_1:61;
reconsider x1 as Element of X by A28;
A34: (
f|union rng(F|(Seg m))).x1 < r by A28,MESFUNC1:def 11;
(f|union rng(F|(Seg m))).x1 = f.x1 by A29,FUNCT_1:47;
then
(f|union rng(F|(Seg m))).x1 = (f|union rng(F|(Seg(m+1)))).x1
by A33,FUNCT_1:47;
hence thesis by A33,A34,MESFUNC1:def 11;
end;
then less_dom(f|union rng(F|(Seg m)), r)
c= less_dom(f|union rng(F|(Seg(m+1))), r);
then less_dom
(f|union rng(F|(Seg(m+1))), r) = less_dom(f|union rng(F|(Seg
m)), r) by A27;
hence thesis by A8,A9,A10,XXREAL_0:2;
end;
suppose
A35: r1 < r;
for
x1 being object st x1 in less_dom(f|union rng(F|(Seg(m+1))), r)
holds x1 in less_dom(f|union rng(F|(Seg m)), r) \/ F.(m+1)
proof
let x1 be object;
assume
A36: x1 in less_dom(f|union rng(F|(Seg(m+1))), r);
then A37: x1
in dom(f|union rng(F|(Seg(m+1)) )) by MESFUNC1:def 11;
then x1 in dom f /\ union rng(F|(Seg(m+1))) by RELAT_1:61;
then A38: x1 in (dom f /\ union rng G1) \/ (
dom f /\ F.(m+1)) by A16,XBOOLE_1:23;
now per cases by A38,XBOOLE_0:def 3;
suppose
A39: x1 in dom f /\ union rng G1;
then reconsider x1 as Element of X;
A40: x1 in dom(f|union rng G1) by A39,RELAT_1:61;
then A41: (f|union rng G1).x1 = f.x1 by FUNCT_1:47;
A42: (f|union rng(F|(Seg(m+1)))).x1 < r
by A36,MESFUNC1:def 11;
(
f|union rng(F|(Seg(m+1)))).x1 = (f|union rng G1).x1
by A37,A41,FUNCT_1:47;
then x1 in less_dom(f|union rng(F|(Seg m)), r)
by A40,A42,MESFUNC1:def 11;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x1 in dom f /\ F.(m+1);
then x1 in F.(m+1) by XBOOLE_0:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
then
A43: less_dom(f|union rng(F|(Seg(m+1))), r)
c= less_dom(f|union rng(F|(Seg m)), r) \/
F.(m+1);
for x1 being object st
x1 in less_dom(f|union rng(F|(Seg m)), r) \/ F.(m+1) holds
x1 in less_dom(f|union rng(F|(Seg(m+1))), r)
proof
let x1 be object;
assume
A44: x1 in less_dom(f|union rng(F|(Seg m)), r)\/ F.(m+1);
now per cases by A44,XBOOLE_0:def 3;
suppose
A45: x1 in less_dom(f|union rng(F|(Seg m)), r);
then A46: x1
in dom(f|union rng(F|( Seg m))) by MESFUNC1:def 11;
then A47: x1 in dom f /\ union rng G1 by RELAT_1:61;
then A48: x1 in union rng G1 by XBOOLE_0:def 4;
A49: x1 in dom f by A47,XBOOLE_0:def 4;
x1 in union rng (F|(Seg(m+1))) by A16,A48,XBOOLE_0:def 3;
then x1
in dom f /\ union rng (F|(Seg(m+1))) by A49,XBOOLE_0:def 4;
then A50: x1
in dom(f|union rng(F|( Seg(m+1)))) by RELAT_1:61;
reconsider x1 as Element of X by A45;
A51: (f|union rng(F|(Seg m))).x1 < r
by A45,MESFUNC1:def 11;
(f|union rng(F|(Seg m))).x1 = f.x1 by A46,FUNCT_1:47;
then (f|union rng(F|(Seg m))).x1 =
(f|union rng(F|(Seg(m+1)))).x1 by A50,FUNCT_1:47;
hence thesis by A50,A51,MESFUNC1:def 11;
end;
suppose
A52: x1 in F.(m+1);
then A53: x1
in union rng (F|(Seg(m+ 1))) by A16,XBOOLE_0:def 3;
A54: x1 in dom f by A2,A14,A52,TARSKI:def 4;
then x1 in dom f /\ union rng (F|(Seg(m+1)))
by A53,XBOOLE_0:def 4;
then A55: x1
in dom(f|union rng (F|( Seg(m+1)))) by RELAT_1:61;
reconsider x1 as Element of X by A54;
A56: f.x1 = r1 by A3,A13,A15,A52;
reconsider y = f.x1 as R_eal;
y = (f|union rng (F|(Seg(m+1)))).x1 by A55,FUNCT_1:47;
hence thesis by A35,A55,A56,MESFUNC1:def 11;
end;
end;
hence thesis;
end;
then less_dom(f|union rng(F|(Seg m)), r) \/ F.(m+1)
c= less_dom(f|union rng(F|(Seg(m+1))), r);
then less_dom
(f|union rng(F|(Seg(m+1))), r) = less_dom(f|union rng(F|(Seg
m)), r) \/ F.(m+1) by A43;
then A57: A
/\ less_dom(f|union rng(F|(Seg(m+1))), r)
= (A /\ less_dom(f|union rng(F|(Seg m)), r)) \/ (A /\ F.(m+1))
by XBOOLE_1:23;
A
/\ less_dom(f|union rng(F|(Seg m)), r) in S & A /\ F.(m+1) in S by A8,A9
,A10,A14,FINSUB_1:def 2,XXREAL_0:2;
hence thesis by A57,FINSUB_1:def 1;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
A58: for n being Nat holds P[n] from NAT_1:sch 2(A4,A7);
F|(Seg len F) = F by FINSEQ_3:49;
then f|(dom f) is A-measurable by A2,A58;
hence thesis by RELAT_1:68;
end;