:: Integral of Complex-Valued Measurable Function
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received July 30, 2008
:: Copyright (c) 2008-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, MEASURE6, ARYTM_3, ARYTM_1, RELAT_1, REAL_1, XBOOLE_0,
PARTFUN1, COMPLEX1, SUBSET_1, FUNCT_1, PROB_1, MEASURE1, XCMPLX_0,
MESFUNC1, VALUED_1, CARD_1, TARSKI, INTEGRA5, MESFUNC5, XXREAL_0,
RFUNCT_3, SUPINF_2, POWER, SQUARE_1, PREPOWER;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XXREAL_3,
XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, SUPINF_2, PREPOWER, POWER, SQUARE_1, MEASURE6,
MEASURE1, EXTREAL1, COMSEQ_3, VALUED_0, MESFUNC1,
VALUED_1, MESFUNC2, PROB_1,
MESFUNC5, MESFUNC6;
constructors REAL_1, PREPOWER, POWER, SQUARE_1, COMPLEX1, MEASURE6, EXTREAL1,
MESFUNC1, MESFUNC2, MESFUNC5, MESFUNC6, SUPINF_1, RELSET_1, ABIAN,
BINOP_2, VALUED_0, COMSEQ_3;
registrations XBOOLE_0, SUBSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED,
MEASURE1, VALUED_0, XCMPLX_0, RELAT_1, FUNCT_1, RELSET_1, SQUARE_1,
ORDINAL1, XXREAL_3;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions SUPINF_2;
equalities MESFUNC5, VALUED_1, MESFUNC6, COMPLEX1, XCMPLX_0;
expansions MESFUNC5, MESFUNC6;
theorems TARSKI, PARTFUN1, FUNCT_1, SUPINF_2, EXTREAL1, MESFUNC1, XBOOLE_0,
XBOOLE_1, XCMPLX_1, HOLDER_1, PREPOWER, MESFUNC2, XREAL_1, MESFUNC5,
XXREAL_0, VALUED_1, MESFUNC6, SUBSET_1, COMPLEX1, XREAL_0, RELAT_1,
POWER, SQUARE_1, RELSET_1, FINSUB_1, COMSEQ_3, XCMPLX_0;
schemes SEQ_1;
begin :: Definitions for Complex-valued Functions
theorem
for a,b be Real holds a + b = a+b & - a =
-a & a - b = a-b & a * b = a*b;
begin :: The Measurability of Complex-valued Functions
reserve X for non empty set,
Y for set,
S for SigmaField of X,
M for sigma_Measure of S,
f,g for PartFunc of X,COMPLEX,
r for Real,
c for Complex,
E,A,B for Element of S;
definition
let X be non empty set;
let S be SigmaField of X;
let E be Element of S;
let f be PartFunc of X,COMPLEX;
attr f is E-measurable means
Re f is E-measurable & Im f is E-measurable;
end;
theorem Th2:
r(#)(Re f) = Re(r(#)f) & r(#)(Im f) = Im(r(#)f)
proof
A1: dom(r(#)(Re f)) = dom Re f by VALUED_1:def 5;
A3: Im r = 0 by COMPLEX1:def 2;
A4: dom Re f = dom f by COMSEQ_3:def 3;
A5: Re r = r by COMPLEX1:def 1;
A6: dom(r(#)f) = dom f by VALUED_1:def 5;
A7: dom Re(r(#)f) = dom(r(#)f) by COMSEQ_3:def 3;
now
let x be object;
A8: Re(r * f.x) = Re r * Re(f.x) - Im r * Im(f.x) by COMPLEX1:9;
assume
A9: x in dom(r(#)(Re f));
then
A10: (Re f).x = Re(f.x) by A1,COMSEQ_3:def 3;
Re(r(#)f).x = Re((r(#)f).x) by A1,A6,A7,A4,A9,COMSEQ_3:def 3;
then Re(r(#)f).x = r * Re(f.x) by A1,A6,A4,A5,A3,A9,A8,VALUED_1:def 5;
hence (r(#)(Re f)).x = Re(r(#)f).x by A9,A10,VALUED_1:def 5;
end;
hence r(#)(Re f) = Re(r(#)f) by A1,A6,A7,A4,FUNCT_1:2;
A11: dom(r(#)(Im f)) = dom Im f by VALUED_1:def 5;
A12: dom Im f = dom f by COMSEQ_3:def 4;
A13: dom Im(r(#)f) = dom(r(#)f) by COMSEQ_3:def 4;
now
let x be object;
A14: Im(r * f.x) = Im r * Re(f.x) + Re r * Im(f.x) by COMPLEX1:9;
assume
A15: x in dom(r(#)Im(f));
then
A16: (Im f).x = Im(f.x) by A11,COMSEQ_3:def 4;
Im(r(#)f).x = Im((r(#)f).x) by A11,A6,A13,A12,A15,COMSEQ_3:def 4;
then Im(r(#)f).x = r * Im(f.x) by A11,A6,A12,A5,A3,A15,A14,VALUED_1:def 5;
hence (r(#)Im(f)).x = Im(r(#)f).x by A15,A16,VALUED_1:def 5;
end;
hence thesis by A11,A6,A13,A12,FUNCT_1:2;
end;
theorem Th3:
Re(c(#)f) = (Re c)(#)(Re f) - (Im c)(#)(Im f) & Im(c(#)f) = (Im c
)(#)(Re f) + (Re c)(#)(Im f)
proof
A1: dom((Re c)(#)(Re f)) = dom Re f by VALUED_1:def 5;
A2: dom((Im c)(#)(Im f)) = dom Im f by VALUED_1:def 5;
A3: dom(c(#)f) = dom f by VALUED_1:def 5;
A4: dom(Re(c(#)f)) = dom(c(#)f) by COMSEQ_3:def 3;
A5: dom Re f = dom f by COMSEQ_3:def 3;
A6: dom Im f = dom f by COMSEQ_3:def 4;
A7: dom( Re(c)(#)Re(f) - Im(c)(#)Im(f) ) = dom(Re(c)(#)Re(f)) /\ dom(Im(c)
(#)Im(f)) by VALUED_1:12;
now
let x be object;
A8: Re(c * f.x) = Re(c) * Re(f.x) - Im(c) * Im(f.x) by COMPLEX1:9;
assume
A9: x in dom(Re(c(#)f));
then
A10: (Im(c)(#)Im(f)).x = Im(c) * Im(f).x by A4,A6,A2,A3,VALUED_1:def 5;
A11: Im(f).x = Im(f.x) by A4,A6,A3,A9,COMSEQ_3:def 4;
A12: Re(f).x = Re(f.x) by A4,A5,A3,A9,COMSEQ_3:def 3;
Re(c(#)f).x = Re((c(#)f).x) by A9,COMSEQ_3:def 3;
then
A13: Re(c(#)f).x = Re(c * f.x) by A4,A9,VALUED_1:def 5;
(Re(c)(#)Re(f)).x = Re(c) * Re(f).x by A4,A5,A1,A3,A9,VALUED_1:def 5;
hence Re(c(#)f).x = ( Re(c)(#)Re(f) - Im(c)(#)Im(f) ).x by A4,A5,A6,A1,A2
,A3,A7,A9,A13,A10,A12,A11,A8,VALUED_1:13;
end;
hence Re(c(#)f) = Re(c)(#)Re(f) - Im(c)(#)Im(f) by A4,A5,A6,A1,A2,A3,A7,
FUNCT_1:2;
A14: dom((Im c)(#)(Re f)) = dom Re f by VALUED_1:def 5;
A15: dom((Re c)(#)(Im f)) = dom Im f by VALUED_1:def 5;
A16: dom(Im(c(#)f)) = dom(c(#)f) by COMSEQ_3:def 4;
A17: dom( Im(c)(#)Re(f) + Re(c)(#)Im(f) ) = dom(Im(c)(#)Re(f)) /\ dom(Re(c)
(#)Im(f)) by VALUED_1:def 1;
now
let x be object;
assume
A18: x in dom(Im(c(#)f));
then
A19: (Im(c)(#)Re(f)).x = Im(c) * Re(f).x by A5,A16,A14,A3,VALUED_1:def 5;
Im(c(#)f).x = Im((c(#)f).x) by A18,COMSEQ_3:def 4;
then
A20: Im(c(#)f).x = Im(c * f.x) by A16,A18,VALUED_1:def 5;
A21: (Im f).x = Im(f.x) by A16,A6,A3,A18,COMSEQ_3:def 4;
A22: (Re f).x = Re(f.x) by A5,A16,A3,A18,COMSEQ_3:def 3;
A23: (Re(c)(#)Im(f)).x = Re(c) * Im(f).x by A16,A6,A15,A3,A18,VALUED_1:def 5;
(Im(c)(#)Re(f) + Re(c)(#)Im(f)).x = (Im(c)(#)Re(f)).x + (Re(c)(#)Im(f
)). x by A5,A16,A6,A14,A15,A3,A17,A18,VALUED_1:def 1;
hence Im(c(#)f).x = ( Im(c)(#)Re(f) + Re(c)(#)Im(f) ).x by A20,A19,A23,A22
,A21,COMPLEX1:9;
end;
hence thesis by A5,A16,A6,A14,A15,A3,A17,FUNCT_1:2;
end;
theorem Th4:
-(Im f) = Re(<i>(#)f) & Re f = Im(<i>(#)f)
proof
A1: dom -(Im f) = dom Im f by VALUED_1:8;
A2: dom(<i>(#)f) = dom f by VALUED_1:def 5;
A3: dom Im f = dom f by COMSEQ_3:def 4;
A4: dom Re(<i>(#)f) = dom(<i>(#)f) by COMSEQ_3:def 3;
now
let x be object;
A5: (-Im(f)).x = -((Im f).x) by VALUED_1:8;
A6: Re(<i> * f.x) = Re(<i>) * Re(f.x) - Im(<i>) * Im(f.x) by COMPLEX1:9;
assume
A7: x in dom -(Im f);
then Re(<i>(#)f).x = Re((<i>(#)f).x) by A1,A4,A2,A3,COMSEQ_3:def 3;
then Re(<i>(#)f).x = -Im(f.x) by A1,A2,A3,A7,A6,COMPLEX1:7,VALUED_1:def 5;
hence (-Im(f)).x = Re(<i>(#)f).x by A1,A7,A5,COMSEQ_3:def 4;
end;
hence -Im(f) = Re(<i>(#)f) by A4,A2,A3,FUNCT_1:2,VALUED_1:8;
A8: dom Re f = dom f by COMSEQ_3:def 3;
A9: dom Im(<i>(#)f) = dom(<i>(#)f) by COMSEQ_3:def 4;
now
let x be object;
A10: Im(<i> * f.x) = Im(<i>) * Re(f.x) + Re(<i>) * Im(f.x) by COMPLEX1:9;
assume
A11: x in dom Re f;
then Im(<i>(#)f).x = Im((<i>(#)f).x) by A8,A2,A9,COMSEQ_3:def 4;
then Im(<i>(#)f).x = Re(f.x) by A8,A2,A11,A10,COMPLEX1:7,VALUED_1:def 5;
hence Re(f).x = Im(<i>(#)f).x by A11,COMSEQ_3:def 3;
end;
hence thesis by A8,A2,A9,FUNCT_1:2;
end;
theorem Th5:
Re(f+g) = Re f + Re g & Im(f+g) = Im f + Im g
proof
A1: dom(Re(f+g)) = dom(f+g) by COMSEQ_3:def 3;
A2: dom Re g = dom g by COMSEQ_3:def 3;
A3: dom Re f = dom f by COMSEQ_3:def 3;
then dom((Re f)+(Re g)) = dom f /\ dom g by A2,VALUED_1:def 1;
then
A4: dom(Re(f+g)) = dom((Re f)+(Re g)) by A1,VALUED_1:def 1;
now
let x be object;
assume
A5: x in dom(Re(f+g));
then Re(f+g).x = Re((f+g).x) by COMSEQ_3:def 3;
then Re(f+g).x = Re(f.x + g.x) by A1,A5,VALUED_1:def 1;
then
A6: Re(f+g).x = Re(f.x) + Re(g.x) by COMPLEX1:8;
A7: x in dom f /\ dom g by A1,A5,VALUED_1:def 1;
then x in dom Re g by A2,XBOOLE_0:def 4;
then
A8: (Re g).x = Re(g.x) by COMSEQ_3:def 3;
x in dom Re f by A3,A7,XBOOLE_0:def 4;
then (Re f).x = Re(f.x) by COMSEQ_3:def 3;
hence Re(f+g).x = (Re(f)+Re(g)).x by A4,A5,A6,A8,VALUED_1:def 1;
end;
hence Re(f+g) = Re(f)+Re(g) by A4,FUNCT_1:2;
A9: dom Im(f+g) = dom(f+g) by COMSEQ_3:def 4;
A10: dom Im g = dom g by COMSEQ_3:def 4;
A11: dom Im f = dom f by COMSEQ_3:def 4;
then dom(Im f + Im g) = dom f /\ dom g by A10,VALUED_1:def 1;
then
A12: dom Im(f+g) = dom(Im f + Im g) by A9,VALUED_1:def 1;
now
let x be object;
assume
A13: x in dom Im(f+g);
then Im(f+g).x = Im((f+g).x) by COMSEQ_3:def 4;
then Im(f+g).x = Im(f.x + g.x) by A9,A13,VALUED_1:def 1;
then
A14: Im(f+g).x = Im(f.x) + Im(g.x) by COMPLEX1:8;
A15: x in dom f /\ dom g by A9,A13,VALUED_1:def 1;
then x in dom Im g by A10,XBOOLE_0:def 4;
then
A16: (Im g).x = Im(g.x) by COMSEQ_3:def 4;
x in dom Im f by A11,A15,XBOOLE_0:def 4;
then (Im f).x = Im(f.x) by COMSEQ_3:def 4;
hence Im(f+g).x = (Im(f)+Im(g)).x by A12,A13,A14,A16,VALUED_1:def 1;
end;
hence thesis by A12,FUNCT_1:2;
end;
theorem Th6:
Re(f-g) = Re f - Re g & Im(f-g) = Im f - Im g
proof
Re(f-g) = Re f + Re -g by Th5;
then
A1: Re(f-g) = Re f + (-1)(#)(Re g) by Th2;
Im(f-g) = Im f + Im -g by Th5;
hence thesis by A1,Th2;
end;
theorem Th7: :: MESFUNC7:2
(Re f)|A = Re(f|A) & (Im f)|A = Im(f|A)
proof
dom((Re f)|A) = (dom Re f) /\ A by RELAT_1:61
.= dom f /\ A by COMSEQ_3:def 3;
then
A1: dom((Re f)|A) = dom(f|A) by RELAT_1:61
.= dom Re(f|A) by COMSEQ_3:def 3;
now
let x be object;
assume
A2: x in dom(Re(f)|A);
then
A3: x in dom Re(f) /\ A by RELAT_1:61;
then
A4: x in dom Re f by XBOOLE_0:def 4;
A5: x in A by A3,XBOOLE_0:def 4;
thus Re(f|A).x = Re((f|A).x) by A1,A2,COMSEQ_3:def 3
.= Re(f.x) by A5,FUNCT_1:49
.= (Re f).x by A4,COMSEQ_3:def 3
.= ((Re f)|A).x by A5,FUNCT_1:49;
end;
hence Re(f)|A = Re(f|A) by A1,FUNCT_1:2;
dom((Im f)|A) = (dom Im f) /\ A by RELAT_1:61
.= dom f /\ A by COMSEQ_3:def 4;
then
A6: dom((Im f)|A) = dom(f|A) by RELAT_1:61
.= dom Im(f|A) by COMSEQ_3:def 4;
now
let x be object;
assume
A7: x in dom(Im(f)|A);
then
A8: x in dom Im(f) /\ A by RELAT_1:61;
then
A9: x in dom Im f by XBOOLE_0:def 4;
A10: x in A by A8,XBOOLE_0:def 4;
thus Im(f|A).x = Im((f|A).x) by A6,A7,COMSEQ_3:def 4
.= Im(f.x) by A10,FUNCT_1:49
.= (Im f).x by A9,COMSEQ_3:def 4
.= ((Im f)|A).x by A10,FUNCT_1:49;
end;
hence thesis by A6,FUNCT_1:2;
end;
theorem Th8:
f = Re f + <i>(#)(Im f)
proof
A1: dom f = dom Re f by COMSEQ_3:def 3;
A2: dom f = dom Im f by COMSEQ_3:def 4;
A3: dom(Re f + <i>(#)(Im f)) = dom Re f /\ dom(<i>(#)(Im f)) by VALUED_1:def 1
.= dom f /\ dom f by A1,A2,VALUED_1:def 5;
A4: dom(<i>(#)(Im f)) = dom Im f by VALUED_1:def 5;
now
let x be object;
assume
A5: x in dom(Re f + <i>(#)(Im f));
then (Re f + <i>(#)(Im f)).x = (Re f).x + (<i>(#)(Im f)).x by
VALUED_1:def 1
.= Re(f.x) + (<i>(#)(Im f)).x by A1,A3,A5,COMSEQ_3:def 3
.= Re(f.x) + <i> * (Im f).x by A2,A4,A3,A5,VALUED_1:def 5
.= Re(f.x) + <i> * Im(f.x) by A2,A3,A5,COMSEQ_3:def 4;
hence (Re f + <i>(#)(Im f)).x = f.x by COMPLEX1:13;
end;
hence thesis by A3,FUNCT_1:2;
end;
theorem
B c= A & f is A-measurable implies f is B-measurable
by MESFUNC6:16;
theorem
f is A-measurable & f is B-measurable implies f is (A\/B)-measurable
by MESFUNC6:17;
theorem
f is A-measurable & g is A-measurable implies f+g is A-measurable
proof
assume that
A1: f is A-measurable and
A2: g is A-measurable;
A3: Im g is A-measurable by A2;
Im f is A-measurable by A1;
then Im f + Im g is A-measurable by A3,MESFUNC6:26;
then
A4: Im(f+g) is A-measurable by Th5;
A5: Re g is A-measurable by A2;
Re f is A-measurable by A1;
then Re f + Re g is A-measurable by A5,MESFUNC6:26;
then Re(f+g) is A-measurable by Th5;
hence thesis by A4;
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;
A4: Im g is A-measurable by A2;
A5: A c= dom Re g by A3,COMSEQ_3:def 3;
A6: Re g is A-measurable by A2;
A7: A c= dom Im g by A3,COMSEQ_3:def 4;
Im f is A-measurable by A1;
then Im f - Im g is A-measurable by A4,A7,MESFUNC6:29;
then
A8: Im(f-g) is A-measurable by Th6;
Re f is A-measurable by A1;
then Re f - Re g is A-measurable by A6,A5,MESFUNC6:29;
then Re(f-g) is A-measurable by Th6;
hence thesis by A8;
end;
theorem
Y c= dom(f+g) implies dom(f|Y+g|Y)=Y & (f+g)|Y = f|Y+g|Y
proof
A1: dom(f+g) = dom f /\ dom g by VALUED_1:def 1;
assume
A2: Y c= dom(f+g);
then
A3: dom((f+g)|Y) = Y by RELAT_1:62;
dom(g|Y) = dom g /\ Y by RELAT_1:61;
then
A4: dom(g|Y) = Y by A2,A1,XBOOLE_1:18,28;
dom(f|Y) = dom f /\ Y by RELAT_1:61;
then
A5: dom(f|Y) = Y by A2,A1,XBOOLE_1:18,28;
then
A6: dom(f|Y+g|Y) = Y /\ Y by A4,VALUED_1:def 1;
now
let x be object;
assume
A7: x in dom((f+g)|Y);
hence ((f+g)|Y).x = (f+g).x by FUNCT_1:47
.=f.x+g.x by A2,A3,A7,VALUED_1:def 1
.=(f|Y).x + g.x by A3,A5,A7,FUNCT_1:47
.=(f|Y).x + (g|Y).x by A3,A4,A7,FUNCT_1:47
.= ((f|Y)+(g|Y)).x by A3,A6,A7,VALUED_1:def 1;
end;
hence thesis by A2,A6,FUNCT_1:2,RELAT_1:62;
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: A = dom Im(f) /\ B by A2,COMSEQ_3:def 4;
Im f is B-measurable by A1;
then (Im f)|B is A-measurable by A3,MESFUNC6:76;
then
A4: Im(f|B) is A-measurable by Th7;
A5: A = dom Re(f) /\ B by A2,COMSEQ_3:def 3;
Re f is B-measurable by A1;
then (Re f)|B is A-measurable by A5,MESFUNC6:76;
then Re(f|B) is A-measurable by Th7;
hence thesis by A4;
end;
theorem
dom f in S & dom g in S implies dom(f+g) in S
proof
assume that
A1: dom f in S and
A2: dom g in S;
reconsider E1 = dom f, E2 = dom g as Element of S by A1,A2;
dom(f+g) = E1 /\ E2 by VALUED_1:def 1;
hence thesis;
end;
theorem
dom f = A implies (f is B-measurable iff f is (A/\B)-measurable)
proof
assume
A1: dom f = A;
then
A2: dom Re f = A by COMSEQ_3:def 3;
A3: dom Im f = A by A1,COMSEQ_3:def 4;
hence f is B-measurable implies f is (A/\B)-measurable by A2,MESFUNC6:80;
thus thesis by A2,A3,MESFUNC6:80;
end;
theorem Th17:
f is A-measurable & A c= dom f implies c(#)f is A-measurable
proof
assume that
A1: f is A-measurable and
A2: A c= dom f;
A3: dom Im f = dom f by COMSEQ_3:def 4;
A4: Im f is A-measurable by A1;
then
A5: Re(c)(#)Im(f) is A-measurable by A2,A3,MESFUNC6:21;
A6: Im(c)(#)Im(f) is A-measurable by A2,A4,A3,MESFUNC6:21;
A7: dom Re f = dom f by COMSEQ_3:def 3;
A8: Re f is A-measurable by A1;
then Im(c)(#)Re(f) is A-measurable by A2,A7,MESFUNC6:21;
then Im(c)(#)Re(f) + Re(c)(#)Im(f) is A-measurable by A5,MESFUNC6:26;
then
A9: Im(c(#)f) is A-measurable by Th3;
dom(Im(c)(#)Im(f)) = dom Im(f) by VALUED_1:def 5;
then
A10: A c= dom(Im(c)(#)Im(f)) by A2,COMSEQ_3:def 4;
Re(c)(#)Re(f) is A-measurable by A2,A8,A7,MESFUNC6:21;
then Re(c)(#)Re(f) - Im(c)(#)Im(f) is A-measurable by A6,A10,MESFUNC6:29;
then Re(c(#)f) is A-measurable by Th3;
hence thesis by A9;
end;
theorem
( ex A be Element of S st dom f = A ) implies for c be Complex,
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;
hereby
let c be Complex, B be Element of S;
A2: dom((Re c)(#)(Re f)) = dom Re f by VALUED_1:def 5;
A3: dom((Im c)(#)(Im f)) = dom Im f by VALUED_1:def 5;
dom(Re(c(#)f)) = dom((Re c)(#)(Re f) - (Im c)(#)(Im f)) by Th3;
then
A4: dom(Re(c(#)f)) = dom((Re c)(#)(Re f)) /\ dom((Im c)(#)(Im f)) by
VALUED_1:12;
A5: dom((Im c)(#)(Re f)) = dom Re f by VALUED_1:def 5;
dom(Im(c(#)f)) = dom((Im c)(#)(Re f) + (Re c)(#)(Im f)) by Th3;
then
A6: dom(Im(c(#)f)) = dom((Im c)(#)(Re f)) /\ dom((Re c)(#)(Im f)) by
VALUED_1:def 1;
A7: dom((Re c)(#)(Im f)) = dom Im f by VALUED_1:def 5;
A8: dom Re f = dom f by COMSEQ_3:def 3;
A9: dom Im f = dom f by COMSEQ_3:def 4;
assume
A10: f is B-measurable;
then Im f is B-measurable;
then
A11: Im f is (A/\B)-measurable by A1,A9,MESFUNC6:80;
Re f is B-measurable by A10;
then Re f is (A/\B)-measurable by A1,A8,MESFUNC6:80;
then f is (A/\B)-measurable by A11;
then
A12: c(#)f is (A/\B)-measurable by A1,Th17,XBOOLE_1:17;
then Im(c(#)f) is (A/\B)-measurable;
then
A13: Im(c(#)f) is B-measurable by A1,A8,A9,A5,A7,A6,MESFUNC6:80;
Re(c(#)f) is (A/\B)-measurable by A12;
then Re(c(#)f) is B-measurable by A1,A8,A9,A2,A3,A4,MESFUNC6:80;
hence c(#)f is B-measurable by A13;
end;
end;
begin :: The Integral of a Complex-valued Measurable Function
definition
let X be non empty set;
let S be SigmaField of X;
let M be sigma_Measure of S;
let f be PartFunc of X,COMPLEX;
pred f is_integrable_on M means
Re f is_integrable_on M & Im f is_integrable_on M;
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,COMPLEX;
assume
A1: f is_integrable_on M;
func Integral(M,f) -> Complex means
:Def3:
ex R,I be Real st R =
Integral(M,Re f) & I = Integral(M,Im f) & it = R+ I*<i>;
existence
proof
A2: Im f is_integrable_on M by A1;
then
A3: -infty < Integral(M,Im f) by MESFUNC6:90;
A4: Re f is_integrable_on M by A1;
then
A5: Integral(M,Re f) < +infty by MESFUNC6:90;
A6: Integral(M,Im f) < +infty by A2,MESFUNC6:90;
-infty < Integral(M,Re f) by A4,MESFUNC6:90;
then reconsider R=Integral(M,Re f), I=Integral(M,Im f)
as Element of REAL by A5,A3,A6,
XXREAL_0:14;
take R + I*<i>;
thus thesis;
end;
uniqueness;
end;
Lm1: for X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f
be PartFunc of X,ExtREAL holds max+f is nonnegative & max-f is nonnegative
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;
A1: for x be object st x in dom max- f holds 0<= (max-f).x by MESFUNC2:13;
for x be object st x in dom max+ f holds 0<= (max+f).x by MESFUNC2:12;
hence thesis by A1,SUPINF_2:52;
end;
theorem Th19:
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,ExtREAL, A be Element of S st (ex E be Element of S st
E = dom f & f is E-measurable) & M.A = 0 holds f|A is_integrable_on M
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f be
PartFunc of X,ExtREAL, A be Element of S;
assume that
A1: ex E be Element of S st E = dom f & f is E-measurable and
A2: M.A = 0;
A3: dom f=dom (max+ f) by MESFUNC2:def 2;
max+f is nonnegative by Lm1;
then integral+(M,(max+ f)|A)=0 by A1,A2,A3,MESFUNC2:25,MESFUNC5:82;
then
A4: integral+(M,max+(f|A)) < +infty by MESFUNC5:28;
consider E be Element of S such that
A5: E = dom f and
A6: f is E-measurable by A1;
A7: dom f /\ (A /\ E) = A /\ E by A5,XBOOLE_1:17,28;
A8: dom f=dom (max- f) by MESFUNC2:def 3;
max-f is nonnegative by Lm1;
then integral+(M,(max- f)|A)=0 by A1,A2,A8,MESFUNC2:26,MESFUNC5:82;
then
A9: integral+(M,max-(f|A)) < +infty by MESFUNC5:28;
A10: dom (f|A) = dom f /\ A by RELAT_1:61;
f is (A/\E)-measurable by A6,MESFUNC1:30,XBOOLE_1:17;
then
A11: f|(A /\ E) is (A/\E)-measurable by A7,MESFUNC5:42;
f|(A /\ E) = f|A /\ f|E by RELAT_1:79
.= f|A /\ f by A5
.= f|A by RELAT_1:59,XBOOLE_1:28;
hence thesis by A5,A11,A10,A4,A9;
end;
theorem Th20:
for X be non empty set, S be SigmaField of X, M be sigma_Measure
of S, f be PartFunc of X,REAL, E,A be Element of S st (ex E be Element of S st
E = dom f & f is E-measurable) & M.A = 0 holds f|A is_integrable_on M
by Th19;
theorem
(ex E be Element of S st E = dom f & f is E-measurable) & M.A = 0
implies f|A is_integrable_on M & Integral(M,f|A) = 0
proof
set g = f|A;
assume that
A1: ex E be Element of S st E = dom f & f is E-measurable and
A2: M.A = 0;
consider E be Element of S such that
A3: E = dom f and
A4: f is E-measurable by A1;
A5: dom Im f = dom f by COMSEQ_3:def 4;
A6: Im f is E-measurable by A4;
then
A7: Integral(M,Im(f)|A)=0 by A2,A3,A5,MESFUNC6:88;
(Im f)|A is_integrable_on M by A2,A3,A6,A5,Th20;
then
A8: Im g is_integrable_on M by Th7;
A9: dom Re f = dom f by COMSEQ_3:def 3;
A10: Im g = (Im f)|A by Th7;
A11: Re f is E-measurable by A4;
A12: Re g = (Re f)|A by Th7;
then reconsider
R=Integral(M,Re g), I=Integral(M,Im g) as Real by A2,A3,A11,A6,A9,A5,A10,
MESFUNC6:88;
(Re f)|A is_integrable_on M by A2,A3,A11,A9,Th20;
then Re g is_integrable_on M by Th7;
hence g is_integrable_on M by A8;
hence Integral(M,g) = R + I * <i> by Def3
.= 0 by A2,A3,A11,A9,A7,A12,A10,MESFUNC6:88;
end;
theorem
E = dom f & f is_integrable_on M & M.A =0 implies Integral(M,f|(E\A))
= Integral(M,f)
proof
assume that
A1: E = dom f and
A2: f is_integrable_on M and
A3: M.A =0;
set C=E\A;
A4: dom f = dom Re f by COMSEQ_3:def 3;
A5: Im f is_integrable_on M by A2;
then R_EAL(Im f) is_integrable_on M;
then consider IE be Element of S such that
A6: IE = dom(R_EAL(Im f)) and
A7: R_EAL(Im f) is IE-measurable;
A8: dom f = dom Im f by COMSEQ_3:def 4;
A9: Integral(M,Im(f)|C) = Integral(M,Im(f|C)) by Th7;
Im f is IE-measurable by A7;
then
A10: Integral(M,Im(f|C)) = Integral(M,Im f) by A1,A3,A8,A6,A9,MESFUNC6:89;
(Im f)|C is_integrable_on M by A5,MESFUNC6:91;
then
A11: Im(f|C) is_integrable_on M by Th7;
then
A12: -infty < Integral(M,Im(f|C)) by MESFUNC6:90;
A13: Re f is_integrable_on M by A2;
then R_EAL(Re f) is_integrable_on M;
then consider RE be Element of S such that
A14: RE = dom(R_EAL(Re f)) and
A15: R_EAL(Re f) is RE-measurable;
A16: Integral(M,Re(f)|C) = Integral(M,Re(f|C)) by Th7;
Re f is RE-measurable by A15;
then
A17: Integral(M,Re(f|C)) = Integral(M,Re f) by A1,A3,A4,A14,A16,MESFUNC6:89;
(Re f)|C is_integrable_on M by A13,MESFUNC6:91;
then
A18: Re(f|C) is_integrable_on M by Th7;
then
A19: Integral(M,Re(f|C)) < +infty by MESFUNC6:90;
A20: Integral(M,Im(f|C)) < +infty by A11,MESFUNC6:90;
-infty < Integral(M,Re(f|C)) by A18,MESFUNC6:90;
then reconsider R2=Integral(M,Re(f|C)), I2=Integral(M,Im(f|C))
as Element of REAL by A19
,A12,A20,XXREAL_0:14;
f|(E\A) is_integrable_on M by A18,A11;
hence Integral(M,f|(E\A)) = R2 + I2 * <i> by Def3
.= Integral(M,f) by A2,A17,A10,Def3;
end;
theorem Th23:
f is_integrable_on M implies f|A is_integrable_on M
proof
assume
A1: f is_integrable_on M;
then Im f is_integrable_on M;
then (Im f)|A is_integrable_on M by MESFUNC6:91;
then
A2: Im(f|A) is_integrable_on M by Th7;
Re f is_integrable_on M by A1;
then (Re f)|A is_integrable_on M by MESFUNC6:91;
then Re(f|A) is_integrable_on M by Th7;
hence thesis by A2;
end;
theorem
f is_integrable_on M & A misses B implies Integral(M,f|(A\/B)) =
Integral(M,f|A) + Integral(M,f|B)
proof
assume that
A1: f is_integrable_on M and
A2: A misses B;
A3: f|B is_integrable_on M by A1,Th23;
then
A4: Re(f|B) is_integrable_on M;
then
A5: Integral(M,Re(f|B)) < +infty by MESFUNC6:90;
A6: Im(f|B) is_integrable_on M by A3;
then
A7: -infty < Integral(M,Im(f|B)) by MESFUNC6:90;
A8: Integral(M,Im(f|B)) < +infty by A6,MESFUNC6:90;
-infty < Integral(M,Re(f|B)) by A4,MESFUNC6:90;
then reconsider R2=Integral(M,Re(f|B)), I2=Integral(M,Im(f|B))
as Element of REAL by A5
,A7,A8,XXREAL_0:14;
A9: f|A is_integrable_on M by A1,Th23;
then
A10: Re(f|A) is_integrable_on M;
then
A11: Integral(M,Re(f|A)) < +infty by MESFUNC6:90;
set C=A\/B;
A12: f|(A\/B) is_integrable_on M by A1,Th23;
then
A13: Re(f|C) is_integrable_on M;
then
A14: Integral(M,Re(f|C)) < +infty by MESFUNC6:90;
A15: Im(f|C) is_integrable_on M by A12;
then
A16: -infty < Integral(M,Im(f|C)) by MESFUNC6:90;
A17: Integral(M,Im(f|C)) < +infty by A15,MESFUNC6:90;
-infty < Integral(M,Re(f|C)) by A13,MESFUNC6:90;
then reconsider R3=Integral(M,Re(f|C)), I3=Integral(M,Im(f|C))
as Element of REAL
by A14,A16,A17,XXREAL_0:14;
A18: Integral(M,f|(A\/B)) = R3 + I3 * <i> by A12,Def3;
A19: Im(f|A) is_integrable_on M by A9;
then
A20: -infty < Integral(M,Im(f|A)) by MESFUNC6:90;
A21: Integral(M,Im(f|A)) < +infty by A19,MESFUNC6:90;
-infty < Integral(M,Re(f|A)) by A10,MESFUNC6:90;
then reconsider R1=Integral(M,Re(f|A)), I1=Integral(M,Im(f|A))
as Element of REAL by A11
,A20,A21,XXREAL_0:14;
Im f is_integrable_on M by A1;
then
Integral(M,(Im f)|(A\/B)) = Integral(M,(Im f)|A) + Integral(M,(Im f)|B)
by A2,MESFUNC6:92;
then Integral(M,Im(f)|C) = Integral(M,Im(f|A)) + Integral(M,Im(f)|B) by Th7
.= Integral(M,Im(f|A)) + Integral(M,Im(f|B)) by Th7;
then I3 = I1 + (I2 qua ExtReal) by Th7;
then
A22: I3 = I1 + I2;
Re f is_integrable_on M by A1;
then
Integral(M,(Re f)|(A\/B)) = Integral(M,(Re f)|A) + Integral(M,(Re f)|B)
by A2,MESFUNC6:92;
then Integral(M,Re(f)|C) = Integral(M,Re(f|A)) + Integral(M,Re(f)|B) by Th7
.= Integral(M,Re(f|A)) + Integral(M,Re(f|B)) by Th7;
then R3 = R1 + (R2 qua ExtReal) by Th7;
then R3 = R1 + R2;
then Integral(M,f|(A\/B)) = (R1 + I1 * <i>) + (R2 + I2 * <i>) by A22,A18;
then Integral(M,f|(A\/B)) = Integral(M,f|A) + (R2 + I2 * <i>) by A9,Def3;
hence thesis by A3,Def3;
end;
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)
proof
assume that
A1: f is_integrable_on M and
A2: B = (dom f)\A;
A3: Re f is_integrable_on M by A1;
then
A4: Integral(M,Re f) < +infty by MESFUNC6:90;
A5: Im f is_integrable_on M by A1;
then
A6: -infty < Integral(M,Im f) by MESFUNC6:90;
A7: Integral(M,Im f) < +infty by A5,MESFUNC6:90;
-infty < Integral(M,Re f) by A3,MESFUNC6:90;
then reconsider R=Integral(M,Re f), I=Integral(M,Im f)
as Element of REAL by A4,A6,A7,
XXREAL_0:14;
A8: Integral(M,f) = R + I * <i> by A1,Def3;
A9: f|B is_integrable_on M by A1,Th23;
then
A10: Re(f|B) is_integrable_on M;
then
A11: Integral(M,Re(f|B)) < +infty by MESFUNC6:90;
A12: Im(f|B) is_integrable_on M by A9;
then
A13: -infty < Integral(M,Im(f|B)) by MESFUNC6:90;
A14: Integral(M,Im(f|B)) < +infty by A12,MESFUNC6:90;
-infty < Integral(M,Re(f|B)) by A10,MESFUNC6:90;
then reconsider R2=Integral(M,Re(f|B)), I2=Integral(M,Im(f|B))
as Element of REAL by A11
,A13,A14,XXREAL_0:14;
A15: f|A is_integrable_on M by A1,Th23;
then
A16: Re(f|A) is_integrable_on M;
then
A17: Integral(M,Re(f|A)) < +infty by MESFUNC6:90;
A18: Im(f|A) is_integrable_on M by A15;
then
A19: -infty < Integral(M,Im(f|A)) by MESFUNC6:90;
A20: Integral(M,Im(f|A)) < +infty by A18,MESFUNC6:90;
-infty < Integral(M,Re(f|A)) by A16,MESFUNC6:90;
then reconsider R1=Integral(M,Re(f|A)), I1=Integral(M,Im(f|A))
as Element of REAL by A17
,A19,A20,XXREAL_0:14;
dom f = dom Im f by COMSEQ_3:def 4;
then Integral(M,Im(f)) = Integral(M,Im(f)|A)+Integral(M,Im(f)|B) by A2,A5,
MESFUNC6:93;
then Integral(M,Im f) = Integral(M,Im(f|A)) + Integral(M,Im(f)|B) by Th7
.= Integral(M,Im(f|A)) + Integral(M,Im(f|B)) by Th7;
then
A21: I = I1 + I2 by SUPINF_2:1;
dom f = dom Re f by COMSEQ_3:def 3;
then Integral(M,Re(f)) = Integral(M,Re(f)|A)+Integral(M,Re(f)|B) by A2,A3,
MESFUNC6:93;
then Integral(M,Re f) = Integral(M,Re(f|A)) + Integral(M,Re(f)|B) by Th7
.= Integral(M,Re(f|A)) + Integral(M,Re(f|B)) by Th7;
then R = R1 + R2 by SUPINF_2:1;
then Integral(M,f) = (R1 + I1 * <i>) + (R2 + I2 * <i>) by A21,A8;
then Integral(M,f) = Integral(M,f|A) + (R2 + I2 * <i>) by A15,Def3;
hence thesis by A1,A9,Def3,Th23;
end;
definition
let k be Real, X be non empty set, f be PartFunc of X,REAL;
func f to_power k -> PartFunc of X,REAL means
:Def4:
dom it = dom f & for x
be Element of X st x in dom it holds it.x = (f.x) to_power k;
existence
proof
defpred P[set,set] means $1 in dom f & $2= (f.$1) to_power k;
consider F be PartFunc of X,REAL such that
A1: for z be Element of X holds z in dom F iff ex c be Element of REAL
st P[z,c] and
A2: for z be Element of X st z in dom F holds P[z,F.z] from SEQ_1:sch
2;
take F;
now
let z be Element of X;
hereby
A3: (f.z) to_power k is Element of REAL by XREAL_0:def 1;
assume z in dom f;
hence z in dom F by A1,A3;
end;
hereby
assume z in dom F;
then ex c be Element of REAL st P[z,c] by A1;
hence z in dom f;
end;
end;
hence dom F = dom f by SUBSET_1:3;
thus thesis by A2;
end;
uniqueness
proof
deffunc f0(set) = (f.$1) to_power k;
thus for h,g being PartFunc of X,REAL st (dom h=dom f & for z be Element
of X st z in dom h holds h.z = f0(z)) & (dom g=dom f & for z be Element of X st
z in dom g holds g.z = f0(z)) holds h = g from SEQ_1:sch 4;
end;
end;
registration
let X;
cluster nonnegative for PartFunc of X,REAL;
existence
proof
reconsider f = {} as Function;
reconsider f as PartFunc of X,REAL by RELSET_1:12;
take f;
let x be ExtReal;
thus thesis;
end;
end;
registration
let k be non negative Real, X;
let f be nonnegative PartFunc of X,REAL;
cluster f to_power k -> nonnegative;
coherence
proof
now
let x be object;
assume
A1: x in dom (f to_power k);
per cases;
suppose
k = 0;
then (f.x) to_power k = 1 by POWER:24;
hence 0 <= (f to_power k).x by A1,Def4;
end;
suppose
A2: k > 0;
per cases by MESFUNC6:51;
suppose
0 < f.x;
then 0 < (f.x) to_power k by POWER:34;
hence 0 <= (f to_power k).x by A1,Def4;
end;
suppose
0 = f.x;
then 0 = ((f.x) to_power k) by A2,POWER:def 2;
hence 0 <= (f to_power k).x by A1,Def4;
end;
end;
end;
hence thesis by MESFUNC6:52;
end;
end;
theorem Th26:
for k be Real, X,S,E for f be PartFunc of X,REAL st f is
nonnegative & 0 <= k holds (f to_power k) is nonnegative;
theorem Th27:
for x be object,X,S,E for f be PartFunc of X,REAL st f is
nonnegative holds (f.x) to_power (1/2) = sqrt(f.x)
proof
let x be object,X,S,E;
let f be PartFunc of X,REAL;
assume f is nonnegative;
then
A1: 0 <= f.x by MESFUNC6:51;
hence (f.x) to_power (1/2) = 2-root (f.x) by POWER:45
.= 2 -Root (f.x) by A1,POWER:def 1
.= sqrt (f.x) by A1,PREPOWER:32;
end;
theorem Th28:
for f be PartFunc of X,REAL, a be Real st A c= dom f holds A /\
less_dom(f,a) = A\(A /\ great_eq_dom(f,a))
proof
let f be PartFunc of X,REAL, a be Real;
now
let x be object;
assume
A1: x in A /\ less_dom(f,a);
then x in less_dom(f,a) by XBOOLE_0:def 4;
then ex y be Real st y = f.x & y < a by MESFUNC6:3;
then not (ex y1 be Real st y1 = f.x & a <= y1);
then not x in great_eq_dom(f,a) by MESFUNC6:6;
then
A2: not x in (A /\ great_eq_dom(f,a)) by XBOOLE_0:def 4;
x in A by A1,XBOOLE_0:def 4;
hence x in A\(A /\ great_eq_dom(f,a)) by A2,XBOOLE_0:def 5;
end;
then
A3: A /\ less_dom(f,a) c= A\(A /\ great_eq_dom(f,a)) by TARSKI:def 3;
assume
A4: A c= dom f;
now
let x be object;
assume
A5: x in A\(A /\ great_eq_dom(f,a));
then
A6: x in A by XBOOLE_0:def 5;
not x in A /\ great_eq_dom(f,a) by A5,XBOOLE_0:def 5;
then not x in great_eq_dom(f,a) by A6,XBOOLE_0:def 4;
then not a <= f.x by A4,A6,MESFUNC6:6;
then x in less_dom(f,a) by A4,A6,MESFUNC6:3;
hence x in A /\ less_dom(f,a) by A6,XBOOLE_0:def 4;
end;
then A\(A /\ great_eq_dom(f,a)) c= A /\ less_dom(f,a) by TARSKI:def 3;
hence thesis by A3,XBOOLE_0:def 10;
end;
reconsider jj=1 as Real;
theorem Th29:
for k be Real, X,S,E for f be PartFunc of X,REAL st f is
nonnegative & 0 <= k & E c= dom f & f is E-measurable holds (f to_power k)
is E-measurable
proof
let k be Real, X,S,E;
let f be PartFunc of X,REAL;
reconsider k1=k as Real;
assume that
A1: f is nonnegative and
A2: 0 <= k and
A3: E c= dom f and
A4: f is E-measurable;
A5: dom(f to_power k) = dom f by Def4;
per cases by A2;
suppose
A6: k = 0;
A7: E c= dom (f to_power k) by A3,Def4;
now
let r be Real;
reconsider r1=r as Real;
per cases;
suppose
A8: r <= 1;
now
let x be object;
assume
A9: x in E;
then (f to_power k).x = (f.x) to_power k by A3,A5,Def4;
then r <= (f to_power k).x by A6,A8,POWER:24;
hence x in great_eq_dom(f to_power k,r1) by A3,A5,A9,MESFUNC6:6;
end;
then E c= great_eq_dom(f to_power k,r) by TARSKI:def 3;
then E /\ great_eq_dom(f to_power k,r) = E by XBOOLE_1:28;
then E /\ less_dom(f to_power k,r1) = E \ E by A7,Th28;
hence E /\ less_dom(f to_power k,r) in S;
end;
suppose
A10: 1 < r;
now
let x be object;
assume
A11: x in E;
then (f to_power k).x = (f.x) to_power k by A3,A5,Def4;
then (f to_power k).x < r by A6,A10,POWER:24;
hence x in less_dom(f to_power k,r) by A3,A5,A11,MESFUNC6:3;
end;
then E c= less_dom(f to_power k,r) by TARSKI:def 3;
then E /\ less_dom(f to_power k,r) = E by XBOOLE_1:28;
hence E /\ less_dom(f to_power k,r) in S;
end;
end;
hence thesis by MESFUNC6:12;
end;
suppose
A12: k > 0;
for r be Real holds E /\ great_eq_dom(f to_power k,r) in S
proof
let r be Real;
reconsider r1=r as Real;
per cases;
suppose
A13: r1 <= 0;
now
let x be object;
assume x in E;
then x in dom f by A3;
then
A14: x in dom (f to_power k) by Def4;
0 <= (f to_power k).x by A1,A12,MESFUNC6:51;
hence x in great_eq_dom(f to_power k,r1) by A13,A14,MESFUNC6:6;
end;
then E c= great_eq_dom(f to_power k,r) by TARSKI:def 3;
then E /\ great_eq_dom(f to_power k,r) = E by XBOOLE_1:28;
hence thesis;
end;
suppose
A15: 0 < r1;
A16: now
set R = r to_power (jj/k);
let x be object;
reconsider xx=x as set by TARSKI:1;
A17: 0 < r to_power (jj/k) by A15,POWER:34;
assume
A18: x in great_eq_dom(f,r1 to_power (1/k));
then
A19: x in dom (f to_power k) by A5,MESFUNC6:6;
R to_power k = r to_power (1/k*k) by A15,POWER:33;
then
A20: R to_power k = r to_power 1 by A12,XCMPLX_1:87;
ex y be Real st y = f.x & r1 to_power (1/k) <= y
by A18,MESFUNC6:6;
then r1 to_power jj <= (f.xx) to_power k1
by A12,A17,A20,HOLDER_1:3;
then r <= (f.xx) to_power k by POWER:25;
then r <= (f to_power k).xx by A19,Def4;
hence x in great_eq_dom(f to_power k,r1) by A19,MESFUNC6:6;
end;
now
let x be object;
reconsider xx=x as set by TARSKI:1;
assume
A21: x in great_eq_dom(f to_power k,r1);
then
A22: x in dom (f to_power k) by MESFUNC6:6;
0 <= f.xx by A1,MESFUNC6:51;
then
((f.xx) to_power k1) to_power (1/k1) = (f.xx) to_power (k1 * 1/k1
) by A12,HOLDER_1:2;
then ((f.xx) to_power k1) to_power (1/k1) = (f.xx) to_power 1 by A12,
XCMPLX_1:87;
then
A23: ((f.xx) to_power k) to_power (1/k) = f.x by POWER:25;
ex y2 be Real st y2 = (f to_power k).x & r1 <= y2
by A21,MESFUNC6:6;
then r <= (f.xx) to_power k by A22,Def4;
then
r to_power (1/k1) <= ((f.xx) to_power k1) to_power (1/k1) by A12,A15,
HOLDER_1:3;
hence x in great_eq_dom(f,r1 to_power (1/k)) by A5,A22,A23,MESFUNC6:6
;
end;
then E /\ great_eq_dom(f to_power k,r1) = E /\ great_eq_dom(f,r1
to_power (1/k)) by A16,TARSKI:2;
hence thesis by A3,A4,MESFUNC6:13;
end;
end;
hence thesis by A3,A5,MESFUNC6:13;
end;
end;
theorem Th30:
f is A-measurable & A c= dom f implies |.f.| is A-measurable
proof
assume that
A1: f is A-measurable and
A2: A c= dom f;
A3: dom Im f = dom f by COMSEQ_3:def 4;
A4: now
let x be object;
assume x in dom |.Im f.|;
then |.Im f.|.x = |.(Im f).x qua Complex .| by VALUED_1:def 11;
hence 0 <= |.Im f.|.x by COMPLEX1:46;
end;
then
A5: |.Im f.| to_power 2 is nonnegative by Th26,MESFUNC6:52;
A6: dom |.Im f.| = dom Im f by VALUED_1:def 11;
then
A7: dom(|.Im f.| to_power 2) = dom f by A3,Def4;
Im f is A-measurable by A1;
then |.Im f.| is A-measurable by A2,A3,MESFUNC6:48;
then
A8: |.Im f.| to_power 2 is A-measurable by A2,A6,A3,A4,Th29,MESFUNC6:52;
A9: dom Re f = dom f by COMSEQ_3:def 3;
A10: now
let x be object;
A11: 0 <= |.(Re f).x qua Complex .| by COMPLEX1:46;
assume x in dom |.Re f.|;
hence 0 <= |. Re f.|.x by A11,VALUED_1:def 11;
end;
then
A12: |.Re(f).| to_power 2 is nonnegative by Th26,MESFUNC6:52;
set F = |.Re f.| to_power 2 + |.Im f.| to_power 2;
A13: dom |.f.| = dom f by VALUED_1:def 11;
A14: dom |.Re f.| = dom Re f by VALUED_1:def 11;
then
A15: dom(|.Re f.| to_power 2) = dom f by A9,Def4;
A16: dom F = dom( |.Re f.| to_power 2 ) /\ dom( |.Im f.| to_power 2 ) by
VALUED_1:def 1;
then
A17: dom(|.f.|) = dom (F to_power (1/2)) by A13,A15,A7,Def4;
now
let x be object;
assume
A18: x in dom |.f.|;
then (|.Re f.| to_power 2).x = (|.Re f.|.x) to_power 2 by A13,A15,Def4;
then (|.Re f.| to_power 2).x
= |.Re(f).x qua Complex .| to_power 2 by A14,A13,A9,A18,
VALUED_1:def 11;
then (|.Re f.| to_power 2).x =
|.Re(f.x) qua Complex.| to_power 2 by A13,A9,A18,
COMSEQ_3:def 3;
then (|.Re f.| to_power 2).x = |.Re(f.x) qua Complex.|^2 by POWER:46;
then
A19: (|.Re f.| to_power 2).x = (Re(f.x))^2 by COMPLEX1:75;
(|.Im f.| to_power 2).x = (|.Im f.|.x) to_power 2 by A13,A7,A18,Def4;
then (|.Im f.| to_power 2).x
= |.Im(f).x qua Complex .| to_power 2 by A6,A13,A3,A18,
VALUED_1:def 11;
then (|.Im f.| to_power 2).x
= |.Im(f.x) qua Complex.| to_power 2 by A13,A3,A18,
COMSEQ_3:def 4;
then (|.Im f.| to_power 2).x = |.Im(f.x) qua Complex.|^2 by POWER:46;
then
A20: (|.Im f.| to_power 2).x = (Im(f.x))^2 by COMPLEX1:75;
(F.x) to_power (1/2) = sqrt (F.x) by A12,A5,Th27,MESFUNC6:56
.= sqrt ( (Re(f.x))^2 + (Im(f.x))^2 ) by A13,A16,A15,A7,A18,A19,A20,
VALUED_1:def 1;
then (F to_power (1/2)).x = |.f.x .| by A17,A18,Def4;
hence |.f.|.x = (F to_power (1/2)).x by A18,VALUED_1:def 11;
end;
then
A21: |.f.| = F to_power (1/2) by A17,FUNCT_1:2;
Re f is A-measurable by A1;
then |.Re f.| is A-measurable by A2,A9,MESFUNC6:48;
then |.Re f.| to_power 2 is A-measurable by A2,A14,A9,A10,Th29,MESFUNC6:52
;
then F is A-measurable by A8,MESFUNC6:26;
hence thesis by A2,A12,A5,A16,A15,A7,A21,Th29,MESFUNC6:56;
end;
theorem Th31:
(ex A be Element of S st A = dom f & f is A-measurable )
implies (f is_integrable_on M iff |.f.| is_integrable_on M)
proof
A1: dom (|.Re f.| + |.Im f.|) = dom |.Re f.| /\ dom |.Im f.| by VALUED_1:def 1;
A2: dom |.Re f.| = dom Re f by VALUED_1:def 11;
A3: dom |.Im f.| = dom Im f by VALUED_1:def 11;
A4: dom |.f.| = dom f by VALUED_1:def 11;
assume ex A be Element of S st A = dom f & f is A-measurable;
then consider A be Element of S such that
A5: A = dom f and
A6: f is A-measurable;
A7: dom Re f = A by A5,COMSEQ_3:def 3;
A8: Im f is A-measurable by A6;
A9: Re f is A-measurable by A6;
A10: dom Im f = A by A5,COMSEQ_3:def 4;
A11: |.f.| is A-measurable by A5,A6,Th30;
hereby
A12: now
let x be Element of X;
assume
A13: x in dom |.f.|;
then
A14: |.f.|.x = |.f.x .| by VALUED_1:def 11;
A15: |.(Im f).x qua Complex .| = |.Im f.|.x
by A5,A10,A3,A4,A13,VALUED_1:def 11;
A16: |.(Re f).x qua Complex .| = |.Re f.|.x
by A5,A7,A2,A4,A13,VALUED_1:def 11;
A17: (Im f).x = Im(f.x) by A5,A10,A4,A13,COMSEQ_3:def 4;
A18: (Re f).x = Re(f.x) by A5,A7,A4,A13,COMSEQ_3:def 3;
(|.Re f.| + |.Im f.|).x = |.Re f.|.x + |.Im f.|.x by A5,A7,A10,A1,A2,A3
,A4,A13,VALUED_1:def 1;
hence |.(|.f.|.x qua Complex).|
<= (|.Re f.| + |.Im f.|).x by A18,A17,A14,A16,A15,
COMPLEX1:78;
end;
assume
A19: f is_integrable_on M;
then Im f is_integrable_on M;
then
A20: |.Im f.| is_integrable_on M by A10,A8,MESFUNC6:94;
Re f is_integrable_on M by A19;
then |.Re f.| is_integrable_on M by A7,A9,MESFUNC6:94;
then |.Re f.| + |.Im f.| is_integrable_on M by A20,MESFUNC6:100;
hence |.f.| is_integrable_on M by A5,A7,A10,A1,A2,A3,A4,A11,A12,MESFUNC6:96
;
end;
hereby
assume
A21: |.f.| is_integrable_on M;
now
let x be Element of X;
A22: |.Im(f.x) qua Complex.| <= |.f.x.| by COMPLEX1:79;
assume
A23: x in dom Im f;
then |.f.|.x = |.f.x .| by A5,A10,A4,VALUED_1:def 11;
hence |.Im(f).x qua Complex .| <= |.f.|.x
by A23,A22,COMSEQ_3:def 4;
end;
then
A24: Im f is_integrable_on M by A5,A10,A8,A4,A21,MESFUNC6:96;
now
let x be Element of X;
A25: |.Re(f.x) qua Complex.| <= |.f.x .| by COMPLEX1:79;
assume
A26: x in dom Re f;
then |.f.|.x = |.f.x .| by A5,A7,A4,VALUED_1:def 11;
hence |.Re(f).x qua Complex .| <= |.f.|.x
by A26,A25,COMSEQ_3:def 3;
end;
then Re f is_integrable_on M by A5,A7,A9,A4,A21,MESFUNC6:96;
hence f is_integrable_on M by A24;
end;
end;
theorem
f is_integrable_on M & g is_integrable_on M implies dom (f+g) in S
proof
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M;
A3: Re g is_integrable_on M by A2;
A4: Im g is_integrable_on M by A2;
Im f is_integrable_on M by A1;
then dom(Im(f)+Im(g)) in S by A4,MESFUNC6:99;
then
A5: dom(Im(f+g)) in S by Th5;
Re f is_integrable_on M by A1;
then dom(Re(f)+Re(g)) in S by A3,MESFUNC6:99;
then
A6: dom(Re(f+g)) in S by Th5;
dom(<i>(#)Im(f+g)) = dom(Im(f+g)) by VALUED_1:def 5;
then dom(Re(f+g) + <i>(#)Im(f+g)) = dom(Re(f+g)) /\ dom(Im(f+g)) by
VALUED_1:def 1;
then dom(Re(f+g) + <i>(#)Im(f+g)) in S by A6,A5,FINSUB_1:def 2;
hence thesis by Th8;
end;
theorem Th33:
f is_integrable_on M & g is_integrable_on M implies f+g is_integrable_on M
proof
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M;
A3: Im g is_integrable_on M by A2;
Im f is_integrable_on M by A1;
then Im(f)+ Im(g) is_integrable_on M by A3,MESFUNC6:100;
then
A4: Im(f+g) is_integrable_on M by Th5;
A5: Re g is_integrable_on M by A2;
Re f is_integrable_on M by A1;
then Re(f)+ Re(g) is_integrable_on M by A5,MESFUNC6:100;
then Re(f+g) is_integrable_on M by Th5;
hence thesis by A4;
end;
theorem Th34:
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_integrable_on M & g is_integrable_on M
holds f-g is_integrable_on M
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;
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M;
R_EAL g is_integrable_on M by A2;
then (-jj)(#)R_EAL g is_integrable_on M by MESFUNC5:110;
then -R_EAL g is_integrable_on M by MESFUNC2:9;
then
A3: R_EAL -g is_integrable_on M by MESFUNC6:28;
R_EAL f is_integrable_on M by A1;
then R_EAL f + R_EAL -g is_integrable_on M by A3,MESFUNC5:108;
then R_EAL(f-g) is_integrable_on M by MESFUNC6:23;
hence thesis;
end;
theorem
f is_integrable_on M & g is_integrable_on M implies f-g is_integrable_on M
proof
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M;
A3: Im g is_integrable_on M by A2;
Im f is_integrable_on M by A1;
then Im(f)- Im(g) is_integrable_on M by A3,Th34;
then
A4: Im(f-g) is_integrable_on M by Th6;
A5: Re g is_integrable_on M by A2;
Re f is_integrable_on M by A1;
then Re(f)- Re(g) is_integrable_on M by A5,Th34;
then Re(f-g) is_integrable_on M by Th6;
hence thesis by A4;
end;
theorem Th36:
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 that
A1: f is_integrable_on M and
A2: g is_integrable_on M;
A3: Re g is_integrable_on M by A2;
Re f is_integrable_on M by A1;
then consider E be Element of S such that
A4: E = dom Re f /\ dom Re g and
A5: Integral(M,Re(f)+Re(g))=Integral(M,(Re f)|E)+Integral(M,(Re g)|E) by A3,
MESFUNC6:101;
A6: f|E is_integrable_on M by A1,Th23;
then
A7: Re(f|E) is_integrable_on M;
then
A8: Integral(M,Re(f|E)) < +infty by MESFUNC6:90;
A9: Im(f|E) is_integrable_on M by A6;
then
A10: -infty < Integral(M,Im(f|E)) by MESFUNC6:90;
A11: Integral(M,Im(f|E)) < +infty by A9,MESFUNC6:90;
-infty < Integral(M,Re(f|E)) by A7,MESFUNC6:90;
then reconsider R1=Integral(M,Re(f|E)), I1=Integral(M,Im(f|E))
as Element of REAL by A8
,A10,A11,XXREAL_0:14;
A12: dom f = dom Re f by COMSEQ_3:def 3;
A13: Im g is_integrable_on M by A2;
Im f is_integrable_on M by A1;
then
A14: ex Ei be Element of S st Ei = dom Im f /\ dom Im g & Integral(M,Im(f)+Im
(g))=Integral(M,Im(f)|Ei)+Integral(M,Im(g)|Ei) by A13,MESFUNC6:101;
A15: Integral(M,Im(f)+Im(g)) = Integral(M,Im(f+g)) by Th5;
A16: f+g is_integrable_on M by A1,A2,Th33;
then
A17: Re(f+g) is_integrable_on M;
then
A18: Integral(M,Re(f+g)) < +infty by MESFUNC6:90;
A19: Im(f+g) is_integrable_on M by A16;
then
A20: -infty < Integral(M,Im(f+g)) by MESFUNC6:90;
A21: Integral(M,Im(f+g)) < +infty by A19,MESFUNC6:90;
-infty < Integral(M,Re(f+g)) by A17,MESFUNC6:90;
then reconsider R=Integral(M,Re(f+g)), I=Integral(M,Im(f+g))
as Element of REAL by A18
,A20,A21,XXREAL_0:14;
A22: Integral(M,f+g) = R + I * <i> by A16,Def3;
A23: dom g = dom Im g by COMSEQ_3:def 4;
A24: g|E is_integrable_on M by A2,Th23;
then
A25: Re(g|E) is_integrable_on M;
then
A26: Integral(M,Re(g|E)) < +infty by MESFUNC6:90;
A27: Im(g|E) is_integrable_on M by A24;
then
A28: -infty < Integral(M,Im(g|E)) by MESFUNC6:90;
A29: Integral(M,Im(g|E)) < +infty by A27,MESFUNC6:90;
-infty < Integral(M,Re(g|E)) by A25,MESFUNC6:90;
then reconsider R2=Integral(M,Re(g|E)), I2=Integral(M,Im(g|E))
as Element of REAL by A26
,A28,A29,XXREAL_0:14;
A30: dom g = dom Re g by COMSEQ_3:def 3;
Integral(M,Re(f)+Re(g)) = Integral(M,Re(f+g)) by Th5;
then Integral(M,Re(f+g)) = Integral(M,Re(f|E)) + Integral(M,Re(g)|E) by A5
,Th7
.= Integral(M,Re(f|E)) + Integral(M,Re(g|E)) by Th7;
then
A31: R = R1 + R2 by SUPINF_2:1;
dom f = dom Im f by COMSEQ_3:def 4;
then Integral(M,Im(f+g)) = Integral(M,Im(f|E)) + Integral(M,Im(g)|E) by A4
,A12,A30,A23,A14,A15,Th7;
then I = I1 + (I2 qua ExtReal) by Th7;
then I = I1 + I2;
then Integral(M,f+g) = (R1 + I1 * <i>) + (R2 + I2 * <i>) by A31,A22;
then Integral(M,f+g) = Integral(M,f|E) + (R2 + I2 * <i>) by A6,Def3;
then Integral(M,f+g) = Integral(M,f|E)+Integral(M,g|E) by A24,Def3;
hence thesis by A4,A12,A30;
end;
theorem
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_integrable_on M & g is_integrable_on M holds
ex E be Element of S st E = dom f /\ dom g & Integral(M,f-g)=Integral(M,f|E)+
Integral(M,(-g)|E)
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;
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M;
R_EAL g is_integrable_on M by A2;
then (-jj)(#)R_EAL g is_integrable_on M by MESFUNC5:110;
then -R_EAL g is_integrable_on M by MESFUNC2:9;
then
A3: R_EAL -g is_integrable_on M by MESFUNC6:28;
R_EAL f is_integrable_on M by A1;
then consider E be Element of S such that
A4: E = dom(R_EAL f) /\ dom(R_EAL -g) and
A5: Integral(M,R_EAL f + R_EAL -g) = Integral(M,(R_EAL f)|E) + Integral(
M,(R_EAL -g)|E) by A3,MESFUNC5:109;
take E;
dom(R_EAL -g) = dom(-R_EAL g) by MESFUNC6:28;
hence thesis by A4,A5,MESFUNC1:def 7,MESFUNC6:23;
end;
theorem Th38:
f is_integrable_on M implies r(#)f is_integrable_on M & Integral
(M,r(#)f) = r * Integral(M,f)
proof
A1: Integral(M,r(#)Re(f)) = Integral(M,Re(r(#)f)) by Th2;
A2: Integral(M,r(#)Im(f)) = Integral(M,Im(r(#)f)) by Th2;
assume
A3: f is_integrable_on M;
then
A4: Re f is_integrable_on M;
then
A5: Integral(M,Re f) < +infty by MESFUNC6:90;
r(#)Re(f) is_integrable_on M by A4,MESFUNC6:102;
then
A6: Re(r(#)f) is_integrable_on M by Th2;
then
A7: Integral(M,Re(r(#)f)) < +infty by MESFUNC6:90;
A8: Im f is_integrable_on M by A3;
then
A9: -infty < Integral(M,Im f) by MESFUNC6:90;
A10: Integral(M,Im f) < +infty by A8,MESFUNC6:90;
-infty < Integral(M,Re f) by A4,MESFUNC6:90;
then reconsider R1=Integral(M,Re f), I1=Integral(M,Im f)
as Element of REAL by A5,A9,A10
,XXREAL_0:14;
A11: (r qua ExtReal) * R1 = r * R1;
A12: (r qua ExtReal) * I1 = r * I1;
r(#)Im(f) is_integrable_on M by A8,MESFUNC6:102;
then
A13: Im(r(#)f) is_integrable_on M by Th2;
then
A14: -infty < Integral(M,Im(r(#)f)) by MESFUNC6:90;
A15: Integral(M,Im(r(#)f)) < +infty by A13,MESFUNC6:90;
-infty < Integral(M,Re(r(#)f)) by A6,MESFUNC6:90;
then reconsider
R2=Integral(M,Re(r(#)f)), I2=Integral(M,Im(r(#)f))
as Element of REAL by A7,A14,A15,
XXREAL_0:14;
A16: Integral(M,r(#)Im(f)) = r * Integral(M,Im f) by A8,MESFUNC6:102;
A17: r(#)f is_integrable_on M by A6,A13;
Integral(M,r(#)Re(f))
= (r qua ExtReal) * Integral(M,Re f) by A4,MESFUNC6:102;
then R2 + I2 * <i> = r * (R1 + I1 * <i>) by A16,A1,A2,A11,A12;
then Integral(M,r(#)f) = r * (R1 + I1 * <i>) by A17,Def3;
hence thesis by A3,A6,A13,Def3;
end;
theorem Th39:
f is_integrable_on M implies <i>(#)f is_integrable_on M &
Integral(M,<i>(#)f) = <i> * Integral(M,f)
proof
A1: Re(<i>(#)f) = -Im(f) by Th4;
assume
A2: f is_integrable_on M;
then
A3: Im f is_integrable_on M;
A4: Im(<i>(#)f)= Re f by Th4;
then
A5: Im(<i>(#)f) is_integrable_on M by A2;
Re(<i>(#)f) is_integrable_on M by A3,A1,MESFUNC6:102;
hence <i>(#)f is_integrable_on M by A5;
then consider R1,I1 be Real such that
A6: R1=Integral(M,Re(<i>(#)f)) and
A7: I1 =Integral(M,Im(<i>(#)f)) and
A8: Integral(M,<i>(#)f)=R1+ I1 * <i> by Def3;
consider R,I be Real such that
A9: R=Integral(M,Re f) and
A10: I =Integral(M,Im f) and
A11: Integral(M,f)=R+ I * <i> by A2,Def3;
R1 = (-1) * (I qua ExtReal) by A3,A1,A10,A6,MESFUNC6:102
.=(-1)*I;
hence thesis by A4,A9,A11,A7,A8;
end;
theorem Th40:
f is_integrable_on M implies c(#)f is_integrable_on M & Integral
(M,c(#)f) = c * Integral(M,f)
proof
A1: c = Re(c) + Im(c) * <i> by COMPLEX1:13;
A2: dom(<i>(#)f) = dom f by VALUED_1:def 5;
assume
A3: f is_integrable_on M;
then
A4: Integral(M,(Re c)(#)f) = Re c * Integral(M,f) by Th38;
A5: <i>(#)f is_integrable_on M by A3,Th39;
then
A6: (Im c)(#)(<i>(#)f) is_integrable_on M by Th38;
A7: (Re c)(#)f is_integrable_on M by A3,Th38;
then consider E be Element of S such that
A8: E = dom ((Re c)(#)f) /\ dom ((Im c)(#)(<i>(#)f)) and
A9: Integral(M,(Re c)(#)f + (Im c)(#)(<i>(#)f)) = Integral(M,((Re c)(#)
f)|E) + Integral(M,((Im c)(#)(<i>(#)f))|E) by A6,Th36;
A10: dom(c(#)f) = dom f by VALUED_1:def 5;
A11: Integral(M,(Im c)(#)(<i>(#)f)) = Im c * Integral(M,<i>(#)f) by A5,Th38;
A12: dom(Re(c)(#)f) = dom f by VALUED_1:def 5;
A13: dom((Im c)(#)(<i>(#)f)) = dom(<i>(#)f) by VALUED_1:def 5;
A14: dom((Re c)(#)f + (Im c)(#)(<i>(#)f)) = dom((Re c)(#)f) /\ dom((Im c)(#)(
<i>(#)f)) by VALUED_1:def 1;
now
let x be Element of X;
assume
A15: x in dom(c(#)f);
then
A16: (c(#)f).x = c * f.x by VALUED_1:def 5;
A17: ((Im c)(#)(<i>(#)f)).x = Im c * (<i>(#)f).x by A10,A2,A13,A15,
VALUED_1:def 5;
A18: ((Re c)(#)f).x= Re c * f.x by A10,A12,A15,VALUED_1:def 5;
A19: (<i>(#)f).x = <i> * f.x by A10,A2,A15,VALUED_1:def 5;
((Re c)(#)f + (Im c)(#)(<i>(#)f)).x = ((Re c)(#)f).x + ((Im c)(#)(<i>
(#) f)).x by A10,A12,A2,A13,A14,A15,VALUED_1:def 1;
hence (c(#)f).x = ((Re c)(#)f + (Im c)(#)(<i>(#)f)).x by A1,A16,A18,A17,A19
;
end;
then
A20: c(#)f = (Re c)(#)f + (Im c)(#)(<i>(#)f) by A10,A12,A2,A13,A14,PARTFUN1:5;
hence c(#)f is_integrable_on M by A7,A6,Th33;
A21: Integral(M,<i>(#)f) = <i> * Integral(M,f) by A3,Th39;
thus
Integral(M,c(#)f) = Re c * Integral(M,f) + (Im c)*<i>* Integral(M,f) by A12
,A2,A13,A20,A4,A21,A11,A8,A9
.= c * Integral(M,f) by A1;
end;
Lm2: ( ex A be Element of S st A = dom f & f is A-measurable ) & f
is_integrable_on M & Integral(M,f) = 0 implies |. Integral(M,f).| <= Integral(M
,|.f.|)
proof
assume that
A1: ex A be Element of S st A = dom f & f is A-measurable and
A2: f is_integrable_on M and
A3: Integral(M,f) = 0;
A4: |.f.| is_integrable_on M by A1,A2,Th31;
consider R,I be Real such that
A5: R = Integral(M,Re f) and
I = Integral(M,Im f) and
A6: Integral(M,f)=R + I * <i> by A2,Def3;
R = 0 by A3,A6,COMPLEX1:4,12;
then
A7: |.Integral(M,Re f).| = 0 by A5,EXTREAL1:16;
Re f is_integrable_on M by A2;
then
A8: |.Integral(M,Re f).| <= Integral(M,|.Re f.|) by MESFUNC6:95;
A9: dom |.f.| = dom f by VALUED_1:def 11;
consider A be Element of S such that
A10: A = dom f and
A11: f is A-measurable by A1;
A12: dom Re f = A by A10,COMSEQ_3:def 3;
A13: now
let x be Element of X;
assume
A14: x in dom Re f;
then
A15: Re(f).x = Re(f.x) by COMSEQ_3:def 3;
|.f.|.x = |.f.x .| by A10,A12,A9,A14,VALUED_1:def 11;
hence |.Re(f).x qua Complex .| <= |.f.|.x by A15,COMPLEX1:79;
end;
Re f is A-measurable by A11;
hence thesis by A3,A4,A8,A10,A12,A9,A13,A7,COMPLEX1:44,MESFUNC6:96;
end;
theorem Th41:
for f be PartFunc of X,REAL,Y,r holds (r(#)f)|Y = r(#)(f|Y)
proof
let f be PartFunc of X,REAL,Y,r;
A1: dom ((r(#)f)|Y) = dom (r(#)f) /\ Y by RELAT_1:61
.= dom f /\ Y by VALUED_1:def 5
.= dom (f|Y) by RELAT_1:61;
A2: dom((r(#)f)|Y) c= dom (r(#)f) by RELAT_1:60;
A3: now
let x be Element of X;
assume
A4: x in dom((r(#)f)|Y);
then x in dom (r(#)(f|Y)) by A1,VALUED_1:def 5;
then (r(#)(f|Y)).x = r*((f|Y).x) by VALUED_1:def 5;
then (r(#)(f|Y)).x = r*((f.x)) by A1,A4,FUNCT_1:47;
then (r(#)(f|Y)).x = (r(#)f).x by A2,A4,VALUED_1:def 5;
hence (r(#)(f|Y)).x = ((r(#)f)|Y).x by A4,FUNCT_1:47;
end;
dom ((r(#)f)|Y) = dom (r(#)(f|Y)) by A1,VALUED_1:def 5;
hence thesis by A3,PARTFUN1:5;
end;
theorem Th42:
for f,g be PartFunc of X,REAL st ( ex A be Element of S st A =
dom f /\ dom g & f is A-measurable & g is A-measurable ) & f
is_integrable_on M & g is_integrable_on M & g-f is nonnegative holds ex E be
Element of S st E = dom f /\ dom g & Integral(M,f|E) <= Integral(M,g|E)
proof
let f,g be PartFunc of X,REAL;
assume that
A1: ex A be Element of S st A = dom f /\ dom g & f is A-measurable &
g is A-measurable and
A2: f is_integrable_on M and
A3: g is_integrable_on M and
A4: g-f is nonnegative;
set h=(-1)(#)f;
h is_integrable_on M by A2,MESFUNC6:102;
then consider E be Element of S such that
A5: E = dom h /\ dom g and
A6: Integral(M,h+g) = Integral(M,h|E)+Integral(M,g|E) by A3,MESFUNC6:101;
A7: f|E is_integrable_on M by A2,MESFUNC6:91;
then
A8: Integral(M,f|E) < +infty by MESFUNC6:90;
-infty < Integral(M,f|E) by A7,MESFUNC6:90;
then reconsider c1=Integral(M,f|E) as Element of REAL by A8,XXREAL_0:14;
A9: (-1) * Integral(M,f|E) = (-1)*c1 by EXTREAL1:1;
A10: g|E is_integrable_on M by A3,MESFUNC6:91;
then
A11: Integral(M,g|E) < +infty by MESFUNC6:90;
-infty < Integral(M,g|E) by A10,MESFUNC6:90;
then reconsider c2=Integral(M,g|E) as Element of REAL by A11,XXREAL_0:14;
take E;
A12: h|E = (-1)(#)(f|E) by Th41;
consider A be Element of S such that
A13: A = dom f /\ dom g and
A14: f is A-measurable and
A15: g is A-measurable by A1;
dom h = dom f by VALUED_1:def 5;
then
A16: dom(h+g) = A by A13,VALUED_1:def 1;
h is A-measurable by A13,A14,MESFUNC6:21,XBOOLE_1:17;
then 0 <= Integral(M,h|E)+Integral(M,g|E) by A4,A6,A15,A16,MESFUNC6:26,84;
then 0 <= (-1) * Integral(M,f|E) + Integral(M,g|E) by A7,A12,
MESFUNC6:102;
then 0 <= -c1 + c2 by A9,SUPINF_2:1;
then (0 qua Real) +c1 <= -c1+c2+c1 by XREAL_1:6;
hence thesis by A5,VALUED_1:def 5;
end;
Lm3: ( ex A be Element of S st A = dom f & f is A-measurable ) & f
is_integrable_on M & Integral(M,f) <> 0 implies |. Integral(M,f).| <= Integral(
M,|.f.|)
proof
assume that
A1: ex A be Element of S st A = dom f & f is A-measurable and
A2: f is_integrable_on M and
A3: Integral(M,f) <> 0;
A4: |.f.| is_integrable_on M by A1,A2,Th31;
set a = Integral(M,f);
0 < |.a.| by A3,COMPLEX1:47;
then
A5: |.a.|/|.a.| = 1 by XCMPLX_1:60;
set h = f (#) (|.f.|");
set b = a / |.a.|;
A6: dom |.f.| = dom f by VALUED_1:def 11;
|.b.|*|.b*'.| = |.b*b*'.| by COMPLEX1:65;
then |.b.|*|.b*'.| = |.b*b.| by COMPLEX1:69;
then
A7: |.b.|*|.b*'.| = |.a / |.a.|.|*|.a / |.a.|.| by COMPLEX1:65;
A8: h = f /" |.f.|;
then
A9: dom h = dom f /\ dom |.f.| by VALUED_1:16;
then
A10: dom(b*'(#)h) = dom f by A6,VALUED_1:def 5;
then
A11: dom(|.f.|(#)(b*'(#)h)) = dom f /\ dom f by A6,VALUED_1:def 4;
then
A12: dom(Re(|.f.|(#)(b*'(#)h))) = dom f by COMSEQ_3:def 3;
A13: dom(|.f.|(#)h) = dom|.f.| /\ dom h by VALUED_1:def 4;
then
A14: dom(b*'(#)(|.f.|(#)h)) = dom f by A6,A9,VALUED_1:def 5;
now
let x be object;
assume
A15: x in dom(b*'(#)(|.f.|(#)h));
then x in dom(|.f.|(#)(b*'(#)h)) by A6,A9,A13,A11,VALUED_1:def 5;
then (|.f.|(#)(b*'(#)h)).x = (|.f.|.x)*((b*'(#)h).x) by VALUED_1:def 4;
then (|.f.|(#)(b*'(#)h)).x = |.f.x .|*((b*'(#)h).x) by A6,A14,A15,
VALUED_1:def 11;
then
A16: (|.f.|(#)(b*'(#)h)).x = (b*'*(h.x))*|.f.x .| by A14,A10,A15,VALUED_1:def 5
;
(b*'(#)(|.f.|(#)h)).x = b*'*((|.f.|(#)h).x) by A15,VALUED_1:def 5;
then
(b*'(#)(|.f.|(#)h)).x = b*'*((|.f.|.x)*(h.x)) by A6,A9,A13,A14,A15,
VALUED_1:def 4;
then (b*'(#)(|.f.|(#)h)).x = b*'*(|.f.x .|*(h.x)) by A6,A14,A15,
VALUED_1:def 11;
hence (b*'(#)(|.f.|(#)h)).x = (|.f.|(#)(b*'(#)h)).x by A16;
end;
then
A17: b*'(#)(|.f.|(#)h) = |.f.|(#)(b*'(#)h) by A14,A11,FUNCT_1:2;
A18: |.a / |.a qua Complex.| qua Complex.|
= |.a.|/|.|.a qua Complex.| qua Complex.|
by COMPLEX1:67;
now
let x be set;
A19: h.x = f.x / |.f.|.x by A8,VALUED_1:17;
assume
A20: x in dom(Re(|.f.|(#)(b*'(#)h))) /\ dom |.f.|;
then |.f.|.x = |.f.x .| by A6,A12,VALUED_1:def 11;
then
A21: |.h.x .| = |.f.x .| / |.|.f.x .| qua Complex.| by A19,COMPLEX1:67;
per cases;
suppose
A22: f.x <> 0;
A23: Re((|.f.|(#)(b*'(#)h)).x) = Re(|.f.|(#)(b*'(#)h)).x by A6,A12,A20,
COMSEQ_3:def 3;
(|.f.|(#)(b*'(#)h)).x = (|.f.|.x)*((b*'(#)h).x) by A6,A11,A12,A20,
VALUED_1:def 4;
then (|.f.|(#)(b*'(#)h)).x = |.f.x .|*((b*'(#)h).x) by A6,A12,A20,
VALUED_1:def 11;
then
A24: |.(|.f.|(#)(b*'(#)h)).x qua Complex .|
= |.|.f.x .| qua Complex.|*|.(b*'(#)h).x qua Complex .|
by COMPLEX1:65;
x in dom(b*'(#)h) by A9,A12,A20,VALUED_1:def 5;
then (b*'(#)h).x = b*'*(h.x) by VALUED_1:def 5;
then
A25: |.(b*'(#)h).x .| = |.b*'.|*|.h.x .| by COMPLEX1:65;
0 < |.f.x .| by A22,COMPLEX1:47;
then |.f.x .| / |.f.x .| = 1 by XCMPLX_1:60;
then Re((|.f.|(#)(b*'(#)h)).x) <= |.f.x .|
by A7,A18,A5,A21,A25,A24,
COMPLEX1:54;
hence Re(|.f.|(#)(b*'(#)h)).x <= |.f.|.x by A6,A12,A20,A23,
VALUED_1:def 11;
end;
suppose
A26: f.x = 0;
(|.f.|(#)(b*'(#)h)).x = (|.f.|.x)*((b*'(#)h).x) by A6,A11,A12,A20,
VALUED_1:def 4;
then (|.f.|(#)(b*'(#)h)).x = |.f.x .|*((b*'(#)h).x) by A6,A12,A20,
VALUED_1:def 11;
then
A27: |.(|.f.|(#)(b*'(#)h)).x qua Complex .|
= |.|.f.x qua Complex .| qua Complex.|*|.(b*'(#)h).x qua Complex .|
by COMPLEX1:65;
(Re(f.x))^2 + (Im(f.x))^2 = 0 by A26,COMPLEX1:5;
then
A28: Re((|.f.|(#)(b*'(#)h)).x) <= |.f.x qua Complex .|
by A27,COMPLEX1:54;
Re((|.f.|(#)(b*'(#)h)).x) = Re(|.f.|(#)(b*'(#)h)).x by A6,A12,A20,
COMSEQ_3:def 3;
hence Re(|.f.|(#)(b*'(#)h)).x <= |.f.|.x by A6,A12,A20,A28,
VALUED_1:def 11;
end;
end;
then
A29: |.f.| - Re(|.f.|(#)(b*'(#)h)) is nonnegative by MESFUNC6:58;
set F = Re(|.f.|(#)(b*'(#)h));
reconsider b1=b as Element of COMPLEX by XCMPLX_0:def 2;
A30: Re(b1*b1*') = (Re b1)^2 + (Im b1)^2 by COMPLEX1:40;
consider A be Element of S such that
A31: A = dom f and
A32: f is A-measurable by A1;
A33: |.f.| is A-measurable by A31,A32,Th30;
A34: now
let x be object;
A35: h.x = (f.x)/|.f.|.x by A8,VALUED_1:17;
assume
A36: x in dom f;
then
A37: |.f.|.x = |.f.x .| by A6,VALUED_1:def 11;
A38: (|.f.|(#)h).x = (|.f.|.x)*(h.x) by A6,A9,A13,A36,VALUED_1:def 4;
per cases;
suppose
f.x <> 0;
then 0 < |.f.x .| by COMPLEX1:47;
hence f.x = (|.f.|(#)h).x by A38,A37,A35,XCMPLX_1:87;
end;
suppose
A39: f.x = 0;
then (Re(f.x))^2 + (Im(f.x))^2 = 0 by COMPLEX1:5;
then f.x = (h.x)*|.f.x .| by A39;
hence f.x = (|.f.|(#)h).x by A6,A36,A38,VALUED_1:def 11;
end;
end;
then
A40: f = |.f.| (#) h by A6,A9,A13,FUNCT_1:2;
then
A41: b*'(#)(|.f.|(#)h) is_integrable_on M by A2,Th40;
then consider R1,I1 be Real such that
A42: R1 = Integral(M,Re(|.f.|(#)(b*'(#)h))) and
I1 = Integral(M,Im(|.f.|(#)(b*'(#)h))) and
A43: Integral(M,|.f.|(#)(b*'(#)h)) = R1 + I1 * <i> by A17,Def3;
A44: Im(b1*b1*') = 0 by COMPLEX1:40;
reconsider aa = |.a.| as Element of REAL by XREAL_0:def 1;
b*b*' = Re(b*b*') + (Im(b*b*'))*<i> by COMPLEX1:13;
then b*b*' = |.b*b qua Complex.| by A30,A44,COMPLEX1:68;
then (b*' * a) / |.a qua Complex.| = 1 by A7,A18,A5,COMPLEX1:65;
then
A45: b*' * a = |.a.| by XCMPLX_1:58;
Re(R1 + I1 * <i>) = R1 by COMPLEX1:12;
then Re |.aa qua Complex.| = R1 by A2,A45,A40,A17,A43,Th40;
then
A46: |.aa qua Complex.| = Integral(M,Re(|.f.|(#)(b*'(#)h)))
by A42,COMPLEX1:def 1;
|.f.| (#) h is A-measurable by A32,A6,A9,A13,A34,FUNCT_1:2;
then b*'(#)(|.f.|(#)h) is A-measurable by A31,A6,A9,A13,Th17;
then
A47: Re(|.f.|(#)(b*'(#)h)) is A-measurable by A17;
Re(|.f.|(#)(b*'(#)h)) is_integrable_on M by A17,A41;
then consider E be Element of S such that
A48: E = dom F /\ dom |.f.| and
A49: Integral(M,F|E) <= Integral(M,|.f.||E) by A4,A31,A6,A33,A47,A12,A29,Th42;
thus thesis by A6,A46,A12,A48,A49;
end;
theorem
( ex A be Element of S st A = dom f & f is A-measurable ) & f
is_integrable_on M implies |. Integral(M,f).| <= Integral(M,|.f.|)
proof
assume that
A1: ex A be Element of S st A = dom f & f is A-measurable and
A2: f is_integrable_on M;
per cases;
suppose
Integral(M,f) = 0;
hence thesis by A1,A2,Lm2;
end;
suppose
Integral(M,f) <> 0;
hence thesis by A1,A2,Lm3;
end;
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,COMPLEX;
let B be Element of S;
func Integral_on(M,B,f) -> Complex 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 and
A2: g is_integrable_on M and
A3: B c= dom(f+g);
A4: Re f is_integrable_on M by A1;
then Re(f)|B is_integrable_on M by MESFUNC6:91;
then
A5: Re(f|B) is_integrable_on M by Th7;
then
A6: Integral(M,Re(f|B)) < +infty by MESFUNC6:90;
A7: Im f is_integrable_on M by A1;
then Im(f)|B is_integrable_on M by MESFUNC6:91;
then
A8: Im(f|B) is_integrable_on M by Th7;
then
A9: -infty < Integral(M,Im(f|B)) by MESFUNC6:90;
A10: Integral(M,Im(f|B)) < +infty by A8,MESFUNC6:90;
-infty < Integral(M,Re(f|B)) by A5,MESFUNC6:90;
then reconsider R1=Integral(M,Re(f|B)), I1=Integral(M,Im(f|B))
as Element of REAL by A6
,A9,A10,XXREAL_0:14;
f|B is_integrable_on M by A5,A8;
then
A11: Integral(M,f|B) = R1 + I1*<i> by Def3;
A12: Im g is_integrable_on M by A2;
then Im(g)|B is_integrable_on M by MESFUNC6:91;
then
A13: Im(g|B) is_integrable_on M by Th7;
then
A14: -infty < Integral(M,Im(g|B)) by MESFUNC6:90;
A15: Re g is_integrable_on M by A2;
then Re(g)|B is_integrable_on M by MESFUNC6:91;
then
A16: Re(g|B) is_integrable_on M by Th7;
then
A17: Integral(M,Re(g|B)) < +infty by MESFUNC6:90;
B c= dom Im(f+g) by A3,COMSEQ_3:def 4;
then
A18: B c= dom(Im(f)+Im(g)) by Th5;
then
Integral_on(M,B,Im(f)+Im(g)) = Integral_on(M,B,Im f) + Integral_on(M,B,
Im g) by A7,A12,MESFUNC6:103;
then
A19: Integral(M,Im(f+g)|B) = Integral(M,Im(f)|B) + Integral(M,Im(g)|B) by Th5;
A20: Integral(M,Im(g|B)) < +infty by A13,MESFUNC6:90;
-infty < Integral(M,Re(g|B)) by A16,MESFUNC6:90;
then reconsider R2=Integral(M,Re(g|B)), I2=Integral(M,Im(g|B))
as Element of REAL by A17
,A14,A20,XXREAL_0:14;
g|B is_integrable_on M by A16,A13;
then
A21: Integral(M,g|B) = R2 + I2*<i> by Def3;
A22: Integral(M,Im(g)|B) = I2 by Th7;
Im(f)+Im(g) is_integrable_on M by A7,A12,A18,MESFUNC6:103;
then
A23: Im(f+g) is_integrable_on M by Th5;
then Im(f+g)|B is_integrable_on M by MESFUNC6:91;
then
A24: Im((f+g)|B) is_integrable_on M by Th7;
then
A25: -infty < Integral(M,Im((f+g)|B)) by MESFUNC6:90;
B c= dom Re(f+g) by A3,COMSEQ_3:def 3;
then
A26: B c= dom(Re(f)+Re(g)) by Th5;
then
Integral_on(M,B,Re(f)+Re(g)) = Integral_on(M,B,Re f) + Integral_on(M,B,
Re g) by A4,A15,MESFUNC6:103;
then
A27: Integral(M,Re(f+g)|B) = Integral(M,Re(f)|B) + Integral(M,Re(g)|B) by Th5;
Re(f)+Re(g) is_integrable_on M by A4,A15,A26,MESFUNC6:103;
then
A28: Re(f+g) is_integrable_on M by Th5;
then Re(f+g)|B is_integrable_on M by MESFUNC6:91;
then
A29: Re((f+g)|B) is_integrable_on M by Th7;
then
A30: Integral(M,Re((f+g)|B)) < +infty by MESFUNC6:90;
A31: Integral(M,Im((f+g)|B)) < +infty by A24,MESFUNC6:90;
-infty < Integral(M,Re((f+g)|B)) by A29,MESFUNC6:90;
then reconsider
R=Integral(M,Re((f+g)|B)), I=Integral(M,Im((f+g)|B))
as Element of REAL by A30,A25,A31,
XXREAL_0:14;
A32: Integral(M,Re(g)|B) = R2 by Th7;
Integral(M,Im(f)|B) = I1 by Th7;
then I = I1 + (I2 qua ExtReal) by A19,A22,Th7;
then
A33: I = I1 + I2;
Integral(M,Re(f)|B) = R1 by Th7;
then R = R1 + (R2 qua ExtReal) by A27,A32,Th7;
then
A34: R = R1 + R2;
(f+g)|B is_integrable_on M by A29,A24;
then Integral_on(M,B,f+g) = R + I * <i> by Def3
.= Integral_on(M,B,f) + Integral_on(M,B,g) by A34,A33,A11,A21;
hence thesis by A28,A23;
end;
theorem
f is_integrable_on M implies Integral_on(M,B,c(#)f) = c * Integral_on( M,B,f)
proof
assume f is_integrable_on M;
then
A1: f|B is_integrable_on M by Th23;
A2: dom((c(#)f)|B) = dom(c(#)f) /\ B by RELAT_1:61;
then dom((c(#)f)|B) = dom f /\ B by VALUED_1:def 5;
then
A3: dom((c(#)f)|B) = dom(f|B) by RELAT_1:61;
A4: now
let x be object;
assume
A5: x in dom((c(#)f)|B);
then
A6: (c(#)f)|B.x= (c(#)f).x by FUNCT_1:47;
x in dom (c(#)f) by A2,A5,XBOOLE_0:def 4;
then (c(#)f)|B.x= c * f.x by A6,VALUED_1:def 5;
then
A7: (c(#)f)|B.x= c * f|B.x by A3,A5,FUNCT_1:47;
x in dom (c(#)(f|B)) by A3,A5,VALUED_1:def 5;
hence (c(#)f)|B.x= (c(#)(f|B)).x by A7,VALUED_1:def 5;
end;
dom((c(#)f)|B) = dom(c(#)(f|B)) by A3,VALUED_1:def 5;
then (c(#)f)|B = c(#)(f|B) by A4,FUNCT_1:2;
hence thesis by A1,Th40;
end;
begin :: Several Properties of Real-valued Measurable Functions
reserve f for PartFunc of X,REAL,
a for Real;
theorem
for f be PartFunc of X,REAL, a be Real st A c= dom f holds A /\
great_eq_dom(f,a) = A\(A /\ less_dom(f,a))
proof
let f be PartFunc of X,REAL, a be Real;
now
let x be object;
assume
A1: x in A /\ great_eq_dom(f,a);
then x in great_eq_dom(f,a) by XBOOLE_0:def 4;
then ex y be Real st y = f.x & a <= y by MESFUNC6:6;
then not (ex y1 be Real st y1 = f.x & y1 < a);
then not x in less_dom(f,a) by MESFUNC6:3;
then
A2: not x in (A /\ less_dom(f,a)) by XBOOLE_0:def 4;
x in A by A1,XBOOLE_0:def 4;
hence x in A\(A /\ less_dom(f,a)) by A2,XBOOLE_0:def 5;
end;
then
A3: A /\ great_eq_dom(f,a) c= A\(A /\ less_dom(f,a)) by TARSKI:def 3;
assume
A4: A c= dom f;
now
let x be object;
assume
A5: x in A\(A /\ less_dom(f,a));
then
A6: x in A by XBOOLE_0:def 5;
not x in A /\ less_dom(f,a) by A5,XBOOLE_0:def 5;
then not x in less_dom(f,a) by A6,XBOOLE_0:def 4;
then not f.x < a by A4,A6,MESFUNC6:3;
then x in great_eq_dom(f,a) by A4,A6,MESFUNC6:6;
hence x in A /\ great_eq_dom(f,a) by A6,XBOOLE_0:def 4;
end;
then A\(A /\ less_dom(f,a)) c= A /\ great_eq_dom(f,a) by TARSKI:def 3;
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem
for f be PartFunc of X,REAL, a be Real st A c= dom f holds A /\
great_dom(f,a) = A\(A /\ less_eq_dom(f,a))
proof
let f be PartFunc of X,REAL, a be Real;
now
let x be object;
assume
A1: x in A /\ great_dom(f,a);
then x in great_dom(f,a) by XBOOLE_0:def 4;
then ex y be Real st y = f.x & a < y by MESFUNC6:5;
then not (ex y1 be Real st y1 = f.x & y1 <= a);
then not x in less_eq_dom(f,a) by MESFUNC6:4;
then
A2: not x in (A /\ less_eq_dom(f,a)) by XBOOLE_0:def 4;
x in A by A1,XBOOLE_0:def 4;
hence x in A\(A /\ less_eq_dom(f,a)) by A2,XBOOLE_0:def 5;
end;
then
A3: A /\ great_dom(f,a) c= A\(A /\ less_eq_dom(f,a)) by TARSKI:def 3;
assume
A4: A c= dom f;
now
let x be object;
assume
A5: x in A\(A /\ less_eq_dom(f,a));
then
A6: x in A by XBOOLE_0:def 5;
not x in A /\ less_eq_dom(f,a) by A5,XBOOLE_0:def 5;
then not x in less_eq_dom(f,a) by A6,XBOOLE_0:def 4;
then not f.x <= a by A4,A6,MESFUNC6:4;
then x in great_dom(f,a) by A4,A6,MESFUNC6:5;
hence x in A /\ great_dom(f,a) by A6,XBOOLE_0:def 4;
end;
then A\(A /\ less_eq_dom(f,a)) c= A /\ great_dom(f,a) by TARSKI:def 3;
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem
for f be PartFunc of X,REAL, a be Real st A c= dom f holds A /\
less_eq_dom(f,a) = A\(A /\ great_dom(f,a))
proof
let f be PartFunc of X,REAL, a be Real;
now
let x be object;
assume
A1: x in A /\ less_eq_dom(f,a);
then x in less_eq_dom(f,a) by XBOOLE_0:def 4;
then ex y be Real st y = f.x & y <= a by MESFUNC6:4;
then not (ex y1 be Real st y1 = f.x & a < y1);
then not x in great_dom(f,a) by MESFUNC6:5;
then
A2: not x in (A /\ great_dom(f,a)) by XBOOLE_0:def 4;
x in A by A1,XBOOLE_0:def 4;
hence x in A\(A /\ great_dom(f,a)) by A2,XBOOLE_0:def 5;
end;
then
A3: A /\ less_eq_dom(f,a) c= A\(A /\ great_dom(f,a)) by TARSKI:def 3;
assume
A4: A c= dom f;
now
let x be object;
assume
A5: x in A\(A /\ great_dom(f,a));
then
A6: x in A by XBOOLE_0:def 5;
not x in A /\ great_dom(f,a) by A5,XBOOLE_0:def 5;
then not x in great_dom(f,a) by A6,XBOOLE_0:def 4;
then not a < f.x by A4,A6,MESFUNC6:5;
then x in less_eq_dom(f,a) by A4,A6,MESFUNC6:4;
hence x in A /\ less_eq_dom(f,a) by A6,XBOOLE_0:def 4;
end;
then A\(A /\ great_dom(f,a)) c= A /\ less_eq_dom(f,a) by TARSKI:def 3;
hence thesis by A3,XBOOLE_0:def 10;
end;
theorem
A /\ eq_dom(f,a) = A /\ great_eq_dom(f,a) /\ less_eq_dom(f,a)
proof
now
let x be object;
assume
A1: x in A /\ great_eq_dom(f,a) /\ less_eq_dom(f,a);
then
A2: x in less_eq_dom(f,a) by XBOOLE_0:def 4;
then
A3: x in dom f by MESFUNC6:4;
A4: x in A /\ great_eq_dom(f,a) by A1,XBOOLE_0:def 4;
then x in great_eq_dom(f,a) by XBOOLE_0:def 4;
then
A5: ex y1 be Real st y1 = f.x & a <= y1 by MESFUNC6:6;
ex y2 be Real st y2 = f.x & y2 <= a by A2,MESFUNC6:4;
then a = f.x by A5,XXREAL_0:1;
then
A6: x in eq_dom(f,a) by A3,MESFUNC6:7;
x in A by A4,XBOOLE_0:def 4;
hence x in A /\ eq_dom(f,a) by A6,XBOOLE_0:def 4;
end;
then
A7: A /\ great_eq_dom(f,a) /\ less_eq_dom(f,a) c= A /\ eq_dom(f,a) by
TARSKI:def 3;
now
let x be object;
assume
A8: x in A /\ eq_dom(f,a);
then
A9: x in A by XBOOLE_0:def 4;
A10: x in eq_dom(f,a) by A8,XBOOLE_0:def 4;
then
A11: ex y be Real st y = f.x & a = y by MESFUNC6:7;
A12: x in dom f by A10,MESFUNC6:7;
then x in great_eq_dom(f,a) by A11,MESFUNC6:6;
then
A13: x in A /\ great_eq_dom(f,a) by A9,XBOOLE_0:def 4;
x in less_eq_dom(f,a) by A11,A12,MESFUNC6:4;
hence x in A /\ great_eq_dom(f,a) /\ less_eq_dom(f,a) by A13,XBOOLE_0:def 4
;
end;
then A /\ eq_dom(f,a) c= A /\ great_eq_dom(f,a) /\ less_eq_dom(f,a) by
TARSKI:def 3;
hence thesis by A7,XBOOLE_0:def 10;
end;