:: Integral of Non Positive Functions
:: by Noboru Endou
::
:: Received September 3, 2017
:: Copyright (c) 2017-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, XXREAL_0, SUBSET_1, CARD_1, ARYTM_3, ARYTM_1, RELAT_1,
NAT_1, REAL_1, CARD_3, FUNCT_1, FINSEQ_1, XBOOLE_0, TARSKI, PROB_1,
FUNCOP_1, SUPINF_2, VALUED_0, FUNCT_2, PARTFUN1, MEASURE1, ORDINAL2,
SERIES_1, MESFUNC5, SEQ_2, SEQFUNC, PBOOLE, VALUED_1, MESFUNC1, MESFUNC8,
MESFUNC2, MESFUNC3, COMPLEX1, XCMPLX_0, RFUNCT_3, INT_1, MSSUBFAM;
notations TARSKI, XBOOLE_0, SUBSET_1, XXREAL_3, XXREAL_0, XREAL_0, ORDINAL1,
NUMBERS, FUNCT_1, RELSET_1, FUNCT_2, FUNCOP_1, PARTFUN1, PROB_1, PROB_3,
NAT_1, NAT_D, VALUED_0, FINSEQ_1, SUPINF_2, SEQFUNC, MEASURE1, MESFUNC1,
MESFUNC2, MESFUNC3, MESFUNC5, MESFUNC8, DBLSEQ_3, MESFUNC9, EXTREAL1;
constructors SEQFUNC, PROB_3, MESFUNC8, MESFUNC9, EXTREAL1, SUPINF_1,
MESFUNC2, DBLSEQ_3, MEASUR11, MESFUNC3, NAT_D;
registrations ORDINAL1, XBOOLE_0, RELAT_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1,
NUMBERS, VALUED_0, MESFUNC9, RELSET_1, PARTFUN1, XXREAL_3, DBLSEQ_3,
MEASUR11, MESFUNC5;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, XBOOLE_0;
equalities FINSEQ_1;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, XBOOLE_0, XREAL_0, FINSEQ_1, NAT_1, FUNCT_1, XXREAL_0,
FINSEQ_3, XBOOLE_1, XREAL_1, FUNCOP_1, XXREAL_3, FUNCT_2, RELAT_1,
MESFUNC5, EXTREAL1, MESFUNC9, FINSEQ_2, PARTFUN1, ORDINAL1, MESFUNC1,
SUPINF_2, MESFUNC8, MESFUNC2, MEASUR10, DBLSEQ_3, MEASUR11, MESFUNC3,
NAT_D, NAT_2;
schemes FINSEQ_1, NAT_1, FUNCT_2, SEQFUNC;
begin :: Preliminaries
registration
let X be non empty set, f be nonnegative PartFunc of X,ExtREAL;
cluster -f -> nonpositive;
correctness
proof
-f = (-1)(#)f by MESFUNC2:9;
hence -f is nonpositive by MESFUNC5:20;
end;
end;
registration
let X be non empty set, f be nonpositive PartFunc of X,ExtREAL;
cluster -f -> nonnegative;
correctness
proof
for x be object st x in dom (-f) holds 0 <= (-f).x
proof
let x be object;
assume A1: x in dom(-f);
f.x <= 0 by MESFUNC5:8; then
-(f.x) >= 0;
hence (-f).x >= 0 by A1,MESFUNC1:def 7;
end;
hence -f is nonnegative by SUPINF_2:52;
end;
end;
theorem Th1:
for X be non empty set, f be nonpositive PartFunc of X,ExtREAL, E be set
holds f|E is nonpositive
proof
let X be non empty set, f be nonpositive PartFunc of X,ExtREAL, E be set;
now let x be set;
assume x in dom(f|E); then
(f|E).x = f.x by FUNCT_1:47;
hence (f|E).x <= 0 by MESFUNC5:8;
end;
hence f|E is nonpositive by MESFUNC5:9;
end;
theorem Th2:
for X be non empty set, A be set, r be Real, f be PartFunc of X,ExtREAL
holds (r(#)f)|A = r(#)(f|A)
proof
let X be non empty set, A be set, r be Real, f be PartFunc of X,ExtREAL;
A1: dom(r(#)f) = dom f by MESFUNC1:def 6; then
A2: dom((r(#)f)|A) = dom f /\ A by RELAT_1:61; then
A3: dom((r(#)f)|A) = dom(f|A) by RELAT_1:61; then
A4: dom((r(#)f)|A) = dom(r(#)(f|A)) by MESFUNC1:def 6;
now let x be Element of X;
assume B1: x in dom((r(#)f)|A); then
B2: x in dom f by A2,XBOOLE_0:def 4;
((r(#)f)|A).x = (r(#)f).x by B1,FUNCT_1:47; then
((r(#)f)|A).x = r * f.x by B2,A1,MESFUNC1:def 6; then
((r(#)f)|A).x = r * (f|A).x by B1,A3,FUNCT_1:47;
hence ((r(#)f)|A).x = (r(#)(f|A)).x by B1,A4,MESFUNC1:def 6;
end;
hence (r(#)f)|A = r(#)(f|A) by A4,PARTFUN1:5;
end;
theorem Th3:
for X be non empty set, A be set, f be PartFunc of X,ExtREAL
holds -(f|A) = (-f)|A
proof
let X be non empty set, A be set, f be PartFunc of X,ExtREAL;
-(f|A) = (-1)(#)(f|A) by MESFUNC2:9; then
-(f|A) = ((-1)(#)f)|A by Th2;
hence thesis by MESFUNC2:9;
end;
theorem Th4:
for X be non empty set, f be PartFunc of X,ExtREAL,c be Real st
f is nonpositive holds
(0 <= c implies c(#)f is nonpositive) &
(c <= 0 implies c(#)f is nonnegative)
proof
let X be non empty set;
let f be PartFunc of X,ExtREAL;
let c be Real;
set g = c(#)f;
assume
A1: f is nonpositive;
hereby
set g = c(#)f;
assume
A2: 0 <= c;
for x be set st x in dom g holds g.x <= 0
proof
let x be set;
f.x <= 0 by A1,MESFUNC5:8; then
A3: c*f.x <= 0 by A2;
assume x in dom g;
hence thesis by A3,MESFUNC1:def 6;
end;
hence c(#)f is nonpositive by MESFUNC5:9;
end;
assume
A4: c <= 0;
now
let x be object;
f.x <= 0 by A1,MESFUNC5:8; then
A5: 0 <= c*f.x by A4;
assume x in dom g;
hence 0 <= g.x by A5,MESFUNC1:def 6;
end;
hence thesis by SUPINF_2:52;
end;
theorem Th5:
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 &
|.f.| is nonnegative
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
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 max+f is nonnegative & max-f is nonnegative by A1,SUPINF_2:52;
now
let x be object;
assume x in dom |.f.|;
then (|.f.|).x =|. f.x .| by MESFUNC1:def 10;
hence 0 <= (|.f.|).x by EXTREAL1:14;
end;
hence thesis by SUPINF_2:52;
end;
theorem
for X be non empty set, f be PartFunc of X,ExtREAL, x be object holds
f.x <= (max+f).x & f.x >= -(max-f).x
proof
let X be non empty set, f be PartFunc of X,ExtREAL, x be object;
per cases;
suppose x in dom f; then
x in dom(max+f) & x in dom(max-f) by MESFUNC2:def 2,def 3; then
A1: (max+f).x = max(f.x,0) & (max-f).x = max(-f.x,0)
by MESFUNC2:def 2,def 3;
reconsider a = (max-f).x, b = -(f.x) as ExtReal;
-b >= -a by A1,XXREAL_0:25,XXREAL_3:38;
hence f.x <= (max+f).x & f.x >= -(max-f).x by A1,XXREAL_0:25;
end;
suppose A2: not x in dom f; then
not x in dom(max+f) & not x in dom(max-f) by MESFUNC2:def 2,def 3; then
f.x = 0 & (max+f).x = 0 & (max-f).x = 0 by A2,FUNCT_1:def 2;
hence f.x <= (max+f).x & f.x >= -(max-f).x;
end;
end;
Lm1:
for X be non empty set, f be PartFunc of X,ExtREAL, r be Real holds
(r > 0 implies less_dom(f,r) = less_dom(max+f,r)) &
(r <= 0 implies less_dom(f,r) = great_dom(max-f,-r))
proof
let X be non empty set, f be PartFunc of X,ExtREAL, r be Real;
hereby assume A1: r > 0;
reconsider r1 = r as ExtReal;
now let x be Element of X;
assume x in less_dom(max+f,r); then
A2: x in dom(max+f) & (max+f).x < r by MESFUNC1:def 11; then
A3: x in dom f by MESFUNC2:def 2;
max(f.x,0) < r1 by A2,MESFUNC2:def 2; then
f.x < r1 by XXREAL_0:31;
hence x in less_dom(f,r) by A3,MESFUNC1:def 11;
end; then
A4: less_dom(max+f,r) c= less_dom(f,r);
now let x be Element of X;
assume x in less_dom(f,r); then
A5: x in dom f & f.x < r by MESFUNC1:def 11; then
A6: x in dom(max+f) by MESFUNC2:def 2; then
(max+f).x = max(f.x,0) by MESFUNC2:def 2; then
(max+f).x < r by A1,A5,XXREAL_0:29;
hence x in less_dom(max+f,r) by A6,MESFUNC1:def 11;
end; then
less_dom(f,r) c= less_dom(max+f,r);
hence less_dom(max+f,r) = less_dom(f,r) by A4;
end;
assume A7: r <= 0;
reconsider r1 = r as ExtReal;
now let x be Element of X;
assume x in great_dom(max-f,-r); then
A8: x in dom(max-f) & (max-f).x > -r by MESFUNC1:def 13; then
A9: x in dom f by MESFUNC2:def 3;
A10: max(-(f.x),0) > -r1 by A8,MESFUNC2:def 3;
now assume 0 > -(f.x); then
max(-(f.x),0) = 0 by XXREAL_0:def 10;
hence contradiction by A7,A10;
end; then
max(-(f.x),0) = -(f.x) by XXREAL_0:def 10; then
f.x < r1 by A10,XXREAL_3:38;
hence x in less_dom(f,r) by A9,MESFUNC1:def 11;
end; then
A11:great_dom(max-f,-r) c= less_dom(f,r);
now let x be Element of X;
assume x in less_dom(f,r); then
A12: x in dom f & f.x < r by MESFUNC1:def 11; then
A13: x in dom(max-f) by MESFUNC2:def 3;
max(-(f.x),0) = -(f.x) by A7,A12,XXREAL_0:def 10; then
(max-f).x = -(f.x) by A13,MESFUNC2:def 3; then
(max-f).x > -r1 by A12,XXREAL_3:38;
hence x in great_dom(max-f,-r) by A13,MESFUNC1:def 13;
end; then
less_dom(f,r) c= great_dom(max-f,-r);
hence great_dom(max-f,-r) = less_dom(f,r) by A11;
end;
theorem
for X be non empty set, f be PartFunc of X,ExtREAL,
r be positive Real holds less_dom(f,r) = less_dom(max+f,r) by Lm1;
theorem
for X be non empty set, f be PartFunc of X,ExtREAL,
r be non positive Real holds less_dom(f,r) = great_dom(max-f,-r) by Lm1;
theorem Th9:
for X be non empty set, f,g be PartFunc of X,ExtREAL,
a be ExtReal, r be Real
st r <> 0 & g = r(#)f holds eq_dom(f,a) = eq_dom(g,a*r)
proof
let X be non empty set, f,g be PartFunc of X,ExtREAL,
a be ExtReal, r be Real;
assume that
A1: r <> 0 and
a2: g = r(#)f;
A2: dom f = dom g by a2,MESFUNC1:def 6;
now let x be object;
assume x in eq_dom(f,a); then
x in dom f & f.x = a by MESFUNC1:def 15; then
x in dom g & g.x = r*a by a2,A2,MESFUNC1:def 6;
hence x in eq_dom(g,a*r) by MESFUNC1:def 15;
end; then
A3: eq_dom(f,a) c= eq_dom(g,a*r);
now let x be object;
assume x in eq_dom(g,a*r); then
A4: x in dom g & g.x = a*r by MESFUNC1:def 15; then
r* f.x = a*r by a2,MESFUNC1:def 6; then
f.x = a by A1,XXREAL_3:68;
hence x in eq_dom(f,a) by A2,A4,MESFUNC1:def 15;
end; then
eq_dom(g,a*r) c= eq_dom(f,a);
hence thesis by A3;
end;
theorem Th10:
for X be non empty set, S be SigmaField of X, f be PartFunc of X,ExtREAL,
A be Element of S st A c= dom f holds
f is A-measurable iff
max+f is A-measurable & max-f is A-measurable
proof
let X be non empty set, S be SigmaField of X, f be PartFunc of X,ExtREAL,
A be Element of S;
assume A1: A c= dom f;
hence f is A-measurable implies
max+f is A-measurable & max-f is A-measurable by MESFUNC2:25,26;
assume A2: max+f is A-measurable & max-f is A-measurable;
A3:dom (max-f) = dom f by MESFUNC2:def 3;
now let r be Real;
per cases;
suppose r > 0; then
less_dom(f,r) = less_dom(max+f,r) by Lm1;
hence A /\ less_dom(f,r) in S by A2,MESFUNC1:def 16;
end;
suppose r <= 0; then
less_dom(f,r) = great_dom(max-f,-r) by Lm1;
hence A /\ less_dom(f,r) in S by A1,A2,A3,MESFUNC1:29;
end;
end;
hence f is A-measurable by MESFUNC1:def 16;
end;
Lm2: ::equivalent to NAT_1:10
for i,j being Nat st i <= j holds ex k be Nat st j = i + k
proof
let i,j be Nat;
defpred P[Nat] means i <= $1 implies ex k be Nat st $1 = i + k;
A1: for j be Nat st P[j] holds P[j+1]
proof
let j be Nat such that
A2: i <= j implies ex k be Nat st j = i + k;
assume A3: i <= j+1;
per cases by A3,NAT_1:8;
suppose i <= j;
then consider k be Nat such that
A4: j = i + k by A2;
reconsider k1=k+1 as Nat;
take k1;
thus j+1 = i+k1 by A4;
end;
suppose B1: i = j + 1;
reconsider k1=0 as Nat;
take k1;
thus j+1 = i+k1 by B1;
end;
end;
A6: P[0]
proof
assume
A7: i <= 0;
take 0;
thus thesis by A7;
end;
for j be Nat holds P[j] from NAT_1:sch 2(A6,A1);
hence thesis;
end;
definition
let X be non empty set, f be Function of X,ExtREAL, r be Real;
redefine func r(#)f -> Function of X,ExtREAL; :: redefines (#) (MESFUNC1, definition)
correctness
proof
dom (r(#)f) = dom f by MESFUNC1:def 6; then
dom (r(#)f) = X by FUNCT_2:def 1;
hence r(#)f is Function of X,ExtREAL by FUNCT_2:def 1;
end;
end;
theorem Th11:
for X be non empty set, r be Real, f be without+infty Function of X,ExtREAL
st r >= 0 holds r(#)f is without+infty
proof
let X be non empty set, r be Real, f be without+infty Function of X,ExtREAL;
assume A1: r >= 0;
now let x be set;
assume A2: x in dom(r(#)f); then
A3: x in dom f by MESFUNC1:def 6;
per cases by A1;
suppose A4: r > 0; then
r * f.x < r * +infty by A3,MESFUNC5:11,XXREAL_3:72; then
r * f.x < +infty by A4,XXREAL_3:def 5;
hence (r(#)f).x < +infty by A2,MESFUNC1:def 6;
end;
suppose r = 0; then
r * f.x < +infty;
hence (r(#)f).x < +infty by A2,MESFUNC1:def 6;
end;
end;
hence r(#)f is without+infty by MESFUNC5:11;
end;
registration
let X be non empty set;
let f be without+infty Function of X,ExtREAL;
let r be non negative Real;
cluster r(#)f -> without+infty for Function of X,ExtREAL;
coherence by Th11;
end;
theorem Th12:
for X be non empty set, r be Real, f be without+infty Function of X,ExtREAL
st r <= 0 holds r(#)f is without-infty
proof
let X be non empty set, r be Real, f be without+infty Function of X,ExtREAL;
assume A1: r <= 0;
now let x be set;
assume A2: x in dom(r(#)f); then
A3: x in dom f by MESFUNC1:def 6;
per cases by A1;
suppose A4: r < 0; then
r * f.x > r * +infty by A3,MESFUNC5:11,XXREAL_3:102; then
r * f.x > -infty by A4,XXREAL_3:def 5;
hence (r(#)f).x > -infty by A2,MESFUNC1:def 6;
end;
suppose r = 0; then
r * f.x > -infty;
hence (r(#)f).x > -infty by A2,MESFUNC1:def 6;
end;
end;
hence r(#)f is without-infty by MESFUNC5:10;
end;
registration
let X be non empty set;
let f be without+infty Function of X,ExtREAL;
let r be non positive Real;
cluster r(#)f -> without-infty;
correctness by Th12;
end;
theorem Th13:
for X be non empty set, r be Real, f be without-infty Function of X,ExtREAL
st r >= 0 holds r(#)f is without-infty
proof
let X be non empty set, r be Real, f be without-infty Function of X,ExtREAL;
assume A1: r >= 0;
now let x be set;
assume A2: x in dom(r(#)f); then
A3: x in dom f by MESFUNC1:def 6;
per cases by A1;
suppose A4: r > 0; then
r * f.x > r * -infty by A3,MESFUNC5:10,XXREAL_3:72; then
r * f.x > -infty by A4,XXREAL_3:def 5;
hence (r(#)f).x > -infty by A2,MESFUNC1:def 6;
end;
suppose r = 0; then
r * f.x > -infty;
hence (r(#)f).x > -infty by A2,MESFUNC1:def 6;
end;
end;
hence r(#)f is without-infty by MESFUNC5:10;
end;
registration
let X be non empty set;
let f be without-infty Function of X,ExtREAL;
let r be non negative Real;
cluster r(#)f -> without-infty;
correctness by Th13;
end;
theorem Th14:
for X be non empty set, r be Real, f be without-infty Function of X,ExtREAL
st r <= 0 holds r(#)f is without+infty
proof
let X be non empty set, r be Real, f be without-infty Function of X,ExtREAL;
assume A1: r <= 0;
now let x be set;
assume A2: x in dom(r(#)f); then
A3: x in dom f by MESFUNC1:def 6;
per cases by A1;
suppose A4: r < 0; then
r * f.x < r * -infty by A3,MESFUNC5:10,XXREAL_3:102; then
r * f.x < +infty by A4,XXREAL_3:def 5;
hence (r(#)f).x < +infty by A2,MESFUNC1:def 6;
end;
suppose r = 0; then
r * f.x < +infty;
hence (r(#)f).x < +infty by A2,MESFUNC1:def 6;
end;
end;
hence r(#)f is without+infty by MESFUNC5:11;
end;
registration
let X be non empty set;
let f be without-infty Function of X,ExtREAL;
let r be non positive Real;
cluster r(#)f -> without+infty;
correctness by Th14;
end;
theorem Th15:
for X be non empty set, r be Real,
f be without-infty without+infty Function of X,ExtREAL holds
r(#)f is without-infty without+infty
proof
let X be non empty set, r be Real,
f be without-infty without+infty Function of X,ExtREAL;
per cases;
suppose r >= 0;
hence r(#)f is without-infty without+infty;
end;
suppose r < 0;
hence r(#)f is without-infty without+infty;
end;
end;
registration
let X be non empty set;
let f be without-infty without+infty Function of X,ExtREAL;
let r be Real;
cluster r(#)f -> without-infty without+infty;
correctness by Th15;
end;
theorem Th16:
for X be non empty set, r be positive Real, f be Function of X,ExtREAL
holds f is without+infty iff r(#)f is without+infty
proof
let X be non empty set, r be positive Real, f be Function of X,ExtREAL;
thus f is without+infty implies r(#)f is without+infty;
assume A2: r(#)f is without+infty;
now let x be set;
assume x in dom f; then
A3: x in dom(r(#)f) by MESFUNC1:def 6; then
(r(#)f).x = r * f.x by MESFUNC1:def 6; then
r * f.x < +infty by A2,A3,MESFUNC5:11; then
f.x <> +infty by XXREAL_3:def 5;
hence f.x < +infty by XXREAL_0:4;
end;
hence f is without+infty by MESFUNC5:11;
end;
theorem Th17:
for X be non empty set, r be negative Real, f be Function of X,ExtREAL
holds f is without+infty iff r(#)f is without-infty
proof
let X be non empty set, r be negative Real, f be Function of X,ExtREAL;
thus f is without+infty implies r(#)f is without-infty;
assume A2: r(#)f is without-infty;
now let x be set;
assume x in dom f; then
A3: x in dom(r(#)f) by MESFUNC1:def 6; then
(r(#)f).x = r * f.x by MESFUNC1:def 6; then
r * f.x > -infty by A2,A3,MESFUNC5:10; then
f.x <> +infty by XXREAL_3:def 5;
hence f.x < +infty by XXREAL_0:4;
end;
hence f is without+infty by MESFUNC5:11;
end;
theorem Th18:
for X be non empty set, r be positive Real, f be Function of X,ExtREAL
holds f is without-infty iff r(#)f is without-infty
proof
let X be non empty set, r be positive Real, f be Function of X,ExtREAL;
thus f is without-infty implies r(#)f is without-infty;
assume A2: r(#)f is without-infty;
now let x be set;
assume x in dom f; then
A3: x in dom(r(#)f) by MESFUNC1:def 6; then
(r(#)f).x = r * f.x by MESFUNC1:def 6; then
r * f.x > -infty by A2,A3,MESFUNC5:10; then
f.x <> -infty by XXREAL_3:def 5;
hence f.x > -infty by XXREAL_0:6;
end;
hence f is without-infty by MESFUNC5:10;
end;
theorem Th19:
for X be non empty set, r be negative Real, f be Function of X,ExtREAL
holds f is without-infty iff r(#)f is without+infty
proof
let X be non empty set, r be negative Real, f be Function of X,ExtREAL;
thus f is without-infty implies r(#)f is without+infty;
assume A2: r(#)f is without+infty;
now let x be set;
assume x in dom f; then
A3: x in dom(r(#)f) by MESFUNC1:def 6; then
(r(#)f).x = r * f.x by MESFUNC1:def 6; then
r * f.x < +infty by A2,A3,MESFUNC5:11; then
f.x <> -infty by XXREAL_3:def 5;
hence f.x > -infty by XXREAL_0:6;
end;
hence f is without-infty by MESFUNC5:10;
end;
theorem
for X be non empty set, r be non zero Real, f be Function of X,ExtREAL
holds f is without-infty without+infty iff
r(#)f is without-infty without+infty
proof
let X be non empty set, r be non zero Real, f be Function of X,ExtREAL;
per cases;
suppose r > 0;
hence f is without-infty without+infty
iff r(#)f is without-infty without+infty by Th16,Th18;
end;
suppose r < 0;
hence f is without-infty without+infty
iff r(#)f is without-infty without+infty by Th17,Th19;
end;
end;
theorem Th21:
for X,Y be non empty set, f be PartFunc of X,ExtREAL, r be Real
st f = Y --> r holds f is without-infty without+infty
proof
let X,Y be non empty set, f be PartFunc of X,ExtREAL, r be Real;
assume A1: f = Y --> r; then
for x be object holds f.x > -infty by XREAL_0:def 1,XXREAL_0:12;
hence f is without-infty by MESFUNC5:def 5;
for x be object holds f.x < +infty by A1,XREAL_0:def 1,XXREAL_0:9;
hence f is without+infty by MESFUNC5:def 6;
end;
theorem
for X be non empty set, f be Function of X,ExtREAL holds
0(#)f = X --> 0
& 0(#)f is without-infty without+infty
proof
let X be non empty set, f be Function of X,ExtREAL;
A1:X --> 0 is Function of X,ExtREAL by FUNCOP_1:45,XXREAL_0:def 1;
for x be Element of X holds (0(#)f).x = (X --> 0).x
proof
let x be Element of X;
x in X; then
x in dom(0(#)f) by FUNCT_2:def 1; then
(0(#)f).x = 0 * f.x by MESFUNC1:def 6;
hence (0(#)f).x = (X --> 0).x by FUNCOP_1:7;
end;
hence 0(#)f = X --> 0 by A1,FUNCT_2:def 8;
hence 0(#)f is without-infty without+infty by Th21;
end;
theorem Th23:
for X be non empty set, f,g be PartFunc of X,ExtREAL st
f is without-infty without+infty holds
dom(f+g)=dom f /\ dom g & dom(f-g)=dom f /\ dom g
& dom(g-f)=dom f /\ dom g
proof
let X be non empty set, f,g be PartFunc of X,ExtREAL;
assume A1: f is without-infty without+infty; then
not -infty in rng f by MESFUNC5:def 3; then
A2: f"{-infty} = {} by FUNCT_1:72;
not +infty in rng f by A1,MESFUNC5:def 4; then
A3: f"{+infty} = {} by FUNCT_1:72; then
f"{+infty} /\ g"{-infty} \/ f"{-infty} /\ g"{+infty} = {} by A2; then
dom(f+g) = (dom f /\ dom g)\{} by MESFUNC1:def 3;
hence dom(f+g)=dom f /\ dom g;
A4: f"{+infty} /\ g"{+infty} \/ f"{-infty} /\ g"{-infty} = {} by A2,A3; then
dom(f-g) = (dom f /\ dom g)\{} by MESFUNC1:def 4;
hence dom(f-g)=dom f /\ dom g;
dom(g-f) = (dom f /\ dom g)\{} by A4,MESFUNC1:def 4;
hence dom(g-f)=dom f /\ dom g;
end;
theorem
for X be non empty set, f1,f2 be Function of X,ExtREAL
st f2 is without-infty without+infty holds
f1+f2 is Function of X,ExtREAL
& for x be Element of X holds (f1+f2).x = f1.x + f2.x
proof
let X be non empty set, f1,f2 be Function of X,ExtREAL;
assume A1: f2 is without-infty without+infty;
dom f1 = X & dom f2 = X by FUNCT_2:def 1; then
A2:dom(f1+f2) = X /\ X by A1,Th23;
hence f1+f2 is Function of X,ExtREAL by FUNCT_2:def 1;
thus thesis by A2,MESFUNC1:def 3;
end;
theorem
for X be non empty set, f1,f2 be Function of X,ExtREAL
st f1 is without-infty without+infty holds
f1-f2 is Function of X,ExtREAL
& for x be Element of X holds (f1-f2).x = f1.x - f2.x
proof
let X be non empty set, f1,f2 be Function of X,ExtREAL;
assume A1: f1 is without-infty without+infty;
dom f1 = X & dom f2 = X by FUNCT_2:def 1; then
A2:dom(f1-f2) = X /\ X by A1,Th23;
hence f1-f2 is Function of X,ExtREAL by FUNCT_2:def 1;
thus thesis by A2,MESFUNC1:def 4;
end;
theorem
for X be non empty set, f1,f2 be Function of X,ExtREAL
st f2 is without-infty without+infty holds
f1-f2 is Function of X,ExtREAL
& for x be Element of X holds (f1-f2).x = f1.x - f2.x
proof
let X be non empty set, f1,f2 be Function of X,ExtREAL;
assume A1: f2 is without-infty without+infty;
dom f1 = X & dom f2 = X by FUNCT_2:def 1; then
A2:dom(f1-f2) = X /\ X by A1,Th23;
hence f1-f2 is Function of X,ExtREAL by FUNCT_2:def 1;
thus thesis by A2,MESFUNC1:def 4;
end;
theorem
for X,Y be non empty set, f1,f2 be PartFunc of X,ExtREAL st
dom f1 c= Y & f2 = Y --> 0 holds f1+f2 = f1 & f1-f2 = f1 & f2-f1 = -f1
proof
let X,Y be non empty set, f1,f2 be PartFunc of X,ExtREAL;
assume that
A1: dom f1 c= Y and
A2: f2 = Y --> 0;
A3: dom f2 = Y by A2,FUNCOP_1:13;
f2 is without-infty without+infty by A2,Th21; then
A4: dom(f1+f2) = dom f1 /\ dom f2
& dom(f1-f2) = dom f1 /\ dom f2
& dom(f2-f1) = dom f1 /\ dom f2 by Th23; then
A5: dom(f1+f2) = dom f1 & dom(f1-f2) = dom f1 & dom(f2-f1) = dom f1
by A1,A3,XBOOLE_1:28; then
A6: dom(-f1) = dom(f2-f1) by MESFUNC1:def 7;
now let x be Element of X;
assume A7: x in dom(f1+f2); then
A8: f2.x = 0 by A1,A2,A5,FUNCOP_1:7;
(f1+f2).x = f1.x + f2.x by A7,MESFUNC1:def 3;
hence (f1+f2).x = f1.x by A8,XXREAL_3:4;
end;
hence f1+f2 = f1 by A4,A1,A3,XBOOLE_1:28,PARTFUN1:5;
now let x be Element of X;
assume A9: x in dom(f1-f2); then
A10: f2.x = 0 by A1,A2,A5,FUNCOP_1:7;
(f1-f2).x = f1.x - f2.x by A9,MESFUNC1:def 4;
hence (f1-f2).x = f1.x by A10,XXREAL_3:15;
end;
hence f1-f2 = f1 by A4,A1,A3,XBOOLE_1:28,PARTFUN1:5;
now let x be Element of X;
assume A11: x in dom(f2-f1); then
A12: f2.x = 0 by A1,A2,A5,FUNCOP_1:7;
(f2-f1).x = f2.x - f1.x by A11,MESFUNC1:def 4
.= -f1.x + f2.x by XXREAL_3:def 4
.= -f1.x by A12,XXREAL_3:4;
hence (f2-f1).x = (-f1).x by A11,A6,MESFUNC1:def 7;
end;
hence f2-f1 = -f1 by A6,PARTFUN1:5;
end;
theorem Th28:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f,g be PartFunc of X,ExtREAL st f is_simple_func_in S &
g is_simple_func_in S holds f+g is_simple_func_in S
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g
be PartFunc of X,ExtREAL such that
A1: f is_simple_func_in S and
A4: g is_simple_func_in S;
g is real-valued by A4,MESFUNC2:def 4;
then
A8: dom (f+g) = dom f /\ dom g by MESFUNC2:2;
consider F be Finite_Sep_Sequence of S, a be FinSequence of ExtREAL such that
A10: F,a are_Re-presentation_of f by A1,MESFUNC3:12;
consider G be Finite_Sep_Sequence of S, b be FinSequence of ExtREAL such that
A9: G,b are_Re-presentation_of g by A4,MESFUNC3:12;
set la = len a;
set lb = len b;
A11: dom F = dom a & dom G= dom b by A9,A10,MESFUNC3:def 1;
deffunc FG1(Nat) = F.(($1-'1) div lb + 1) /\ G.(($1-'1) mod lb + 1);
consider FG be FinSequence such that
A12: len FG = la*lb and
A13: for k be Nat st k in dom FG holds FG.k=FG1(k) from FINSEQ_1:sch 2;
A14: dom FG = Seg(la*lb) by A12,FINSEQ_1:def 3;
now
let k be Nat;
assume k in dom FG; then
FG.k = F.((k-'1) div lb + 1) /\ G.((k-'1) mod lb + 1) by A13;
hence FG.k in S;
end;
then reconsider FG as FinSequence of S by FINSEQ_2:12;
for k,l be Nat st k in dom FG & l in dom FG & k <> l holds FG.k misses FG.l
proof
let k,l be Nat;
assume that
A25: k in dom FG and
A26: l in dom FG and
A27: k <> l;
set m=(l-'1) mod lb + 1;
set n=(l-'1) div lb + 1;
set j=(k-'1) mod lb + 1;
set i=(k-'1) div lb + 1;
A29: FG.k = F.i /\ G.j by A13,A25;
A30: k in Seg (la*lb) by A12,A25,FINSEQ_1:def 3;
A31: 1 <= k & k <= la*lb & 1 <= l & l <= la*lb by A12,A25,A26,FINSEQ_3:25;
then
A33: lb divides (la*lb) & 1 <= la*lb by NAT_D:def 3,XXREAL_0:2;
A34: lb <> 0 by A30;
then lb >= 1 by NAT_1:14; then
A35: ((la*lb) -' 1) div lb = ((la*lb) div lb) - 1 by A33,NAT_2:15;
(k -' 1) <= (la*lb -' 1) by A31,NAT_D:42;
then (k -' 1) div lb <= (la*lb div lb) - 1 by A35,NAT_2:24;
then i <= la*lb div lb by XREAL_1:19;
then i <= la by A34,NAT_D:18; then
A37: i in dom F by A11,NAT_1:11,FINSEQ_3:25;
m <= lb & j <= lb by A34,NAT_D:1,NAT_1:13; then
A42: m in dom G & j in dom G by A11,NAT_1:11,FINSEQ_3:25;
(l -' 1) <= (la*lb -' 1) by A31,NAT_D:42;
then (l -' 1) div lb <= (la*lb div lb) - 1 by A35,NAT_2:24;
then n <= la*lb div lb by XREAL_1:19;
then n <= la by A34,NAT_D:18; then
A44: n in dom F by A11,NAT_1:11,FINSEQ_3:25;
(l-'1)+1=(n-1)*lb+(m-1)+1 by A34,NAT_D:2;
then
A40: l - 1 + 1 = (n-1)*lb+m by A31,XREAL_1:233;
(k-'1)+1=(i-1)*lb+(j-1)+1 by A34,NAT_D:2; then
A41: k - 1 + 1 = (i-1)*lb + j by A31,XREAL_1:233;
per cases by A27,A40,A41;
suppose
i <> n; then
A45: F.i misses F.n by A37,A44,MESFUNC3:4;
FG.k /\ FG.l= (F.i /\ G.j) /\ (F.n /\ G.m) by A13,A26,A29
.= F.i /\ (G.j /\ (F.n /\ G.m)) by XBOOLE_1:16
.= F.i /\ (F.n /\ (G.j /\ G.m)) by XBOOLE_1:16
.= (F.i /\ F.n) /\ (G.j /\ G.m) by XBOOLE_1:16
.= {} by A45;
hence thesis;
end;
suppose
j <> m; then
A46: G.j misses G.m by A42,MESFUNC3:4;
FG.k /\ FG.l= (F.i /\ G.j) /\ (F.n /\ G.m) by A13,A26,A29
.= F.i /\ (G.j /\ (F.n /\ G.m)) by XBOOLE_1:16
.= F.i /\ (F.n /\ (G.j /\ G.m)) by XBOOLE_1:16
.= {} by A46;
hence thesis;
end;
end;
then reconsider FG as Finite_Sep_Sequence of S by MESFUNC3:4;
A51: dom f = union rng F by A10,MESFUNC3:def 1;
A70: dom g = union rng G by A9,MESFUNC3:def 1;
A71: dom (f+g) = union rng FG
proof
thus dom (f+g) c= union rng FG
proof
let z be object;
assume z in dom (f+g); then
A72: z in dom f & z in dom g by A8,XBOOLE_0:def 4;
then consider Y be set such that
A73: z in Y and
A74: Y in rng F by A51,TARSKI:def 4;
consider Z be set such that
A75: z in Z and
A76: Z in rng G by A70,A72,TARSKI:def 4;
consider j be object such that
A77: j in dom G and
A78: Z = G.j by A76,FUNCT_1:def 3;
reconsider j as Element of NAT by A77;
consider j9 being Nat such that
A81: j = 1 + j9 by A77,Lm2,FINSEQ_3:25;
consider i be object such that
A82: i in dom F and
A83: Y = F.i by A74,FUNCT_1:def 3;
reconsider i as Element of NAT by A82;
consider i9 being Nat such that
A85: i = 1 + i9 by A82,Lm2,FINSEQ_3:25;
A80: 1 <= j & j <= lb by A11,A77,FINSEQ_3:25; then
A87: j9 < lb by A81,NAT_1:13;
reconsider k = (i-1)*lb+j as Nat by A85;
A88: k >= 0 + j by A85,XREAL_1:6; then
A89: k -' 1 = k - 1 by A80,XREAL_1:233,XXREAL_0:2
.= i9*lb + j9 by A85,A81; then
A90: i = (k-'1) div lb +1 by A85,A87,NAT_D:def 1;
i <= la by A11,A82,FINSEQ_3:25;
then i-1 <= la-1 by XREAL_1:9;
then (i-1)*lb <= (la - 1)*lb by XREAL_1:64; then
A91: k <= (la - 1) * lb + j by XREAL_1:6;
(la - 1) * lb + j <= (la - 1) * lb + lb by A80,XREAL_1:6; then
A92: k <= la*lb by A91,XXREAL_0:2;
B1: k >= 1 by A80,A88,XXREAL_0:2; then
A93: k in Seg (la*lb) by A92;
k in dom FG by A12,B1,A92,FINSEQ_3:25; then
A94: FG.k in rng FG by FUNCT_1:def 3;
A95: j = (k-'1) mod lb +1 by A81,A89,A87,NAT_D:def 2;
z in F.i /\ G.j by A73,A83,A75,A78,XBOOLE_0:def 4;
then z in FG.k by A13,A14,A90,A95,A93;
hence thesis by A94,TARSKI:def 4;
end;
let z be object;
assume z in union rng FG;
then consider Y be set such that
A96: z in Y and
A97: Y in rng FG by TARSKI:def 4;
consider k be object such that
A98: k in dom FG and
A99: Y = FG.k by A97,FUNCT_1:def 3;
reconsider k as Element of NAT by A98;
set j=(k-'1) mod lb +1;
set i=(k-'1) div lb +1;
FG.k=F.i /\ G.j by A13,A98; then
A100: z in F.i & z in G.j by A96,A99,XBOOLE_0:def 4;
A102: 1 <= k & k <= la*lb by A12,A98,FINSEQ_3:25;
A103: lb <> 0 by A102; then
A104: lb >= 1 by NAT_1:14;
lb divides (la*lb) & 1 <= la*lb by A102,NAT_D:def 3,XXREAL_0:2; then
A105: ((la*lb) -' 1) div lb = ((la*lb) div lb) - 1 by A104,NAT_2:15;
A106: la*lb div lb = la by A103,NAT_D:18;
(k -' 1) <= (la*lb -' 1) by A102,NAT_D:42;
then (k -' 1) div lb <= (la*lb div lb) - 1 by A105,NAT_2:24;
then i <= la*lb div lb by XREAL_1:19;
then i in dom F by A11,A106,NAT_1:11,FINSEQ_3:25;
then F.i in rng F by FUNCT_1:def 3; then
a107: z in dom f by A51,A100,TARSKI:def 4;
1 <= j <= lb by A103,NAT_D:1,NAT_1:11,13;
then j in dom G by A11,FINSEQ_3:25;
then G.j in rng G by FUNCT_1:def 3;
then z in dom g by A70,A100,TARSKI:def 4;
hence thesis by A8,a107,XBOOLE_0:def 4;
end;
A107: for k being Nat,x,y being Element of X st k in dom FG & x in FG.k & y
in FG.k holds (f+g).x = (f+g).y
proof
let k be Nat;
let x,y be Element of X;
assume that
A108: k in dom FG and
A109: x in FG.k & y in FG.k;
set i=(k-'1) div lb + 1;
set j=(k-'1) mod lb + 1;
A110: i >= 1 & j >= 1 by NAT_1:11;
FG.k = F.i /\ G.j by A13,A108; then
A112: x in F.i & x in G.j & y in F.i & y in G.j by A109,XBOOLE_0:def 4;
A113: 1 <= k & k <= la*lb by A12,A108,FINSEQ_3:25; then
A115: (k -' 1) <= (la*lb -' 1) by NAT_D:42;
A116: lb divides (la*lb) & 1 <= la*lb by A113,NAT_D:def 3,XXREAL_0:2;
A117: lb <> 0 by A113;
then lb >= 1 by NAT_1:14;
then ((la*lb) -' 1) div lb = ((la*lb) div lb) - 1 by A116,NAT_2:15;
then (k -' 1) div lb <= (la*lb div lb) - 1 by A115,NAT_2:24;
then i <= la*lb div lb by XREAL_1:19;
then i <= la by A117,NAT_D:18; then
A119: f.x=a.i & f.y = a.i by A10,A11,A110,A112,FINSEQ_3:25,MESFUNC3:def 1;
A120: j <= lb by A117,NAT_D:1,NAT_1:13;
FG.k in rng FG by A108,FUNCT_1:def 3; then
A124: x in dom (f+g) & y in dom (f+g) by A71,A109,TARSKI:def 4;
hence (f+g).x= f.x+g.x by MESFUNC1:def 3
.= a.i+b.j by A9,A11,A110,A120,A112,A119,FINSEQ_3:25,MESFUNC3:def 1
.= f.y+g.y by A9,A11,A110,A120,A112,A119,FINSEQ_3:25,MESFUNC3:def 1
.= (f+g).y by A124,MESFUNC1:def 3;
end;
now
let x be Element of X;
assume
A188: x in dom (f+g);
then |. (f+g).x .| = |. f.x + g.x .| by MESFUNC1:def 3; then
A189: |. (f+g).x .| <= |. f.x .| + |. g.x .| by EXTREAL1:24;
x in dom f & x in dom g by A188,A8,XBOOLE_0:def 4; then
|. f.x .| < +infty & |. g.x .| < +infty
by A1,A4,MESFUNC2:def 1,def 4;
then |. f.x .| + |. g.x .| <> +infty by XXREAL_3:16;
hence |. (f+g).x .| < +infty by A189,XXREAL_0:2,4;
end;
hence f+g is_simple_func_in S by A71,A107,MESFUNC2:def 1,def 4;
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,ExtREAL st f is_simple_func_in S &
g is_simple_func_in S holds f-g is_simple_func_in S
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S, f,g
be PartFunc of X,ExtREAL such that
A1: f is_simple_func_in S and
A4: g is_simple_func_in S;
(-1)(#)g is_simple_func_in S by A4,MESFUNC5:39; then
-g is_simple_func_in S by MESFUNC2:9; then
f+(-g) is_simple_func_in S by A1,Th28; then
-(g-f) is_simple_func_in S by MEASUR11:64;
hence f-g is_simple_func_in S by MEASUR11:64;
end;
theorem Th30:
for X be non empty set, S be SigmaField of X, f be PartFunc of X,ExtREAL
st f is_simple_func_in S holds -f is_simple_func_in S
proof
let X be non empty set, S be SigmaField of X, f be PartFunc of X,ExtREAL;
assume A1:f is_simple_func_in S;
-f = (-1)(#)f by MESFUNC2:9;
hence -f is_simple_func_in S by A1,MESFUNC5:39;
end;
theorem
for X be non empty set, f be nonnegative PartFunc of X,ExtREAL holds f = max+f
proof
let X be non empty set, f be nonnegative PartFunc of X,ExtREAL;
b3:dom f = dom(max+f) by MESFUNC2:def 2;
for x be Element of X st x in dom f holds f.x = (max+f).x
proof
let x be Element of X;
assume b2: x in dom f;
max(f.x,0) = f.x by SUPINF_2:51,XXREAL_0:def 10;
hence f.x = (max+f).x by b2,b3,MESFUNC2:def 2;
end;
hence f = max+f by b3,PARTFUN1:5;
end;
theorem Th32:
for X be non empty set, f be nonpositive PartFunc of X,ExtREAL
holds f = -(max-f)
proof
let X be non empty set, f be nonpositive PartFunc of X,ExtREAL;
b1:dom f = dom(max-f) by MESFUNC2:def 3 .= dom(-(max-f)) by MESFUNC1:def 7;
b3:dom f = dom(max+f) by MESFUNC2:def 2;
for x be Element of X st x in dom f holds f.x = (-(max-f)).x
proof
let x be Element of X;
assume b2: x in dom f;
max(f.x,0) = 0 by MESFUNC5:8,XXREAL_0:def 10; then
(max+f).x = 0 by b2,b3,MESFUNC2:def 2; then
(max-f).x = -(f.x) by b2,MESFUNC2:20; then
f.x = -(max-f).x;
hence f.x = (-(max-f)).x by b1,b2,MESFUNC1:def 7;
end;
hence f = -(max-f) by b1,PARTFUN1:5;
end;
theorem Th33:
for C being non empty set, f being PartFunc of C,ExtREAL, c be
Real st c <= 0 holds max+(c(#)f) = (-c)(#)max-f & max-(c(#)f) = (-c)(#)max+f
proof
let C be non empty set;
let f be PartFunc of C,ExtREAL;
let c be Real;
assume
A1: c <= 0;
A2: dom max+(c(#)f) = dom(c(#)f) by MESFUNC2:def 2
.= dom f by MESFUNC1:def 6
.= dom max-f by MESFUNC2:def 3
.= dom((-c)(#)max-f) by MESFUNC1:def 6;
for x be Element of C st x in dom max+(c(#)f) holds
(max+(c(#)f)).x = ((-c)(#)max-f).x
proof
let x be Element of C;
assume
A3: x in dom max+(c(#)f); then
A4: x in dom(c(#)f) by MESFUNC2:def 2;
then x in dom f by MESFUNC1:def 6; then
A5: x in dom max- f by MESFUNC2:def 3;
A6: (max+(c(#)f)).x = max((c(#)f).x,0) by A3,MESFUNC2:def 2
.= max( c * f.x,0) by A4,MESFUNC1:def 6;
B1: ((-c)(#)max-f).x = (-c) * max-f.x by A2,A3,MESFUNC1:def 6
.= (-c) * max(-(f.x),0) by A5,MESFUNC2:def 3;
per cases;
suppose f.x >= 0; then
(max+(c(#)f)).x = 0 & max(-(f.x),0) = 0 by A1,A6,XXREAL_0:def 10;
hence thesis by B1;
end;
suppose D1: f.x < 0; then
B2: (max+(c(#)f)).x = c * f.x & max(-(f.x),0) = -(f.x)
by A1,A6,XXREAL_0:def 10;
per cases by D1,XXREAL_0:14;
suppose E1: f.x = -infty;
per cases by A1;
suppose c = 0; then
(max+(c(#)f)).x = 0 & ((-c)(#)max-f).x = 0
by B1,A6,XXREAL_0:def 10;
hence thesis;
end;
suppose F1: c < 0; then
(-c) * (-(f.x)) = +infty by E1,XXREAL_3:5,def 5;
hence thesis by B1,B2,E1,F1,XXREAL_3:def 5;
end;
end;
suppose f.x in REAL; then
reconsider a = f.x as Real;
(-c) * (-a) = (-c) * (-(f.x)); then
(-c) * (-(f.x)) = c * a .= c * f.x;
hence thesis by B1,B2;
end;
end;
end;
hence max+(c(#)f) = (-c)(#)max-f by A2,PARTFUN1:5;
A7: dom(max-(c(#)f)) = dom(c(#)f) by MESFUNC2:def 3
.= dom f by MESFUNC1:def 6
.= dom max+f by MESFUNC2:def 2
.= dom((-c)(#)max+f) by MESFUNC1:def 6;
for x be Element of C st x in dom max-(c(#)f) holds (max-(c(#)f)).x = (
(-c)(#)max+f).x
proof
let x be Element of C;
assume
A8: x in dom max-(c(#)f);
then
A9: x in dom(c(#)f) by MESFUNC2:def 3;
then x in dom f by MESFUNC1:def 6;
then
A10: x in dom max+ f by MESFUNC2:def 2;
A11: (max-(c(#)f)).x = max(-(c(#)f).x,0) by A8,MESFUNC2:def 3
.= max(-( c)*f.x,0) by A9,MESFUNC1:def 6;
A12:((-c)(#)max+f).x = (-c) * max+f.x by A7,A8,MESFUNC1:def 6
.= (-c) * max(f.x,0) by A10,MESFUNC2:def 2
.= max((-c) * (f.x),(-c) * (0 qua ExtReal)) by A1,MESFUNC5:6
.= max((-c)*f.x, 0);
-(c) * f.x = (-c) * f.x
proof
per cases by XXREAL_0:14;
suppose E1: f.x = +infty;
per cases by A1;
suppose c = 0; then
c * f.x = 0 & (-c) * f.x = 0;
hence -(c) * f.x = (-c) * f.x;
end;
suppose E2: c < 0; then
c * f.x = -infty by E1,XXREAL_3:def 5;
hence -(c) * f.x = (-c) * f.x by E1,E2,XXREAL_3:5,def 5;
end;
end;
suppose E1: f.x = -infty;
per cases by A1;
suppose c = 0; then
c * f.x = 0 & (-c) * f.x = 0;
hence -(c) * f.x = (-c) * f.x;
end;
suppose E2: c < 0; then
c * f.x = +infty by E1,XXREAL_3:def 5;
hence -(c) * f.x = (-c) * f.x by E1,E2,XXREAL_3:6,def 5;
end;
end;
suppose f.x in REAL; then
reconsider a = f.x as Real;
(-c)*a = (-c)*f.x; then
(-c)*f.x = -(c * a);
hence -(c) * f.x = (-c) * f.x;
end;
end;
hence thesis by A11,A12;
end;
hence thesis by A7,PARTFUN1:5;
end;
theorem Th34:
for X be non empty set, f be PartFunc of X,ExtREAL holds
max+f = max-(-f)
proof
let X be non empty set, f be PartFunc of X,ExtREAL;
-f = (-1)(#)f by MESFUNC2:9; then
max-(-f) = (- -1)(#)max+f by Th33;
hence thesis by MESFUNC2:1;
end;
theorem Th35:
for X be non empty set, f be PartFunc of X,ExtREAL, r1,r2 be Real
holds r1(#)(r2(#)f) = (r1*r2)(#)f
proof
let X be non empty set, f be PartFunc of X,ExtREAL, r1,r2 be Real;
A1:dom(r1(#)(r2(#)f)) = dom(r2(#)f) by MESFUNC1:def 6; then
A2:dom(r1(#)(r2(#)f)) = dom f by MESFUNC1:def 6;
A3:dom((r1*r2)(#)f) = dom f by MESFUNC1:def 6;
for x be Element of X st x in dom(r1(#)(r2(#)f)) holds
(r1(#)(r2(#)f)).x = ((r1*r2)(#)f).x
proof
let x be Element of X;
assume A4: x in dom(r1(#)(r2(#)f)); then
(r1(#)(r2(#)f)).x = r1 * (r2(#)f).x by MESFUNC1:def 6; then
A5: (r1(#)(r2(#)f)).x = r1 * (r2 * f.x) by A1,A4,MESFUNC1:def 6;
((r1*r2)(#)f).x = (r1*r2)*f.x by A2,A3,A4,MESFUNC1:def 6;
hence thesis by A5,XXREAL_3:66;
end;
hence r1(#)(r2(#)f) = (r1*r2)(#)f by A2,A3,PARTFUN1:5;
end;
theorem Th36:
for X be non empty set, f,g be PartFunc of X,ExtREAL st f = -g holds g = -f
proof
let X be non empty set, f,g be PartFunc of X,ExtREAL;
assume f = -g; then
f = (-1)(#)g by MESFUNC2:9; then
-f = (-1)(#)((-1)(#)g) by MESFUNC2:9; then
-f = ((-1)*(-1))(#)g by Th35;
hence g = -f by MESFUNC2:1;
end;
definition
let X be non empty set;
let F be Functional_Sequence of X,ExtREAL;
let r be Real;
func r(#)F -> Functional_Sequence of X,ExtREAL means :Def1:
for n being Nat holds it.n = r(#)(F.n);
existence
proof
deffunc U(Nat) = r(#)(F.$1);
thus ex f being Functional_Sequence of X,ExtREAL st
for n being Nat holds f.n = U(n) from SEQFUNC:sch 1;
end;
uniqueness
proof
let H1,H2 be Functional_Sequence of X,ExtREAL such that
A1: for n being Nat holds H1.n=r(#)(F.n) and
A2: for n being Nat holds H2.n=r(#)(F.n);
now
let n be Element of NAT;
H1.n=r(#)(F.n) by A1;
hence H1.n=H2.n by A2;
end;
hence H1=H2 by FUNCT_2:63;
end;
end;
definition
let X be non empty set;
let F be Functional_Sequence of X,ExtREAL;
func -F -> Functional_Sequence of X,ExtREAL equals
(-1)(#)F;
correctness;
end;
theorem Th37:
for X be non empty set, F be Functional_Sequence of X,ExtREAL, n be Nat
holds (-F).n = -(F.n)
proof
let X be non empty set, F be Functional_Sequence of X,ExtREAL, n be Nat;
thus (-F).n = (-1)(#)(F.n) by Def1 .= -(F.n) by MESFUNC2:9;
end;
theorem Th38:
for X be non empty set, F be Functional_Sequence of X,ExtREAL,
x be Element of X holds (-F)#x = -(F#x)
proof
let X be non empty set, F be Functional_Sequence of X,ExtREAL,
x be Element of X;
now let n be Element of NAT;
A1: dom(-(F#x)) = NAT by FUNCT_2:def 1;
A2: ((-F)#x).n = ((-F).n).x by MESFUNC5:def 13
.= (-(F.n)).x by Th37;
A3: (-(F#x)).n = -((F#x).n) by A1,MESFUNC1:def 7
.= -((F.n).x) by MESFUNC5:def 13;
A4: dom(F.n) = dom(-(F.n)) by MESFUNC1:def 7;
per cases;
suppose x in dom(F.n);
hence ((-F)#x).n = (-(F#x)).n by A3,A2,A4,MESFUNC1:def 7;
end;
suppose A5: not x in dom(F.n); then
A6: not x in dom(-(F.n)) by MESFUNC1:def 7;
(-(F#x)).n = -0 by A3,A5,FUNCT_1:def 2;
hence ((-F)#x).n = (-(F#x)).n by A6,A2,FUNCT_1:def 2;
end;
end;
hence (-F)#x = -(F#x) by FUNCT_2:def 8;
end;
theorem Th39:
for X be non empty set, F be Functional_Sequence of X,ExtREAL,
x be Element of X holds
(F#x is convergent_to_+infty iff (-F)#x is convergent_to_-infty) &
(F#x is convergent_to_-infty iff (-F)#x is convergent_to_+infty) &
(F#x is convergent_to_finite_number
iff (-F)#x is convergent_to_finite_number) &
(F#x is convergent iff (-F)#x is convergent) &
(F#x is convergent implies lim((-F)#x) = - lim(F#x))
proof
let X be non empty set, F be Functional_Sequence of X,ExtREAL,
x be Element of X;
A1: F#x is convergent_to_+infty implies
-(F#x) is convergent_to_-infty by DBLSEQ_3:17;
-(F#x) is convergent_to_-infty implies
-(-(F#x)) is convergent_to_+infty by DBLSEQ_3:17;
hence A2: F#x is convergent_to_+infty
iff (-F)#x is convergent_to_-infty by A1,DBLSEQ_3:2,Th38;
A3: F#x is convergent_to_-infty implies
-(F#x) is convergent_to_+infty by DBLSEQ_3:17;
-(F#x) is convergent_to_+infty implies
-(-(F#x)) is convergent_to_-infty by DBLSEQ_3:17;
hence A4: F#x is convergent_to_-infty
iff (-F)#x is convergent_to_+infty by A3,DBLSEQ_3:2,Th38;
A5: F#x is convergent_to_finite_number implies
-(F#x) is convergent_to_finite_number by DBLSEQ_3:17;
-(F#x) is convergent_to_finite_number implies
-(-(F#x)) is convergent_to_finite_number by DBLSEQ_3:17;
hence A6: F#x is convergent_to_finite_number
iff (-F)#x is convergent_to_finite_number by A5,Th38,DBLSEQ_3:2;
thus F#x is convergent iff (-F)#x is convergent
by A2,A4,A6,MESFUNC5:def 11;
hereby assume F#x is convergent; then
lim (-(F#x)) = - lim(F#x) by DBLSEQ_3:17;
hence lim((-F)#x) = - lim(F#x) by Th38;
end;
end;
theorem Th40:
for X be non empty set, F be Functional_Sequence of X,ExtREAL
st F is with_the_same_dom holds -F is with_the_same_dom
proof
let X be non empty set, F be Functional_Sequence of X,ExtREAL;
assume A1: F is with_the_same_dom;
now let n,m be Nat;
(-F).n = -(F.n) & (-F).m = -(F.m) by Th37; then
dom((-F).n) = dom(F.n) & dom((-F).m) = dom(F.m) by MESFUNC1:def 7;
hence dom((-F).n) = dom((-F).m) by A1,MESFUNC8:def 2;
end;
hence -F is with_the_same_dom by MESFUNC8:def 2;
end;
theorem Th41:
for X be non empty set, F be Functional_Sequence of X,ExtREAL
st F is additive holds -F is additive
proof
let X be non empty set, F be Functional_Sequence of X,ExtREAL;
assume A1: F is additive;
now let n,m be Nat;
assume n <> m;
let x be set;
assume x in dom((-F).n) /\ dom((-F).m); then
x in dom(-(F.n)) /\ dom((-F).m) by Th37; then
A3: x in dom(-(F.n)) /\ dom(-(F.m)) by Th37; then
x in dom(-(F.n)) & x in dom(-(F.m)) by XBOOLE_0:def 4; then
(-(F.n)).x = -((F.n).x) & (-(F.m)).x = -((F.m).x)
by MESFUNC1:def 7; then
A4: ((-F).n).x = -((F.n).x) & ((-F).m).x = -((F.m).x) by Th37;
x in dom(F.n) /\ dom(-(F.m)) by A3,MESFUNC1:def 7; then
x in dom(F.n) /\ dom(F.m) by MESFUNC1:def 7;
hence ((-F).n).x <> +infty or ((-F).m).x <> -infty
by A4,XXREAL_3:6,A1,MESFUNC9:def 5;
end;
hence -F is additive by MESFUNC9:def 5;
end;
theorem Th42:
for X be non empty set, F be Functional_Sequence of X,ExtREAL, n be Nat
holds (Partial_Sums(-F)).n = (-(Partial_Sums F)).n
proof
let X be non empty set, F be Functional_Sequence of X,ExtREAL, n be Nat;
defpred P[Nat] means (Partial_Sums(-F)).$1 = (-(Partial_Sums F)).$1;
(Partial_Sums(-F)).0 = (-F).0 by MESFUNC9:def 4
.= -(F.0) by Th37 .= -((Partial_Sums F).0) by MESFUNC9:def 4; then
A1: P[0] by Th37;
A2: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A3: P[k];
(Partial_Sums(-F)).(k+1)
= (Partial_Sums(-F)).k + (-F).(k+1) by MESFUNC9:def 4
.= (-(Partial_Sums F)).k + -(F.(k+1)) by A3,Th37
.= -((Partial_Sums F).k) + -(F.(k+1)) by Th37
.= -((Partial_Sums F).k + F.(k+1)) by MEASUR11:64
.= -((Partial_Sums F).(k+1)) by MESFUNC9:def 4;
hence P[k+1] by Th37;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A1,A2);
hence (Partial_Sums(-F)).n = (-(Partial_Sums F)).n;
end;
theorem Th43:
for seq be ExtREAL_sequence, n be Nat holds
(Partial_Sums(-seq)).n = -((Partial_Sums seq).n)
proof
let seq be ExtREAL_sequence, n be Nat;
defpred P[Nat] means (Partial_Sums(-seq)).$1 = -((Partial_Sums seq).$1);
A1: dom(-seq) = NAT by FUNCT_2:def 1;
(Partial_Sums(-seq)).0 = (-seq).0 by MESFUNC9:def 1
.= -(seq.0) by A1,MESFUNC1:def 7; then
A3: P[0] by MESFUNC9:def 1;
A4: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume A5: P[k];
(Partial_Sums(-seq)).(k+1)
= (Partial_Sums(-seq)).k + (-seq).(k+1) by MESFUNC9:def 1
.= -((Partial_Sums seq).k) + -(seq.(k+1)) by A1,A5,MESFUNC1:def 7
.= -((Partial_Sums seq).k + seq.(k+1)) by XXREAL_3:9;
hence P[k+1] by MESFUNC9:def 1;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A3,A4);
hence (Partial_Sums(-seq)).n = -((Partial_Sums seq).n);
end;
theorem Th44:
for seq be ExtREAL_sequence holds Partial_Sums(-seq) = -(Partial_Sums seq)
proof
let seq be ExtREAL_sequence;
now let n be Element of NAT;
A1: dom(-(Partial_Sums seq)) = NAT by FUNCT_2:def 1;
(Partial_Sums(-seq)).n = -((Partial_Sums seq).n) by Th43;
hence (Partial_Sums(-seq)).n = (-(Partial_Sums seq)).n
by A1,MESFUNC1:def 7;
end;
hence (Partial_Sums(-seq)) = -(Partial_Sums seq) by FUNCT_2:def 8;
end;
theorem Th45:
for seq be ExtREAL_sequence st seq is summable holds -seq is summable
proof
let seq be ExtREAL_sequence;
assume seq is summable; then
A1:Partial_Sums seq is convergent by MESFUNC9:def 2;
(Partial_Sums(-seq)) = -(Partial_Sums seq) by Th44;
hence -seq is summable by A1,DBLSEQ_3:17,MESFUNC9:def 2;
end;
theorem Th46:
for X be non empty set, F be Functional_Sequence of X,ExtREAL
st (for n be Nat holds F.n is without+infty) holds F is additive
proof
let X be non empty set, F be Functional_Sequence of X,ExtREAL;
assume for n be Nat holds F.n is without+infty; then
for n,m be Nat st n <> m for x be set st x in dom(F.n) /\ dom(F.m)
holds (F.n).x <> +infty or (F.m).x <> -infty by MESFUNC5:def 6;
hence F is additive by MESFUNC9:def 5;
end;
theorem Th47:
for X be non empty set, F be Functional_Sequence of X,ExtREAL
st (for n be Nat holds F.n is without-infty) holds F is additive
proof
let X be non empty set, F be Functional_Sequence of X,ExtREAL;
assume for n be Nat holds F.n is without-infty; then
for n,m be Nat st n <> m for x be set st x in dom(F.n)/\dom(F.m)
holds (F.n).x <> +infty or (F.m).x <> -infty by MESFUNC5:def 5;
hence F is additive by MESFUNC9:def 5;
end;
theorem Th48:
for X be non empty set, F be Functional_Sequence of X,ExtREAL,
x be Element of X st F#x is summable holds
(-F)#x is summable & Sum((-F)#x) = -Sum(F#x)
proof
let X be non empty set, F be Functional_Sequence of X,ExtREAL,
x be Element of X;
assume A1: F#x is summable; then
-(F#x) is summable by Th45;
hence (-F)#x is summable by Th38;
A2: -(F#x) = (-F)#x by Th38;
Partial_Sums(F#x) is convergent by A1,MESFUNC9:def 2; then
lim -(Partial_Sums(F#x)) = - lim Partial_Sums(F#x) by DBLSEQ_3:17; then
lim Partial_Sums(-(F#x)) = - lim Partial_Sums(F#x) by Th44; then
lim Partial_Sums((-F)#x) = - Sum (F#x) by A2,MESFUNC9:def 3;
hence Sum((-F)#x) = -Sum(F#x) by MESFUNC9:def 3;
end;
theorem Th49:
for X be non empty set, S be SigmaField of X,
F be Functional_Sequence of X,ExtREAL st
F is additive & F is with_the_same_dom &
(for x be Element of X st x in dom(F.0) holds F#x is summable)
holds lim Partial_Sums (-F) = -(lim Partial_Sums F)
proof
let X be non empty set, S be SigmaField of X,
F be Functional_Sequence of X,ExtREAL;
assume that
A1: F is additive and
A2: F is with_the_same_dom and
A3: for x be Element of X st x in dom(F.0) holds F#x is summable;
set G = -F;
for n be Element of NAT holds (Partial_Sums G).n = (-(Partial_Sums F)).n
by Th42; then
A4: Partial_Sums G = -(Partial_Sums F) by FUNCT_2:def 7;
A5: dom(lim Partial_Sums G) = dom((Partial_Sums G).0) by MESFUNC8:def 9
.= dom(G.0) by MESFUNC9:def 4 .= dom(-(F.0)) by Th37
.= dom(F.0) by MESFUNC1:def 7;
A6: dom(-(lim Partial_Sums F)) = dom(lim Partial_Sums F) by MESFUNC1:def 7;
then
A7: dom(-(lim Partial_Sums F)) = dom((Partial_Sums F).0) by MESFUNC8:def 9
.= dom(F.0) by MESFUNC9:def 4;
for x be Element of X st x in dom(lim Partial_Sums G) holds
(lim Partial_Sums G).x = (-(lim Partial_Sums F)).x
proof
let x be Element of X;
assume A8: x in dom(lim Partial_Sums G); then
F#x is summable by A3,A5; then
Partial_Sums(F#x) is convergent by MESFUNC9:def 2; then
A9: (Partial_Sums F)#x is convergent by A1,A2,A8,A5,MESFUNC9:33;
(Partial_Sums G)#x = -((Partial_Sums F)#x) by A4,Th38; then
A10: lim((Partial_Sums G)#x) = - lim((Partial_Sums F)#x)
by A9,DBLSEQ_3:17;
(-(lim Partial_Sums F)).x = -( (lim Partial_Sums F).x)
by A7,A5,A8,MESFUNC1:def 7; then
(-(lim Partial_Sums F)).x = -( lim((Partial_Sums F)#x) )
by A7,A5,A8,A6,MESFUNC8:def 9;
hence (lim Partial_Sums G).x = (-(lim Partial_Sums F)).x
by A8,A10,MESFUNC8:def 9;
end;
hence lim Partial_Sums G = -(lim Partial_Sums F) by A7,A5,PARTFUN1:5;
end;
theorem Th50:
for X be non empty set, S be SigmaField of X,
F,G be Functional_Sequence of X,ExtREAL, E be Element of S
st E c= dom(F.0) & F is additive & F is with_the_same_dom
& (for n be Nat holds G.n = (F.n)|E)
holds lim(Partial_Sums G) = (lim(Partial_Sums F))|E
proof
let X be non empty set, S be SigmaField of X,
F,G be Functional_Sequence of X,ExtREAL, E be Element of S;
assume that
A1: E c= dom(F.0) and
A2: F is additive and
A3: F is with_the_same_dom and
A5: for n be Nat holds G.n = (F.n)|E;
A6: G is additive with_the_same_dom Functional_Sequence of X,ExtREAL
by A2,A3,A5,MESFUNC9:18,31;
dom((F.0)|E) = E by A1,RELAT_1:62; then
A8: E = dom(G.0) by A5;
A9: for x be Element of X st x in E holds F#x = G#x
proof
let x be Element of X;
assume
A10: x in E;
for n be Element of NAT holds (F#x).n = (G#x).n
proof
let n be Element of NAT;
dom(G.n) = E by A8,MESFUNC8:def 2,A3,A5,MESFUNC9:18;
then x in dom((F.n)|E) by A5,A10;
then ((F.n)|E).x = (F.n).x by FUNCT_1:47;
then
A11: (G.n).x = (F.n).x by A5;
(F#x).n = (F.n).x by MESFUNC5:def 13;
hence thesis by A11,MESFUNC5:def 13;
end;
hence thesis by FUNCT_2:def 7;
end;
set E1 = dom(F.0);
set PF = Partial_Sums F;
set PG = Partial_Sums G;
A13: dom(lim PG) = dom(PG.0) by MESFUNC8:def 9;
dom(PF.0) = E1 by A2,A3,MESFUNC9:29;
then
A14: E c= dom(lim(PF)) by A1,MESFUNC8:def 9;
A15: for x being Element of X st x in dom(lim PG) holds (lim PG).x = (lim PF).x
proof
let x be Element of X;
set PFx = Partial_Sums(F#x);
set PGx = Partial_Sums(G#x);
assume
A16: x in dom(lim PG); then
x in dom(G.0) by A6,A13,MESFUNC9:29; then
x in dom((F.0)|E) by A5;
then
A17: x in E by A1,RELAT_1:62;
for n be Element of NAT holds (PG#x).n = (PF#x).n
proof
let n be Element of NAT;
A18: PGx.n = (PG#x).n by A6,A8,A17,MESFUNC9:32;
PFx.n = (PF#x).n by A1,A2,A3,A17,MESFUNC9:32;
hence thesis by A9,A17,A18;
end;
then
A19: lim(PG#x) = lim(PF#x) by FUNCT_2:63;
(lim PG).x = lim(PG#x) by A16,MESFUNC8:def 9;
hence thesis by A14,A17,A19,MESFUNC8:def 9;
end;
A20: dom(PG.0) = dom(G.0) by A6,MESFUNC9:29;
A22: dom((lim PF)|E) = E by A14,RELAT_1:62;
for x be Element of X st x in dom((lim PG)|E) holds ((lim PG)|E).x =
((lim PF)|E).x
proof
let x be Element of X;
assume
A24: x in dom((lim PG)|E);
then ((lim PF)|E).x = (lim PF).x by A8,A13,A20,A22,FUNCT_1:47;
hence thesis by A8,A13,A20,A15,A24;
end;
hence thesis by A8,A20,A13,A22,PARTFUN1:5;
end;
begin :: Integral of non positive measurable functions
theorem
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be nonnegative PartFunc of X, ExtREAL
holds integral'(M,max-(-f)) = integral'(M,f)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be nonnegative PartFunc of X, ExtREAL;
-f = -(max-(-f)) by Th32; then
f = -(-max-(-f)) by Th36; then
f = (-1)(#)(-max-(-f)) by MESFUNC2:9; then
f = (-1)(#)((-1)(#)(max-(-f))) by MESFUNC2:9; then
f = ((-1)*(-1))(#)(max-(-f)) by Th35;
hence integral'(M,max-(-f)) = integral'(M,f) by MESFUNC2:1;
end;
theorem Th52:
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 A = dom f & f is A-measurable holds Integral(M,-f) = - Integral(M,f)
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: A = dom f and
A2: f is A-measurable;
set g = -f;
A4: f = -g by Th36;
B6: dom(max-f) = A & dom(max+f) = A by A1,MESFUNC2:def 2,def 3;
B7: max-f is A-measurable & max+f is A-measurable by A1,A2,Th10;
A6: dom g = A by A1,MESFUNC1:def 7; then
A7: dom(max+g) = A & dom(max-g) = A by MESFUNC2:def 2,def 3;
g is A-measurable by A1,A2,MEASUR11:63; then
A9: max+g is A-measurable & max-g is A-measurable by A6,Th10; then
P1: integral+(M,max+g) = Integral(M,max+g) by A7,Th5,MESFUNC5:88
.= Integral(M,max-(-g)) by Th34
.= integral+(M,max-f) by A4,B6,B7,Th5,MESFUNC5:88;
integral+(M,max-g) = Integral(M,max-g) by A7,A9,Th5,MESFUNC5:88
.= Integral(M,max+(-g)) by MESFUNC2:14
.= integral+(M,max+f) by A4,B6,B7,Th5,MESFUNC5:88; then
Integral(M,f)
= integral+(M,max-g) - integral+(M,max+g) by P1,MESFUNC5:def 16
.= -(integral+(M,max+g) - integral+(M,max-g)) by XXREAL_3:26;
hence thesis by MESFUNC5:def 16;
end;
theorem
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be nonnegative PartFunc of X,ExtREAL, E be Element of S
st E = dom f & f is E-measurable
holds Integral(M,max-f) = 0 & integral+(M,max-f) = 0
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be nonnegative PartFunc of X,ExtREAL, E be Element of S;
assume that
A1: E = dom f and
A2: f is E-measurable;
A3: E = dom(max-f) by A1,MESFUNC2:def 3;
A4: max-f is E-measurable by A1,A2,Th10;
for x be object st x in dom(max-f) holds (max-f).x = 0
proof
let x be object;
assume A5: x in dom(max-f); then
A6: x in dom(max+f) by A1,A3,MESFUNC2:def 2;
per cases by SUPINF_2:51;
suppose f.x = 0; then
(max+f).x = f.x by A5,MESFUNC2:18;
hence (max-f).x = 0 by A5,MESFUNC2:19;
end;
suppose f.x > 0; then
max(f.x,0) = f.x by XXREAL_0:def 10; then
(max+f).x = f.x by A6,MESFUNC2:def 2;
hence (max-f).x = 0 by A5,MESFUNC2:19;
end;
end;
hence Integral(M,max-f) = 0 * M.(dom(max-f)) by A3,MEASUR10:27 .= 0;
hence integral+(M,max-f) = 0 by A3,A4,Th5,MESFUNC5:88;
end;
theorem
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, E be Element of S
st E = dom f & f is E-measurable holds
Integral(M,f) = Integral(M,max+f) - Integral(M,max-f)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, E be Element of S;
assume that
A1: E = dom f and
A2: f is E-measurable;
A3: E = dom(max+f) & E = dom(max-f) by A1,MESFUNC2:def 2,def 3;
max+f is E-measurable & max-f is E-measurable by A1,A2,Th10; then
Integral(M,max+f) = integral+(M,max+f)
& Integral(M,max-f) = integral+(M,max-f) by A3,Th5,MESFUNC5:88;
hence Integral(M,f) = Integral(M,max+f) - Integral(M,max-f)
by MESFUNC5:def 16;
end;
theorem Th55:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, E be Element of S
st E c= dom f & f is E-measurable holds
Integral(M,(-f)|E) = - Integral(M,f|E)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, E be Element of S;
assume that
A1: E c= dom f and
A2: f is E-measurable;
A3: E = dom(f|E) by A1,RELAT_1:62; then
A4: E = dom f /\ E by RELAT_1:61;
(-f)|E = -(f|E) by Th3;
hence Integral(M,(-f)|E) = - Integral(M,f|E)
by A3,A4,A2,MESFUNC5:42,Th52;
end;
theorem Th56:
for X be non empty set, S be SigmaField of X, f be PartFunc of X,ExtREAL
st (ex A be Element of S st A = dom f & f is A-measurable)
& f qua ext-real-valued Function is nonpositive
ex F be Functional_Sequence of X,ExtREAL st (for n be Nat
holds F.n is_simple_func_in S & dom(F.n) = dom f) & (for n be Nat holds F.n is
nonpositive) & (for n,m be Nat st n <=m holds for x be Element of X st x in dom
f holds (F.n).x >= (F.m).x ) & for x be Element of X st x in dom f holds (F#x)
is convergent & lim(F#x) = f.x
proof
let X be non empty set, S be SigmaField of X, f be PartFunc of X,ExtREAL;
assume that
A1: ex A be Element of S st A = dom f & f is A-measurable and
A2: f qua ext-real-valued Function is nonpositive;
set g = -f;
consider A be Element of S such that
A3: A = dom f & f is A-measurable by A1;
A4: A = dom g by A3,MESFUNC1:def 7; then
consider G be Functional_Sequence of X,ExtREAL such that
A6: (for n be Nat holds G.n is_simple_func_in S & dom(G.n) = dom g)
& (for n be Nat holds G.n is nonnegative)
& (for n,m be Nat st n <=m holds
for x be Element of X st x in dom g holds
(G.n).x <= (G.m).x )
& for x be Element of X st x in dom g holds (G#x) is convergent
& lim(G#x) = g.x by A2,A3,MEASUR11:63,MESFUNC5:64;
take F=-G;
thus
A8: for n be Nat holds F.n is_simple_func_in S & dom(F.n) = dom f
proof
let n be Nat;
A9: dom(G.n) = dom g by A6;
A10: F.n = -(G.n) by Th37;
hence F.n is_simple_func_in S by A6,Th30;
thus dom(F.n) = dom f by A3,A4,A9,A10,MESFUNC1:def 7;
end;
thus for n be Nat holds F.n is nonpositive
proof
let n be Nat;
A12: G.n is nonnegative by A6;
F.n = -(G.n) by Th37;
hence F.n is nonpositive by A12;
end;
thus for n,m be Nat st n <=m holds
for x be Element of X st x in dom f holds (F.n).x >= (F.m).x
proof
let n,m be Nat;
assume A14: n <= m;
let x be Element of X;
assume A15: x in dom f;
dom(F.n) = dom f & F.n = -(G.n)
& dom(F.m) = dom f & F.m = -(G.m) by A8,Th37; then
(F.n).x = -((G.n).x) & (F.m).x = -((G.m).x) by A15,MESFUNC1:def 7;
hence (F.n).x >= (F.m).x by A15,A3,A4,A6,A14,XXREAL_3:38;
end;
thus for x be Element of X st x in dom f
holds (F#x) is convergent & lim(F#x) = f.x
proof
let x be Element of X;
assume A17: x in dom f; then
A18: (G#x) is convergent & lim(G#x) = g.x by A3,A4,A6;
hence (F#x) is convergent by Th39;
lim(F#x) = - g.x by A18,Th39; then
lim(F#x) = - (-f.x) by A3,A4,A17,MESFUNC1:def 7;
hence lim(F#x) = f.x;
end;
end;
theorem Th57:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S, f be nonpositive PartFunc of X,ExtREAL
st (ex A be Element of S st A = dom f & f is A-measurable) holds
Integral(M,f) = - integral+(M,max- f) & Integral(M,f) = - integral+(M,-f)
& Integral(M,f) = - Integral(M,-f)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S, f be nonpositive PartFunc of X,ExtREAL;
assume ex A be Element of S st A = dom f & f is A-measurable; then
consider A be Element of S such that
A2: A = dom f & f is A-measurable;
A3: dom(max+f) = A by A2,MESFUNC2:def 2;
A4: f = -(max-f) by Th32; then
A5: -f = max-f by Th36;
for x be Element of X st x in dom(max+f) holds (max+f).x = 0
proof
let x be Element of X;
assume x in dom(max+f); then
f.x = -((max-f).x) by A2,A3,A4,MESFUNC1:def 7; then
-(f.x) = (max-f).x;
hence (max+f).x = 0 by MESFUNC2:21;
end; then
A6: integral+(M,max+f) = 0 by A3,A2,MESFUNC2:25,MESFUNC5:87;
A7: Integral(M,f) = integral+(M,max+f) - integral+(M,max-f) by MESFUNC5:def 16
.= integral+(M,max+f) + -integral+(M,max-f) by XXREAL_3:def 4;
hence Integral(M,f) = - integral+(M,max- f) by A6,XXREAL_3:4;
thus
A8: Integral(M,f) = - integral+(M,-f) by A5,A7,A6,XXREAL_3:4;
A = dom(-f) by A2,MESFUNC1:def 7;
hence Integral(M,f) = - Integral(M,-f) by A8,A2,MEASUR11:63,MESFUNC5:88;
end;
theorem Th58:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be nonpositive PartFunc of X,ExtREAL st f is_simple_func_in S
holds Integral(M,f) = -integral'(M,-f) & Integral(M,f) = -integral'(M,max-f)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be nonpositive PartFunc of X,ExtREAL;
assume A1: f is_simple_func_in S; then
reconsider A = dom f as Element of S by MESFUNC5:37;
A2:f is A-measurable by A1,MESFUNC2:34;
integral+(M,-f) = integral'(M,-f) by A1,Th30,MESFUNC5:77;
hence A3: Integral(M,f) = - integral'(M,-f) by A2,Th57;
f = -(max-f) by Th32;
hence Integral(M,f) = - integral'(M,max-f) by A3,Th36;
end;
Lm3:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X, ExtREAL, c be Real
st f is_simple_func_in S & f is nonpositive
& 0 <= c
holds Integral(M,c(#)f) = -(c * integral'(M,-f))
& Integral(M,c(#)f) = (-c) * integral'(M,-f)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X, ExtREAL, c be Real;
assume that
A1: f is_simple_func_in S and
A2: f is nonpositive and
A3: 0 <= c;
A4:c(#)f is_simple_func_in S by A1,MESFUNC5:39;
f = -(max-f) by A2,Th32; then
A6:-f = max-f by Th36;
A7:-f is_simple_func_in S by A1,Th30;
A8:max-(c(#)f) = c(#)(max-f) by A3,MESFUNC5:26;
c(#)f is nonpositive by A2,A3,Th4;
hence Integral(M,c(#)f) = - integral'(M,max-(c(#)f)) by A4,Th58
.= - (c * integral'(M,-f)) by A3,A7,A6,A8,Th5,MESFUNC5:66;
hence Integral(M,c(#)f) = (-c) * integral'(M,-f) by XXREAL_3:92;
end;
Lm4:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X, ExtREAL, c be Real
st f is_simple_func_in S & f is nonnegative & c <= 0
holds Integral(M,c(#)f) = c * integral'(M,f)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X, ExtREAL, c be Real;
assume that
A1: f is_simple_func_in S and
A2: f is nonnegative and
A3: c <= 0;
set d = -c;
A4:-f is_simple_func_in S by A1,Th30;
d(#)(-f) = d(#)((-1)(#)f) by MESFUNC2:9 .= (d*(-1))(#)f by Th35; then
Integral(M,c(#)f) = (-d) * integral'(M,-(-f)) by A3,A2,A4,Lm3;
hence Integral(M,c(#)f) = c * integral'(M,f) by DBLSEQ_3:2;
end;
theorem Th59:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X, ExtREAL, c be Real
st f is_simple_func_in S & f is nonnegative
holds Integral(M,c(#)f) = c * integral'(M,f)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X, ExtREAL, c be Real;
assume that
A1: f is_simple_func_in S and
a2: f is nonnegative;
per cases;
suppose A2: c >= 0; then
A3: c(#)f is_simple_func_in S & c(#)f is nonnegative by A1,a2,MESFUNC5:20,39;
integral'(M,c(#)f) = c * integral'(M,f) by A1,a2,A2,MESFUNC5:66;
hence Integral(M,c(#)f) = c * integral'(M,f) by A3,MESFUNC5:89;
end;
suppose c < 0;
hence Integral(M,c(#)f) = c * integral'(M,f) by A1,a2,Lm4;
end;
end;
theorem
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X, ExtREAL, c be Real
st f is_simple_func_in S & f is nonpositive
holds Integral(M,c(#)f) = (-c) * integral'(M,-f)
& Integral(M,c(#)f) = -(c * integral'(M,-f))
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X, ExtREAL, c be Real;
assume that
A1: f is_simple_func_in S and
A2: f is nonpositive;
set d = -c;
A3:d(#)(-f) = d(#)((-1)(#)f) by MESFUNC2:9 .= (d*(-1))(#)f by Th35;
hence Integral(M,c(#)f) = (-c) * integral'(M,-f) by A2,A1,Th30,Th59;
Integral(M,c(#)f) = d * integral'(M,-f) by A2,A1,A3,Th30,Th59;
hence Integral(M,c(#)f) = -(c * integral'(M,-f)) by XXREAL_3:92;
end;
theorem Th61:
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL st (ex A be Element of S st A = dom f & f
is A-measurable) & f is nonpositive holds 0 >= Integral(M,f)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL;
assume that
A1: ex A be Element of S st A = dom f & f is A-measurable and
A2: f is nonpositive;
consider A be Element of S such that
A3: A = dom f and
a3: f is A-measurable by A1;
A4: A = dom(-f) by A3,MESFUNC1:def 7;
Integral(M,-f) >= 0 by A4,A2,A3,a3,MEASUR11:63,MESFUNC5:90; then
A7: integral+(M,-f) >= 0 by A4,A2,A3,a3,MEASUR11:63,MESFUNC5:88;
Integral(M,f) = - integral+(M,-f) by A2,A3,a3,Th57;
hence 0 >= Integral(M,f) by A7;
end;
theorem
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, A,B,E be Element of S
st E = dom f & f is E-measurable & f is nonpositive & A misses B
holds Integral(M,f|(A\/B)) = Integral(M,f|A)+Integral(M,f|B)
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,B,E be Element of S;
assume that
A1: E = dom f & f is E-measurable and
A2: f is nonpositive and
A3: A misses B;
set f1 = f|(A\/B);
set f2 = f|A;
set f3 = f|B;
set g = -f;
reconsider E1 = E /\ (A \/ B) as Element of S;
A4: dom(f|(A\/B)) = E1 by A1,RELAT_1:61;
A5: E1 = dom f /\ E1 by A1,XBOOLE_1:17,28;
A6: f is E1-measurable by A1,XBOOLE_1:17,MESFUNC1:30;
A7: f|E1 = f|E|(A\/B) by RELAT_1:71;
g|(A\/B) = -(f|(A\/B)) by Th3; then
A8: Integral(M,g|(A\/B)) = -Integral(M,f|(A\/B))
by A1,A4,A5,A6,A7,Th52,MESFUNC5:42;
reconsider E2 = E /\ A as Element of S;
A9: dom(f|A) = E2 by A1,RELAT_1:61;
A10:E2 = dom f /\ E2 by A1,XBOOLE_1:17,28;
A11:f is E2-measurable by A1,XBOOLE_1:17,MESFUNC1:30;
A12:f|E2 = f|E|A by RELAT_1:71;
g|A = -(f|A) by Th3; then
A13:Integral(M,g|A) = - Integral(M,f|A)
by A1,A9,A10,A11,A12,Th52,MESFUNC5:42;
reconsider E3 = E /\ B as Element of S;
A14:dom(f|B) = E3 by A1,RELAT_1:61;
A15:E3 = dom f /\ E3 by A1,XBOOLE_1:17,28;
A16:f is E3-measurable by A1,XBOOLE_1:17,MESFUNC1:30;
A17:f|E3 = f|E|B by RELAT_1:71;
g|B = -(f|B) by Th3; then
A18:Integral(M,g|B) = - Integral(M,f|B)
by A1,A14,A15,A16,A17,Th52,MESFUNC5:42;
E = dom g by A1,MESFUNC1:def 7; then
Integral(M,g|(A\/B)) = Integral(M,g|A) + Integral(M,g|B)
by A2,A3,A1,MEASUR11:63,MESFUNC5:91; then
-Integral(M,f|(A\/B)) = -(Integral(M,f|A) + Integral(M,f|B))
by A8,A13,A18,XXREAL_3:9;
hence Integral(M,f|(A\/B)) = Integral(M,f|A) + Integral(M,f|B)
by XXREAL_3:10;
end;
theorem
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, A,E be Element of S
st E = dom f & f is E-measurable & f is nonpositive
holds 0 >= Integral(M,f|A)
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,E be Element of S;
assume that
A1: E = dom f and
A2: f is E-measurable and
A3: f is nonpositive;
reconsider E1 = E /\ A as Element of S;
A4: dom(f|A) = E1 by A1,RELAT_1:61;
A5: E1 = dom f /\ E1 by A1,XBOOLE_1:17,28;
f is E1-measurable by A2,XBOOLE_1:17,MESFUNC1:30; then
A6: f|E1 is E1-measurable by A5,MESFUNC5:42;
f|E1 = f|E|A by RELAT_1:71;
hence 0>= Integral(M,f|A) by A1,A3,A4,A6,Th61,Th1;
end;
theorem
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
f be PartFunc of X,ExtREAL, A,B,E be Element of S
st E = dom f & f is E-measurable & f is nonpositive & A c= B
holds Integral(M,f|A) >= Integral(M,f|B)
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,B,E be Element of S;
assume that
A1: E = dom f and
A2: f is E-measurable and
A3: f is nonpositive and
A4: A c= B;
set g = -f;
E = dom g by A1,MESFUNC1:def 7; then
A5: Integral(M,g|A) <= Integral(M,g|B) by A1,A2,A3,A4,MESFUNC5:93,MEASUR11:63;
reconsider E1 = E /\ A as Element of S;
A6: dom(f|A) = E1 by A1,RELAT_1:61;
A7: E1 = dom f /\ E1 by A1,XBOOLE_1:17,28;
A8: f is E1-measurable by A2,XBOOLE_1:17,MESFUNC1:30;
A9: f|E1 = f|E|A by RELAT_1:71;
g|A = -(f|A) by Th3; then
A10:Integral(M,g|A) = -Integral(M,f|A) by A1,A6,A7,A8,A9,Th52,MESFUNC5:42;
reconsider E2 = E /\ B as Element of S;
A11:dom(f|B) = E2 by A1,RELAT_1:61;
A12:E2 = dom f /\ E2 by A1,XBOOLE_1:17,28;
A13:f is E2-measurable by A2,XBOOLE_1:17,MESFUNC1:30;
A14:f|E2 = f|E|B by RELAT_1:71;
g|B = -(f|B) by Th3; then
Integral(M,g|B) = -Integral(M,f|B)
by A1,A11,A12,A13,A14,Th52,MESFUNC5:42;
hence Integral(M,f|A) >= Integral(M,f|B) by A5,A10,XXREAL_3:38;
end;
begin :: Convergent theorems for non positive function's integration
theorem
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S, f be PartFunc of X,ExtREAL st
E = dom f & f is E-measurable & f is nonpositive & M.(E /\
eq_dom(f,-infty)) <> 0 holds Integral(M,f) = -infty
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S, f be PartFunc of X,ExtREAL;
assume that
A1: E = dom f and
A2: f is E-measurable and
A3: f is nonpositive and
A4: M.(E /\ eq_dom(f,-infty)) <> 0;
set g = -f;
A5: E = dom g by A1,MESFUNC1:def 7;
g = (-1)(#)f by MESFUNC2:9; then
eq_dom(f,-infty) = eq_dom(g,-infty*(-1)) by Th9; then
eq_dom(f,-infty) = eq_dom(g,+infty) by XXREAL_3:def 5; then
Integral(M,g) = +infty by A1,A2,A3,A4,A5,MESFUNC9:13,MEASUR11:63; then
-Integral(M,f) = +infty by A1,A2,Th52;
hence Integral(M,f) = -infty by XXREAL_3:6;
end;
theorem
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S, f,g be PartFunc of X,ExtREAL st
E c= dom f & E c= dom g & f is E-measurable & g
is E-measurable & f is nonpositive & (for x be Element of X st x in E holds
g.x <= f.x ) holds Integral(M,g|E) <= Integral(M,f|E)
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S, f,g be PartFunc of X,ExtREAL;
assume that
A1: E c= dom f and
A2: E c= dom g and
A3: f is E-measurable & g is E-measurable and
A4: f is nonpositive and
A5: for x be Element of X st x in E holds g.x <= f.x;
set f1 = -f, g1 = -g;
A6: E c= dom f1 & E c= dom g1 by A1,A2,MESFUNC1:def 7;
A7: f1 is E-measurable & g1 is E-measurable by A1,A2,A3,MEASUR11:63;
A11:for x be Element of X st x in E holds f1.x <= g1.x
proof
let x be Element of X;
assume A9: x in E; then
f1.x = -(f.x) & g1.x = -(g.x) by A6,MESFUNC1:def 7;
hence f1.x <= g1.x by A5,A9,XXREAL_3:38;
end;
A12:dom f /\ E = E & dom g /\ E = E by A1,A2,XBOOLE_1:28;
A14:E = dom(f|E) & E = dom(g|E) by A12,RELAT_1:61;
f1|E = -(f|E) & g1|E = -(g|E) by Th3; then
Integral(M,f1|E) = -Integral(M,f|E) & Integral(M,g1|E) = -Integral(M,g|E)
by A3,A12,A14,Th52,MESFUNC5:42;
hence Integral(M,g|E) <= Integral(M,f|E)
by A4,A6,A7,A11,XXREAL_3:38,MESFUNC9:15;
end;
theorem Th67:
for X be non empty set, F be Functional_Sequence of X,ExtREAL,
S be SigmaField of X, E be Element of S, m be Nat st
F is with_the_same_dom & E = dom(F.0) &
(for n be Nat holds F.n is E-measurable & F.n is without+infty)
holds (Partial_Sums F).m is E-measurable
proof
let X be non empty set, F be Functional_Sequence of X,ExtREAL,
S be SigmaField of X, E be Element of S, m be Nat;
assume that
A1: F is with_the_same_dom and
A2: E = dom(F.0) and
A3: for n be Nat holds F.n is E-measurable & F.n is without+infty;
now let n be Nat;
E = dom(F.n) by A1,A2,MESFUNC8:def 2; then
-(F.n) is E-measurable by A3,MEASUR11:63;
hence (-F).n is E-measurable by Th37;
F.n is without+infty by A3; then
-(F.n) is without-infty;
hence (-F).n is without-infty by Th37;
end; then
(Partial_Sums (-F)).m is E-measurable by MESFUNC9:41; then
(-(Partial_Sums F)).m is E-measurable by Th42; then
A5: -((Partial_Sums F).m) is E-measurable by Th37;
dom((Partial_Sums F).m) = E by A1,A2,A3,Th46,MESFUNC9:29; then
dom(-((Partial_Sums F).m)) = E by MESFUNC1:def 7; then
-(-((Partial_Sums F).m)) is E-measurable by A5,MEASUR11:63;
hence (Partial_Sums F).m is E-measurable by DBLSEQ_3:2;
end;
theorem
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
F be Functional_Sequence of X,ExtREAL, E be Element of S,
I be ExtREAL_sequence, m be Nat
st E = dom(F.0) & F is additive & F is with_the_same_dom
& (for n be Nat holds
F.n is E-measurable & F.n is nonpositive & I.n = Integral(M,F.n))
holds Integral(M,(Partial_Sums F).m) = (Partial_Sums I).m
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
F be Functional_Sequence of X,ExtREAL, E be Element of S,
I be ExtREAL_sequence, m be Nat;
assume that
A1: E = dom(F.0) and
A2: F is additive and
A3: F is with_the_same_dom and
A4: for n be Nat holds
F.n is E-measurable & F.n is nonpositive & I.n = Integral(M,F.n);
set G = -F, J = -I;
G.0 = -(F.0) by Th37; then
A5: E = dom(G.0) by A1,MESFUNC1:def 7;
A6: G is with_the_same_dom by A3,Th40;
A7: E = dom((Partial_Sums F).m) by A1,A2,A3,MESFUNC9:29;
A8: for n be Nat holds
F.n is E-measurable & F.n is without+infty
proof
let n be Nat;
thus F.n is E-measurable by A4;
F.n is nonpositive by A4;
hence F.n is without+infty;
end;
for n be Nat holds
G.n is E-measurable & G.n is nonnegative & J.n = Integral(M,G.n)
proof
let n be Nat;
A9: F.n is nonpositive & I.n = Integral(M,F.n) by A4;
A10: G.n = -(F.n) by Th37;
dom J = NAT by FUNCT_2:def 1; then
A11: n in dom J by ORDINAL1:def 12;
A12: dom(F.n) = E by A1,A3,MESFUNC8:def 2;
hence G.n is E-measurable by A4,A10,MEASUR11:63;
thus G.n is nonnegative by A9,A10;
Integral(M,G.n) = -Integral(M,F.n) by A4,A10,A12,Th52;
hence J.n = Integral(M,G.n) by A9,A11,MESFUNC1:def 7;
end; then
Integral(M,(Partial_Sums G).m) = (Partial_Sums J).m
by A5,A2,A6,Th41,MESFUNC9:46; then
Integral(M,(-(Partial_Sums F)).m) = (Partial_Sums J).m by Th42; then
Integral(M,(-(Partial_Sums F)).m) = -((Partial_Sums I).m) by Th43; then
Integral(M,-((Partial_Sums F).m)) = -((Partial_Sums I).m) by Th37; then
-Integral(M,(Partial_Sums F).m) = -((Partial_Sums I).m)
by A1,A3,A7,A8,Th67,Th52;
hence Integral(M,(Partial_Sums F).m) = (Partial_Sums I).m by XXREAL_3:10;
end;
theorem
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
F be Functional_Sequence of X,ExtREAL, E be Element of S,
f be PartFunc of X,ExtREAL
st E c= dom f & f is nonpositive & f is E-measurable &
(for n be Nat holds
F.n is_simple_func_in S & F.n is nonpositive & E c= dom(F.n)) &
(for x be Element of X st x in E holds F#x is summable & f.x = Sum(F#x))
holds ex I be ExtREAL_sequence st
(for n be Nat holds I.n = Integral(M,(F.n)|E)) & I is summable &
Integral(M,f|E) = Sum I
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
F be Functional_Sequence of X,ExtREAL, E be Element of S,
f be PartFunc of X,ExtREAL;
assume that
A1: E c= dom f and
A2: f is nonpositive and
A3: f is E-measurable and
A4: for n be Nat holds
F.n is_simple_func_in S & F.n is nonpositive & E c= dom(F.n) and
A5: for x be Element of X st x in E holds F#x is summable & f.x = Sum(F#x);
set g = -f, G = -F;
A6: E c= dom g by A1,MESFUNC1:def 7;
now let n be Nat;
F.n is nonpositive by A4; then
-(F.n) is without-infty;
hence G.n is without-infty by Th37;
end; then
A7: G is additive by Th47;
A8: for n be Nat holds
G.n is_simple_func_in S & G.n is nonnegative & E c= dom(G.n)
proof
let n be Nat;
(-1)(#)(F.n) is_simple_func_in S by A4,MESFUNC5:39; then
-(F.n) is_simple_func_in S by MESFUNC2:9;
hence G.n is_simple_func_in S by Th37;
F.n is nonpositive by A4; then
-(F.n) is nonnegative;
hence G.n is nonnegative by Th37;
E c= dom(F.n) by A4; then
E c= dom(-(F.n)) by MESFUNC1:def 7;
hence E c= dom(G.n) by Th37;
end;
A9: for x be Element of X st x in E holds G#x is summable & g.x = Sum(G#x)
proof
let x be Element of X;
assume A10: x in E; then
A11: F#x is summable & f.x = Sum(F#x) by A5;
hence G#x is summable by Th48;
g.x = -(f.x) by A6,A10,MESFUNC1:def 7;
hence g.x = Sum(G#x) by A11,Th48;
end;
consider J be ExtREAL_sequence such that
A12: (for n be Nat holds J.n = Integral(M,(G.n)|E)) & J is summable
& Integral(M,g|E) = Sum J by A2,A1,A3,A6,A7,A8,A9,MESFUNC9:47,MEASUR11:63;
take I = -J;
thus for n be Nat holds I.n = Integral(M,(F.n)|E)
proof
let n be Nat;
dom I = NAT by FUNCT_2:def 1; then
n in dom I by ORDINAL1:def 12; then
I.n = -(J.n) by MESFUNC1:def 7; then
A13: I.n = - Integral(M,(G.n)|E) by A12;
A14: E c= dom(G.n) by A8;
A15: G.n is E-measurable by A8,MESFUNC2:34;
G.n = -(F.n) by Th37; then
F.n = -(G.n) by Th36;
hence I.n = Integral(M,(F.n)|E) by A13,A14,A15,Th55;
end;
thus I is summable by A12,Th45;
A16:Integral(M,g|E) = - Integral(M,f|E) by A1,A3,Th55;
Partial_Sums J is convergent by A12,MESFUNC9:def 2; then
lim -(Partial_Sums J) = - lim (Partial_Sums J) by DBLSEQ_3:17
.= - Integral(M,g|E) by A12,MESFUNC9:def 3; then
lim Partial_Sums I = - Integral(M,g|E) by Th44;
hence Integral(M,f|E) = Sum I by A16,MESFUNC9:def 3;
end;
theorem
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S, f be PartFunc of X,ExtREAL
st E c= dom f & f is nonpositive & f is E-measurable
holds
ex F be Functional_Sequence of X,ExtREAL st
F is additive
& (for n be Nat holds
F.n is_simple_func_in S & F.n is nonpositive & F.n is E-measurable)
& (for x be Element of X st x in E holds
F#x is summable & f.x = Sum(F#x))
& ex I be ExtREAL_sequence st
(for n be Nat holds I.n = Integral(M,(F.n)|E))
& I is summable
& Integral(M,f|E) = Sum I
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
E be Element of S, f be PartFunc of X,ExtREAL;
assume that
A1: E c= dom f and
A2: f is nonpositive and
A3: f is E-measurable;
set g = -f;
A4: E c= dom g by A1,MESFUNC1:def 7; then
consider G be Functional_Sequence of X,ExtREAL such that
A5: G is additive
& (for n be Nat holds
G.n is_simple_func_in S & G.n is nonnegative & G.n is E-measurable)
& (for x be Element of X st x in E holds
G#x is summable & g.x = Sum(G#x))
& ex J be ExtREAL_sequence st
(for n be Nat holds J.n = Integral(M,(G.n)|E))
& J is summable
& Integral(M,g|E) = Sum J by A1,A2,A3,MESFUNC9:48,MEASUR11:63;
take F = -G;
thus F is additive by A5,Th41;
thus for n be Nat holds
F.n is_simple_func_in S & F.n is nonpositive & F.n is E-measurable
proof
let n be Nat;
(-1)(#)(G.n) is_simple_func_in S by A5,MESFUNC5:39; then
-(G.n) is_simple_func_in S by MESFUNC2:9;
hence
A6: F.n is_simple_func_in S by Th37;
G.n is nonnegative by A5; then
-(G.n) is nonpositive;
hence F.n is nonpositive by Th37;
thus F.n is E-measurable by A6,MESFUNC2:34;
end;
thus for x be Element of X st x in E holds F#x is summable & f.x = Sum(F#x)
proof
let x be Element of X;
assume A7: x in E; then
A8: G#x is summable & g.x = Sum(G#x) by A5;
hence F#x is summable by Th48;
g.x = -(f.x) by A7,A4,MESFUNC1:def 7; then
f.x = - Sum(G#x) by A8;
hence f.x = Sum((F#x)) by A8,Th48;
end;
thus ex I be ExtREAL_sequence st
(for n be Nat holds I.n = Integral(M,(F.n)|E))
& I is summable
& Integral(M,f|E) = Sum I
proof
consider J be ExtREAL_sequence such that
A9: (for n be Nat holds J.n = Integral(M,(G.n)|E))
& J is summable
& Integral(M,g|E) = Sum J by A5;
take I = -J;
thus for n be Nat holds I.n = Integral(M,(F.n)|E)
proof
let n be Nat;
dom I = NAT by FUNCT_2:def 1; then
A10: n in dom I by ORDINAL1:def 12;
A11: J.n = Integral(M,(G.n)|E) by A9;
F.n = -(G.n) by Th37; then
A12: (F.n)|E = -((G.n)|E) by Th3;
A13: G.n is_simple_func_in S by A5; then
consider GG be Finite_Sep_Sequence of S such that
A14: dom(G.n) = union rng GG &
for k be Nat,x,y be Element of X st k in dom GG & x in GG.k & y in GG.k
holds (G.n).x = (G.n).y by MESFUNC2:def 4;
reconsider V = union rng GG as Element of S by MESFUNC2:31;
reconsider VE = V /\ E as Element of S;
A15: VE = dom((G.n)|E) by A14,RELAT_1:61;
(G.n)|E is VE-measurable by A13,MESFUNC2:34,MESFUNC5:34; then
Integral(M,(F.n)|E) = -Integral(M,(G.n)|E) by A12,A15,Th52;
hence I.n = Integral(M,(F.n)|E) by A10,A11,MESFUNC1:def 7;
end;
thus I is summable by A9,Th45;
A16: Partial_Sums J is convergent by A9,MESFUNC9:def 2;
A17: Sum I = lim Partial_Sums I by MESFUNC9:def 3
.= lim (-(Partial_Sums J)) by Th44
.= -(lim Partial_Sums J) by A16,DBLSEQ_3:17
.= - Integral(M,g|E) by A9,MESFUNC9:def 3;
A18: dom(f|E) = E by A1,RELAT_1:62;
A19: E = dom f /\ E by A1,XBOOLE_1:28;
g|E = -(f|E) by Th3; then
Integral(M,g|E) = - Integral(M,f|E) by A3,A18,A19,Th52,MESFUNC5:42;
hence Integral(M,f|E) = Sum I by A17;
end;
end;
theorem
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
F be Functional_Sequence of X,ExtREAL, E be Element of S st
E = dom(F.0) & F is with_the_same_dom & (for n be Nat holds F.n
is nonpositive & F.n is E-measurable )
holds ex FF be sequence of
Funcs(NAT,PFuncs(X,ExtREAL)) st for n be Nat holds (for m be Nat holds (FF.n).m
is_simple_func_in S & dom((FF.n).m) = dom(F.n)) & (for m be Nat holds (FF.n).m
is nonpositive) & (for j,k be Nat st j <= k holds for x be Element of X st x in
dom(F.n) holds ((FF.n).j).x >= ((FF.n).k).x) & for x be Element of X st x in
dom(F.n) holds (FF.n)#x is convergent & lim((FF.n)#x) = (F.n).x
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
F be Functional_Sequence of X,ExtREAL, E be Element of S;
assume that
A1: E = dom(F.0) and
A2: F is with_the_same_dom and
A3: for n be Nat holds F.n is nonpositive & F.n is E-measurable;
defpred Q[Element of NAT,set] means for G be Functional_Sequence of X,
ExtREAL st $2 = G holds (for m be Nat holds G.m is_simple_func_in S & dom(G.m)
= dom(F.$1)) & (for m be Nat holds G.m is nonpositive) & (for j,k be Nat st j
<= k holds for x be Element of X st x in dom(F.$1) holds (G.j).x >= (G.k).x) &
(for x be Element of X st x in dom(F.$1) holds G#x is convergent & lim(G#x) = (
F.$1).x);
A4: for n be Element of NAT holds ex G be Functional_Sequence of X,ExtREAL st
(for m be Nat holds G.m is_simple_func_in S & dom(G.m) = dom(F.n)) & (for m be
Nat holds G.m is nonpositive) & (for j,k be Nat st j <= k holds for x be
Element of X st x in dom(F.n) holds (G.j).x >= (G.k).x ) & for x be Element of
X st x in dom(F.n) holds (G#x) is convergent & lim(G#x) = (F.n).x
proof
let n be Element of NAT;
A5: F.n is E-measurable by A3;
F.n is nonpositive by A3;
hence thesis by A1,A2,A5,Th56,MESFUNC8:def 2;
end;
A7: for n be Element of NAT ex G be Element of Funcs(NAT,PFuncs(X,ExtREAL))
st Q[n,G]
proof
let n be Element of NAT;
consider G be Functional_Sequence of X,ExtREAL such that
A8: for m be Nat holds G.m is_simple_func_in S & dom(G.m) = dom(F.n) and
A9: for m be Nat holds G.m is nonpositive and
A10: for j,k be Nat st j <= k holds for x be Element of X st x in dom(
F. n) holds (G.j).x >= (G.k).x and
A11: for x be Element of X st x in dom(F.n) holds (G#x) is convergent
& lim(G#x) = (F.n).x by A4;
reconsider G as Element of Funcs(NAT,PFuncs(X,ExtREAL)) by FUNCT_2:8;
take G;
thus thesis by A8,A9,A10,A11;
end;
consider FF be sequence of Funcs(NAT,PFuncs(X,ExtREAL)) such that
A12: for n be Element of NAT holds Q[n,FF.n] from FUNCT_2:sch 3(A7);
take FF;
thus for n be Nat holds (for m be Nat holds (FF.n).m is_simple_func_in S &
dom((FF.n).m) = dom(F.n)) & (for m be Nat holds (FF.n).m is nonpositive) & (for
j,k be Nat st j <= k holds for x be Element of X st x in dom(F.n) holds ((FF.n)
.j).x >= ((FF.n).k).x) & for x be Element of X st x in dom(F.n) holds (FF.n)#x
is convergent & lim((FF.n)#x) = (F.n).x
proof
let n be Nat;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
for G be Functional_Sequence of X,ExtREAL st FF.n1 = G holds (for m
be Nat holds G.m is_simple_func_in S & dom(G.m) = dom(F.n1)) & (for m be Nat
holds G.m is nonpositive) & (for j,k be Nat st j <= k holds for x be Element of
X st x in dom(F.n1) holds (G.j).x >= (G.k).x) & for x be Element of X st x in
dom(F.n1) holds G#x is convergent & lim(G#x) = (F.n1).x by A12;
hence thesis;
end;
end;
theorem
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
F be Functional_Sequence of X,ExtREAL, E be Element of S
st E = dom(F.0) & F is additive & F is with_the_same_dom
& (for n be Nat holds F.n is E-measurable & F.n is nonpositive)
holds
ex I be ExtREAL_sequence st for n be Nat holds
I.n = Integral(M,F.n) & Integral(M,(Partial_Sums F).n) = (Partial_Sums I).n
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
F be Functional_Sequence of X,ExtREAL, E be Element of S;
assume that
A1: E = dom(F.0) and
A2: F is additive and
A3: F is with_the_same_dom and
A4: for n be Nat holds F.n is E-measurable & F.n is nonpositive;
set G = -F;
G.0 = -(F.0) by Th37; then
A5: E = dom(G.0) by A1,MESFUNC1:def 7;
A7: G is with_the_same_dom by A3,Th40;
for n be Nat holds G.n is E-measurable & G.n is nonnegative
proof
let n be Nat;
E = dom(F.n) & F.n is E-measurable by A4,A1,A3,MESFUNC8:def 2; then
-(F.n) is E-measurable by MEASUR11:63;
hence G.n is E-measurable by Th37;
F.n is nonpositive by A4; then
-(F.n) is nonnegative;
hence G.n is nonnegative by Th37;
end; then
consider J be ExtREAL_sequence such that
A8: for n be Nat holds J.n = Integral(M,G.n)
& Integral(M,(Partial_Sums G).n) = (Partial_Sums J).n
by A5,A7,A2,Th41,MESFUNC9:50;
set I = -J;
take I;
A10: for n be Nat holds
F.n is E-measurable & F.n is without+infty
proof
let n be Nat;
thus F.n is E-measurable by A4;
F.n is nonpositive by A4;
hence F.n is without+infty;
end;
hereby let n be Nat;
dom I = NAT by FUNCT_2:def 1; then
n in dom I by ORDINAL1:def 12; then
I.n = -(J.n) by MESFUNC1:def 7; then
A9: I.n = - Integral(M,G.n) by A8;
E = dom(F.n) & F.n is E-measurable & (G.n) = -(F.n)
by A4,A1,A3,Th37,MESFUNC8:def 2; then
Integral(M,G.n) = - Integral(M,F.n) by Th52;
hence I.n = Integral(M,F.n) by A9;
A11: E = dom((Partial_Sums F).n) by A1,A2,A3,MESFUNC9:29;
(Partial_Sums G).n = (-(Partial_Sums F)).n by Th42
.= -((Partial_Sums F).n) by Th37; then
A13: Integral(M,(Partial_Sums G).n)
= - Integral(M,(Partial_Sums F).n) by A10,A1,A3,A11,Th52,Th67;
(Partial_Sums I).n = -((Partial_Sums J).n) by Th43
.= - Integral(M,(Partial_Sums G).n) by A8;
hence Integral(M,(Partial_Sums F).n) = (Partial_Sums I).n by A13;
end;
end;
theorem
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
F be Functional_Sequence of X,ExtREAL, E be Element of S
st E c= dom(F.0) & F is additive & F is with_the_same_dom
& (for n be Nat holds F.n is nonpositive & F.n is E-measurable)
& (for x be Element of X st x in E holds F#x is summable)
holds ex I be ExtREAL_sequence st
(for n be Nat holds I.n = Integral(M,(F.n)|E))
& I is summable & Integral(M,(lim(Partial_Sums F))|E) = Sum I
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
F be Functional_Sequence of X,ExtREAL, E be Element of S;
assume that
A1: E c= dom(F.0) and
A2: F is additive and
A3: F is with_the_same_dom and
A4: for n be Nat holds F.n is nonpositive & F.n is E-measurable and
A5: for x be Element of X st x in E holds F#x is summable;
set G = -F;
G.0 = -(F.0) by Th37; then
A6: E c= dom(G.0) by A1,MESFUNC1:def 7;
A7: G is additive by A2,Th41;
A8: G is with_the_same_dom by A3,Th40;
A9: for n be Nat holds G.n is nonnegative & G.n is E-measurable
proof
let n be Nat;
F.n is nonpositive by A4; then
-(F.n) is nonnegative;
hence G.n is nonnegative by Th37;
E c= dom(F.n) by A1,A3,MESFUNC8:def 2; then
-(F.n) is E-measurable by A4,MEASUR11:63;
hence G.n is E-measurable by Th37;
end;
A10:for x be Element of X st x in E holds G#x is summable
proof
let x be Element of X;
assume x in E; then
F#x is summable by A5;
hence G#x is summable by Th48;
end; then
consider J be ExtREAL_sequence such that
A11: (for n be Nat holds J.n = Integral(M,(G.n)|E))
& J is summable & Integral(M,(lim(Partial_Sums G))|E) = Sum J
by A6,A7,A3,Th40,A9,MESFUNC9:51;
take I = -J;
thus for n be Nat holds I.n = Integral(M,(F.n)|E)
proof
let n be Nat;
n in NAT by ORDINAL1:def 12; then
A14: n in dom I by FUNCT_2:def 1;
A12: E c= dom(G.n) by A6,A3,Th40,MESFUNC8:def 2;
G.n = -(F.n) by Th37; then
F.n = -(G.n) by Th36; then
Integral(M,(F.n)|E) = - Integral(M,(G.n)|E) by A12,A9,Th55; then
J.n = - Integral(M,(F.n)|E) by A11; then
I.n = - - Integral(M,(F.n)|E) by A14,MESFUNC1:def 7;
hence I.n = Integral(M,(F.n)|E);
end;
thus I is summable by A11,Th45;
A15:Partial_Sums J is convergent by A11,MESFUNC9:def 2;
A16:Sum I = lim Partial_Sums I by MESFUNC9:def 3
.= lim (-(Partial_Sums J)) by Th44
.= -(lim Partial_Sums J) by A15,DBLSEQ_3:17
.= - Integral(M,(lim(Partial_Sums G))|E) by A11,MESFUNC9:def 3;
deffunc F1(Nat) = (F.$1)|E;
consider F1 be Functional_Sequence of X,ExtREAL such that
A17: for n be Nat holds F1.n = F1(n) from SEQFUNC:sch 1;
reconsider F1 as additive with_the_same_dom
Functional_Sequence of X,ExtREAL by A2,A3,A17,MESFUNC9:18,31;
A18:lim(Partial_Sums F1) = (lim(Partial_Sums F))|E
by A1,A2,A3,A17,Th50;
deffunc G1(Nat) = (G.$1)|E;
consider G1 be Functional_Sequence of X,ExtREAL such that
A19: for n be Nat holds G1.n = G1(n) from SEQFUNC:sch 1;
reconsider G1 as additive with_the_same_dom
Functional_Sequence of X,ExtREAL by A7,A8,A19,MESFUNC9:18,31;
A20:lim(Partial_Sums G1) = (lim(Partial_Sums G))|E
by A6,A7,A19,A3,Th40,Th50;
for n be Element of NAT holds F1.n = (-G1).n
proof
let n be Element of NAT;
G.n = -(F.n) by Th37; then
A21: (-G).n = - -(F.n) by Th37 .= F.n by DBLSEQ_3:2;
A22: F1.n = (F.n)|E by A17;
(-G1).n = -(G1.n) by Th37; then
(-G1).n = -(G.n|E) by A19; then
(-G1).n = (-(G.n))|E by Th3;
hence F1.n = (-G1).n by A21,A22,Th37;
end; then
A23:F1 = -G1 by FUNCT_2:def 7;
G1.0 = (G.0)|E by A19; then
A24:dom (G1.0) = E by A6,RELAT_1:62; then
A25:for x be Element of X st x in dom(G1.0) holds G1#x is summable
by A6,A10,A19,MESFUNC9:21; then
A26:lim Partial_Sums F1 = -(lim Partial_Sums G1) by A23,Th49;
for n be Nat holds G1.n is E-measurable & G1.n is without-infty
proof
let n be Nat;
thus G1.n is E-measurable by A6,A9,A19,A3,Th40,MESFUNC9:20;
(G.n)|E is nonnegative by A9,MESFUNC5:15;
hence G1.n is without-infty by A19;
end; then
A27:for n be Nat holds (Partial_Sums G1).n is E-measurable
by MESFUNC9:41;
dom(lim(Partial_Sums G1)) = dom((Partial_Sums G1).0) by MESFUNC8:def 9
.= dom(G1.0) by MESFUNC9:def 4; then
Integral(M,(-(lim(Partial_Sums G1)))|E)
= - Integral(M,(lim(Partial_Sums G1))|E)
by A24,A25,A27,Th55,MESFUNC9:44;
hence Integral(M,(lim(Partial_Sums F))|E) = Sum I by A16,A18,A20,A26;
end;
theorem
for X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
F be Functional_Sequence of X,ExtREAL, E be Element of S
st E = dom(F.0) & F.0 is nonpositive & F is with_the_same_dom
& (for n be Nat holds F.n is E-measurable)
& (for n,m be Nat st n <=m holds for x be Element of X st x in E
holds (F.n).x >= (F.m).x )
& (for x be Element of X st x in E holds F#x is convergent)
holds
ex I be ExtREAL_sequence st (for n be Nat holds I.n = Integral(M,F.n))
& I is convergent & Integral(M,lim F) = lim I
proof
let X be non empty set, S be SigmaField of X, M be sigma_Measure of S,
F be Functional_Sequence of X,ExtREAL, E be Element of S;
assume that
A1: E = dom(F.0) and
A2: F.0 is nonpositive and
A3: F is with_the_same_dom and
A4: for n be Nat holds F.n is E-measurable and
A5: for n,m be Nat st n <=m holds for x be Element of X st x in E
holds (F.n).x >= (F.m).x and
A6: for x be Element of X st x in E holds F#x is convergent;
set G = -F;
A7: G.0 = -(F.0) by Th37; then
A8: E = dom(G.0) by A1,MESFUNC1:def 7;
A11:for n be Nat holds G.n is E-measurable
proof
let n be Nat;
E = dom(F.n) by A1,A3,MESFUNC8:def 2; then
-(F.n) is E-measurable by A4,MEASUR11:63;
hence G.n is E-measurable by Th37;
end;
A13:for n,m be Nat st n <= m holds for x be Element of X st x in E
holds (G.n).x <= (G.m).x
proof
let n,m be Nat;
assume A14: n <= m;
let x be Element of X;
assume A15: x in E; then
A17: x in dom(G.n) & x in dom(G.m) by A8,A3,Th40,MESFUNC8:def 2;
G.n = -(F.n) & G.m = -(F.m) by Th37; then
(G.n).x = -((F.n).x) & (G.m).x = -((F.m).x) by A17,MESFUNC1:def 7;
hence (G.n).x <= (G.m).x by A15,A5,A14,XXREAL_3:38;
end;
A18:for x be Element of X st x in E holds G#x is convergent
proof
let x be Element of X;
assume x in E; then
F#x is convergent by A6; then
-(F#x) is convergent by DBLSEQ_3:17;
hence G#x is convergent by Th38;
end;
consider J be ExtREAL_sequence such that
A19: (for n be Nat holds J.n = Integral(M,G.n))
& J is convergent & Integral(M,lim G) = lim J
by A8,A2,A7,A3,Th40,A11,A13,A18,MESFUNC9:52;
set I = -J;
take I;
thus for n be Nat holds I.n = Integral(M,F.n)
proof
let n be Nat;
n in NAT by ORDINAL1:def 12; then
A20: n in dom I by FUNCT_2:def 1;
A21: dom(F.n) = E by A1,A3,MESFUNC8:def 2;
G.n = -(F.n) by Th37; then
Integral(M,G.n) = - Integral(M,F.n)
by A21,A4,Th52; then
J.n = - Integral(M,F.n) by A19; then
I.n = -(-Integral(M,F.n)) by A20,MESFUNC1:def 7;
hence I.n = Integral(M,F.n);
end;
thus I is convergent by A19,DBLSEQ_3:17;
A23:lim I = - Integral(M,lim G) by A19,DBLSEQ_3:17;
A24:E = dom(lim F) by A1,MESFUNC8:def 9; then
A25:dom(-(lim F)) = E by MESFUNC1:def 7; then
A26:dom(lim G) = dom(-(lim F)) by A8,MESFUNC8:def 9;
for x be Element of X st x in dom(lim G) holds (lim G).x = (-(lim F)).x
proof
let x be Element of X;
assume A27: x in dom(lim G); then
A30: (lim G).x = lim(G#x) by MESFUNC8:def 9;
A28: F#x is convergent by A27,A26,A25,A6;
G#x = -(F#x) by Th38; then
A29: lim(G#x) = - lim(F#x) by A28,DBLSEQ_3:17;
lim(F#x) = (lim F).x by A27,A26,A25,A24,MESFUNC8:def 9;
hence (lim G).x = (-(lim F)).x by A29,A30,A27,A26,MESFUNC1:def 7;
end; then
lim G = -(lim F) by A26,PARTFUN1:5; then
Integral(M,lim G) = - Integral(M,lim F)
by A1,A3,A4,A6,A24,Th52,MESFUNC8:25;
hence Integral(M,lim F) = lim I by A23;
end;