:: The Lebesgue Monotone Convergence Theorem
:: by Noboru Endou , Keiko Narita and Yasunari Shidama
::
:: Received March 18, 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, XBOOLE_0, PROB_1, MEASURE1, SUBSET_1, SEQFUNC, MESFUNC5,
PARTFUN1, XXREAL_0, NAT_1, RELAT_1, ARYTM_3, ARYTM_1, FUNCT_1, ORDINAL2,
CARD_1, COMPLEX1, SEQ_2, SUPINF_2, XXREAL_2, RINFSUP1, TARSKI, REAL_1,
PBOOLE, MESFUNC1, VALUED_1, FUNCT_3, MESFUNC2, SUPINF_1, VALUED_0,
RFUNCT_3, SERIES_1, CARD_3, MESFUNC8, MSSUBFAM, SETFAM_1, INTEGRA5,
FUNCOP_1, ZFMISC_1, FUNCT_2, MEASURE2, MESFUNC9, FUNCT_7, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_3,
XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, XXREAL_0, VALUED_0, RELAT_1,
FUNCT_1, RELSET_1, BINOP_1, FUNCT_2, PARTFUN1, NAT_1, PROB_1, SETFAM_1,
SUPINF_1, SUPINF_2, XXREAL_2, MEASURE1, MEASURE2, EXTREAL1, MESFUNC1,
MEASURE6, MESFUNC2, SEQFUNC, MESFUNC5, MESFUNC8, RINFSUP2, FUNCOP_1;
constructors REAL_1, EXTREAL1, BINOP_1, NEWTON, MESFUNC1, MEASURE2, MEASURE6,
MESFUNC2, MESFUNC5, MESFUNC8, RINFSUP2, SUPINF_1, SEQFUNC, RELSET_1,
BINOP_2, NUMBERS;
registrations SUBSET_1, NAT_1, XREAL_0, MEMBERED, ORDINAL1, PARTFUN1,
MEASURE1, FUNCT_2, RELAT_1, XBOOLE_0, NUMBERS, XXREAL_0, XCMPLX_0,
MESFUNC8, FUNCT_1, VALUED_0, XXREAL_3, RELSET_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions MESFUNC5, MESFUNC8, TARSKI, VALUED_0;
equalities MESFUNC5, BINOP_1, RINFSUP2, XXREAL_3, SUPINF_2;
expansions MESFUNC5, MESFUNC8, TARSKI, FUNCT_2;
theorems TARSKI, PARTFUN1, FUNCT_1, SUPINF_2, EXTREAL1, MESFUNC1, XREAL_0,
XBOOLE_0, XBOOLE_1, XCMPLX_1, MESFUNC2, XREAL_1, XXREAL_0, MESFUNC5,
PROB_1, NAT_1, RELAT_1, FUNCT_3, ZFMISC_1, FUNCT_2, MEASURE1, MESFUNC6,
SEQFUNC, ORDINAL1, SETFAM_1, MESFUNC8, RINFSUP2, MESFUNC7, SEQ_4,
RELSET_1, MEASURE2, XXREAL_2, VALUED_0, FUNCOP_1, XXREAL_3;
schemes FUNCT_2, NAT_1, BINOP_1, RECDEF_1, SEQFUNC, FUNCT_1;
begin :: Preliminaries
reserve X for non empty set,
S for SigmaField of X,
M for sigma_Measure of S,
E for Element of S,
F,G for Functional_Sequence of X,ExtREAL,
I for ExtREAL_sequence,
f,g for PartFunc of X,ExtREAL,
seq, seq1, seq2 for ExtREAL_sequence,
p for ExtReal,
n,m for Nat,
x for Element of X,
z,D for set;
theorem
f is without+infty & g is without+infty implies dom(f+g)=dom f /\ dom g
proof
assume that
A1: f is without+infty and
A2: g is without+infty;
not +infty in rng g by A2;
then
A3: g"{+infty} = {} by FUNCT_1:72;
not +infty in rng f by A1;
then f"{+infty} = {} by FUNCT_1:72;
then f"{+infty} /\ g"{-infty} \/ f"{-infty} /\ g"{+infty} = {} by A3;
then dom(f+g) = (dom f /\ dom g)\{} by MESFUNC1:def 3;
hence thesis;
end;
theorem
f is without+infty & g is without-infty implies dom(f-g)=dom f /\ dom g
proof
assume that
A1: f is without+infty and
A2: g is without-infty;
not +infty in rng f by A1;
then
A3: f"{+infty} = {} by FUNCT_1:72;
not -infty in rng g by A2;
then g"{-infty} = {} by FUNCT_1:72;
then g"{+infty} /\ f"{+infty} \/ g"{-infty} /\ f"{-infty} = {} by A3;
then dom(f-g) = (dom f /\ dom g)\{} by MESFUNC1:def 4;
hence thesis;
end;
theorem Th3:
f is without-infty & g is without-infty implies f+g is without-infty
proof
assume that
A1: f is without-infty and
A2: g is without-infty;
for x be set st x in dom(f+g) holds -infty < (f+g).x
proof
let x be set;
assume
A3: x in dom(f+g);
A4: -infty < f.x by A1;
A5: -infty < g.x by A2;
(f+g).x = f.x + g.x by A3,MESFUNC1:def 3;
hence thesis by A4,A5,XXREAL_0:6,XXREAL_3:17;
end;
hence thesis by MESFUNC5:10;
end;
theorem Th4:
f is without+infty & g is without+infty implies f+g is without+infty
proof
assume that
A1: f is without+infty and
A2: g is without+infty;
for x be set st x in dom(f+g) holds (f+g).x < +infty
proof
let x be set;
assume
A3: x in dom(f+g);
A4: f.x < +infty by A1;
A5: g.x < +infty by A2;
(f+g).x = f.x + g.x by A3,MESFUNC1:def 3;
hence thesis by A4,A5,XXREAL_0:4,XXREAL_3:16;
end;
hence thesis by MESFUNC5:11;
end;
theorem
f is without-infty & g is without+infty implies f-g is without-infty
proof
assume that
A1: f is without-infty and
A2: g is without+infty;
for x be set st x in dom(f-g) holds -infty < (f-g).x
proof
let x be set;
assume
A3: x in dom(f-g);
A4: -infty < f.x by A1;
A5: g.x < +infty by A2;
(f-g).x = f.x - g.x by A3,MESFUNC1:def 4;
hence thesis by A4,A5,XXREAL_0:6,XXREAL_3:19;
end;
hence thesis by MESFUNC5:10;
end;
theorem
f is without+infty & g is without-infty implies f-g is without+infty
proof
assume that
A1: f is without+infty and
A2: g is without-infty;
for x be set st x in dom(f-g) holds (f-g).x < +infty
proof
let x be set;
assume
A3: x in dom(f-g);
A4: f.x < +infty by A1;
A5: -infty < g.x by A2;
(f-g).x = f.x - g.x by A3,MESFUNC1:def 4;
hence thesis by A4,A5,XXREAL_0:4,XXREAL_3:18;
end;
hence thesis by MESFUNC5:11;
end;
theorem Th7:
( seq is convergent_to_finite_number implies ex g be Real
st lim seq = g & for p be Real st 0<p ex n be Nat st for m be Nat st n<=
m holds |. seq.m - lim seq .| < p ) & ( seq is convergent_to_+infty implies lim
seq = +infty ) & ( seq is convergent_to_-infty implies lim seq = -infty )
proof
A1: now
assume
A2: seq is convergent_to_finite_number;
then
A3: not seq is convergent_to_+infty by MESFUNC5:50;
A4: not seq is convergent_to_-infty by A2,MESFUNC5:51;
seq is convergent by A2;
then consider g be Real such that
A5: lim seq = g and
A6: for p be Real st 0<p ex n be Nat st for m be Nat st n<=m
holds |.seq.m - lim seq.| < p and
seq is convergent_to_finite_number by A3,A4,MESFUNC5:def 12;
take g;
thus ex g be Real st lim seq = g & for p be Real st 0<p ex n
be Nat st for m be Nat st n<=m holds |. seq.m - lim seq .| < p by A5,A6;
end;
A7: now
assume
A8: seq is convergent_to_-infty;
then seq is convergent;
hence lim seq = -infty by A8,MESFUNC5:def 12;
end;
now
assume
A9: seq is convergent_to_+infty;
then seq is convergent;
hence lim seq = +infty by A9,MESFUNC5:def 12;
end;
hence thesis by A1,A7;
end;
theorem Th8:
seq is nonnegative implies not seq is convergent_to_-infty
proof
assume
A1: seq is nonnegative;
assume seq is convergent_to_-infty;
then consider n be Nat such that
A2: for m be Nat st n<=m holds seq.m <= -1;
seq.n <= -1 by A2;
hence contradiction by A1,SUPINF_2:51;
end;
theorem Th9:
seq is convergent & (for k be Nat holds seq.k <= p) implies lim seq <= p
proof
assume that
A1: seq is convergent and
A2: for k be Nat holds seq.k <= p;
for y be ExtReal holds y in rng seq implies y <= p
proof
let y be ExtReal;
assume y in rng seq;
then consider x be object such that
A3: x in dom seq and
A4: y = seq.x by FUNCT_1:def 3;
reconsider x as Nat by A3;
seq.x <= p by A2;
hence thesis by A4;
end;
then
A5: p is UpperBound of rng seq by XXREAL_2:def 1;
reconsider SUPSEQ = superior_realsequence seq as sequence of ExtREAL;
consider Y be non empty Subset of ExtREAL such that
A6: Y = {seq.k where k is Nat: 0 <= k} and
A7: SUPSEQ.0 = sup Y by RINFSUP2:def 7;
now
let x be object;
assume x in rng seq;
then consider k be object such that
A8: k in dom seq and
A9: x = seq.k by FUNCT_1:def 3;
thus x in Y by A6,A8,A9;
end;
then
A10: rng seq c= Y;
for n be Element of NAT holds inf SUPSEQ <= SUPSEQ.n
proof
let n be Element of NAT;
NAT = dom SUPSEQ by FUNCT_2:def 1;
then SUPSEQ.n in rng SUPSEQ by FUNCT_1:def 3;
hence thesis by XXREAL_2:3;
end;
then
A11: inf SUPSEQ <= SUPSEQ.0;
now
let x be object;
assume x in Y;
then consider k be Nat such that
A12: x = seq.k & 0 <= k by A6;
A13: k in NAT by ORDINAL1:def 12;
dom seq = NAT by FUNCT_2:def 1;
hence x in rng seq by A12,FUNCT_1:3,A13;
end;
then Y c= rng seq;
then Y = rng seq by A10,XBOOLE_0:def 10;
then (superior_realsequence seq).0 <= p by A5,A7,XXREAL_2:def 3;
then lim_sup seq <= p by A11,XXREAL_0:2;
hence thesis by A1,RINFSUP2:41;
end;
theorem Th10:
seq is convergent & (for k be Nat holds p <= seq.k) implies p <= lim seq
proof
assume that
A1: seq is convergent and
A2: for k be Nat holds p <= seq.k;
for y be ExtReal holds y in rng seq implies p <= y
proof
let y be ExtReal;
assume y in rng seq;
then consider x be object such that
A3: x in dom seq and
A4: y = seq.x by FUNCT_1:def 3;
reconsider x as Nat by A3;
seq.x >= p by A2;
hence thesis by A4;
end;
then
A5: p is LowerBound of rng seq by XXREAL_2:def 2;
reconsider INFSEQ = inferior_realsequence seq as sequence of ExtREAL;
consider Y be non empty Subset of ExtREAL such that
A6: Y = {seq.k where k is Nat: 0 <= k} and
A7: INFSEQ.0 = inf Y by RINFSUP2:def 6;
now
let x be object;
assume x in rng seq;
then consider k be object such that
A8: k in dom seq and
A9: x = seq.k by FUNCT_1:def 3;
thus x in Y by A6,A8,A9;
end;
then
A10: rng seq c= Y;
for n be Element of NAT holds sup INFSEQ >= INFSEQ.n
proof
let n be Element of NAT;
NAT = dom INFSEQ by FUNCT_2:def 1;
then INFSEQ.n in rng INFSEQ by FUNCT_1:def 3;
hence thesis by XXREAL_2:4;
end;
then
A11: sup INFSEQ >= INFSEQ.0;
now
let x be object;
assume x in Y;
then consider k be Nat such that
A12: x = seq.k & 0 <= k by A6;
A13: k in NAT by ORDINAL1:def 12;
dom seq = NAT by FUNCT_2:def 1;
hence x in rng seq by A12,FUNCT_1:3,A13;
end;
then Y c= rng seq;
then Y = rng seq by A10,XBOOLE_0:def 10;
then (inferior_realsequence seq).0 >= p by A5,A7,XXREAL_2:def 4;
then lim_inf seq >= p by A11,XXREAL_0:2;
hence thesis by A1,RINFSUP2:41;
end;
reconsider zz=0 as ExtReal;
theorem Th11:
seq1 is convergent & seq2 is convergent & seq1 is nonnegative &
seq2 is nonnegative & (for k be Nat holds seq.k = seq1.k + seq2.k) implies seq
is nonnegative & seq is convergent & lim seq = lim seq1 + lim seq2
proof
assume that
A1: seq1 is convergent and
A2: seq2 is convergent and
A3: seq1 is nonnegative and
A4: seq2 is nonnegative and
A5: for k be Nat holds seq.k = seq1.k + seq2.k;
A6: not seq2 is convergent_to_-infty by A4,Th8;
for n be object st n in dom seq holds 0. <= seq.n
proof
let n be object;
assume n in dom seq;
then reconsider n1=n as Nat;
A7: 0 <= seq2.n1 by A4,SUPINF_2:51;
A8: seq.n1 = seq1.n1 + seq2.n1 by A5;
0 <= seq1.n1 by A3,SUPINF_2:51;
hence thesis by A7,A8;
end;
hence seq is nonnegative by SUPINF_2:52;
A9: not seq1 is convergent_to_-infty by A3,Th8;
for n be Nat holds 0 <= seq2.n by A4,SUPINF_2:51;
then
A10: lim seq2 <> -infty by A2,Th10;
per cases by A1,A9;
suppose
A11: seq1 is convergent_to_+infty;
for g be Real st 0 < g ex n be Nat st for m be Nat st n<=m
holds g <= seq.m
proof
let g be Real;
assume 0 < g;
then consider n be Nat such that
A12: for m be Nat st n <= m holds g <= seq1.m by A11;
take n;
let m be Nat;
assume n<=m;
then
A13: g <= seq1.m by A12;
0 <= seq2.m by A4,SUPINF_2:51;
then g + zz <= seq1.m + seq2.m by A13,XXREAL_3:36;
then g <= seq1.m + seq2.m by XXREAL_3:4;
hence thesis by A5;
end;
then
A14: seq is convergent_to_+infty;
hence seq is convergent;
then
A15: lim seq = +infty by A14,MESFUNC5:def 12;
lim seq1 = +infty by A1,A11,MESFUNC5:def 12;
hence thesis by A10,A15,XXREAL_3:def 2;
end;
suppose
A16: seq1 is convergent_to_finite_number;
then
A17: not seq1 is convergent_to_-infty by MESFUNC5:51;
not seq1 is convergent_to_+infty by A16,MESFUNC5:50;
then consider g be Real such that
A18: lim seq1 = g and
A19: for p be Real st 0<p ex n be Nat st for m be Nat st n<=m
holds |. seq1.m - lim seq1 .| < p and
seq1 is convergent_to_finite_number by A1,A17,MESFUNC5:def 12;
per cases by A2,A6;
suppose
A20: seq2 is convergent_to_+infty;
for g be Real st 0 < g ex n be Nat st for m be Nat st n<=m
holds g <= seq.m
proof
let g be Real;
assume 0 < g;
then consider n be Nat such that
A21: for m be Nat st n <= m holds g <= seq2.m by A20;
take n;
let m be Nat;
assume n<=m;
then
A22: g <= seq2.m by A21;
0 <= seq1.m by A3,SUPINF_2:51;
then g + zz <= seq1.m + seq2.m by A22,XXREAL_3:36;
then g <= seq1.m + seq2.m by XXREAL_3:4;
hence thesis by A5;
end;
then
A23: seq is convergent_to_+infty;
hence seq is convergent;
then
A24: lim seq = +infty by A23,MESFUNC5:def 12;
lim seq2 = +infty by A2,A20,MESFUNC5:def 12;
hence thesis by A18,A24,XXREAL_3:def 2;
end;
suppose
A25: seq2 is convergent_to_finite_number;
then
A26: seq2 is not convergent_to_-infty by MESFUNC5:51;
seq2 is not convergent_to_+infty by A25,MESFUNC5:50;
then consider h be Real such that
A27: lim seq2 = h and
A28: for p be Real st 0<p ex n be Nat st for m be Nat st n<=m
holds |. seq2.m - lim seq2 .| < p and
seq2 is convergent_to_finite_number by A2,A26,MESFUNC5:def 12;
reconsider h9=h, g9=g as Real;
reconsider gh = g+h as R_eal by XXREAL_0:def 1;
A29: for p be Real st 0<p ex n be Nat st for m be Nat st n <= m
holds |. seq.m - (g+h).| < p
proof
let p be Real;
reconsider pp= p as Element of REAL by XREAL_0:def 1;
assume
A30: 0 < p;
then consider n1 be Nat such that
A31: for m be Nat st n1 <= m holds |. seq1.m - lim seq1 .| < p/2 by A19;
consider n2 be Nat such that
A32: for m be Nat st n2 <= m holds |. seq2.m - lim seq2 .| < p/2 by A28,A30;
reconsider n19=n1, n29=n2 as Element of NAT by ORDINAL1:def 12;
reconsider n = max(n19,n29) as Nat;
take n;
let m be Nat;
assume
A33: n <= m;
A34: pp/2 in REAL by XREAL_0:def 1;
n2 <= n by XXREAL_0:25;
then n2 <= m by A33,XXREAL_0:2;
then
A35: |. seq2.m - lim seq2 .| < pp/2 by A32;
then |. seq2.m - lim seq2 .| < +infty by XXREAL_0:2,9,A34;
then
A36: seq2.m - h in REAL by A27,EXTREAL1:41;
n1 <= n by XXREAL_0:25;
then n1 <= m by A33,XXREAL_0:2;
then
A37: |. seq1.m - lim seq1 .| < pp/2 by A31;
then |. seq1.m - lim seq1 .| < +infty by XXREAL_0:2,9,A34;
then seq1.m - g in REAL by A18,EXTREAL1:41;
then consider e1,e2 be Real such that
A38: e1 = seq1.m - g and
A39: e2 = seq2.m - h by A36;
A40: |. seq2.m - h .| = |.e2 qua Complex.| by A39,EXTREAL1:12;
A41: 0 <= seq2.m by A4,SUPINF_2:51;
then
A42: seq2.m - h <> -infty by XXREAL_3:19;
A43: 0 <= seq1.m by A3,SUPINF_2:51;
A44: |. seq1.m - g .| = |.e1 qua Complex.| by A38,EXTREAL1:12;
then
A45: |. seq2.m - h .| + |. seq1.m - g .|
= |.e1 qua Complex.| + |.e2 qua Complex.|
by A40,SUPINF_2:1;
(g+h) = g + (h qua ExtReal);
then seq.m - (g+h) = seq.m - h - g by XXREAL_3:31
.= seq1.m + seq2.m - h - g by A5
.= seq1.m + (seq2.m - h) - g by A43,A41,XXREAL_3:30
.= (seq2.m - h) + (seq1.m - g) by A43,A42,XXREAL_3:30;
then
A46: |. seq.m - (g+h) .| <= |. seq2.m - h .| + |. seq1.m - g .|
by EXTREAL1:24;
|.e1 qua Complex.| + |.e2 qua Complex.| < p/2 + p/2
by A18,A27,A37,A35,A44,A40,XREAL_1:8;
hence thesis by A46,A45,XXREAL_0:2;
end;
then
A47: seq is convergent_to_finite_number;
hence seq is convergent;
then lim seq = gh by A29,A47,MESFUNC5:def 12;
hence thesis by A18,A27,SUPINF_2:1;
end;
end;
end;
theorem Th12:
(for n be Nat holds G.n = (F.n)|D) & x in D implies (F#x is
convergent_to_+infty implies G#x is convergent_to_+infty) & (F#x is
convergent_to_-infty implies G#x is convergent_to_-infty) & (F#x is
convergent_to_finite_number implies G#x is convergent_to_finite_number) & (F#x
is convergent implies G#x is convergent)
proof
assume that
A1: for n be Nat holds G.n = (F.n)|D and
A2: x in D;
thus
A3: F#x is convergent_to_+infty implies G#x is convergent_to_+infty
proof
assume
A4: F#x is convergent_to_+infty;
let g be Real;
assume 0 < g;
then consider n be Nat such that
A5: for m be Nat st n <= m holds g <= (F#x).m by A4;
take n;
let m be Nat;
assume n <= m;
then g <= (F#x).m by A5;
then g <= (F.m).x by MESFUNC5:def 13;
then g <= ((F.m)|D).x by A2,FUNCT_1:49;
then g <= (G.m).x by A1;
hence g <= (G#x).m by MESFUNC5:def 13;
end;
thus
A6: F#x is convergent_to_-infty implies G#x is convergent_to_-infty
proof
assume
A7: F#x is convergent_to_-infty;
let g be Real;
assume g < 0;
then consider n be Nat such that
A8: for m be Nat st n <= m holds (F#x).m <= g by A7;
take n;
let m be Nat;
assume n <= m;
then (F#x).m <= g by A8;
then (F.m).x <= g by MESFUNC5:def 13;
then ((F.m)|D).x <= g by A2,FUNCT_1:49;
then (G.m).x <= g by A1;
hence (G#x).m <= g by MESFUNC5:def 13;
end;
thus
A9: F#x is convergent_to_finite_number implies G#x is
convergent_to_finite_number
proof
assume F#x is convergent_to_finite_number;
then consider g be Real such that
A10: lim(F#x) = g and
A11: for p be Real st 0<p ex n be Nat st for m be Nat st n<=m
holds |. (F#x).m - lim(F#x) .| < p by Th7;
for p be Real st 0 < p ex n be Nat st for m be Nat st n <= m
holds |. (G#x).m - (g) .| < p
proof
let p be Real;
assume 0 < p;
then consider n be Nat such that
A12: for m be Nat st n <= m holds |. (F#x).m - lim(F#x) .| < p by A11;
take n;
let m be Nat;
(F#x).m = (F.m).x by MESFUNC5:def 13;
then (F#x).m = ((F.m)|D).x by A2,FUNCT_1:49;
then
A13: (F#x).m = (G.m).x by A1;
assume n <= m;
then |. (F#x).m - lim(F#x) .| < p by A12;
hence thesis by A10,A13,MESFUNC5:def 13;
end;
hence thesis;
end;
assume
A14: F#x is convergent;
per cases by A14;
suppose
F#x is convergent_to_+infty;
hence thesis by A3;
end;
suppose
F#x is convergent_to_-infty;
hence thesis by A6;
end;
suppose
F#x is convergent_to_finite_number;
hence thesis by A9;
end;
end;
theorem Th13:
E = dom f & f is E-measurable & f is nonnegative & M.(E /\
eq_dom(f,+infty)) <> 0 implies Integral(M,f) = +infty
proof
assume that
A1: E = dom f and
A2: f is E-measurable and
A3: f is nonnegative and
A4: M.(E /\ eq_dom(f,+infty)) <> 0;
reconsider EE = E /\ eq_dom(f,+infty) as Element of S by A1,A2,MESFUNC1:33;
A5: dom(f|E) = E by A1;
E = dom f /\ E by A1;
then
A6: f|E is E-measurable by A2,MESFUNC5:42;
integral+(M,f|EE) <= integral+(M,f|E) by A1,A2,A3,MESFUNC5:83,XBOOLE_1:17;
then
A7: integral+(M,f|EE) <= Integral(M,f|E) by A3,A6,A5,MESFUNC5:15,88;
A8: EE = dom f /\ EE by A1,XBOOLE_1:17,28;
f is EE-measurable by A2,MESFUNC1:30,XBOOLE_1:17;
then
A9: f|EE is EE-measurable by A8,MESFUNC5:42;
A10: f|EE is nonnegative by A3,MESFUNC5:15;
reconsider ES = {} as Element of S by PROB_1:4;
deffunc G(Element of NAT) = $1(#)((chi(EE,X))|EE);
consider G be Function such that
A11: dom G = NAT & for n be Element of NAT holds G.n = G(n) from FUNCT_1
:sch 4;
now
let g be object;
assume g in rng G;
then consider m be object such that
A12: m in dom G and
A13: g = G.m by FUNCT_1:def 3;
reconsider m as Element of NAT by A11,A12;
g = m(#)((chi(EE,X))|EE) by A11,A13;
hence g in PFuncs(X,ExtREAL) by PARTFUN1:45;
end;
then rng G c= PFuncs(X,ExtREAL);
then reconsider G as Functional_Sequence of X,ExtREAL by A11,FUNCT_2:def 1
,RELSET_1:4;
A14: for n be Nat holds dom(G.n) = EE & for x be set st x in dom(G.n) holds (
G.n).x = n
proof
let n be Nat;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
EE c= X;
then EE c= dom(chi(EE,X)) by FUNCT_3:def 3;
then
A15: dom((chi(EE,X))|EE) = EE by RELAT_1:62;
A16: G.n = n1(#)((chi(EE,X))|EE) by A11;
hence
A17: dom(G.n) = EE by A15,MESFUNC1:def 6;
let x be set;
assume
A18: x in dom(G.n);
then reconsider x1=x as Element of X;
chi(EE,X).x1 = 1. by A17,A18,FUNCT_3:def 3;
then ((chi(EE,X))|EE).x1 = 1. by A15,A17,A18,FUNCT_1:47;
then (G.n).x = ( n1) * 1. by A16,A18,MESFUNC1:def 6;
hence thesis by XXREAL_3:81;
end;
A19: for n be Nat holds G.n is nonnegative
proof
let n be Nat;
for x be object st x in dom(G.n) holds 0 <= (G.n).x by A14;
hence thesis by SUPINF_2:52;
end;
deffunc K(Element of NAT) = integral'(M,G.$1);
consider K be sequence of ExtREAL such that
A20: for n be Element of NAT holds K.n = K(n) from FUNCT_2:sch 4;
reconsider K as ExtREAL_sequence;
A21: for n be Nat holds K.n=integral'(M,G.n)
proof
let n be Nat;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
K.n = integral'(M,G.n1) by A20;
hence thesis;
end;
A22: dom(f|EE) = EE by A1,RELAT_1:62,XBOOLE_1:17;
A23: for n,m be Nat st n <=m holds for x be Element of X st x in dom(f|EE)
holds (G.n).x <= (G.m).x
proof
let n,m be Nat such that
A24: n <= m;
let x be Element of X;
assume
A25: x in dom(f|EE);
then x in dom(G.n) by A22,A14;
then
A26: (G.n).x = n by A14;
x in dom(G.m) by A22,A14,A25;
hence thesis by A14,A24,A26;
end;
A27: for n be Nat holds dom(G.n) = dom(f|EE) & G.n is_simple_func_in S
proof
let n be Nat;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
thus
A28: dom(G.n) = dom(f|EE) by A22,A14;
for x be object st x in dom(G.n) holds (G.n).x = n1 by A14;
hence thesis by A22,A28,MESFUNC6:2;
end;
A29: for i be Element of NAT holds K.i = ( i)*(M.(dom(G.i)))
proof
let i be Element of NAT;
reconsider ii=i as R_eal by XXREAL_0:def 1;
for x be object st x in dom(G.i) holds (G.ii).x = ii by A14;
then integral'(M,G.i) = (ii)*(M.(dom(G.ii)))
by A27,MESFUNC5:71;
hence thesis by A21;
end;
M.ES <= M.EE by MEASURE1:31,XBOOLE_1:2;
then
A30: In(0,REAL) < M.EE by A4,VALUED_0:def 19;
A31: not rng K is bounded_above
proof
assume rng K is bounded_above;
then consider UB be Real such that
A32: UB is UpperBound of rng K by XXREAL_2:def 10;
reconsider r = UB as Real;
per cases by A30,XXREAL_0:10;
suppose
A33: M.EE = +infty;
K.1 = ( 1) * (M.(dom(G.1))) by A29;
then K.1 = ( 1) * (M.EE) by A14;
then
A34: K.1 = +infty by A33,XXREAL_3:def 5;
dom K = NAT by FUNCT_2:def 1;
then K.1 in rng K by FUNCT_1:3;
then K.1 <= UB by A32,XXREAL_2:def 1;
hence contradiction by A34,XXREAL_0:4;
end;
suppose
M.EE in REAL;
then reconsider ee = M.EE as Real;
consider n be Nat such that
A35: r/ee < n by SEQ_4:3;
A36: n in NAT by ORDINAL1:def 12;
K.n = ( n) * (M.(dom(G.n))) by A29,A36;
then K.n = ( n) * (M.EE) by A14;
then
A37: K.n = n * ee by EXTREAL1:1;
(r/ee) * ee < n * ee by A30,A35,XREAL_1:68;
then r / (ee/ee) < K.n by A37,XCMPLX_1:82;
then
A38: r < K.n by A4,XCMPLX_1:51;
dom K = NAT by FUNCT_2:def 1;
then K.n in rng K by FUNCT_1:3,A36;
then K.n <= r by A32,XXREAL_2:def 1;
hence contradiction by A38;
end;
end;
for n,m be Nat st m <= n holds K.m <= K.n
proof
let n,m be Nat;
A39: n in NAT by ORDINAL1:def 12;
A40: m in NAT by ORDINAL1:def 12;
dom(G.m) = EE by A14;
then
A41: K.m = ( m)*M.EE by A29,A40;
dom(G.n) = EE by A14;
then
A42: K.n = ( n)*M.EE by A29,A39;
assume m <= n;
hence thesis by A30,A41,A42,XXREAL_3:71;
end;
then
A43: K is non-decreasing by RINFSUP2:7;
then
A44: lim K = sup K by RINFSUP2:37;
A45: for x be Element of X st x in dom(f|EE) holds G#x is convergent & lim(G#
x) = (f|EE).x
proof
let x be Element of X;
assume
A46: x in dom(f|EE);
then
A47: x in EE by A1,RELAT_1:62,XBOOLE_1:17;
then x in eq_dom(f,+infty) by XBOOLE_0:def 4;
then f.x = +infty by MESFUNC1:def 15;
then
A48: (f|EE).x = +infty by A47,FUNCT_1:49;
A49: rng(G#x) is not bounded_above
proof
assume rng(G#x) is bounded_above;
then consider UB be Real such that
A50: UB is UpperBound of rng(G#x) by XXREAL_2:def 10;
reconsider r = UB as Real;
consider n be Nat such that
A51: r < n by SEQ_4:3;
x in dom(G.n) by A14,A47;
then (G.n).x = n by A14;
then
A52: UB < (G#x).n by A51,MESFUNC5:def 13;
A53: n in NAT by ORDINAL1:def 12;
dom(G#x) = NAT by FUNCT_2:def 1;
then (G#x).n in rng(G#x) by FUNCT_1:3,A53;
hence contradiction by A52,A50,XXREAL_2:def 1;
end;
for n,m be Nat st m<=n holds (G#x).m <= (G#x).n
proof
let n,m be Nat;
dom(G.n) = EE by A14;
then
A54: (G.n).x = n by A22,A14,A46;
dom(G.m) = EE by A14;
then (G.m).x = m by A22,A14,A46;
then
A55: (G#x).m = m by MESFUNC5:def 13;
assume m <= n;
hence thesis by A54,A55,MESFUNC5:def 13;
end;
then
A56: G#x is non-decreasing by RINFSUP2:7;
sup rng(G#x) is UpperBound of rng(G#x) by XXREAL_2:def 3;
then sup(G#x) = +infty by A49,XXREAL_2:53;
hence thesis by A56,A48,RINFSUP2:37;
end;
sup rng K is UpperBound of rng K by XXREAL_2:def 3;
then
A57: sup K = +infty by A31,XXREAL_2:53;
K is convergent by A43,RINFSUP2:37;
then integral+(M,f|EE) = +infty by A10,A22,A9,A27,A19,A23,A45,A21,A44,A57,
MESFUNC5:def 15;
then Integral(M,f|E) = +infty by A7,XXREAL_0:4;
hence thesis by A1;
end;
reconsider jj=1 as Real;
theorem
Integral(M,chi(E,X)) = M.E & Integral(M,(chi(E,X))|E) = M.E
proof
reconsider XX = X as Element of S by MEASURE1:7;
set F = XX \ E;
A1: now
let x be Element of X;
assume
A2: x in dom(max- chi(E,X));
per cases;
suppose
x in E;
then chi(E,X).x = 1 by FUNCT_3:def 3;
then max(-(chi(E,X).x),0.) = 0. by XXREAL_0:def 10;
hence (max-(chi(E,X))).x = 0 by A2,MESFUNC2:def 3;
end;
suppose
not x in E;
then chi(E,X).x = 0. by FUNCT_3:def 3;
then -chi(E,X).x = 0;
then max(-(chi(E,X).x),0.) = 0;
hence (max-(chi(E,X))).x = 0 by A2,MESFUNC2:def 3;
end;
end;
A3: XX = dom chi(E,X) by FUNCT_3:def 3;
then
A4: XX = dom(max+(chi(E,X))) by MESFUNC7:23;
A5: XX /\ F = F by XBOOLE_1:28;
then
A6: dom((max+(chi(E,X)))|F) = F by A4,RELAT_1:61;
A7: now
let x be Element of X;
assume
A8: x in dom((max+(chi(E,X)))|F);
then chi(E,X).x = 0 by A6,FUNCT_3:37;
then (max+(chi(E,X))).x = 0 by MESFUNC7:23;
hence ((max+(chi(E,X)))|F).x = 0 by A8,FUNCT_1:47;
end;
A9: chi(E,X) is XX-measurable by MESFUNC2:29;
then
A10: max+(chi(E,X)) is XX-measurable by MESFUNC7:23;
then max+(chi(E,X)) is F-measurable by MESFUNC1:30;
then
A11: integral+(M,(max+ chi(E,X))|F) = 0 by A4,A5,A6,A7,MESFUNC5:42,87;
A12: XX /\ E = E by XBOOLE_1:28;
then
A13: dom((max+(chi(E,X)))|E) = E by A4,RELAT_1:61;
E \/ F = XX by A12,XBOOLE_1:51;
then
A14: (max+ chi(E,X))|(E\/F) = max+ chi(E,X);
A15: for x be object st x in dom max+(chi(E,X)) holds 0. <= (max+(chi(E,X))).x
by MESFUNC2:12;
then
A16: max+(chi(E,X)) is nonnegative by SUPINF_2:52;
then integral+(M,(max+ chi(E,X))|(E\/F)) = integral+(M,(max+ chi(E,X))|E) +
integral+(M,(max+ chi(E,X))|F) by A4,A10,MESFUNC5:81,XBOOLE_1:79;
then
A17: integral+(M,max+ chi(E,X)) = integral+(M,(max+ chi(E,X))|E) by A14,A11,
XXREAL_3:4;
A18: now
let x be object;
assume
A19: x in dom((max+(chi(E,X)))|E);
then chi(E,X).x = 1 by A13,FUNCT_3:def 3;
then (max+(chi(E,X))).x = 1 by MESFUNC7:23;
hence ((max+(chi(E,X)))|E).x = 1 by A19,FUNCT_1:47;
end;
then (max+(chi(E,X)))|E is_simple_func_in S by A13,MESFUNC6:2;
then integral+(M,max+ chi(E,X)) = integral'(M,(max+ chi(E,X))|E) by A16,A17,
MESFUNC5:15,77;
then
A20: integral+(M,max+ chi(E,X)) = jj * M.(dom((max+(chi(E,X)))|E))
by A13,A18,MESFUNC5:104;
max+(chi(E,X)) is E-measurable by A10,MESFUNC1:30;
then (max+(chi(E,X)))|E is E-measurable by A4,A12,MESFUNC5:42;
then
A21: (chi(E,X))|E is E-measurable by MESFUNC7:23;
(max+(chi(E,X)))|E is nonnegative by A15,MESFUNC5:15,SUPINF_2:52;
then
A22: (chi(E,X))|E is nonnegative by MESFUNC7:23;
E = dom((chi(E,X))|E) by A13,MESFUNC7:23;
then
A23: Integral(M,(chi(E,X))|E) =integral+(M,(chi(E,X))|E) by A21,A22,MESFUNC5:88
;
XX = dom(max- chi(E,X)) by A3,MESFUNC2:def 3;
then integral+(M,max- chi(E,X)) = 0 by A3,A9,A1,MESFUNC2:26,MESFUNC5:87;
then Integral(M,chi(E,X)) = 1 * M.E by A13,A20,XXREAL_3:15;
hence Integral(M,chi(E,X)) = M.E by XXREAL_3:81;
(chi(E,X))|E = (max+ chi(E,X))|E by MESFUNC7:23;
hence thesis by A13,A17,A20,A23,XXREAL_3:81;
end;
theorem Th15:
E c= dom f & E c= dom g & f is E-measurable & g
is E-measurable & f is nonnegative & (for x be Element of X st x in E holds
f.x <= g.x) implies Integral(M,f|E) <= Integral(M,g|E)
proof
assume that
A1: E c= dom f and
A2: E c= dom g and
A3: f is E-measurable and
A4: g is E-measurable and
A5: f is nonnegative and
A6: for x be Element of X st x in E holds f.x <= g.x;
set F2 = g|E;
A7: E = dom(f|E) by A1,RELAT_1:62;
set F1 = f|E;
A8: F1 is nonnegative by A5,MESFUNC5:15;
A9: E = dom(g|E) by A2,RELAT_1:62;
A10: for x be Element of X st x in dom F1 holds F1.x <= F2.x
proof
let x be Element of X;
assume
A11: x in dom F1;
then
A12: F1.x = f.x by FUNCT_1:47;
F2.x = g.x by A7,A9,A11,FUNCT_1:47;
hence thesis by A6,A7,A11,A12;
end;
for x be object st x in dom F2 holds 0 <= F2.x
proof
let x be object;
assume
A13: x in dom F2;
0 <= F1.x by A8,SUPINF_2:51;
hence thesis by A7,A9,A10,A13;
end;
then
A14: F2 is nonnegative by SUPINF_2:52;
A15: dom g /\ E = E by A2,XBOOLE_1:28;
then
A16: F2 is E-measurable by A4,MESFUNC5:42;
A17: dom f /\ E = E by A1,XBOOLE_1:28;
then F1 is E-measurable by A3,MESFUNC5:42;
then integral+(M,F1) <= integral+(M,F2) by A8,A7,A9,A10,A14,A16,MESFUNC5:85;
then Integral(M,F1) <= integral+(M,F2) by A3,A8,A7,A17,MESFUNC5:42,88;
hence thesis by A4,A9,A14,A15,MESFUNC5:42,88;
end;
begin :: Selected Properties of Extended Real Sequence
definition
let s be ext-real-valued Function;
func Partial_Sums s -> ExtREAL_sequence means
:Def1:
it.0=s.0 & for n be Nat holds it.(n+1) = it.n + s.(n+1);
existence
proof
deffunc U(Nat,R_eal) = $2 + s.($1+1);
consider f being sequence of ExtREAL such that
A1: f.0 = s.0 & for n being Nat holds f.(n+1) = U(n,f.n) from NAT_1:
sch 12;
take f;
thus thesis by A1;
end;
uniqueness
proof
let s1,s2 be ExtREAL_sequence;
assume that
A2: s1.0=s.0 and
A3: for n be Nat holds s1.(n+1)=s1.n + s.(n+1) and
A4: s2.0=s.0 and
A5: for n be Nat holds s2.(n+1)=s2.n + s.(n+1);
defpred X[Nat] means s1.$1 = s2.$1;
A6: for k be Nat st X[k] holds X[k+1]
proof
let k be Nat;
assume s1.k =s2.k;
hence s1.(k+1) = s2.k + s.(k+1) by A3
.= s2.(k+1) by A5;
end;
A7: X[ 0 ] by A2,A4;
for n be Nat holds X[n] from NAT_1:sch 2(A7,A6);
hence s1 = s2;
end;
end;
definition
let s be ext-real-valued Function;
attr s is summable means
Partial_Sums s is convergent;
end;
definition
let s be ext-real-valued Function;
func Sum s -> R_eal equals
lim Partial_Sums s;
correctness;
end;
theorem Th16:
seq is nonnegative implies Partial_Sums seq is nonnegative &
Partial_Sums seq is non-decreasing
proof
set PS = Partial_Sums seq;
defpred P[Nat] means 0 <= PS.$1;
assume
A1: seq is nonnegative;
A2: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A3: P[k];
A4: PS.(k+1) = PS.k + seq.(k+1) by Def1;
seq.(k+1) >= 0 by A1,SUPINF_2:51;
hence thesis by A3,A4;
end;
PS.0 = seq.0 by Def1;
then
A5: P[ 0 ] by A1,SUPINF_2:51;
for m be Nat holds P[m] from NAT_1:sch 2(A5,A2);
then for k be object st k in dom PS holds 0 <= PS.k;
hence PS is nonnegative by SUPINF_2:52;
for n,m be Nat st m <= n holds (Partial_Sums seq).m <= (
Partial_Sums seq).n
proof
let n,m be Nat;
reconsider m1=m as Nat;
defpred Q[Nat] means PS.m1 <= PS.$1;
A6: for k be Nat holds PS.k <= PS.(k+1)
proof
let k be Nat;
A7: 0 <= seq.(k+1) by A1,SUPINF_2:51;
PS.(k+1) = PS.k + seq.(k+1) by Def1;
hence thesis by A7,XXREAL_3:39;
end;
A8: for k be Nat st k >= m1 & (for l be Nat st l >= m1 & l < k holds Q[l])
holds Q[k]
proof
let k be Nat;
assume that
A9: k >= m1 and
A10: for l be Nat st l >= m1 & l < k holds Q[l];
now
assume k > m1;
then
A11: k >= m1 + 1 by NAT_1:13;
per cases by A11,XXREAL_0:1;
suppose
k = m1 + 1;
hence thesis by A6;
end;
suppose
A12: k > m1 + 1;
then reconsider l = k-1 as Element of NAT by NAT_1:20;
k < k+1 by NAT_1:13;
then
A13: k > l by XREAL_1:19;
k = l+1;
then
A14: PS.l <= PS.k by A6;
l >= m1 by A12,XREAL_1:19;
then PS.m1 <= PS.l by A10,A13;
hence thesis by A14,XXREAL_0:2;
end;
end;
hence thesis by A9,XXREAL_0:1;
end;
A15: for k be Nat st k >= m1 holds Q[k] from NAT_1:sch 9(A8);
assume m <= n;
hence thesis by A15;
end;
hence thesis by RINFSUP2:7;
end;
theorem
(for n be Nat holds 0 < seq.n) implies for m be Nat holds 0 < (
Partial_Sums seq).m
proof
defpred P[Nat] means 0 < (Partial_Sums seq).$1;
assume
A1: for n be Nat holds 0 < seq.n;
A2: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A3: P[k];
A4: (Partial_Sums seq).(k+1) = (Partial_Sums seq).k + seq.(k+1) by Def1;
seq.(k+1) > 0 by A1;
hence thesis by A3,A4;
end;
(Partial_Sums seq).0 = seq.0 by Def1;
then
A5: P[ 0 ] by A1;
thus for m be Nat holds P[m] from NAT_1:sch 2(A5,A2);
end;
theorem Th18:
F is with_the_same_dom & (for n be Nat holds G.n = (F.n)|D)
implies G is with_the_same_dom
proof
assume that
A1: F is with_the_same_dom and
A2: for n be Nat holds G.n = (F.n)|D;
let n,m be Nat;
G.m = (F.m)|D by A2;
then
A3: dom(G.m) = dom(F.m) /\ D by RELAT_1:61;
G.n = (F.n)|D by A2;
then dom(G.n) = dom(F.n) /\ D by RELAT_1:61;
hence thesis by A1,A3;
end;
theorem Th19:
D c= dom(F.0) & (for n be Nat holds G.n = (F.n)|D) & (for x be
Element of X st x in D holds F#x is convergent) implies (lim F)|D = lim G
proof
assume that
A1: D c= dom(F.0) and
A2: for n be Nat holds G.n = (F.n)|D and
A3: for x be Element of X st x in D holds F#x is convergent;
G.0 = (F.0)|D by A2;
then
A4: dom(G.0) = D by A1,RELAT_1:62;
A5: dom((lim F)|D) = dom(lim F) /\ D by RELAT_1:61;
then dom((lim F)|D) = dom(F.0) /\ D by MESFUNC8:def 9;
then dom((lim F)|D) = D by A1,XBOOLE_1:28;
then
A6: dom((lim F)|D) = dom(lim G) by A4,MESFUNC8:def 9;
now
let x be Element of X;
assume
A7: x in dom((lim F)|D);
then
A8: ((lim F)|D).x = (lim F).x by FUNCT_1:47;
x in dom(lim F) by A5,A7,XBOOLE_0:def 4;
then
A9: ((lim F)|D).x = lim(F#x) by A8,MESFUNC8:def 9;
A10: x in D by A7,RELAT_1:57;
then
A11: F#x is convergent by A3;
per cases by A11;
suppose
A12: F#x is convergent_to_+infty;
then G#x is convergent_to_+infty by A2,A10,Th12;
then lim(G#x) = +infty by Th7;
then (lim G).x = +infty by A6,A7,MESFUNC8:def 9;
hence (lim G).x = ((lim F)|D).x by A9,A12,Th7;
end;
suppose
A13: F#x is convergent_to_-infty;
then G#x is convergent_to_-infty by A2,A10,Th12;
then lim(G#x) = -infty by Th7;
then (lim G).x = -infty by A6,A7,MESFUNC8:def 9;
hence (lim G).x = ((lim F)|D).x by A9,A13,Th7;
end;
suppose
A14: F#x is convergent_to_finite_number;
then consider g be Real such that
A15: lim(F#x) = g and
A16: for p be Real st 0<p ex n be Nat st for m be Nat st n<=m
holds |. (F#x).m - lim(F#x) .| < p by Th7;
A17: now
let p be Real;
assume 0 < p;
then consider n be Nat such that
A18: for m be Nat st n <= m holds |. (F#x).m - lim(F#x) .| < p by A16;
take n;
let m be Nat;
(F#x).m = (F.m).x by MESFUNC5:def 13;
then (F#x).m = ((F.m)|D).x by A10,FUNCT_1:49;
then
A19: (F#x).m = (G.m).x by A2;
assume n <= m;
then |. (F#x).m - lim(F#x) .| < p by A18;
hence |. (G#x).m - g .| < p by A15,A19,MESFUNC5:def 13;
end;
reconsider g as R_eal by XXREAL_0:def 1;
A20: G#x is convergent_to_finite_number by A2,A10,A14,Th12;
then G#x is convergent;
then lim(G#x) = g by A17,A20,MESFUNC5:def 12;
hence (lim G).x = ((lim F)|D).x by A6,A7,A9,A15,MESFUNC8:def 9;
end;
end;
hence thesis by A6,PARTFUN1:5;
end;
theorem Th20:
F is with_the_same_dom & E c= dom(F.0) & (for m be Nat holds F.m
is E-measurable & G.m= (F.m)|E) implies G.n is E-measurable
proof
assume that
A1: F is with_the_same_dom and
A2: E c= dom(F.0) and
A3: for m be Nat holds F.m is E-measurable & G.m= (F.m)|E;
dom(F.n) = dom(F.0) by A1;
then dom(F.n) /\ E = E by A2,XBOOLE_1:28;
then (F.n)|E is E-measurable by A3,MESFUNC5:42;
hence thesis by A3;
end;
theorem Th21:
E c= dom(F.0) & G is with_the_same_dom & (for x be Element of X
st x in E holds F#x is summable) & (for n be Nat holds G.n= (F.n)|E) implies
for x be Element of X st x in E holds G#x is summable
proof
assume that
A1: E c= dom(F.0) and
A2: G is with_the_same_dom and
A3: for x be Element of X st x in E holds F#x is summable and
A4: for n be Nat holds G.n= (F.n)|E;
let x be Element of X;
assume
A5: x in E;
dom((F.0)|E) = E by A1,RELAT_1:62;
then
A6: E = dom(G.0) by A4;
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 A2,A6;
then x in dom((F.n)|E) by A4,A5;
then ((F.n)|E).x = (F.n).x by FUNCT_1:47;
then
A7: (G.n).x = (F.n).x by A4;
(F#x).n = (F.n).x by MESFUNC5:def 13;
hence thesis by A7,MESFUNC5:def 13;
end;
then
A8: Partial_Sums(F#x) = Partial_Sums(G#x) by FUNCT_2:63;
F#x is summable by A3,A5;
then Partial_Sums(F#x) is convergent;
hence thesis by A8;
end;
begin :: Partial Sums of Functional Sequence and their Properties
definition
let X be non empty set, F be Functional_Sequence of X,ExtREAL;
func Partial_Sums F -> Functional_Sequence of X,ExtREAL means
:Def4:
it.0 = F.0 & for n be Nat holds it.(n+1) = it.n + F.(n+1);
existence
proof
defpred P[Nat,set,set] means (not $2 is PartFunc of X,ExtREAL &
$3 = F.$1) or ($2 is PartFunc of X,ExtREAL & for F2 be PartFunc of X,ExtREAL st
F2 = $2 holds $3 = F2 + F.($1+1));
A1: for n being Nat for x being set ex y being set st P[n,x,y]
proof
let n be Nat;
let x be set;
thus ex y be set st P[n,x,y]
proof
per cases;
suppose
A2: not x is PartFunc of X,ExtREAL;
take y = F.n;
thus not x is PartFunc of X,ExtREAL & y = F.n or (x is PartFunc of X
,ExtREAL & for F2 be PartFunc of X,ExtREAL st F2 = x holds y = F2 + F.(n+1))
by A2;
end;
suppose
x is PartFunc of X,ExtREAL;
then reconsider G2 = x as PartFunc of X,ExtREAL;
take y = G2 + F.(n+1);
thus not x is PartFunc of X,ExtREAL & y = F.n or (x is PartFunc of X
,ExtREAL & for F2 be PartFunc of X,ExtREAL st F2 = x holds y = F2 + F.(n+1));
end;
end;
end;
consider IT being Function such that
A3: dom IT = NAT & IT.0 = F.0 & for n being Nat holds P[n,
IT.n,IT.(n+1)] from RECDEF_1:sch 1(A1);
now
defpred IND[Nat] means IT.$1 is PartFunc of X,ExtREAL;
let f be object;
assume f in rng IT;
then consider m be object such that
A4: m in dom IT and
A5: f = IT.m by FUNCT_1:def 3;
reconsider m as Element of NAT by A3,A4;
A6: for n be Nat st IND[n] holds IND[n+1]
proof
let n be Nat;
assume IND[n];
then reconsider F2 = IT.n as PartFunc of X,ExtREAL;
IT.(n+1) = F2 + F.(n+1) by A3;
hence thesis;
end;
A7: IND[ 0 ] by A3;
for n be Nat holds IND[n] from NAT_1:sch 2(A7,A6);
then IT.m is PartFunc of X,ExtREAL;
hence f in PFuncs(X,ExtREAL) by A5,PARTFUN1:45;
end;
then rng IT c= PFuncs(X,ExtREAL);
then reconsider IT as Functional_Sequence of X,ExtREAL by A3,FUNCT_2:def 1
,RELSET_1:4;
take IT;
thus thesis by A3;
end;
uniqueness
proof
let PS1,PS2 be Functional_Sequence of X,ExtREAL;
assume that
A8: PS1.0 = F.0 and
A9: for n be Nat holds PS1.(n+1) = PS1.n + F.(n+1) and
A10: PS2.0 = F.0 and
A11: for n be Nat holds PS2.(n+1) = PS2.n + F.(n+1);
defpred IND[Nat] means PS1.$1 = PS2.$1;
A12: for n be Nat st IND[n] holds IND[n+1]
proof
let n be Nat;
assume
A13: IND[n];
PS1.(n+1) = PS1.n + F.(n+1) by A9;
hence thesis by A11,A13;
end;
A14: IND[ 0 ] by A8,A10;
for n be Nat holds IND[n] from NAT_1:sch 2(A14,A12);
then for m be Element of NAT holds PS1.m = PS2.m;
hence thesis;
end;
end;
definition
let X be set, F be Functional_Sequence of X,ExtREAL;
attr F is additive means
for n,m be Nat st n <> m holds for x be set
st x in dom(F.n) /\ dom(F.m) holds (F.n).x <> +infty or (F.m).x <> -infty;
end;
Lm1: z in dom((Partial_Sums F).n) & m <= n implies z in dom((Partial_Sums F).m
)
proof
set PF = Partial_Sums F;
assume that
A1: z in dom(PF.n) and
A2: m <= n;
defpred P[Nat] means m <= $1 & $1 <= n implies not z in dom(PF.$1);
assume
A3: not z in dom(PF.m);
A4: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A5: P[k];
assume that
A6: m <= k+1 and
A7: k+1 <= n;
per cases by A6,NAT_1:8;
suppose
A8: m <= k;
PF.(k+1) = PF.k + F.(k+1) by Def4;
then
A9: dom(PF.(k+1)) = (dom(PF.k) /\ dom(F.(k+1))) \(((PF.k)"{-infty} /\ (
F.(k+1))"{+infty}) \/ ((PF.k)"{+infty} /\ (F.(k+1))"{-infty})) by
MESFUNC1:def 3;
not z in dom(PF.k) /\ dom(F.(k+1)) by A5,A7,A8,NAT_1:13,XBOOLE_0:def 4;
hence thesis by A9,XBOOLE_0:def 5;
end;
suppose
m = k+1;
hence thesis by A3;
end;
end;
A10: P[ 0 ] by A3;
for k be Nat holds P[k] from NAT_1:sch 2(A10,A4);
hence contradiction by A1,A2;
end;
theorem Th22:
z in dom((Partial_Sums F).n) & m <= n implies z in dom((
Partial_Sums F).m) & z in dom(F.m)
proof
set PF = Partial_Sums F;
assume that
A1: z in dom(PF.n) and
A2: m <= n;
thus
A3: z in dom(PF.m) by A1,A2,Lm1;
per cases;
suppose
m = 0;
then PF.m = F.m by Def4;
hence thesis by A1,A2,Lm1;
end;
suppose
m <> 0;
then consider k be Nat such that
A4: m = k + 1 by NAT_1:6;
PF.m = PF.k + F.m by A4,Def4;
then dom(PF.m) = (dom(PF.k) /\ dom(F.m)) \(((PF.k)"{-infty} /\ (F.m)"{
+infty}) \/ ((PF.k)"{+infty} /\ (F.m)"{-infty})) by MESFUNC1:def 3;
then z in dom(PF.k) /\ dom(F.m) by A3,XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 4;
end;
end;
theorem Th23:
z in dom((Partial_Sums F).n) & ((Partial_Sums F).n).z = +infty
implies ex m be Nat st m <= n & (F.m).z = +infty
proof
set PF = Partial_Sums F;
assume that
A1: z in dom(PF.n) and
A2: (PF.n).z = +infty;
now
defpred P[Nat] means $1 <= n implies (PF.$1).z <> +infty;
assume
A3: for m be Element of NAT st m <= n holds (F.m).z <> +infty;
A4: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A5: P[k];
assume
A6: k+1 <= n;
then k <= n by NAT_1:13;
then
A7: z in dom(PF.k) by A1,Th22;
not (PF.k).z in {+infty} by A5,A6,NAT_1:13,TARSKI:def 1;
then not z in (PF.k)"{+infty} by FUNCT_1:def 7;
then
A8: not z in (PF.k)"{+infty} /\ (F.(k+1))"{-infty} by XBOOLE_0:def 4;
z in dom(F.(k+1)) by A1,A6,Th22;
then
A9: z in dom(PF.k) /\ dom(F.(k+1)) by A7,XBOOLE_0:def 4;
A10: PF.(k+1) = PF.k + F.(k+1) by Def4;
A11: (F.(k+1)).z <> +infty by A3,A6;
then not (F.(k+1)).z in {+infty} by TARSKI:def 1;
then not z in (F.(k+1))"{+infty} by FUNCT_1:def 7;
then not z in (PF.k)"{-infty} /\ (F.(k+1))"{+infty} by XBOOLE_0:def 4;
then
not z in ((PF.k)"{+infty} /\ (F.(k+1))"{-infty}) \/ ((PF.k)"{-infty
} /\ (F.(k+1))"{+infty}) by A8,XBOOLE_0:def 3;
then
z in (dom(PF.k) /\ dom(F.(k+1))) \ (((PF.k)"{+infty} /\ (F.(k+1))"{
-infty}) \/ ((PF.k)"{-infty} /\ (F.(k+1))"{+infty})) by A9,XBOOLE_0:def 5;
then z in dom(PF.(k+1)) by A10,MESFUNC1:def 3;
then (PF.(k+1)).z = (PF.k).z + (F.(k+1)).z by A10,MESFUNC1:def 3;
hence thesis by A5,A6,A11,NAT_1:13,XXREAL_3:16;
end;
PF.0 = F.0 by Def4;
then
A12: P[ 0 ] by A3;
for k being Nat holds P[k] from NAT_1:sch 2(A12,A4);
hence contradiction by A2;
end;
hence thesis;
end;
theorem
F is additive & z in dom((Partial_Sums F).n) & ((Partial_Sums F).n).z
= +infty & m <= n implies (F.m).z <> -infty
proof
assume that
A1: F is additive and
A2: z in dom((Partial_Sums F).n) and
A3: ((Partial_Sums F).n).z = +infty and
A4: m <= n;
A5: z in dom(F.m) by A2,A4,Th22;
consider k be Nat such that
A6: k <= n and
A7: (F.k).z = +infty by A2,A3,Th23;
z in dom(F.k) by A2,A6,Th22;
then z in dom(F.m) /\ dom(F.k) by A5,XBOOLE_0:def 4;
hence thesis by A1,A7;
end;
theorem Th25:
z in dom((Partial_Sums F).n) & ((Partial_Sums F).n).z = -infty
implies ex m be Nat st m <= n & (F.m).z = -infty
proof
set PF = Partial_Sums F;
assume that
A1: z in dom(PF.n) and
A2: (PF.n).z = -infty;
now
defpred P[Nat] means $1 <= n implies (PF.$1).z <> -infty;
assume
A3: for m be Nat st m <= n holds (F.m).z <> -infty;
A4: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A5: P[k];
assume
A6: k+1 <= n;
then k <= n by NAT_1:13;
then
A7: z in dom(PF.k) by A1,Th22;
not (PF.k).z in {-infty} by A5,A6,NAT_1:13,TARSKI:def 1;
then not z in (PF.k)"{-infty} by FUNCT_1:def 7;
then
A8: not z in (PF.k)"{-infty} /\ (F.(k+1))"{+infty} by XBOOLE_0:def 4;
z in dom(F.(k+1)) by A1,A6,Th22;
then
A9: z in dom(PF.k) /\ dom(F.(k+1)) by A7,XBOOLE_0:def 4;
A10: PF.(k+1) = PF.k + F.(k+1) by Def4;
A11: (F.(k+1)).z <> -infty by A3,A6;
then not (F.(k+1)).z in {-infty} by TARSKI:def 1;
then not z in (F.(k+1))"{-infty} by FUNCT_1:def 7;
then not z in (PF.k)"{+infty} /\ (F.(k+1))"{-infty} by XBOOLE_0:def 4;
then
not z in ((PF.k)"{-infty} /\ (F.(k+1))"{+infty}) \/ ((PF.k)"{+infty
} /\ (F.(k+1))"{-infty}) by A8,XBOOLE_0:def 3;
then
z in (dom(PF.k) /\ dom(F.(k+1))) \ (((PF.k)"{-infty} /\ (F.(k+1))"{
+infty}) \/ ((PF.k)"{+infty} /\ (F.(k+1))"{-infty})) by A9,XBOOLE_0:def 5;
then z in dom(PF.(k+1)) by A10,MESFUNC1:def 3;
then (PF.(k+1)).z = (PF.k).z + (F.(k+1)).z by A10,MESFUNC1:def 3;
hence thesis by A5,A6,A11,NAT_1:13,XXREAL_3:17;
end;
PF.0 = F.0 by Def4;
then
A12: P[ 0 ] by A3;
for k being Nat holds P[k] from NAT_1:sch 2(A12,A4);
hence contradiction by A2;
end;
hence thesis;
end;
theorem
F is additive & z in dom((Partial_Sums F).n) & ((Partial_Sums F).n).z
= -infty & m <= n implies (F.m).z <> +infty
proof
assume
A1: F is additive;
assume that
A2: z in dom((Partial_Sums F).n) and
A3: ((Partial_Sums F).n).z = -infty;
assume m <= n;
then
A4: z in dom(F.m) by A2,Th22;
consider k be Nat such that
A5: k <= n and
A6: (F.k).z = -infty by A2,A3,Th25;
z in dom(F.k) by A2,A5,Th22;
then z in dom(F.m) /\ dom(F.k) by A4,XBOOLE_0:def 4;
hence thesis by A1,A6;
end;
theorem Th27:
F is additive implies ((Partial_Sums F).n)"{-infty} /\ (F.(n+1))
"{+infty} = {} & ((Partial_Sums F).n)"{+infty} /\ (F.(n+1))"{-infty} = {}
proof
set PF = Partial_Sums F;
assume
A1: F is additive;
now
given z be object such that
A2: z in (PF.n)"{-infty} and
A3: z in (F.(n+1))"{+infty};
A4: z in dom(PF.n) by A2,FUNCT_1:def 7;
(PF.n).z in {-infty} by A2,FUNCT_1:def 7;
then (PF.n).z = -infty by TARSKI:def 1;
then consider k be Nat such that
A5: k <= n and
A6: (F.k).z = -infty by A4,Th25;
A7: z in dom(F.(n+1)) by A3,FUNCT_1:def 7;
(F.(n+1)).z in {+infty} by A3,FUNCT_1:def 7;
then
A8: (F.(n+1)).z = +infty by TARSKI:def 1;
z in dom(F.k) by A4,A5,Th22;
then z in dom(F.k) /\ dom(F.(n+1)) by A7,XBOOLE_0:def 4;
hence contradiction by A1,A8,A6;
end;
then (PF.n)"{-infty} misses (F.(n+1))"{+infty} by XBOOLE_0:3;
hence (PF.n)"{-infty} /\ (F.(n+1))"{+infty} = {} by XBOOLE_0:def 7;
now
given z be object such that
A9: z in (PF.n)"{+infty} and
A10: z in (F.(n+1))"{-infty};
A11: z in dom(PF.n) by A9,FUNCT_1:def 7;
(PF.n).z in {+infty} by A9,FUNCT_1:def 7;
then (PF.n).z = +infty by TARSKI:def 1;
then consider k be Nat such that
A12: k <= n and
A13: (F.k).z = +infty by A11,Th23;
A14: z in dom(F.(n+1)) by A10,FUNCT_1:def 7;
(F.(n+1)).z in {-infty} by A10,FUNCT_1:def 7;
then
A15: (F.(n+1)).z = -infty by TARSKI:def 1;
z in dom(F.k) by A11,A12,Th22;
then z in dom(F.k) /\ dom(F.(n+1)) by A14,XBOOLE_0:def 4;
hence contradiction by A1,A15,A13;
end;
then (PF.n)"{+infty} misses (F.(n+1))"{-infty} by XBOOLE_0:3;
hence thesis by XBOOLE_0:def 7;
end;
theorem Th28:
F is additive implies dom((Partial_Sums F).n) = meet{dom(F.k)
where k is Element of NAT : k <= n}
proof
deffunc DOM1(Nat) = {dom(F.k) where k is Element of NAT : k <= $1};
set PF = Partial_Sums F;
defpred P[Nat] means dom(PF.$1) = meet {dom(F.k) where k is Element of NAT :
k <= $1};
A1: dom(PF.0) = dom(F.0) by Def4;
now
let V be object;
assume V in DOM1(0);
then consider k be Element of NAT such that
A2: V = dom(F.k) and
A3: k <= 0;
k = 0 by A3;
hence V in {dom(F.0)} by A2,TARSKI:def 1;
end;
then
A4: DOM1(0) c= {dom(F.0)};
assume
A5: F is additive;
A6: for m be Nat st P[m] holds P[m+1]
proof
let m be Nat;
A7: PF.(m+1) = PF.m + F.(m+1) by Def4;
A8: (PF.m)"{+infty} /\ (F.(m+1))"{-infty} = {} by A5,Th27;
A9: dom(F.0) in DOM1(m+1);
now
let V be object;
assume
A10: V in meet DOM1(m) /\ dom(F.(m+1));
then
A11: V in dom(F.(m+1)) by XBOOLE_0:def 4;
A12: V in meet DOM1(m) by A10,XBOOLE_0:def 4;
for W be set holds W in DOM1(m+1) implies V in W
proof
let W be set;
assume W in DOM1(m+1);
then consider i be Element of NAT such that
A13: W = dom(F.i) and
A14: i <= m+1;
now
assume i <= m;
then W in DOM1(m) by A13;
hence thesis by A12,SETFAM_1:def 1;
end;
hence thesis by A11,A13,A14,NAT_1:8;
end;
hence V in meet DOM1(m+1) by A9,SETFAM_1:def 1;
end;
then
A15: meet DOM1(m) /\ dom(F.(m+1)) c= meet DOM1(m+1);
A16: dom(F.0) in DOM1(m);
now
now
let V be object;
assume V in DOM1(m);
then consider i be Element of NAT such that
A17: V = dom(F.i) and
A18: i <= m;
i <= m+1 by A18,NAT_1:12;
hence V in DOM1(m+1) by A17;
end;
then DOM1(m) c= DOM1(m+1);
then
A19: meet DOM1(m+1) c= meet DOM1(m) by A16,SETFAM_1:6;
let V be object;
assume
A20: V in meet DOM1(m+1);
dom(F.(m+1)) in DOM1(m+1);
then V in dom(F.(m+1)) by A20,SETFAM_1:def 1;
hence V in meet DOM1(m) /\ dom(F.(m+1)) by A20,A19,XBOOLE_0:def 4;
end;
then
A21: meet DOM1(m+1) c= meet DOM1(m) /\ dom(F.(m+1));
(PF.m)"{-infty} /\ (F.(m+1))"{+infty} = {} by A5,Th27;
then
A22: dom(PF.(m+1)) = (dom(PF.m)/\dom(F.(m+1))) \ ({}\/{}) by A8,A7,
MESFUNC1:def 3;
assume P[m];
hence thesis by A22,A21,A15,XBOOLE_0:def 10;
end;
now
let V be object;
assume V in {dom(F.0)};
then V = dom(F.0) by TARSKI:def 1;
hence V in DOM1(0);
end;
then {dom(F.0)} c= DOM1(0);
then DOM1(0) = {dom(F.0)} by A4,XBOOLE_0:def 10;
then
A23: P[ 0 ] by A1,SETFAM_1:10;
for k be Nat holds P[k] from NAT_1:sch 2(A23,A6);
hence thesis;
end;
theorem Th29:
F is additive & F is with_the_same_dom implies dom((Partial_Sums
F).n) = dom(F.0)
proof
assume that
A1: F is additive and
A2: F is with_the_same_dom;
now
let D be object;
A3: dom(F.0) in {dom(F.k) where k is Element of NAT : k <= n};
assume D in meet {dom(F.k) where k is Element of NAT : k <= n};
then D in dom(F.0) by A3,SETFAM_1:def 1;
hence D in meet {dom(F.0)} by SETFAM_1:10;
end;
then
A4: meet{dom(F.k) where k is Element of NAT : k <= n} c= meet{dom(F.0)};
now
let D be object;
assume D in meet {dom(F.0)};
then
A5: D in dom(F.0) by SETFAM_1:10;
A6: for E be set holds E in {dom(F.k) where k is Element of NAT : k <= n}
implies D in E
proof
let E be set;
assume E in {dom(F.k) where k is Element of NAT : k <= n};
then ex k1 be Element of NAT st E = dom(F.k1) & k1 <= n;
hence thesis by A2,A5;
end;
dom(F.0) in {dom(F.k) where k is Element of NAT : k <= n};
hence D in meet {dom(F.k) where k is Element of NAT : k <= n} by A6,
SETFAM_1:def 1;
end;
then
meet{dom(F.0)} c= meet {dom(F.k) where k is Element of NAT : k <= n};
then meet{dom(F.k) where k is Element of NAT : k <= n} = meet {dom(F.0)} by
A4,XBOOLE_0:def 10;
then dom((Partial_Sums F).n) = meet{dom(F.0)} by A1,Th28;
hence thesis by SETFAM_1:10;
end;
theorem Th30:
(for n be Nat holds F.n is nonnegative) implies F is additive
by SUPINF_2:51;
theorem Th31:
F is additive & (for n holds G.n = (F.n)|D) implies G is additive
proof
assume that
A1: F is additive and
A2: for n holds G.n = (F.n)|D;
let n,m be Nat;
A3: G.m = (F.m)|D by A2;
then
A4: dom(G.m) c= dom(F.m) by RELAT_1:60;
assume n <> m;
let x be set;
assume
A5: x in dom(G.n) /\ dom(G.m);
then
A6: x in dom(G.m) by XBOOLE_0:def 4;
A7: G.n = (F.n)|D by A2;
then dom(G.n) c= dom(F.n) by RELAT_1:60;
then dom(G.n) /\ dom(G.m) c= dom(F.n) /\ dom(F.m) by A4,XBOOLE_1:27;
then
A8: (F.n).x <> +infty or (F.m).x <> -infty by A1,A5;
x in dom(G.n) by A5,XBOOLE_0:def 4;
hence thesis by A7,A3,A8,A6,FUNCT_1:47;
end;
theorem Th32:
F is additive & F is with_the_same_dom & D c= dom(F.0) & x in D
implies (Partial_Sums(F#x)).n = ((Partial_Sums F)#x).n
proof
set PF = Partial_Sums F;
set PFx = Partial_Sums(F#x);
assume that
A1: F is additive and
A2: F is with_the_same_dom and
A3: D c= dom(F.0) and
A4: x in D;
defpred P[Nat] means PFx.$1 = (PF#x).$1;
A5: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A6: P[k];
PFx.(k+1) = PFx.k + (F#x).(k+1) by Def1;
then PFx.(k+1) = (PF#x).k + (F.(k+1)).x by A6,MESFUNC5:def 13;
then
A7: PFx.(k+1) = (PF.k).x + (F.(k+1)).x by MESFUNC5:def 13;
A8: PF.(k+1) = PF.k + F.(k+1) by Def4;
D c= dom(PF.(k+1)) by A1,A2,A3,Th29;
then PFx.(k+1) = (PF.(k+1)).x by A4,A8,A7,MESFUNC1:def 3;
hence thesis by MESFUNC5:def 13;
end;
PFx.0 = (F#x).0 by Def1;
then PFx.0 = (F.0).x by MESFUNC5:def 13;
then PFx.0 = (PF.0).x by Def4;
then
A9: P[ 0 ] by MESFUNC5:def 13;
for k being Nat holds P[k] from NAT_1:sch 2(A9,A5);
hence thesis;
end;
theorem Th33:
F is additive & F is with_the_same_dom & D c= dom(F.0) & x in D
implies ( Partial_Sums(F#x) is convergent_to_finite_number iff (Partial_Sums F)
#x is convergent_to_finite_number ) & ( Partial_Sums(F#x) is
convergent_to_+infty iff (Partial_Sums F)#x is convergent_to_+infty ) & (
Partial_Sums(F#x) is convergent_to_-infty iff (Partial_Sums F)#x is
convergent_to_-infty ) & ( Partial_Sums(F#x) is convergent iff (Partial_Sums F)
#x is convergent )
proof
set PFx = Partial_Sums(F#x);
set PF = Partial_Sums F;
assume that
A1: F is additive and
A2: F is with_the_same_dom and
A3: D c= dom(F.0) and
A4: x in D;
thus
A5: now
assume PFx is convergent_to_finite_number;
then consider g be Real such that
A6: for p be Real st 0<p ex n be Nat st for m be Nat st n<=m
holds |. PFx.m - g .| < p;
now
let p be Real;
assume 0<p;
then consider n be Nat such that
A7: for m be Nat st n<=m holds |. PFx.m - g .| < p by A6;
take n;
let m be Nat;
assume
A8: n<=m;
PFx.m = (PF#x).m by A1,A2,A3,A4,Th32;
hence |. (PF#x).m - g .| < p by A7,A8;
end;
hence PF#x is convergent_to_finite_number;
end;
thus
A9: now
assume PF#x is convergent_to_finite_number;
then consider g be Real such that
A10: for p be Real st 0<p ex n be Nat st for m be Nat st n<=m
holds |. (PF#x).m- g .| < p;
now
let p be Real;
assume 0<p;
then consider n be Nat such that
A11: for m be Nat st n<=m holds |. (PF#x).m- g .| < p by A10;
take n;
let m be Nat;
assume
A12: n<=m;
PFx.m = (PF#x).m by A1,A2,A3,A4,Th32;
hence |. PFx.m - g .| < p by A11,A12;
end;
hence PFx is convergent_to_finite_number;
end;
thus
A13: now
assume
A14: PFx is convergent_to_+infty;
now
let r be Real;
assume 0 < r;
then consider n be Nat such that
A15: for m be Nat st n <= m holds r <= PFx.m by A14;
take n;
let m be Nat;
assume n <= m;
then r <= PFx.m by A15;
hence r <= (PF#x).m by A1,A2,A3,A4,Th32;
end;
hence PF#x is convergent_to_+infty;
end;
thus
A16: now
assume
A17: PF#x is convergent_to_+infty;
now
let r be Real;
assume 0 < r;
then consider n be Nat such that
A18: for m be Nat st n <= m holds r <= (PF#x).m by A17;
take n;
let m be Nat;
assume n <= m;
then r <= (PF#x).m by A18;
hence r <= PFx.m by A1,A2,A3,A4,Th32;
end;
hence PFx is convergent_to_+infty;
end;
thus
A19: now
assume
A20: PFx is convergent_to_-infty;
now
let r be Real;
assume r < 0;
then consider n be Nat such that
A21: for m be Nat st n <= m holds PFx.m <= r by A20;
take n;
let m be Nat;
assume n <= m;
then PFx.m <= r by A21;
hence (PF#x).m <= r by A1,A2,A3,A4,Th32;
end;
hence PF#x is convergent_to_-infty;
end;
thus
A22: now
assume
A23: PF#x is convergent_to_-infty;
now
let r be Real;
assume r < 0;
then consider n be Nat such that
A24: for m be Nat st n <= m holds (PF#x).m <= r by A23;
take n;
let m be Nat;
assume n <= m;
then (PF#x).m <= r by A24;
hence PFx.m <= r by A1,A2,A3,A4,Th32;
end;
hence PFx is convergent_to_-infty;
end;
hereby
assume
A25: PFx is convergent;
per cases by A25;
suppose
PFx is convergent_to_+infty;
hence PF#x is convergent by A13;
end;
suppose
PFx is convergent_to_-infty;
hence PF#x is convergent by A19;
end;
suppose
PFx is convergent_to_finite_number;
hence PF#x is convergent by A5;
end;
end;
assume
A26: PF#x is convergent;
per cases by A26;
suppose
PF#x is convergent_to_+infty;
hence thesis by A16;
end;
suppose
PF#x is convergent_to_-infty;
hence thesis by A22;
end;
suppose
PF#x is convergent_to_finite_number;
hence thesis by A9;
end;
end;
theorem Th34:
F is additive & F is with_the_same_dom & dom f c= dom(F.0) & x
in dom f & F#x is summable & f.x = Sum(F#x) implies f.x = lim((Partial_Sums F)#
x)
proof
set PF = Partial_Sums F;
assume that
A1: F is additive and
A2: F is with_the_same_dom and
A3: dom f c= dom(F.0) and
A4: x in dom f and
A5: F#x is summable and
A6: f.x = Sum(F#x);
set PFx = Partial_Sums(F#x);
PFx is convergent by A5;
then
A7: PF#x is convergent by A1,A2,A3,A4,Th33;
per cases by A7,MESFUNC5:def 12;
suppose
A8: ex g be Real st lim(PF#x) = g & (for p be Real st 0<p
ex n be Nat st for m be Nat st n<=m holds |. (PF#x).m- lim (PF#x) .| < p) & (PF
#x) is convergent_to_finite_number;
then
A9: PFx is convergent_to_finite_number by A1,A2,A3,A4,Th33;
then
A10: not PFx is convergent_to_+infty by MESFUNC5:50;
A11: not PFx is convergent_to_-infty by A9,MESFUNC5:51;
PFx is convergent by A9;
then
A12: ex g be Real st f.x = g & (for p be Real st 0<p ex n be
Nat st for m be Nat st n<=m holds |. PFx.m- f.x .| < p) & PFx is
convergent_to_finite_number by A6,A10,A11,MESFUNC5:def 12;
now
let p be Real;
assume 0<p;
then consider n be Nat such that
A13: for m be Nat st n<=m holds |. PFx.m - f.x .| < p by A12;
take n;
let m be Nat;
assume
A14: n<=m;
PFx.m = (PF#x).m by A1,A2,A3,A4,Th32;
hence |. (PF#x).m - f.x .| < p by A13,A14;
end;
hence thesis by A7,A8,A12,MESFUNC5:def 12;
end;
suppose
A15: lim(PF#x)=+infty & PF#x is convergent_to_+infty;
then
A16: PFx is convergent_to_+infty by A1,A2,A3,A4,Th33;
then PFx is convergent;
hence thesis by A6,A15,A16,MESFUNC5:def 12;
end;
suppose
A17: lim(PF#x)=-infty & PF#x is convergent_to_-infty;
then
A18: PFx is convergent_to_-infty by A1,A2,A3,A4,Th33;
then PFx is convergent;
hence thesis by A6,A17,A18,MESFUNC5:def 12;
end;
end;
theorem Th35:
(for m be Nat holds F.m is_simple_func_in S) implies F is
additive & (Partial_Sums F).n is_simple_func_in S
proof
defpred P[Nat] means (Partial_Sums F).$1 is_simple_func_in S;
assume
A1: for m be Nat holds F.m is_simple_func_in S;
hereby
let n,m be Nat;
assume n <> m;
F.n is_simple_func_in S by A1;
then F.n is without+infty by MESFUNC5:14;
hence for x be set st x in dom(F.n) /\ dom(F.m) holds (F.n).x <> +infty or
(F.m).x <> -infty;
end;
A2: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A3: P[k];
F.(k+1) is_simple_func_in S by A1;
then (Partial_Sums F).k + F.(k+1) is_simple_func_in S by A3,MESFUNC5:38;
hence thesis by Def4;
end;
(Partial_Sums F).0 = F.0 by Def4;
then
A4: P[ 0 ] by A1;
for k be Nat holds P[k] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
theorem Th36:
(for m be Nat holds F.m is nonnegative) implies (Partial_Sums F)
.n is nonnegative
proof
defpred P[Nat] means (Partial_Sums F).$1 is nonnegative;
assume
A1: for m be Nat holds F.m is nonnegative;
A2: now
let k be Nat;
assume
A3: P[k];
A4: (Partial_Sums F).(k+1) = (Partial_Sums F).k + F.(k+1) by Def4;
F.(k+1) is nonnegative by A1;
hence P[k+1] by A3,A4,MESFUNC5:22;
end;
(Partial_Sums F).0 = F.0 by Def4;
then
A5: P[ 0 ] by A1;
for k being Nat holds P[k] from NAT_1:sch 2(A5,A2);
hence thesis;
end;
theorem Th37:
F is with_the_same_dom & x in dom(F.0) & (for k be Nat holds F.k
is nonnegative) & n <= m implies ((Partial_Sums F).n).x <= ((Partial_Sums F).m)
.x
proof
assume
A1: F is with_the_same_dom;
set PF = Partial_Sums F;
assume
A2: x in dom(F.0);
defpred P[Nat] means (PF.n).x <= (PF.$1).x;
assume
A3: for m be Nat holds F.m is nonnegative;
A4: for k be Nat holds (PF.k).x <= (PF.(k+1)).x
proof
let k be Nat;
A5: PF.(k+1) = PF.k + F.(k+1) by Def4;
F.(k+1) is nonnegative by A3;
then
A6: 0. <= (F.(k+1)).x by SUPINF_2:39;
dom(PF.(k+1)) = dom(F.0) by A1,A3,Th29,Th30;
then (PF.(k+1)).x = (PF.k).x + (F.(k+1)).x by A2,A5,MESFUNC1:def 3;
hence thesis by A6,XXREAL_3:39;
end;
A7: for k be Nat st k >= n & (for l be Nat st l >= n & l < k holds P[l])
holds P[k]
proof
let k be Nat;
assume that
A8: k >= n and
A9: for l be Nat st l >= n & l < k holds P[l];
now
A10: now
assume
A11: k > n+1;
then reconsider l = k-1 as Element of NAT by NAT_1:20;
k < k+1 by NAT_1:13;
then
A12: k > l by XREAL_1:19;
k = l+1;
then
A13: (PF.l).x <= (PF.k).x by A4;
l >= n by A11,XREAL_1:19;
then (PF.n).x <= (PF.l).x by A9,A12;
hence thesis by A13,XXREAL_0:2;
end;
assume k > n;
then k >= n + 1 by NAT_1:13;
then k = n+1 or k > n+1 by XXREAL_0:1;
hence thesis by A4,A10;
end;
hence thesis by A8,XXREAL_0:1;
end;
A14: for k being Nat st k >= n holds P[k] from NAT_1:sch 9(A7);
assume n <= m;
hence thesis by A14;
end;
theorem Th38:
F is with_the_same_dom & x in dom(F.0) & (for m be Nat holds F.m
is nonnegative) implies (Partial_Sums F)#x is non-decreasing & (Partial_Sums F)
#x is convergent
proof
assume
A1: F is with_the_same_dom;
assume
A2: x in dom(F.0);
assume
A3: for m be Nat holds F.m is nonnegative;
for n,m be Nat st m<=n holds ((Partial_Sums F)#x).m <= ((
Partial_Sums F)#x).n
proof
let n,m be Nat;
assume m <= n;
then ((Partial_Sums F).m).x <= ((Partial_Sums F).n).x by A1,A2,A3,Th37;
then ((Partial_Sums F)#x).m <= ((Partial_Sums F).n).x by MESFUNC5:def 13;
hence thesis by MESFUNC5:def 13;
end;
hence ((Partial_Sums F)#x) is non-decreasing by RINFSUP2:7;
hence thesis by RINFSUP2:37;
end;
theorem Th39:
(for m be Nat holds F.m is without-infty) implies (Partial_Sums
F).n is without-infty
proof
defpred P[Nat] means (Partial_Sums F).$1 is without-infty;
assume
A1: for m be Nat holds F.m is without-infty;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A3: P[k];
A4: F.(k+1) is without-infty by A1;
(Partial_Sums F).(k+1) = (Partial_Sums F).k + F.(k+1) by Def4;
hence thesis by A3,A4,Th3;
end;
(Partial_Sums F).0 = F.0 by Def4;
then
A5: P[ 0 ] by A1;
for k being Nat holds P[k] from NAT_1:sch 2(A5,A2);
hence thesis;
end;
theorem
(for m be Nat holds F.m is without+infty) implies (Partial_Sums F).n
is without+infty
proof
defpred P[Nat] means (Partial_Sums F).$1 is without+infty;
assume
A1: for m be Nat holds F.m is without+infty;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A3: P[k];
A4: F.(k+1) is without+infty by A1;
(Partial_Sums F).(k+1) = (Partial_Sums F).k + F.(k+1) by Def4;
hence thesis by A3,A4,Th4;
end;
(Partial_Sums F).0 = F.0 by Def4;
then
A5: P[ 0 ] by A1;
for k being Nat holds P[k] from NAT_1:sch 2(A5,A2);
hence thesis;
end;
theorem Th41:
(for n be Nat holds F.n is E-measurable & F.n is
without-infty) implies (Partial_Sums F).m is E-measurable
proof
set PF = Partial_Sums F;
defpred P[Nat] means PF.$1 is E-measurable;
assume
A1: for n be Nat holds F.n is E-measurable & F.n is without-infty;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A3: P[k];
A4: F.(k+1) is E-measurable by A1;
A5: F.(k+1) is without-infty by A1;
PF.k is without-infty by A1,Th39;
then PF.k + F.(k+1) is E-measurable by A3,A4,A5,MESFUNC5:31;
hence thesis by Def4;
end;
PF.0 = F.0 by Def4;
then
A6: P[ 0 ] by A1;
for k being Nat holds P[k] from NAT_1:sch 2(A6,A2);
hence thesis;
end;
theorem Th42:
F is additive & F is with_the_same_dom & G is additive & G is
with_the_same_dom & x in dom(F.0) /\ dom(G.0) & (for k be Nat, y be Element of
X st y in dom(F.0) /\ dom(G.0) holds (F.k).y <= (G.k).y) implies ((Partial_Sums
F).n).x <= ((Partial_Sums G).n).x
proof
assume that
A1: F is additive and
A2: F is with_the_same_dom and
A3: G is additive and
A4: G is with_the_same_dom and
A5: x in dom(F.0) /\ dom(G.0) and
A6: for k be Nat, y be Element of X st y in dom(F.0) /\ dom(G.0) holds (
F.k).y <= (G.k).y;
set PG = Partial_Sums G;
set PF = Partial_Sums F;
defpred P[Nat] means (PF.$1).x <= (PG.$1).x;
A7: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A8: P[k];
dom(PF.(k+1)) = dom(F.0) by A1,A2,Th29;
then
A9: x in dom(PF.(k+1)) by A5,XBOOLE_0:def 4;
dom(PG.(k+1)) = dom(G.0) by A3,A4,Th29;
then
A10: x in dom(PG.(k+1)) by A5,XBOOLE_0:def 4;
PG.(k+1) = PG.k + G.(k+1) by Def4;
then
A11: (PG.(k+1)).x = (PG.k).x + (G.(k+1)).x by A10,MESFUNC1:def 3;
PF.(k+1) = PF.k + F.(k+1) by Def4;
then
A12: (PF.(k+1)).x = (PF.k).x + (F.(k+1)).x by A9,MESFUNC1:def 3;
(F.(k+1)).x <= (G.(k+1)).x by A5,A6;
hence thesis by A8,A12,A11,XXREAL_3:36;
end;
A13: (PG.0) = G.0 by Def4;
(PF.0) = F.0 by Def4;
then
A14: P[ 0 ] by A5,A6,A13;
for k being Nat holds P[k] from NAT_1:sch 2(A14,A7);
hence thesis;
end;
theorem Th43:
for X be non empty set, F be Functional_Sequence of X,ExtREAL st
F is additive & F is with_the_same_dom holds Partial_Sums F is
with_the_same_dom
proof
let X be non empty set, F be Functional_Sequence of X,ExtREAL;
assume that
A1: F is additive and
A2: F is with_the_same_dom;
let n,m be Nat;
dom((Partial_Sums F).n) = dom(F.0) by A1,A2,Th29;
hence thesis by A1,A2,Th29;
end;
theorem Th44:
dom(F.0) = E & F is additive & F is with_the_same_dom & (for n
be Nat holds (Partial_Sums F).n is E-measurable) & (for x be Element of X
st
x in E holds F#x is summable) implies lim(Partial_Sums F) is E-measurable
proof
assume that
A1: dom(F.0) = E and
A2: F is additive and
A3: F is with_the_same_dom and
A4: for n be Nat holds (Partial_Sums F).n is E-measurable and
A5: for x be Element of X st x in E holds F#x is summable;
reconsider PF = Partial_Sums F as with_the_same_dom Functional_Sequence of X
,ExtREAL by A2,A3,Th43;
A6: now
let x be Element of X;
assume
A7: x in E;
then F#x is summable by A5;
then Partial_Sums(F#x) is convergent;
hence PF#x is convergent by A1,A2,A3,A7,Th33;
end;
dom((Partial_Sums F).0) = E by A1,A2,A3,Th29;
hence thesis by A4,A6,MESFUNC8:25;
end;
theorem
(for n be Nat holds F.n is_integrable_on M) implies for m be Nat holds
(Partial_Sums F).m is_integrable_on M
proof
set PF = Partial_Sums F;
defpred P1[Nat] means PF.$1 is_integrable_on M;
assume
A1: for n be Nat holds F.n is_integrable_on M;
A2: for k be Nat st P1[k] holds P1[k+1]
proof
let k be Nat;
assume
A3: P1[k];
F.(k+1) is_integrable_on M by A1;
then PF.k + F.(k+1) is_integrable_on M by A3,MESFUNC5:108;
hence thesis by Def4;
end;
PF.0 = F.0 by Def4;
then
A4: P1[ 0 ] by A1;
thus for m be Nat holds P1[m] from NAT_1:sch 2(A4,A2);
end;
theorem Th46:
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 nonnegative & I.n =
Integral(M,F.n
)) implies Integral(M,(Partial_Sums F).m) = (Partial_Sums I).m
proof
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 nonnegative & I.n
= Integral(M,F.n);
set PF = Partial_Sums F;
A5: for n be Nat holds F.n is without-infty by A4,MESFUNC5:12;
thus Integral(M,(Partial_Sums F).m) = (Partial_Sums I).m
proof
set PI = Partial_Sums I;
defpred P2[Nat] means Integral(M,PF.$1) = (Partial_Sums I).$1;
A6: for k be Nat st P2[k] holds P2[k+1]
proof
let k be Nat;
assume
A7: P2[k];
A8: F.(k+1) is E-measurable by A4;
A9: dom(F.(k+1)) = E by A1,A3;
A10: PF.(k+1) is E-measurable by A4,A5,Th41;
A11: PF.(k+1) is nonnegative by A4,Th36;
A12: F.(k+1) is nonnegative by A4;
A13: PF.k is nonnegative by A4,Th36;
A14: dom(PF.k) = E by A1,A2,A3,Th29;
A15: PF.k is E-measurable by A4,A5,Th41;
then consider D be Element of S such that
A16: D = dom(PF.k + F.(k+1)) and
A17: integral+(M,PF.k + F.(k+1)) = integral+(M,(PF.k)|D) + integral+
(M,( F.(k+1))|D) by A14,A9,A8,A13,A12,MESFUNC5:78;
A18: D = E /\ E by A14,A9,A13,A12,A16,MESFUNC5:22;
then
A19: (PF.k)|D = PF.k by A14;
A20: (F.(k+1))|D = F.(k+1) by A9,A18;
dom(PF.(k+1)) = E by A1,A2,A3,Th29;
then Integral(M,PF.(k+1)) = integral+(M,PF.(k+1)) by A10,A11,MESFUNC5:88
.= integral+(M,(PF.k)|D) + integral+(M,(F.(k+1))|D) by A17,Def4
.= Integral(M,PF.k) + integral+(M,(F.(k+1))|D) by A14,A15,A13,A19,
MESFUNC5:88
.= Integral(M,PF.k) + Integral(M,F.(k+1)) by A9,A8,A12,A20,MESFUNC5:88
.= PI.k + I.(k+1) by A4,A7;
hence thesis by Def1;
end;
Integral(M,PF.0) = Integral(M,F.0) by Def4;
then Integral(M,PF.0) = I.0 by A4;
then
A21: P2[ 0 ] by Def1;
for k be Nat holds P2[k] from NAT_1:sch 2(A21,A6);
hence thesis;
end;
end;
begin :: Sequence of Measurable Functions
Lm2: E c= dom f & f is E-measurable & E ={} & (for n be Nat holds F.n
is_simple_func_in S) implies 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
assume that
A1: E c= dom f and
A2: f is E-measurable and
A3: E ={} and
A4: for n be Nat holds F.n is_simple_func_in S;
take I = NAT --> 0.;
A5: M.E = 0 by A3,VALUED_0:def 19;
thus for n be Nat holds I.n = Integral(M,(F.n)|E)
proof
let n be Nat;
reconsider m = n as Element of NAT by ORDINAL1:def 12;
reconsider D = dom(F.m) as Element of S by A4,MESFUNC5:37;
F.m is D-measurable by A4,MESFUNC2:34;
then Integral(M,(F.m)|E) = 0 by A5,MESFUNC5:94;
hence thesis by FUNCOP_1:7;
end;
defpred P[Nat] means (Partial_Sums I).$1 = 0;
A6: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A7: P[k];
A8: I.(k+1) = 0 by FUNCOP_1:7;
(Partial_Sums I).(k+1) = (Partial_Sums I).k + I.(k+1) by Def1;
hence thesis by A7,A8;
end;
(Partial_Sums I).0 = I.0 by Def1;
then
A9: P[ 0 ] by FUNCOP_1:7;
A10: for k being Nat holds P[k] from NAT_1:sch 2(A9,A6);
A11: for n be Nat holds (Partial_Sums I).n = 0
by A10;
then
A12: lim(Partial_Sums I) = 0 by MESFUNC5:52;
Partial_Sums I is convergent_to_finite_number by A11,MESFUNC5:52;
then Partial_Sums I is convergent;
hence I is summable;
A13: E = dom(f|E) by A1,RELAT_1:62;
then E = dom f /\ E by RELAT_1:61;
then Integral(M,(f|E)|E) = 0 by A2,A5,A13,MESFUNC5:42,94;
hence thesis by A12;
end;
Lm3: E c= dom f & f is nonnegative & f is E-measurable & F is additive & E
common_on_dom F & (for n be Nat holds F.n is_simple_func_in S & F.n is
nonnegative ) & (for x be Element of X st x in E holds F#x is summable & f.x =
Sum(F#x)) implies 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
assume that
A1: E c= dom f and
A2: f is nonnegative and
A3: f is E-measurable and
A4: F is additive and
A5: E common_on_dom F and
A6: for n be Nat holds F.n is_simple_func_in S & F.n is nonnegative and
A7: for x be Element of X st x in E holds F#x is summable & f.x = Sum(F# x);
deffunc G1(Nat) = (F.$1)|E;
consider g1 be Functional_Sequence of X,ExtREAL such that
A8: for n be Nat holds g1.n = G1(n) from SEQFUNC:sch 1;
A9: for n be Nat holds (F.n)|E is_simple_func_in S & (F.n)|E is nonnegative &
dom((F.n)|E) = E
proof
let n be Nat;
reconsider n9=n as Element of NAT by ORDINAL1:def 12;
thus (F.n)|E is_simple_func_in S by A6,MESFUNC5:34;
thus (F.n)|E is nonnegative by A6,MESFUNC5:15;
E c= dom(F.n9) by A5,SEQFUNC:def 9;
hence thesis by RELAT_1:62;
end;
for n,m be Nat holds dom(g1.n) = dom(g1.m)
proof
let n,m be Nat;
dom(g1.m) = dom((F.m)|E) by A8;
then
A10: dom(g1.m) = E by A9;
dom(g1.n) = dom((F.n)|E) by A8;
hence thesis by A9,A10;
end;
then
A11: g1 is with_the_same_dom;
set G = Partial_Sums g1;
deffunc I(Element of NAT) = Integral(M,g1.$1);
consider I be ExtREAL_sequence such that
A12: for n be Element of NAT holds I.n = I(n) from FUNCT_2:sch 4;
take I;
A13: dom(f|E) = E by A1,RELAT_1:62;
then dom f /\ E = E by RELAT_1:61;
then
A14: f|E is E-measurable by A3,MESFUNC5:42;
set L = Partial_Sums I;
A15: for n be Nat holds I.n = Integral(M,(F.n)|E)
proof
let n be Nat;
reconsider m = n as Element of NAT by ORDINAL1:def 12;
I.m = Integral(M,g1.m) by A12;
hence thesis by A8;
end;
A16: for k be Nat holds g1.k is nonnegative
proof
let k be Nat;
(F.k)|E is nonnegative by A9;
hence thesis by A8;
end;
A17: for n be Nat holds G.n is_simple_func_in S & G.n is nonnegative & dom(G.
n)=E
proof
let n be Nat;
A18: for n be Nat holds g1.n is_simple_func_in S
proof
let n be Nat;
(F.n)|E is_simple_func_in S by A9;
hence thesis by A8;
end;
hence G.n is_simple_func_in S by Th35;
thus G.n is nonnegative by A16,Th36;
dom(g1.0) = dom((F.0)|E) by A8;
then dom(g1.0) = E by A9;
hence thesis by A11,A18,Th29,Th35;
end;
G.0 = g1.0 by Def4;
then
A19: G.0 = (F.0)|E by A8;
A20: for n be Nat holds integral'(M,G.n) = L.n
proof
defpred L[Nat] means L.$1 = integral'(M,G.$1);
let n be Nat;
A21: G.0 is nonnegative by A17;
A22: for k be Nat st L[k] holds L[k+1]
proof
let k be Nat;
assume
A23: L[k];
L.(k+1) = (Partial_Sums I).k + I.(k+1) by Def1;
then
A24: L.(k+1) = integral'(M,G.k) + Integral(M,(F.(k+1))|E) by A15,A23;
A25: (F.(k+1))|E is_simple_func_in S by A9;
A26: dom((F.(k+1))|E) = E by A9;
A27: G.k is_simple_func_in S by A17;
G.(k+1) = G.k + g1.(k+1) by Def4;
then
A28: G.(k+1) = G.k + (F.(k+1))|E by A8;
A29: (F.(k+1))|E is nonnegative by A9;
A30: G.k is nonnegative by A17;
A31: dom(G.k) = E by A17;
then E = dom(G.k) /\ dom((F.(k+1))|E) by A26;
then dom( G.k + (F.(k+1))|E ) = E by A25,A29,A27,A30,MESFUNC5:65;
then
A32: integral'(M,G.k + (F.(k+1))|E) = integral'(M,(G.k)|E) + integral'(M
,((F.(k+1))|E)|E) by A25,A29,A27,A30,MESFUNC5:65;
(G.k)|E = G.k by A31;
hence thesis by A28,A24,A25,A29,A32,MESFUNC5:89;
end;
L.0 = I.0 by Def1;
then
A33: L.0 = Integral(M,G.0) by A15,A19;
G.0 is_simple_func_in S by A17;
then
A34: L[ 0 ] by A33,A21,MESFUNC5:89;
A35: for k be Nat holds L[k] from NAT_1:sch 2(A34,A22);
thus thesis by A35;
end;
g1.0 = (F.0)|E by A8;
then
A36: dom(g1.0) = E by A9;
A37: for x be Element of X st x in dom(f|E) holds g1#x is summable & (f|E).x
= Sum(g1#x)
proof
let x be Element of X;
assume
A38: x in dom(f|E);
then
A39: f.x = (f|E).x by FUNCT_1:47;
A40: for n be object st n in NAT holds (F#x).n = (g1#x).n
proof
let n be object;
assume n in NAT;
then reconsider n1 = n as Nat;
A41: (F#x).n = (F.n1).x by MESFUNC5:def 13;
A42: dom((F.n1)|E) = E by A9;
(F.n1)|E = g1.n1 by A8;
then (g1.n1).x = (F.n1).x by A13,A38,A42,FUNCT_1:47;
hence thesis by A41,MESFUNC5:def 13;
end;
A43: f.x = Sum(F#x) by A7,A13,A38;
F#x is summable by A7,A13,A38;
hence thesis by A43,A39,A40,FUNCT_2:12;
end;
A44: f|E is nonnegative by A2,MESFUNC5:15;
then consider
F be Functional_Sequence of X,ExtREAL, K be ExtREAL_sequence such
that
A45: for n be Nat holds F.n is_simple_func_in S & dom(F.n) = dom(f|E) and
A46: for n be Nat holds F.n is nonnegative and
A47: for n,m be Nat st n <=m holds for x be Element of X st x in dom(f|
E) holds (F.n).x <= (F.m).x and
A48: for x be Element of X st x in dom(f|E) holds F#x is convergent &
lim(F#x) = (f|E).x and
A49: for n be Nat holds K.n=integral'(M,F.n) and
K is convergent and
A50: integral+(M,(f|E))=lim K by A13,A14,MESFUNC5:def 15;
A51: g1 is additive by A4,A8,Th31;
A52: for x be Element of X st x in E holds F#x is convergent & G#x is
convergent & lim(F#x) = lim(G#x)
proof
let x be Element of X;
assume
A53: x in E;
hence F#x is convergent by A13,A48;
g1#x is summable by A13,A37,A53;
then Partial_Sums(g1#x) is convergent;
hence G#x is convergent by A11,A51,A36,A53,Th33;
A54: (f|E).x = Sum(g1#x) by A13,A37,A53;
g1#x is summable by A13,A37,A53;
then lim(G#x) = (f|E).x by A4,A13,A8,A11,A36,A53,A54,Th31,Th34;
hence thesis by A13,A48,A53;
end;
A55: 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 by A11,A16,A36,Th37;
then
A56: L is convergent by A13,A17,A20,A45,A46,A47,A49,A52,MESFUNC5:76;
lim L = integral+(M,(f|E)) by A13,A17,A20,A45,A46,A47,A49,A50,A55,A52,
MESFUNC5:76;
hence thesis by A13,A15,A14,A44,A56,MESFUNC5:88;
end;
theorem
E c= dom f & f is nonnegative & f is E-measurable & F is additive &
(for n holds F.n is_simple_func_in S & F.n is nonnegative & E c= dom(F.n)) & (
for x st x in E holds F#x is summable & f.x = Sum(F#x)) implies ex I be
ExtREAL_sequence st (for n holds I.n = Integral(M,(F.n)|E)) & I is summable &
Integral(M,f|E) = Sum I
proof
assume that
A1: E c= dom f and
A2: f is nonnegative and
A3: f is E-measurable and
A4: F is additive and
A5: for n holds F.n is_simple_func_in S & F.n is nonnegative & E c= dom
(F.n) and
A6: for x st x in E holds F#x is summable & f.x = Sum(F#x);
per cases;
suppose
E = {};
hence thesis by A1,A3,A5,Lm2;
end;
suppose
A7: E <> {};
for n be Nat holds F.n is_simple_func_in S & F.n is
nonnegative & E c= dom(F.n) by A5;
then E common_on_dom F by A7,SEQFUNC:def 9;
hence thesis by A1,A2,A3,A4,A5,A6,Lm3;
end;
end;
theorem
E c= dom f & f is nonnegative & f is E-measurable implies ex g be
Functional_Sequence of X,ExtREAL st 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 & f.x = Sum(g#x)) & ex I be
ExtREAL_sequence st (for n be Nat holds I.n = Integral(M,(g.n)|E)) & I is
summable & Integral(M,f|E) = Sum I
proof
assume that
A1: E c= dom f and
A2: f is nonnegative and
A3: f is E-measurable;
set F = f|E;
A4: dom F = E by A1,RELAT_1:62;
E = dom f /\ E by A1,XBOOLE_1:28;
then F is E-measurable by A3,MESFUNC5:42;
then consider h be Functional_Sequence of X,ExtREAL such that
A5: for n be Nat holds h.n is_simple_func_in S & dom(h.n) = dom F and
A6: for n be Nat holds h.n is nonnegative and
A7: for n,m be Nat st n <=m holds for x be Element of X st x in dom F
holds (h.n).x <= (h.m).x and
A8: for x be Element of X st x in dom F holds (h#x) is convergent & lim
(h#x) = F.x by A2,A4,MESFUNC5:15,64;
defpred P[Nat,set,set] means $3 = h.($1+1) - h.$1;
A9: for n being Nat for x being set ex y being set st P[n,x,y];
consider g being Function such that
A10: dom g = NAT & g.0 = h.0 & for n being Nat holds P[n,g.n,
g.(n+1)] from RECDEF_1:sch 1(A9);
now
defpred IND[Nat] means g.$1 is PartFunc of X,ExtREAL;
let f be object;
assume f in rng g;
then consider m be object such that
A11: m in dom g and
A12: f = g.m by FUNCT_1:def 3;
reconsider m as Element of NAT by A10,A11;
A13: for n be Nat st IND[n] holds IND[n+1]
proof
let n be Nat;
assume IND[n];
g.(n+1) = h.(n+1) - h.n by A10;
hence thesis;
end;
A14: IND[ 0 ] by A10;
for n be Nat holds IND[n] from NAT_1:sch 2(A14,A13);
then g.m is PartFunc of X,ExtREAL;
hence f in PFuncs(X,ExtREAL) by A12,PARTFUN1:45;
end;
then rng g c= PFuncs(X,ExtREAL);
then reconsider g as Functional_Sequence of X,ExtREAL by A10,FUNCT_2:def 1
,RELSET_1:4;
take g;
A15: for n be Nat holds g.n is_simple_func_in S & g.n is nonnegative & g.n
is E-measurable & E c= dom(g.n)
proof
let n be Nat;
per cases;
suppose
A16: n = 0;
hence g.n is_simple_func_in S & g.n is nonnegative by A5,A6,A10;
hence g.n is E-measurable by MESFUNC2:34;
thus thesis by A4,A5,A10,A16;
end;
suppose
n <> 0;
then consider m be Nat such that
A17: n = m+1 by NAT_1:6;
reconsider m as Element of NAT by ORDINAL1:def 12;
A18: g.n = h.n - h.m by A10,A17;
then
A19: g.n = h.n + (-(h.m)) by MESFUNC2:8;
A20: h.n is_simple_func_in S by A5;
then
A21: h.n is without-infty by MESFUNC5:14;
A22: dom(h.n) = dom F by A5;
(-jj)(#)(h.m) is_simple_func_in S by A5,MESFUNC5:39;
then
A23: -(h.m) is_simple_func_in S by MESFUNC2:9;
hence g.n is_simple_func_in S by A19,A20,MESFUNC5:38;
A24: h.m is_simple_func_in S by A5;
then h.m is without+infty by MESFUNC5:14;
then
A25: dom(h.n - h.m) = dom(h.n) /\ dom(h.m) by A21,MESFUNC5:17;
A26: dom(h.m) = dom F by A5;
then for x being object st x in dom(h.n - h.m) holds(h.m).x <= (h.n).x
by A7,A17,A25,A22,NAT_1:11;
hence g.n is nonnegative by A18,A20,A24,MESFUNC5:40;
thus g.n is E-measurable by A19,A20,A23,MESFUNC2:34,MESFUNC5:38;
thus thesis by A4,A10,A17,A25,A22,A26;
end;
end;
hence
A27: g is additive by Th35;
thus for n be Nat holds g.n is_simple_func_in S & g.n is nonnegative & g.n
is E-measurable by A15;
A28: now
let x be Element of X;
assume
A29: x in E;
then
A30: (h#x) is convergent by A4,A8;
A31: for m be Nat holds (Partial_Sums(g#x)).m = (h#x).m
proof
defpred P[Nat] means (Partial_Sums(g#x)).$1 = (h#x).$1;
let m be Nat;
A32: for k be Nat st P[k] holds P[k+1]
proof
set Pgx = Partial_Sums(g#x);
let k be Nat;
assume P[k];
then
A33: Pgx.k = (h.k).x by MESFUNC5:def 13;
A34: dom(h.(k+1)) = dom F by A5;
A35: h.(k+1) is_simple_func_in S by A5;
then
A36: h.(k+1) is without-infty by MESFUNC5:14;
then
A37: -infty < (h.(k+1)).x;
h.(k+1) is without+infty by A35,MESFUNC5:14;
then
A38: (h.(k+1)).x < +infty;
A39: dom(h.k) = dom F by A5;
A40: h.k is_simple_func_in S by A5;
then
A41: h.k is without+infty by MESFUNC5:14;
then
A42: (h.k).x < +infty;
h.k is without-infty by A40,MESFUNC5:14;
then
A43: -infty < (h.k).x;
reconsider k as Element of NAT by ORDINAL1:def 12;
reconsider hk1x=(h.(k+1)).x as Element of REAL
by A37,A38,XXREAL_0:14;
A44: g.(k+1) = h.(k+1) - h.k by A10;
reconsider hkx=(h.k).x as Element of REAL
by A43,A42,XXREAL_0:14;
(h.(k+1)).x - (h.k).x = hk1x - hkx by SUPINF_2:3;
then
A45: (h.(k+1)).x - (h.k).x + (h.k).x = hk1x - hkx + hkx by SUPINF_2:1;
Pgx.(k+1) = Pgx.k + ((g#x).(k+1)) by Def1;
then
A46: Pgx.(k+1) = (h.k).x + (g.(k+1)).x by A33,MESFUNC5:def 13;
dom(h.(k+1) - h.k) = dom(h.(k+1)) /\ dom(h.k) by A36,A41,MESFUNC5:17;
then (g.(k+1)).x = (h.(k+1)).x - (h.k).x by A4,A29,A34,A39,A44,
MESFUNC1:def 4;
hence thesis by A46,A45,MESFUNC5:def 13;
end;
(Partial_Sums(g#x)).0 = (g#x).0 by Def1;
then (Partial_Sums(g#x)).0 = (g.0).x by MESFUNC5:def 13;
then
A47: P[ 0 ] by A10,MESFUNC5:def 13;
for k being Nat holds P[k] from NAT_1:sch 2(A47,A32);
hence thesis;
end;
A48: lim(h#x) = F.x by A4,A8,A29;
per cases by A30;
suppose
A49: h#x is convergent_to_finite_number;
then
A50: not h#x is convergent_to_-infty by MESFUNC5:51;
not h#x is convergent_to_+infty by A49,MESFUNC5:50;
then consider s be Real such that
A51: lim(h#x) = s and
A52: for p be Real st 0 < p ex N be Nat st for m be Nat st N
<= m holds |. (h#x).m - lim(h#x) .| < p and
h#x is convergent_to_finite_number by A30,A50,MESFUNC5:def 12;
for p be Real st 0 < p ex N be Nat st for m be Nat st N <= m
holds |. (Partial_Sums(g#x)).m - s .| < p
proof
let p be Real;
assume 0 < p;
then consider N be Nat such that
A53: for m be Nat st N <= m holds |. (h#x).m - lim(h#x) .| < p by A52;
take N;
let m be Nat;
assume N <= m;
then |. (h#x).m - lim(h#x) .| < p by A53;
hence thesis by A31,A51;
end;
then
A54: Partial_Sums(g#x) is convergent_to_finite_number;
then
A55: Partial_Sums(g#x) is convergent;
hence g#x is summable;
for p be Real st 0 < p ex N be Nat st for m be Nat st N <=
m holds |. (Partial_Sums(g#x)).m - lim(h#x) .| < p
proof
let p be Real;
assume 0 < p;
then consider N be Nat such that
A56: for m be Nat st N <= m holds |. (h#x).m - lim(h#x) .| < p by A52;
take N;
let m be Nat;
assume N <= m;
then |. (h#x).m - lim(h#x) .| < p by A56;
hence thesis by A31;
end;
then lim Partial_Sums(g#x) = lim(h#x) by A51,A54,A55,MESFUNC5:def 12;
hence Sum(g#x) = f.x by A29,A48,FUNCT_1:49;
end;
suppose
A57: (h#x) is convergent_to_+infty;
for p be Real st 0 < p ex N be Nat st for m be Nat st N<=m
holds p <= (Partial_Sums(g#x)).m
proof
let p be Real;
assume 0 < p;
then consider N be Nat such that
A58: for m be Nat st N<=m holds p <= (h#x).m by A57;
take N;
let m be Nat;
assume N <= m;
then p <= (h#x).m by A58;
hence thesis by A31;
end;
then
A59: Partial_Sums(g#x) is convergent_to_+infty;
then
A60: Partial_Sums(g#x) is convergent;
then
A61: lim Partial_Sums(g#x) = +infty by A59,MESFUNC5:def 12;
thus g#x is summable by A60;
lim(h#x) = +infty by A30,A57,MESFUNC5:def 12;
hence Sum(g#x) = f.x by A29,A48,A61,FUNCT_1:49;
end;
suppose
A62: (h#x) is convergent_to_-infty;
for p be Real st p < 0 ex N be Nat st for m be Nat st N<=m
holds (Partial_Sums(g#x)).m <= p
proof
let p be Real;
assume p < 0;
then consider N be Nat such that
A63: for m be Nat st N<=m holds (h#x).m <= p by A62;
take N;
let m be Nat;
assume N <= m;
then (h#x).m <= p by A63;
hence thesis by A31;
end;
then
A64: Partial_Sums(g#x) is convergent_to_-infty;
then
A65: Partial_Sums(g#x) is convergent;
then
A66: lim Partial_Sums(g#x) = -infty by A64,MESFUNC5:def 12;
thus g#x is summable by A65;
lim(h#x) = -infty by A30,A62,MESFUNC5:def 12;
hence Sum(g#x) = f.x by A29,A48,A66,FUNCT_1:49;
end;
end;
hence for x be Element of X st x in E holds g#x is summable & f.x = Sum(g#x);
per cases;
suppose
E = {};
hence thesis by A1,A3,A15,Lm2;
end;
suppose
A67: E <> {};
for m be Nat holds g.m is_simple_func_in S & g.m is
nonnegative & g.m is E-measurable & E c= dom(g.m) by A15;
then E common_on_dom g by A67,SEQFUNC:def 9;
hence thesis by A1,A2,A3,A15,A27,A28,Lm3;
end;
end;
registration
let X be non empty set;
cluster additive with_the_same_dom for Functional_Sequence of X,ExtREAL;
existence
proof
deffunc f(Nat) = <:{},X,ExtREAL:>;
consider F be Functional_Sequence of X,ExtREAL such that
A1: for n be Nat holds F.n = f(n) from SEQFUNC:sch 1;
now
let n,m be Nat;
F.n = <:{},X,ExtREAL:> by A1;
hence dom(F.n) = dom(F.m) by A1;
end;
then reconsider
F as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2;
take F;
now
let n,m be Nat;
assume n <> m;
let x be set;
assume
A2: x in dom(F.n) /\ dom(F.m);
F.n = <:{},X,ExtREAL:> by A1;
then x in dom {} /\ dom(F.m) by A2,PARTFUN1:34;
hence (F.n).x <> +infty or (F.m).x <> -infty;
end;
hence thesis;
end;
end;
definition
let C,D,X be non empty set, F be Function of [:C,D:],PFuncs(X,ExtREAL);
let c be Element of C, d be Element of D;
redefine func F.(c,d) -> PartFunc of X,ExtREAL; :: redefines . (BINOP_1, definition)
correctness
proof
thus F.(c,d) is PartFunc of X,ExtREAL by PARTFUN1:47;
end;
end;
definition
let C,D,X be non empty set;
let F be Function of [:C,D:],X;
let c be Element of C;
func ProjMap1(F,c) -> Function of D,X means
for d be Element of D holds it.d = F.(c,d);
existence
proof
deffunc F(Element of D) = F.(c,$1);
consider IT be Function such that
A1: dom IT = D & for d be Element of D holds IT.d = F(d) from FUNCT_1:
sch 4;
now
let d be object;
assume
A2: d in D;
then
A3: [c,d] in [:C,D:] by ZFMISC_1:87;
IT.d = F.(c,d) by A1,A2;
hence IT.d in X by A3,FUNCT_2:5;
end;
then reconsider IT as Function of D,X by A1,FUNCT_2:3;
take IT;
let d be Element of D;
thus thesis by A1;
end;
uniqueness
proof
let P1,P2 be Function of D,X;
assume that
A4: for d be Element of D holds P1.d = F.(c,d) and
A5: for d be Element of D holds P2.d = F.(c,d);
now
let d be object;
assume d in D;
then reconsider d1 = d as Element of D;
P1.d1 = F.(c,d1) by A4;
hence P1.d = P2.d by A5;
end;
hence thesis;
end;
end;
definition
let C,D,X be non empty set;
let F be Function of [:C,D:],X;
let d be Element of D;
func ProjMap2(F,d) -> Function of C,X means
for c be Element of C holds it.c = F.(c,d);
existence
proof
deffunc F(Element of C) = F.($1,d);
consider IT be Function such that
A1: dom IT = C & for c be Element of C holds IT.c = F(c) from FUNCT_1:
sch 4;
now
let c be object;
assume
A2: c in C;
then
A3: [c,d] in [:C,D:] by ZFMISC_1:87;
IT.c = F.(c,d) by A1,A2
.= F.[c,d];
hence IT.c in X by A3,FUNCT_2:5;
end;
then reconsider IT as Function of C,X by A1,FUNCT_2:3;
take IT;
let c be Element of C;
thus thesis by A1;
end;
uniqueness
proof
let P1,P2 be Function of C,X;
assume that
A4: for c be Element of C holds P1.c = F.(c,d) and
A5: for c be Element of C holds P2.c = F.(c,d);
now
let c be object;
assume c in C;
then reconsider c1 = c as Element of C;
P1.c1 = F.(c1,d) by A4;
hence P1.c = P2.c by A5;
end;
hence thesis;
end;
end;
definition
let X,Y be set, F be Function of [:NAT,NAT:],PFuncs(X,Y), n be Nat;
func ProjMap1(F,n) -> Functional_Sequence of X,Y means
:Def8:
for m be Nat holds it.m = F.(n,m);
existence
proof
deffunc P1(Element of NAT) = F.(n,$1);
consider IT be Function such that
A1: dom IT = NAT & for m be Element of NAT holds IT.m = P1(m) from
FUNCT_1:sch 4;
now
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
let y be object;
assume y in rng IT;
then consider k be object such that
A2: k in dom IT and
A3: y = IT.k by FUNCT_1:def 3;
reconsider k as Element of NAT by A1,A2;
y = F.(n1,k) by A1,A3;
hence y in PFuncs(X,Y);
end;
then rng IT c= PFuncs(X,Y);
then reconsider IT as Functional_Sequence of X,Y by A1,FUNCT_2:def 1
,RELSET_1:4;
take IT;
thus for m be Nat holds IT.m = F.(n,m)
proof
let m be Nat;
reconsider n1=n,m1=m as Element of NAT by ORDINAL1:def 12;
IT.m = F.(n1,m1) by A1;
hence thesis;
end;
end;
uniqueness
proof
let G1,G2 be Functional_Sequence of X,Y;
assume that
A4: for m be Nat holds G1.m = F.(n,m) and
A5: for m be Nat holds G2.m = F.(n,m);
for m be Element of NAT holds G1.m = G2.m
proof
let m be Element of NAT;
reconsider m1=m as Nat;
G1.m = F.(n,m1) by A4;
hence thesis by A5;
end;
hence thesis;
end;
func ProjMap2(F,n) -> Functional_Sequence of X,Y means
:Def9:
for m be Nat holds it.m = F.(m,n);
existence
proof
deffunc P2(Element of NAT) = F.($1,n);
consider IT be Function such that
A6: dom IT = NAT & for m be Element of NAT holds IT.m = P2(m) from
FUNCT_1:sch 4;
now
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
let y be object;
assume y in rng IT;
then consider k be object such that
A7: k in dom IT and
A8: y = IT.k by FUNCT_1:def 3;
reconsider k as Element of NAT by A6,A7;
y = F.(k,n1) by A6,A8;
hence y in PFuncs(X,Y);
end;
then rng IT c= PFuncs(X,Y);
then reconsider IT as Functional_Sequence of X,Y by A6,FUNCT_2:def 1
,RELSET_1:4;
take IT;
thus for m be Nat holds IT.m = F.(m,n)
proof
let m be Nat;
reconsider n1=n,m1=m as Element of NAT by ORDINAL1:def 12;
IT.m = F.(m1,n1) by A6;
hence thesis;
end;
end;
uniqueness
proof
let G1,G2 be Functional_Sequence of X,Y;
assume that
A9: for m be Nat holds G1.m = F.(m,n) and
A10: for m be Nat holds G2.m = F.(m,n);
for m be Element of NAT holds G1.m = G2.m
proof
let m be Element of NAT;
reconsider m1=m as Nat;
G1.m = F.(m1,n) by A9;
hence thesis by A10;
end;
hence thesis;
end;
end;
definition
let X be non empty set, F be sequence of Funcs(NAT,PFuncs(X,ExtREAL)), n
be Nat;
redefine func F.n -> Functional_Sequence of X,ExtREAL; :: redefines . (FUNCT_1, definition)
correctness
proof
ex f be Function st F.n = f & dom f = NAT & rng f c= PFuncs(X,ExtREAL)
by FUNCT_2:def 2;
hence thesis by FUNCT_2:def 1,RELSET_1:4;
end;
end;
theorem Th49:
E = dom(F.0) & F is with_the_same_dom & (for n be Nat holds F.n
is nonnegative & F.n is E-measurable) implies 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 nonnegative) & (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
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 nonnegative & 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 nonnegative) & (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 nonnegative) & (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;
A6: F.n is nonnegative by A3;
E = dom(F.n) by A1,A2;
hence thesis by A5,A6,MESFUNC5:64;
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 nonnegative 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 nonnegative) & (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 nonnegative) & (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 Th50:
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 nonnegative) implies 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
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 nonnegative;
set PF = Partial_Sums F;
deffunc I(Element of NAT) = Integral(M,F.$1);
consider I be sequence of ExtREAL such that
A5: for n be Element of NAT holds I.n = I(n) from FUNCT_2:sch 4;
reconsider I as ExtREAL_sequence;
take I;
A6: for n be Nat holds F.n is without-infty by A4,MESFUNC5:12;
thus for n be Nat holds I.n = Integral(M,F.n) & Integral(M,(Partial_Sums F).
n) = (Partial_Sums I).n
proof
set PI = Partial_Sums I;
defpred P2[Nat] means Integral(M,PF.$1) = (Partial_Sums I).$1;
let n be Nat;
reconsider n9=n as Element of NAT by ORDINAL1:def 12;
I.n = Integral(M,F.n9) by A5;
hence I.n = Integral(M,F.n);
A7: for k be Nat st P2[k] holds P2[k+1]
proof
let k be Nat;
assume
A8: P2[k];
A9: F.(k+1) is E-measurable by A4;
A10: dom(F.(k+1)) = E by A1,A3;
A11: PF.(k+1) is E-measurable by A4,A6,Th41;
A12: F.(k+1) is nonnegative by A4;
A13: PF.k is nonnegative by A4,Th36;
A14: dom(PF.k) = E by A1,A2,A3,Th29;
A15: PF.k is E-measurable by A4,A6,Th41;
then consider D be Element of S such that
A16: D = dom(PF.k + F.(k+1)) and
A17: integral+(M,PF.k + F.(k+1)) = integral+(M,(PF.k)|D) + integral+
(M,( F.(k+1))|D) by A14,A10,A9,A13,A12,MESFUNC5:78;
A18: D = dom(PF.k) /\ dom(F.(k+1)) by A13,A12,A16,MESFUNC5:22
.= E by A14,A10;
then
A19: (PF.k)|D = PF.k by A14;
A20: (F.(k+1))|D = F.(k+1) by A10,A18;
dom(PF.(k+1)) = E by A1,A2,A3,Th29;
then Integral(M,PF.(k+1)) = integral+(M,PF.(k+1)) by A4,A11,Th36,
MESFUNC5:88
.= integral+(M,(PF.k)|D) + integral+(M,(F.(k+1))|D) by A17,Def4
.= Integral(M,PF.k) + integral+(M,(F.(k+1))|D) by A14,A15,A13,A19,
MESFUNC5:88
.= Integral(M,PF.k) + Integral(M,F.(k+1)) by A10,A9,A12,A20,MESFUNC5:88
.= PI.k + I.(k+1) by A5,A8;
hence thesis by Def1;
end;
Integral(M,PF.0) = Integral(M,F.0) by Def4;
then Integral(M,PF.0) = I.0 by A5;
then
A21: P2[ 0 ] by Def1;
for k be Nat holds P2[k] from NAT_1:sch 2(A21,A7);
hence thesis;
end;
end;
Lm4: E = dom(F.0) & F is additive & F is with_the_same_dom & (for n be Nat
holds F.n is nonnegative & F.n is E-measurable) & (for x be Element of X
st
x in E holds F#x is summable) implies 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
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 nonnegative & F.n is E-measurable and
A5: for x be Element of X st x in E holds F#x is summable;
consider FF be sequence of Funcs(NAT,PFuncs(X,ExtREAL)) such that
A6: 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 nonnegative) & (
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 by A1,A3,A4,Th49;
defpred PP[Element of NAT,Element of NAT,set] means for n,m be Nat st n = $1
& m = $2 holds $3 = (FF.n).m;
A7: for i1 be Element of NAT for j1 be Element of NAT ex F1 be Element of
PFuncs(X,ExtREAL) st PP[i1,j1,F1]
proof
let i1 be Element of NAT;
let j1 be Element of NAT;
reconsider i = i1, j = j1 as Nat;
reconsider F1 = (FF.i).j as Element of PFuncs(X,ExtREAL) by PARTFUN1:45;
take F1;
thus thesis;
end;
consider FF2 be Function of [:NAT,NAT:],PFuncs(X,ExtREAL) such that
A8: for i be Element of NAT for j be Element of NAT holds PP[i,j,FF2.(i
,j)] from BINOP_1:sch 3(A7);
deffunc Phi(Nat) = (Partial_Sums ProjMap2(FF2,$1)).$1;
consider P be Functional_Sequence of X,ExtREAL such that
A9: for k be Nat holds P.k = Phi(k) from SEQFUNC:sch 1;
A10: for n be Nat holds (for m be Nat holds dom(ProjMap1(FF2,n).m) = E & dom(
ProjMap2(FF2,n).m) = E & ProjMap1(FF2,n).m is_simple_func_in S & ProjMap2(FF2,n
).m is_simple_func_in S) & ProjMap1(FF2,n) is additive & ProjMap2(FF2,n) is
additive & ProjMap1(FF2,n) is with_the_same_dom & ProjMap2(FF2,n) is
with_the_same_dom
proof
let n be Nat;
A11: now
let m be Nat;
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 12;
A12: ProjMap1(FF2,n).m = FF2.(n,m) by Def8;
A13: FF2.(n1,m1) = (FF.n1).m by A8;
A14: dom(F.m1) = dom(F.0) by A3;
A15: ProjMap2(FF2,n).m = FF2.(m,n) by Def9;
A16: FF2.(m1,n1) = (FF.m1).n by A8;
dom(F.n1) = dom(F.m1) by A3;
hence dom(ProjMap1(FF2,n).m) = E & dom(ProjMap2(FF2,n).m) = E by A1,A6
,A12,A15,A13,A16,A14;
thus ProjMap1(FF2,n).m is_simple_func_in S & ProjMap2(FF2,n).m
is_simple_func_in S by A6,A12,A15,A13,A16;
end;
for i1,j1 be Nat holds dom(ProjMap1(FF2,n).i1) = dom(ProjMap1(FF2,n).
j1) & dom(ProjMap2(FF2,n).i1) = dom(ProjMap2(FF2,n).j1)
proof
let i1,j1 be Nat;
A17: dom(ProjMap2(FF2,n).i1) = E by A11;
dom(ProjMap1(FF2,n).i1) = E by A11;
hence thesis by A11,A17;
end;
hence thesis by A11,Th35;
end;
for n,m be Nat holds dom(P.n) = dom(P.m)
proof
let n,m be Nat;
A18: ProjMap2(FF2,n) is with_the_same_dom by A10;
A19: dom(P.n) = dom((Partial_Sums ProjMap2(FF2,n)).n) by A9;
ProjMap2(FF2,n) is additive by A10;
then dom(P.n) = dom((ProjMap2(FF2,n)).0) by A18,A19,Th29;
then dom(P.n) = E by A10;
then
A20: dom(P.n) = dom((ProjMap2(FF2,m)).0) by A10;
A21: ProjMap2(FF2,m) is with_the_same_dom by A10;
ProjMap2(FF2,m) is additive by A10;
then dom(P.n) = dom((Partial_Sums ProjMap2(FF2,m)).m) by A21,A20,Th29;
hence thesis by A9;
end;
then reconsider P as with_the_same_dom Functional_Sequence of X,ExtREAL by
MESFUNC8:def 2;
dom(lim P) = dom(P.0) by MESFUNC8:def 9;
then dom(lim P) = dom((Partial_Sums ProjMap2(FF2,0)).0) by A9;
then dom(lim P) = dom((ProjMap2(FF2,0)).0) by Def4;
then dom(lim P) = dom( FF2.(0,0) ) by Def9;
then
A22: dom(lim P) = dom( (FF.0).0 ) by A8;
then
A23: dom (lim P) = dom(F.0) by A6;
A24: for k be Nat holds for m be Nat, x be Element of X st x in dom(F.0) /\
dom((ProjMap2(FF2,k)).0) holds ((ProjMap2(FF2,k)).m).x <= (F.m).x
proof
let k be Nat;
let m be Nat, x be Element of X;
reconsider m1 = m, k1 = k as Element of NAT by ORDINAL1:def 12;
assume x in dom(F.0) /\ dom((ProjMap2(FF2,k)).0);
then x in dom(F.0) by XBOOLE_0:def 4;
then
A25: x in dom(F.m) by A3;
(FF.m1)#x is non-decreasing
proof
let j,k be ExtReal;
assume that
A26: j in dom((FF.m1)#x) and
A27: k in dom((FF.m1)#x) and
A28: j <= k;
reconsider j,k as Element of NAT by A26,A27;
A29: ((FF.m1)#x).k = ((FF.m1).k).x by MESFUNC5:def 13;
((FF.m1)#x).j = ((FF.m1).j).x by MESFUNC5:def 13;
hence thesis by A6,A25,A28,A29;
end;
then lim((FF.m1)#x) = sup ((FF.m1)#x) by RINFSUP2:37;
then ((FF.m1)#x).k1 <= lim((FF.m1)#x) by RINFSUP2:23;
then
A30: ((FF.m1)#x).k <= (F.m1).x by A6,A25;
(ProjMap2(FF2,k)).m = FF2.(m1,k1) by Def9;
then (ProjMap2(FF2,k)).m = (FF.m).k by A8;
hence thesis by A30,MESFUNC5:def 13;
end;
A31: for x be Element of X, k be Element of NAT st x in dom(lim P) holds (P#
x).k <= ((Partial_Sums F)#x).k
proof
let x be Element of X;
let k be Element of NAT;
assume
A32: x in dom(lim P);
dom((ProjMap2(FF2,k)).0) = E by A10;
then
A33: x in dom(F.0) /\ dom((ProjMap2(FF2,k)).0) by A1,A6,A22,A32;
A34: ProjMap2(FF2,k) is with_the_same_dom by A10;
(P#x).k = (P.k).x by MESFUNC5:def 13;
then
A35: (P#x).k = ((Partial_Sums ProjMap2(FF2,k)).k).x by A9;
A36: for m be Nat, x be Element of X st x in dom(F.0) /\ dom((ProjMap2(
FF2, k)).0) holds ((ProjMap2(FF2,k)).m).x <= (F.m).x by A24;
ProjMap2(FF2,k) is additive by A10;
then ((Partial_Sums ProjMap2(FF2,k)).k).x <= ((Partial_Sums F).k).x by A2
,A3,A33,A34,A36,Th42;
hence thesis by A35,MESFUNC5:def 13;
end;
dom(lim(Partial_Sums F)) = dom((Partial_Sums F).0) by MESFUNC8:def 9;
then
A37: dom(lim(Partial_Sums F)) = E by A1,Def4;
A38: for n,m be Nat holds (ProjMap1(FF2,n)).m is nonnegative & (ProjMap2(FF2,
n)).m is nonnegative
proof
let n,m be Nat;
reconsider n1=n,m1=m as Element of NAT by ORDINAL1:def 12;
(ProjMap1(FF2,n)).m = FF2.(n1,m1) by Def8;
then (ProjMap1(FF2,n)).m = (FF.n).m by A8;
hence (ProjMap1(FF2,n)).m is nonnegative by A6;
(ProjMap2(FF2,n)).m = FF2.(m1,n1) by Def9;
then (ProjMap2(FF2,n)).m = (FF.m).n by A8;
hence thesis by A6;
end;
A39: for n be Element of NAT holds for x be Element of X st x in E holds (
ProjMap1(FF2,n))#x is convergent & (F.n).x = lim( (ProjMap1(FF2,n))#x )
proof
let n be Element of NAT;
reconsider n1 = n as Nat;
let x be Element of X;
assume
A40: x in E;
for k be Nat holds ex m be Nat st k <= m & ((ProjMap1(FF2,n))#x).m > -1
proof
let k be Nat;
take m = k;
A41: ((ProjMap1(FF2,n))#x).m = ((ProjMap1(FF2,n)).m).x by MESFUNC5:def 13;
(ProjMap1(FF2,n)).m is nonnegative by A38;
hence thesis by A41,SUPINF_2:39;
end;
then
A42: not (ProjMap1(FF2,n))#x is convergent_to_-infty;
A43: E = dom(F.n1) by A1,A3;
(ProjMap1(FF2,n))#x is non-decreasing
proof
let i,j be ExtReal;
assume that
A44: i in dom((ProjMap1(FF2,n))#x) and
A45: j in dom((ProjMap1(FF2,n))#x) and
A46: i <= j;
reconsider i1=i, j1=j as Element of NAT by A44,A45;
A47: ((ProjMap1(FF2,n))#x).i1 = ((ProjMap1(FF2,n)).i1).x by MESFUNC5:def 13;
(ProjMap1(FF2,n)).i1 = FF2.(n,i1) by Def8;
then
A48: (ProjMap1(FF2,n)).i1 = (FF.n1).i1 by A8;
A49: ((ProjMap1(FF2,n))#x).j1 = ((ProjMap1(FF2,n)).j1).x by MESFUNC5:def 13;
A50: (ProjMap1(FF2,n)).j1 = FF2.(n,j1) by Def8;
((FF.n1).i1).x <= ((FF.n1).j1).x by A6,A43,A40,A46;
hence thesis by A8,A47,A49,A48,A50;
end;
hence
A51: (ProjMap1(FF2,n))#x is convergent by RINFSUP2:37;
per cases by A51,A42;
suppose
A52: (ProjMap1(FF2,n))#x is convergent_to_finite_number;
then
A53: not (ProjMap1(FF2,n))#x is convergent_to_-infty by MESFUNC5:51;
not (ProjMap1(FF2,n))#x is convergent_to_+infty by A52,MESFUNC5:50;
then consider lP be Real such that
A54: lim( (ProjMap1(FF2,n))#x ) = lP and
A55: for p be Real st 0<p ex nn be Nat st for mm be Nat st nn
<= mm holds |. ((ProjMap1(FF2,n))#x).mm - lim( (ProjMap1(FF2,n))#x ).| < p and
(ProjMap1(FF2,n))#x is convergent_to_finite_number by A51,A53,
MESFUNC5:def 12;
A56: for p be Real st 0<p ex nn be Nat st for mm be Nat st nn<=mm
holds |. ((FF.n1)#x).mm - lP .| < p
proof
let p be Real;
assume 0<p;
then consider nn be Nat such that
A57: for mm be Nat st nn<=mm holds |. ((ProjMap1(FF2,n))#x).mm -
lim( (ProjMap1(FF2,n))#x ).| < p by A55;
take nn;
let mm be Nat;
assume
A58: nn<=mm;
reconsider mm1 = mm as Element of NAT by ORDINAL1:def 12;
(ProjMap1(FF2,n)).mm = FF2.(n,mm) by Def8;
then
A59: (ProjMap1(FF2,n)).mm = (FF.n1).mm1 by A8;
((ProjMap1(FF2,n))#x).mm = ((ProjMap1(FF2,n)).mm).x by MESFUNC5:def 13;
then ((FF.n1)#x).mm = ((ProjMap1(FF2,n))#x).mm by A59,MESFUNC5:def 13;
hence thesis by A54,A57,A58;
end;
then
A60: (FF.n1)#x is convergent_to_finite_number;
reconsider lP as R_eal by XXREAL_0:def 1;
(FF.n1)#x is convergent by A60;
then lim((FF.n1)#x) = lP by A56,A60,MESFUNC5:def 12;
hence thesis by A6,A43,A40,A54;
end;
suppose
A61: (ProjMap1(FF2,n))#x is convergent_to_+infty;
for g be Real st 0 < g ex nn be Nat st for mm be Nat st nn<=
mm holds g <= ((FF.n1)#x).mm
proof
let g be Real;
assume 0 < g;
then consider nn be Nat such that
A62: for mm be Nat st nn<=mm holds g <= ((ProjMap1(FF2,n))#x).mm
by A61;
take nn;
let mm be Nat;
assume nn<=mm;
then
A63: g <= ((ProjMap1(FF2,n))#x).mm by A62;
reconsider mm1 = mm as Element of NAT by ORDINAL1:def 12;
(ProjMap1(FF2,n)).mm = FF2.(n,mm1) by Def8;
then
A64: (ProjMap1(FF2,n)).mm = (FF.n).mm by A8;
((ProjMap1(FF2,n))#x).mm = ((ProjMap1(FF2,n)).mm).x by MESFUNC5:def 13;
hence thesis by A63,A64,MESFUNC5:def 13;
end;
then
A65: (FF.n1)#x is convergent_to_+infty;
then (FF.n1)#x is convergent;
then
A66: lim((FF.n1)#x) = +infty by A65,MESFUNC5:def 12;
lim( (ProjMap1(FF2,n))#x ) = +infty by A51,A61,MESFUNC5:def 12;
hence thesis by A6,A43,A40,A66;
end;
end;
A67: dom(lim(Partial_Sums F)) = dom((Partial_Sums F).0) by MESFUNC8:def 9;
then
A68: dom(lim(Partial_Sums F)) = E by A1,Def4;
A69: for n be Nat holds dom(P.n) = dom(lim(Partial_Sums F))
proof
let n be Nat;
A70: ProjMap2(FF2,n) is with_the_same_dom by A10;
A71: dom(P.n) = dom((Partial_Sums ProjMap2(FF2,n)).n) by A9;
ProjMap2(FF2,n) is additive by A10;
then dom(P.n) = dom((ProjMap2(FF2,n)).0) by A70,A71,Th29;
hence thesis by A68,A10;
end;
A72: for n,m be Nat st n <= m holds for i be Nat, x be Element of X st x in
E holds ((ProjMap2(FF2,n)).i).x <= ((ProjMap2(FF2,m)).i).x
proof
let n,m be Nat;
assume
A73: n <= m;
let i be Nat, x be Element of X;
reconsider i1=i, n1=n, m1=m as Element of NAT by ORDINAL1:def 12;
((ProjMap2(FF2,n)).i).x = (FF2.(i1,n1)).x by Def9;
then
A74: ((ProjMap2(FF2,n)).i).x = ((FF.i).n).x by A8;
((ProjMap2(FF2,m)).i).x = (FF2.(i1,m1)).x by Def9;
then
A75: ((ProjMap2(FF2,m)).i).x = ((FF.i).m).x by A8;
assume x in E;
then x in dom(F.i) by A1,A3;
hence thesis by A6,A73,A74,A75;
end;
A76: for n,m be Nat st n <= m holds for i be Nat, x be Element of X st x in
E holds ((Partial_Sums ProjMap2(FF2,n)).i).x <= ((Partial_Sums ProjMap2(FF2,m))
.i).x
proof
let n,m be Nat;
A77: ProjMap2(FF2,n) is with_the_same_dom by A10;
A78: ProjMap2(FF2,m) is additive by A10;
assume
A79: n <= m;
A80: for i be Nat, x be Element of X st x in dom(ProjMap2(FF2,n).0) /\
dom(ProjMap2(FF2,m).0) holds ((ProjMap2(FF2,n)).i).x <= ((ProjMap2(FF2,m)).i).x
proof
let i be Nat, x be Element of X;
assume x in dom(ProjMap2(FF2,n).0) /\ dom(ProjMap2(FF2,m).0);
then x in dom(ProjMap2(FF2,n).0) by XBOOLE_0:def 4;
then x in E by A10;
hence thesis by A72,A79;
end;
let i be Nat, x be Element of X;
assume
A81: x in E;
then
A82: x in dom(ProjMap2(FF2,m).0) by A10;
x in dom(ProjMap2(FF2,n).0) by A10,A81;
then
A83: x in dom(ProjMap2(FF2,n).0) /\ dom(ProjMap2(FF2,m).0) by A82,
XBOOLE_0:def 4;
A84: ProjMap2(FF2,m) is with_the_same_dom by A10;
ProjMap2(FF2,n) is additive by A10;
hence thesis by A83,A77,A78,A84,A80,Th42;
end;
A85: for n,m be Nat st n <= m holds for x be Element of X st x in E holds (P
.n).x <= (P.m).x
proof
let n,m be Nat;
reconsider n1=n,m1=m as Element of NAT by ORDINAL1:def 12;
assume
A86: n <= m;
let x be Element of X;
A87: ProjMap2(FF2,m) is with_the_same_dom by A10;
A88: for n be Nat holds (ProjMap2(FF2,m)).n is nonnegative by A38;
assume
A89: x in E;
then x in dom(ProjMap2(FF2,m).0) by A10;
then (Partial_Sums ProjMap2(FF2,m))#x is non-decreasing by A87,A88,Th38;
then ((Partial_Sums ProjMap2(FF2,m))#x).n1 <= ((Partial_Sums ProjMap2(FF2
,m))#x).m1 by A86,RINFSUP2:7;
then ((Partial_Sums ProjMap2(FF2,m)).n).x <= ((Partial_Sums ProjMap2(FF2,
m))#x).m1 by MESFUNC5:def 13;
then ((Partial_Sums ProjMap2(FF2,m)).n).x <= ((Partial_Sums ProjMap2(FF2,
m)).m).x by MESFUNC5:def 13;
then
A90: ((Partial_Sums ProjMap2(FF2,m)).n).x <= (P.m).x by A9;
((Partial_Sums ProjMap2(FF2,n)).n).x <= ((Partial_Sums ProjMap2(FF2,
m)).n).x by A76,A86,A89;
then (P.n).x <= ((Partial_Sums ProjMap2(FF2,m)).n).x by A9;
hence thesis by A90,XXREAL_0:2;
end;
A91: for x be Element of X st x in dom(lim P) holds P#x is convergent
proof
let x be Element of X;
assume
A92: x in dom(lim P);
for n,m be Nat st m<=n holds (P#x).m <= (P#x).n
proof
let n,m be Nat;
assume m <= n;
then (P.m).x <= (P.n).x by A1,A85,A23,A92;
then (P#x).m <= (P.n).x by MESFUNC5:def 13;
hence thesis by MESFUNC5:def 13;
end;
then P#x is non-decreasing by RINFSUP2:7;
hence thesis by RINFSUP2:37;
end;
A93: for x be Element of X st x in dom(lim P) holds lim(P#x) = lim((
Partial_Sums F)#x)
proof
defpred PP2[Element of NAT,Element of NAT,set] means for n,m be Nat st n =
$1 & m = $2 holds $3 = (Partial_Sums ProjMap2(FF2,n)).m;
let x be Element of X;
A94: for i1 be Element of NAT for j1 be Element of NAT ex PP2 be Element
of PFuncs(X,ExtREAL) st PP2[i1,j1,PP2]
proof
let i1 be Element of NAT;
let j1 be Element of NAT;
reconsider i = i1, j = j1 as Nat;
reconsider F1 = (Partial_Sums ProjMap2(FF2,i)).j as Element of PFuncs(X,
ExtREAL) by PARTFUN1:45;
take F1;
thus thesis;
end;
consider PP2 be Function of [:NAT,NAT:],PFuncs(X,ExtREAL) such that
A95: for i be Element of NAT for j be Element of NAT holds PP2[i,j,
PP2.(i,j)] from BINOP_1:sch 3(A94);
assume
A96: x in dom(lim P);
then
A97: P#x is convergent by A91;
A98: for p,n be Element of NAT holds (ProjMap2(PP2,n)).p = (Partial_Sums
ProjMap2(FF2,p)).n
proof
let p,n be Element of NAT;
(ProjMap2(PP2,n)).p = PP2.(p,n) by Def9;
hence thesis by A95;
end;
A99: for n be Element of NAT holds ((ProjMap2(PP2,n))#x) is convergent &
((ProjMap2(PP2,n))#x)^\n is convergent & lim ((ProjMap2(PP2,n))#x) = lim (((
ProjMap2(PP2,n))#x)^\n)
proof
let n be Element of NAT;
(ProjMap2(PP2,n))#x is non-decreasing
proof
let j,k be ExtReal;
assume that
A100: j in dom((ProjMap2(PP2,n))#x) and
A101: k in dom((ProjMap2(PP2,n))#x) and
A102: j <= k;
reconsider j,k as Element of NAT by A100,A101;
A103: ProjMap2(FF2,j) is additive by A10;
A104: ProjMap2(FF2,k) is with_the_same_dom by A10;
A105: dom((ProjMap2(FF2,k)).0) = E by A10;
((ProjMap2(PP2,n))#x).k = ((ProjMap2(PP2,n)).k).x by MESFUNC5:def 13;
then
A106: ((ProjMap2(PP2,n))#x).k = ((Partial_Sums ProjMap2(FF2,k)).n).x by A98;
A107: ProjMap2(FF2,k) is additive by A10;
((ProjMap2(PP2,n))#x).j = ((ProjMap2(PP2,n)).j).x by MESFUNC5:def 13;
then
A108: ((ProjMap2(PP2,n))#x).j = ((Partial_Sums ProjMap2(FF2,j)).n).x by A98;
A109: ProjMap2(FF2,j) is with_the_same_dom by A10;
A110: dom((ProjMap2(FF2,j)).0) = E by A10;
then for i be Nat, z be Element of X st z in dom((ProjMap2(FF2,j)).0)
/\ dom((ProjMap2(FF2,k)).0) holds ((ProjMap2(FF2,j)).i).z <= ((ProjMap2(FF2,k))
.i).z by A72,A102,A105;
hence thesis by A1,A23,A96,A108,A106,A103,A109,A107,A104,A110,A105,Th42
;
end;
hence (ProjMap2(PP2,n))#x is convergent by RINFSUP2:37;
hence thesis by RINFSUP2:21;
end;
A111: for n be Nat holds ((Partial_Sums F)#x).n <= lim(P#x)
proof
for p be object st p in NAT holds ((ProjMap2(PP2,0))#x).p = ((
ProjMap1(FF2,0))#x).p
proof
let p be object;
assume p in NAT;
then reconsider p9=p as Element of NAT;
(ProjMap2(PP2,0)).p9 = (Partial_Sums ProjMap2(FF2,p9)).0 by A98;
then (ProjMap2(PP2,0)).p9 = (ProjMap2(FF2,p9)).0 by Def4;
then (ProjMap2(PP2,0)).p9 = FF2.(0,p9) by Def9;
then
A112: (ProjMap2(PP2,0)).p9 = (ProjMap1(FF2,0)).p9 by Def8;
((ProjMap2(PP2,0))#x).p = ((ProjMap2(PP2,0)).p9).x by MESFUNC5:def 13;
hence thesis by A112,MESFUNC5:def 13;
end;
then (ProjMap2(PP2,0))#x = (ProjMap1(FF2,0))#x;
then
A113: lim((ProjMap2(PP2,0))#x) = (F.0).x by A1,A39,A23,A96;
defpred C[Nat] means lim((ProjMap2(PP2,$1))#x) = ((Partial_Sums F)#x).$1;
let n be Nat;
reconsider n9=n as Element of NAT by ORDINAL1:def 12;
A114: lim((P#x)^\n9) = lim(P#x) by A97,RINFSUP2:21;
A115: ((ProjMap2(PP2,n))#x)^\n9 is convergent by A99;
A116: for k be Nat st C[k] holds C[k+1]
proof
let k be Nat;
reconsider k9=k as Element of NAT by ORDINAL1:def 12;
assume
A117: C[k];
A118: (ProjMap2(PP2,k9))#x is convergent by A99;
now
let m be object;
assume m in dom((ProjMap1(FF2,k+1))#x);
then reconsider m1=m as Element of NAT;
(ProjMap1(FF2,k+1)).m1 is nonnegative by A38;
then 0. <= ((ProjMap1(FF2,k+1)).m1).x by SUPINF_2:51;
hence 0. <= ((ProjMap1(FF2,k+1))#x).m by MESFUNC5:def 13;
end;
then
A119: (ProjMap1(FF2,k+1))#x is nonnegative by SUPINF_2:52;
now
let m be object;
assume m in dom((ProjMap2(PP2,k))#x);
then reconsider m1=m as Element of NAT;
A120: (ProjMap2(PP2,k)).m1 = (Partial_Sums ProjMap2(FF2,m1)).k9 by A98;
for l be Nat holds (ProjMap2(FF2,m1)).l is nonnegative by A38;
then (ProjMap2(PP2,k)).m1 is nonnegative by A120,Th36;
then 0. <= ((ProjMap2(PP2,k)).m1).x by SUPINF_2:51;
hence 0. <= ((ProjMap2(PP2,k))#x).m by MESFUNC5:def 13;
end;
then
A121: (ProjMap2(PP2,k))#x is nonnegative by SUPINF_2:52;
x in dom((Partial_Sums F).(k+1)) by A2,A3,A23,A96,Th29;
then
A122: x in dom((Partial_Sums F).k + F.(k+1)) by Def4;
A123: for p be Nat holds ((ProjMap2(PP2,k+1))#x).p = ((ProjMap2(PP2,k)
)#x).p + ((ProjMap1(FF2,k+1))#x).p
proof
let p be Nat;
reconsider p9= p as Element of NAT by ORDINAL1:def 12;
A124: (ProjMap2(FF2,p9)).(k+1) = FF2.(k+1,p9) by Def9;
A125: ProjMap2(FF2,p) is with_the_same_dom by A10;
A126: dom((ProjMap2(FF2,p)).0) = E by A10;
ProjMap2(FF2,p) is additive by A10;
then E c= dom((Partial_Sums ProjMap2(FF2,p)).(k+1)) by A125,A126,Th29
;
then
A127: E c= dom((ProjMap2(PP2,k+1)).p9) by A98;
(ProjMap2(PP2,k+1)).p9 = (Partial_Sums ProjMap2(FF2,p9)).(k+1)
by A98;
then
A128: (ProjMap2(PP2,k+1)).p9 = (Partial_Sums ProjMap2(FF2,p9)).k + (
ProjMap2(FF2,p9)).(k+1) by Def4;
(Partial_Sums ProjMap2(FF2,p9)).k9 = (ProjMap2(PP2,k)).p9 by A98;
then (ProjMap2(PP2,k+1)).p9 = (ProjMap2(PP2,k)).p9 + (ProjMap1(FF2,
k+1)).p9 by A128,A124,Def8;
then ((ProjMap2(PP2,k+1)).p9).x =((ProjMap2(PP2,k)).p9).x + ((
ProjMap1(FF2,k+1)).p9).x by A1,A23,A96,A127,MESFUNC1:def 3;
then
A129: ((ProjMap2(PP2,k+1)).p9).x = ((ProjMap2(PP2,k))#x).p + ((
ProjMap1(FF2,k+1)).p9).x by MESFUNC5:def 13;
((ProjMap2(PP2,k+1))#x).p = ((ProjMap2(PP2,k+1)).p9).x by
MESFUNC5:def 13;
hence thesis by A129,MESFUNC5:def 13;
end;
A130: lim((ProjMap1(FF2,k+1))#x) = (F.(k+1)).x by A1,A39,A23,A96;
(ProjMap1(FF2,k+1))#x is convergent by A1,A39,A23,A96;
then lim((ProjMap2(PP2,k+1))#x) = lim((ProjMap2(PP2,k))#x) + lim((
ProjMap1(FF2,k+1))#x) by A118,A121,A119,A123,Th11;
then lim((ProjMap2(PP2,k+1))#x) = ((Partial_Sums F).k).x + (F.(k+1)).
x by A117,A130,MESFUNC5:def 13;
then lim((ProjMap2(PP2,k+1))#x) = ( (Partial_Sums F).k + F.(k+1) ).x
by A122,MESFUNC1:def 3;
then lim((ProjMap2(PP2,k+1))#x) = ((Partial_Sums F).(k+1)).x by Def4;
hence thesis by MESFUNC5:def 13;
end;
A131: for p be Nat holds (((ProjMap2(PP2,n))#x)^\n9).p <= ((P
#x)^\n9).p
proof
let p be Nat;
A132: n+p in NAT by ORDINAL1:def 12;
A133: n <= n+p by NAT_1:11;
A134: ProjMap2(FF2,n+p) is with_the_same_dom by A10;
A135: for i be Nat holds ProjMap2(FF2,n+p).i is nonnegative by A38;
x in dom((ProjMap2(FF2,n+p)).0) by A1,A10,A23,A96;
then (Partial_Sums ProjMap2(FF2,n+p))#x is non-decreasing by A134,A135
,Th38;
then ((Partial_Sums ProjMap2(FF2,n+p))#x).n9 <= ((Partial_Sums
ProjMap2(FF2,n+p))#x).(n9+p) by A133,RINFSUP2:7;
then
A136: ((Partial_Sums ProjMap2(FF2,n+p))#x).n9 <= ((Partial_Sums
ProjMap2(FF2,n+p)).(n+p)).x by MESFUNC5:def 13;
((P#x)^\n9).p = (P#x).(n+p) by NAT_1:def 3;
then ((P#x)^\n9).p = (P.(n+p)).x by MESFUNC5:def 13;
then
A137: ((P#x)^\n9).p = ((Partial_Sums ProjMap2(FF2,n+p)).(n+p)).x by A9;
(((ProjMap2(PP2,n))#x)^\n9).p = ((ProjMap2(PP2,n))#x).(n+p) by
NAT_1:def 3;
then (((ProjMap2(PP2,n))#x)^\n9).p = ((ProjMap2(PP2,n)).(n+p)).x by
MESFUNC5:def 13;
then (((ProjMap2(PP2,n))#x)^\n9).p = ((Partial_Sums ProjMap2(FF2,n+p)
).n).x by A98,A132;
hence thesis by A137,A136,MESFUNC5:def 13;
end;
((Partial_Sums F)#x).0 = ((Partial_Sums F).0).x by MESFUNC5:def 13;
then
A138: C[ 0 ] by A113,Def4;
A139: for k be Nat holds C[k] from NAT_1:sch 2(A138,A116);
(P#x)^\n9 is convergent by A97,RINFSUP2:21;
then lim(((ProjMap2(PP2,n))#x)^\n9) <= lim((P#x)^\n9) by A115,A131,
RINFSUP2:38;
then lim((ProjMap2(PP2,n))#x) <= lim (P#x) by A99,A114;
hence thesis by A139;
end;
F#x is summable by A1,A5,A23,A96;
then
A140: Partial_Sums(F#x) is convergent;
(Partial_Sums F)#x is convergent
proof
per cases by A140;
suppose
Partial_Sums(F#x) is convergent_to_finite_number;
then (Partial_Sums F)#x is convergent_to_finite_number by A2,A3,A23,A96
,Th33;
hence thesis;
end;
suppose
Partial_Sums(F#x) is convergent_to_+infty;
then (Partial_Sums F)#x is convergent_to_+infty by A2,A3,A23,A96,Th33;
hence thesis;
end;
suppose
Partial_Sums(F#x) is convergent_to_-infty;
then (Partial_Sums F)#x is convergent_to_-infty by A2,A3,A23,A96,Th33;
hence thesis;
end;
end;
then
A141: lim((Partial_Sums F)#x) <= lim(P#x) by A111,Th9;
A142: for k be Nat holds (P#x).k <= ((Partial_Sums F)#x).k
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A31,A96;
end;
(Partial_Sums F)#x is convergent by A3,A4,A23,A96,Th38;
then lim(P#x) <= lim((Partial_Sums F)#x) by A97,A142,RINFSUP2:38;
hence thesis by A141,XXREAL_0:1;
end;
A143: for x be Element of X st x in dom(lim(Partial_Sums F)) holds P#x is
convergent & lim(P#x) = (lim(Partial_Sums F)).x
proof
let x be Element of X;
assume
A144: x in dom(lim(Partial_Sums F));
then x in dom(lim P) by A1,A6,A22,A37;
hence P#x is convergent by A91;
lim(P#x) = lim((Partial_Sums F)#x) by A1,A23,A37,A93,A144;
hence thesis by A144,MESFUNC8:def 9;
end;
A145: for n be Nat holds P.n is nonnegative
proof
let n be Nat;
for k be Nat holds (ProjMap2(FF2,n)).k is nonnegative by A38;
then (Partial_Sums ProjMap2(FF2,n)).n is nonnegative by Th36;
hence thesis by A9;
end;
A146: for x be object st x in dom(lim(Partial_Sums F))
holds (lim(Partial_Sums F)).x >= 0
proof
let x be object;
assume
A147: x in dom(lim(Partial_Sums F));
then reconsider x1=x as Element of X;
A148: for n be Nat holds ((Partial_Sums F)#x1).n >= 0
proof
let n be Nat;
(Partial_Sums F).n is nonnegative by A4,Th36;
then ((Partial_Sums F).n).x1 >= 0 by SUPINF_2:51;
hence thesis by MESFUNC5:def 13;
end;
x in dom(F.0) by A67,A147,Def4;
then (Partial_Sums F)#x1 is convergent by A3,A4,Th38;
then lim((Partial_Sums F)#x1) >= 0 by A148,Th10;
hence thesis by A147,MESFUNC8:def 9;
end;
then
A149: lim(Partial_Sums F) is nonnegative by SUPINF_2:52;
consider I be ExtREAL_sequence such that
A150: for n be Nat holds I.n = Integral(M,F.n) & Integral(M,(
Partial_Sums F).n) = (Partial_Sums I).n by A1,A2,A3,A4,Th50;
for n be object st n in dom I holds 0 <= I.n
proof
let n be object;
assume n in dom I;
then reconsider n1 = n as Nat;
A151: F.n1 is nonnegative by A4;
A152: F.n1 is E-measurable by A4;
E = dom(F.n1) by A1,A3;
then 0 <= Integral(M,F.n1) by A151,A152,MESFUNC5:90;
hence thesis by A150;
end;
then I is nonnegative by SUPINF_2:52;
then
A153: Partial_Sums I is non-decreasing by Th16;
then
A154: Partial_Sums I is convergent by RINFSUP2:37;
deffunc J(Element of NAT) = integral'(M,P.$1);
consider J be sequence of ExtREAL such that
A155: for n be Element of NAT holds J.n = J(n) from FUNCT_2:sch 4;
reconsider J as ExtREAL_sequence;
A156: for n be Nat holds P.n is_simple_func_in S
proof
let n be Nat;
for m be Nat holds ProjMap2(FF2,n).m is_simple_func_in S by A10;
then (Partial_Sums ProjMap2(FF2,n)).n is_simple_func_in S by Th35;
hence thesis by A9;
end;
A157: for n be Nat holds J.n = integral'(M,P.n)
proof
let n be Nat;
reconsider n9=n as Element of NAT by ORDINAL1:def 12;
J.n = integral'(M,P.n9) by A155;
hence thesis;
end;
for n,m be Nat st m<=n holds J.m <= J.n
proof
let n,m be Nat;
A158: P.n is nonnegative by A145;
A159: P.m is_simple_func_in S by A156;
A160: for n,m,l be Nat holds dom(P.n - P.m) = dom(P.l)
proof
let n,m,l be Nat;
P.m is_simple_func_in S by A156;
then
A161: P.m is without+infty by MESFUNC5:14;
P.n is_simple_func_in S by A156;
then P.n is without-infty by MESFUNC5:14;
then dom(P.n - P.m) = dom(P.n) /\ dom(P.m) by A161,MESFUNC5:17;
then dom(P.n - P.m) = dom(lim(Partial_Sums F)) /\ dom(P.m) by A69;
then dom(P.n - P.m) = dom(lim(Partial_Sums F)) /\ dom(lim(Partial_Sums
F)) by A69;
hence thesis by A69;
end;
then
A162: dom(P.n - P.m) = dom(P.n);
then
A163: (P.n)|dom(P.n - P.m) = P.n;
assume
A164: m<=n;
A165: for x be object st x in dom(P.n - P.m) holds (P.m).x <= (P.n).x
proof
let x be object;
assume x in dom(P.n - P.m);
then x in dom(lim(Partial_Sums F)) by A69,A162;
hence thesis by A68,A85,A164;
end;
A166: P.m is nonnegative by A145;
dom(P.n - P.m) = dom(P.m) by A160;
then
A167: (P.m)|dom(P.n - P.m) = P.m;
P.n is_simple_func_in S by A156;
then integral'(M,(P.m)|dom(P.n - P.m)) <= integral'(M,(P.n)|dom(P.n - P.m
)) by A158,A159,A166,A165,MESFUNC5:70;
then J.m <= integral'(M,P.n) by A157,A167,A163;
hence thesis by A157;
end;
then J is non-decreasing by RINFSUP2:7;
then
A168: J is convergent by RINFSUP2:37;
A169: for n be Nat holds F.n is without-infty by A4,MESFUNC5:12;
then
A170: for n be Nat holds (Partial_Sums F).n is E-measurable by A4,Th41;
then lim(Partial_Sums F) is E-measurable by A1,A2,A3,A5,Th44;
then integral+(M,(lim(Partial_Sums F))) = lim J by A68,A156,A85,A157,A69,A143
,A145,A149,A168,MESFUNC5:def 15;
then
A171: Integral(M,(lim(Partial_Sums F))) = lim J by A1,A2,A3,A5,A170,A37,A149
,Th44,MESFUNC5:88;
A172: for n be Nat, x be Element of X st x in dom(F.n) holds (FF.n)#x is
non-decreasing
proof
let n be Nat, x be Element of X;
assume
A173: x in dom(F.n);
let i,j be ExtReal;
assume that
A174: i in dom((FF.n)#x) and
A175: j in dom((FF.n)#x) and
A176: i<=j;
reconsider i,j as Element of NAT by A174,A175;
((FF.n).i).x <= ((FF.n).j).x by A6,A173,A176;
then ((FF.n)#x).i <= ((FF.n).j).x by MESFUNC5:def 13;
hence thesis by MESFUNC5:def 13;
end;
A177: for n,p be Nat st p >= n holds for x be Element of X st x in E holds ((
Partial_Sums ProjMap2(FF2,p)).n).x <= (P.p).x & (P.p).x = ((Partial_Sums
ProjMap2(FF2,p)).p).x & ((Partial_Sums ProjMap2(FF2,p)).p).x <= ((Partial_Sums
F).p).x & ((Partial_Sums F).p).x <= (lim (Partial_Sums F)).x
proof
let n,p be Nat;
reconsider p1=p, n1=n as Element of NAT by ORDINAL1:def 12;
assume
A178: p >= n;
let x be Element of X;
A179: for i be Nat holds ProjMap2(FF2,p).i is nonnegative by A38;
assume
A180: x in E;
then
A181: x in dom((ProjMap2(FF2,p)).0) by A10;
ProjMap2(FF2,p) is with_the_same_dom by A10;
then (Partial_Sums ProjMap2(FF2,p))#x is non-decreasing by A181,A179,Th38;
then ((Partial_Sums ProjMap2(FF2,p))#x).n1 <= ((Partial_Sums ProjMap2(FF2
,p))#x).p1 by A178,RINFSUP2:7;
then ((Partial_Sums ProjMap2(FF2,p)).n).x <= ((Partial_Sums ProjMap2(FF2,
p))#x).p by MESFUNC5:def 13;
then ((Partial_Sums ProjMap2(FF2,p)).n).x <= ((Partial_Sums ProjMap2(FF2,
p)).p).x by MESFUNC5:def 13;
hence ((Partial_Sums ProjMap2(FF2,p)).n).x <= (P.p).x by A9;
thus (P.p).x = ((Partial_Sums ProjMap2(FF2,p)).p).x by A9;
A182: ProjMap2(FF2,p) is additive by A10;
A183: ProjMap2(FF2,p) is with_the_same_dom by A10;
A184: for n be Nat, x be Element of X st x in dom(ProjMap2(FF2,p).0) /\ dom
(F.0) holds (ProjMap2(FF2,p).n).x <= (F.n).x
proof
let n be Nat, x be Element of X;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
assume x in dom(ProjMap2(FF2,p).0) /\ dom(F.0);
then x in dom(F.0) by XBOOLE_0:def 4;
then
A185: x in dom(F.n) by A3;
then (FF.n)#x is non-decreasing by A172;
then lim((FF.n)#x) = sup((FF.n)#x) by RINFSUP2:37;
then ((FF.n)#x).p1 <= lim((FF.n)#x) by RINFSUP2:23;
then
A186: ((FF.n)#x).p <= (F.n).x by A6,A185;
((ProjMap2(FF2,p)).n).x = (FF2.(n1,p1)).x by Def9;
then ((ProjMap2(FF2,p)).n).x = ((FF.n).p).x by A8;
hence thesis by A186,MESFUNC5:def 13;
end;
x in dom(ProjMap2(FF2,p).0) /\ dom(F.0) by A1,A180,A181,XBOOLE_0:def 4;
hence
((Partial_Sums ProjMap2(FF2,p)).p).x <= ((Partial_Sums F).p).x by A2,A3
,A182,A183,A184,Th42;
(Partial_Sums F)#x is non-decreasing by A1,A3,A4,A180,Th38;
then lim((Partial_Sums F)#x) = sup((Partial_Sums F)#x) by RINFSUP2:37;
then ((Partial_Sums F)#x).p1 <= lim((Partial_Sums F)#x) by RINFSUP2:23;
then ((Partial_Sums F).p).x <= lim((Partial_Sums F)#x) by MESFUNC5:def 13;
hence thesis by A68,A180,MESFUNC8:def 9;
end;
for n be Nat holds (Partial_Sums I).n <= Integral(M,(lim(Partial_Sums F)))
proof
let n be Nat;
A187: (Partial_Sums F).n is nonnegative by A4,Th36;
A188: lim(Partial_Sums F) is E-measurable by A1,A2,A3,A5,A170,Th44;
A189: (Partial_Sums F).n is E-measurable by A4,A169,Th41;
A190: E = dom((Partial_Sums F).n) by A1,A2,A3,Th29;
then for x be Element of X st x in dom((Partial_Sums F).n) holds ((
Partial_Sums F).n).x <= (lim(Partial_Sums F)).x by A177;
then integral+(M,(Partial_Sums F).n) <= integral+(M,(lim(Partial_Sums F))
) by A37,A149,A190,A189,A188,A187,MESFUNC5:85;
then Integral(M,(Partial_Sums F).n) <= integral+(M,(lim(Partial_Sums F)))
by A170,A190,A187,MESFUNC5:88;
then Integral(M,(Partial_Sums F).n) <= Integral(M,(lim(Partial_Sums F)))
by A37,A146,A188,MESFUNC5:88,SUPINF_2:52;
hence thesis by A150;
end;
then
A191: lim(Partial_Sums I) <= Integral(M,(lim(Partial_Sums F))) by A153,Th9,
RINFSUP2:37;
take I;
thus for n be Nat holds I.n = Integral(M,(F.n)|E)
proof
let n be Nat;
dom(F.0) = dom(F.n) by A3;
then (F.n)|E = F.n by A1;
hence thesis by A150;
end;
A192: for n be Nat holds J.n = Integral(M,P.n)
proof
let n be Nat;
A193: P.n is nonnegative by A145;
A194: J.n = integral'(M,P.n) by A157;
P.n is_simple_func_in S by A156;
hence thesis by A193,A194,MESFUNC5:89;
end;
for n be Nat holds J.n <= (Partial_Sums I).n
proof
let n be Nat;
A195: P.n is E-measurable by A156,MESFUNC2:34;
A196: (Partial_Sums F).n is nonnegative by A4,Th36;
A197: n in NAT by ORDINAL1:def 12;
A198: for x be Element of X st x in dom(P.n) holds (P.n).x <= ((
Partial_Sums F).n).x
proof
let x be Element of X;
assume x in dom(P.n);
then x in dom(lim(Partial_Sums F)) by A69;
then (P#x).n <= ((Partial_Sums F)#x).n by A1,A23,A37,A31,A197;
then (P.n).x <= ((Partial_Sums F)#x).n by MESFUNC5:def 13;
hence thesis by MESFUNC5:def 13;
end;
A199: P.n is nonnegative by A145;
A200: dom(P.n) = E by A37,A69;
A201: E = dom((Partial_Sums F).n) by A1,A2,A3,Th29;
(Partial_Sums F).n is E-measurable by A4,A169,Th41;
then integral+(M,P.n) <= integral+(M,(Partial_Sums F).n) by A201,A200,A195
,A199,A196,A198,MESFUNC5:85;
then Integral(M,P.n) <= integral+(M,(Partial_Sums F).n) by A145,A200,A195,
MESFUNC5:88;
then Integral(M,P.n) <= Integral(M,(Partial_Sums F).n) by A170,A201,A196,
MESFUNC5:88;
then J.n <= Integral(M,(Partial_Sums F).n) by A192;
hence thesis by A150;
end;
then lim J <= lim (Partial_Sums I) by A168,A154,RINFSUP2:38;
then Sum I = Integral(M,(lim(Partial_Sums F))) by A171,A191,XXREAL_0:1;
hence thesis by A37,A154;
end;
theorem Th51:
E c= dom(F.0) & F is additive & F is with_the_same_dom & (for n
be Nat holds F.n is nonnegative & F.n is E-measurable) & (for x be
Element
of X st x in E holds F#x is summable) implies 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
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 nonnegative & F.n is E-measurable and
A5: for x be Element of X st x in E holds F#x is summable;
deffunc F(Nat) = (F.$1)|E;
consider G be Functional_Sequence of X,ExtREAL such that
A6: for n be Nat holds G.n = F(n) from SEQFUNC:sch 1;
reconsider G as additive with_the_same_dom Functional_Sequence of X,ExtREAL
by A2,A3,A6,Th18,Th31;
A7: for n be Nat holds G.n is nonnegative & G.n is E-measurable
proof
let n be Nat;
(F.n)|E is nonnegative by A4,MESFUNC5:15;
hence G.n is nonnegative by A6;
thus thesis by A1,A3,A4,A6,Th20;
end;
dom((F.0)|E) = E by A1,RELAT_1:62;
then
A8: E = dom(G.0) by A6;
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 n9 be object st n9 in NAT holds (F#x).n9 = (G#x).n9
proof
let n9 be object;
assume n9 in NAT;
then reconsider n = n9 as Nat;
dom(G.n) = E by A8,MESFUNC8:def 2;
then x in dom((F.n)|E) by A6,A10;
then ((F.n)|E).x = (F.n).x by FUNCT_1:47;
then
A11: (G.n).x = (F.n).x by A6;
(F#x).n = (F.n).x by MESFUNC5:def 13;
hence thesis by A11,MESFUNC5:def 13;
end;
hence thesis;
end;
A12: (lim(Partial_Sums G))|E = (lim(Partial_Sums F))|E
proof
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,Th29;
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 being Element of X;
set PFx = Partial_Sums(F#x);
set PGx = Partial_Sums(G#x);
assume
A16: x in dom(lim PG);
then
A17: x in E by A8,A13,Th29;
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 A8,A17,Th32;
PFx.n = (PF#x).n by A1,A2,A3,A17,Th32;
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 Th29;
then
A21: dom((lim PG)|E) = dom(lim PG) by A8,A13;
A22: dom((lim PF)|E) = E by A14,RELAT_1:62;
then
A23: dom((lim PG)|E) = dom((lim PF)|E) by A8,A20,A13;
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
A25: ((lim PF)|E).x = (lim PF).x by A23,FUNCT_1:47;
(lim PG).x = (lim PF).x by A21,A15,A24;
hence thesis by A24,A25,FUNCT_1:47;
end;
hence thesis by A8,A20,A13,A22,PARTFUN1:5;
end;
for x be Element of X st x in E holds G#x is summable by A1,A5,A6,Th21;
then consider I be ExtREAL_sequence such that
A26: for n be Nat holds I.n = Integral(M,(G.n)|E) and
A27: I is summable and
A28: Integral(M,(lim(Partial_Sums G))|E) = Sum I by A8,A7,Lm4;
take I;
now
let n be Nat;
((F.n)|E)|E = (F.n)|E;
then (G.n)|E = (F.n)|E by A6;
hence I.n = Integral(M,(F.n)|E) by A26;
end;
hence thesis by A27,A28,A12;
end;
:: Lebesgue Monotone Convergence Theorem
::$N Lebesgue's Monotone Convergence Theorem
theorem
E = dom(F.0) & F.0 is nonnegative & 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) implies 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
assume that
A1: E = dom(F.0) and
A2: F.0 is nonnegative 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;
A7: lim F is E-measurable by A1,A3,A4,A6,MESFUNC8:25;
A8: for n be Nat holds F.n is nonnegative
proof
let n be Nat;
for x be object st x in dom(F.n) holds 0 <= (F.n).x
proof
let x be object;
assume x in dom(F.n);
then x in E by A1,A3;
then (F.0).x <= (F.n).x by A5;
hence thesis by A2,SUPINF_2:51;
end;
hence thesis by SUPINF_2:52;
end;
per cases;
suppose
ex n be Nat st M.(E /\ eq_dom(F.n,+infty)) <> 0;
then consider N be Nat such that
A9: M.(E /\ eq_dom(F.N,+infty)) <> 0;
A10: E = dom(F.N) by A1,A3;
then reconsider EE = E /\ eq_dom(F.N,+infty) as Element of S by A4,
MESFUNC1:33;
A11: EE c= E by XBOOLE_1:17;
then
A12: F.N is EE-measurable by A4,MESFUNC1:30;
EE c= dom(F.N) by A1,A3,A11;
then
A13: EE = dom((F.N)|EE) by RELAT_1:62;
then EE = dom(F.N) /\ EE by RELAT_1:61;
then
A14: (F.N)|EE is EE-measurable by A12,MESFUNC5:42;
now
let x be object;
assume
A15: x in EE;
then x in eq_dom(F.N,+infty) by XBOOLE_0:def 4;
then (F.N).x = +infty by MESFUNC1:def 15;
then ((F.N)|EE).x = +infty by A13,A15,FUNCT_1:47;
hence x in eq_dom((F.N)|EE,+infty) by A13,A15,MESFUNC1:def 15;
end;
then
A16: EE c= eq_dom((F.N)|EE,+infty);
for x be object st x in eq_dom((F.N)|EE,+infty) holds x in EE by A13,
MESFUNC1:def 15;
then eq_dom((F.N)|EE,+infty) c= EE;
then EE = eq_dom((F.N)|EE,+infty) by A16,XBOOLE_0:def 10;
then
A17: M.(EE /\ eq_dom((F.N)|EE,+infty)) <> 0 by A9;
F.N is E-measurable by A4;
then
A18: Integral(M,(F.N)|EE) <= Integral(M,(F.N)|E) by A8,A10,A11,MESFUNC5:93;
reconsider N1 = N as Element of NAT by ORDINAL1:def 12;
deffunc I1(Element of NAT) = Integral(M,F.$1);
consider I be sequence of ExtREAL such that
A19: for n be Element of NAT holds I.n = I1(n) from FUNCT_2:sch 4;
reconsider I as ExtREAL_sequence;
A20: 0 < M.(E /\ eq_dom(F.N,+infty)) by A9,SUPINF_2:51;
A21: for n be Nat holds I.n = Integral(M,F.n)
proof
let n be Nat;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
I.n = Integral(M,F.n1) by A19;
hence thesis;
end;
take I;
A22: dom(lim F) = dom(F.0) by MESFUNC8:def 9;
for x be object st x in dom(lim F) holds (lim F).x >= 0
proof
let x be object;
assume
A23: x in dom(lim F);
then reconsider x1=x as Element of X;
for n be Nat holds (F#x1).n >= 0
proof
let n be Nat;
A24: (F.0).x1 >= 0 by A2,SUPINF_2:51;
(F.n).x1 >= (F.0).x1 by A1,A5,A22,A23;
hence thesis by A24,MESFUNC5:def 13;
end;
then lim(F#x1) >= 0 by A1,A6,A22,A23,Th10;
hence thesis by A23,MESFUNC8:def 9;
end;
then
A25: lim F is nonnegative by SUPINF_2:52;
A26: E = dom(lim F) by A1,MESFUNC8:def 9;
A27: EE c= E /\ eq_dom(lim F,+infty)
proof
let x be object;
assume
A28: x in EE;
then reconsider x1=x as Element of X;
x in eq_dom(F.N,+infty) by A28,XBOOLE_0:def 4;
then (F.N).x1 = +infty by MESFUNC1:def 15;
then
A29: (F#x1).N = +infty by MESFUNC5:def 13;
A30: x in E by A28,XBOOLE_0:def 4;
for n,m be Nat st m <= n holds (F#x1).m <= (F#x1).n
proof
let n,m be Nat;
assume m <= n;
then (F.m).x1 <= (F.n).x1 by A5,A30;
then (F#x1).m <= (F.n).x1 by MESFUNC5:def 13;
hence thesis by MESFUNC5:def 13;
end;
then
A31: (F#x1) is non-decreasing by RINFSUP2:7;
then
A32: (F#x1)^\N1 is non-decreasing by RINFSUP2:26;
((F#x1)^\N1).0 = (F#x1).(0+N) by NAT_1:def 3;
then for n be Element of NAT holds +infty <= ((F#x1)^\N1).n by A29,A32,
RINFSUP2:7;
then (F#x1)^\N1 is convergent_to_+infty by RINFSUP2:32;
then
A33: lim((F#x1)^\N1) = +infty by Th7;
A34: sup(F#x1) = sup((F#x1)^\N1) by A31,RINFSUP2:26;
lim(F#x1) = sup(F#x1) by A31,RINFSUP2:37;
then lim(F#x1) = +infty by A32,A34,A33,RINFSUP2:37;
then (lim F).x1 = +infty by A1,A22,A30,MESFUNC8:def 9;
then x in eq_dom(lim F,+infty) by A26,A30,MESFUNC1:def 15;
hence thesis by A30,XBOOLE_0:def 4;
end;
A35: for n,m be Nat st m<=n holds I.m<=I.n
proof
let n,m be Nat;
A36: F.m is E-measurable by A4;
assume m <= n;
then
A37: for x be Element of X st x in E holds (F.m).x <= (F.n).x by A5;
A38: E = dom(F.m) by A1,A3;
A39: E = dom(F.n) by A1,A3;
A40: n in NAT by ORDINAL1:def 12;
A41: m in NAT by ORDINAL1:def 12;
F.n is E-measurable by A4;
then Integral(M,(F.m)|E) <= Integral(M,(F.n)|E) by A8,A38,A39,A36,A37
,Th15;
then Integral(M,F.m) <= Integral(M,(F.n)|E) by A38;
then Integral(M,F.m) <= Integral(M,F.n) by A39;
then I.m <= Integral(M,F.n) by A19,A41;
hence thesis by A19,A40;
end;
then
A42: I is non-decreasing by RINFSUP2:7;
then
A43: I^\N1 is non-decreasing by RINFSUP2:26;
F.N is nonnegative by A8;
then Integral(M,(F.N)|EE) = +infty by A13,A14,A17,Th13,MESFUNC5:15;
then +infty <= Integral(M,F.N) by A10,A18;
then
A44: Integral(M,F.N) = +infty by XXREAL_0:4;
for k be Element of NAT holds +infty <= (I^\N1).k
proof
let k be Element of NAT;
I.N1 <= I.(N1+k) by A35,NAT_1:12;
then I.N1 <= (I^\N1).k by NAT_1:def 3;
hence thesis by A44,A21;
end;
then I^\N1 is convergent_to_+infty by RINFSUP2:32;
then
A45: lim(I^\N1) = +infty by Th7;
E /\ eq_dom(lim F,+infty) is Element of S by A7,A26,MESFUNC1:33;
then
A46: M.(E /\ eq_dom(lim F,+infty)) <> 0 by A27,A20,MEASURE1:31;
A47: sup I = sup(I^\N1) by A42,RINFSUP2:26;
lim I = sup I by A42,RINFSUP2:37;
then lim I = +infty by A43,A47,A45,RINFSUP2:37;
hence thesis by A7,A21,A42,A26,A25,A46,Th13,RINFSUP2:37;
end;
suppose
A48: for n be Nat holds M.(E /\ eq_dom(F.n,+infty)) = 0;
defpred L[Element of NAT,set] means $2 = E /\ eq_dom(F.$1,+infty);
A49: for n be Element of NAT ex A be Element of S st L[n,A]
proof
let n be Element of NAT;
E c= dom(F.n) by A1,A3;
then reconsider A = E /\ eq_dom(F.n,+infty) as Element of S by A4,
MESFUNC1:33;
take A;
thus thesis;
end;
consider L be sequence of S such that
A50: for n be Element of NAT holds L[n,L.n] from FUNCT_2:sch 3(A49);
A51: rng L c= S by RELAT_1:def 19;
rng L is N_Sub_set_fam of X by MEASURE1:23;
then reconsider E0 = rng L as N_Measure_fam of S by A51,MEASURE2:def 1;
set E1 = E\(union E0);
deffunc H(Nat) = (F.$1)|E1;
consider H be Functional_Sequence of X,ExtREAL such that
A52: for n be Nat holds H.n = H(n) from SEQFUNC:sch 1;
deffunc I2(Element of NAT) = Integral(M,(F.$1)|E1);
consider I be sequence of ExtREAL such that
A53: for n be Element of NAT holds I.n = I2(n) from FUNCT_2:sch 4;
reconsider I as ExtREAL_sequence;
A54: E1 c= E by XBOOLE_1:36;
then
A55: for n be Nat holds F.n is E1-measurable by A4,MESFUNC1:30;
A56: for n be Nat holds dom(H.n) = E1 & H.n is without-infty & H.n is
without+infty
proof
let n be Nat;
A57: dom(H.n) = dom((F.n)|E1) by A52;
E1 c= dom(F.n) by A1,A3,A54;
hence dom(H.n) = E1 by A57,RELAT_1:62;
(F.n)|E1 is nonnegative by A8,MESFUNC5:15;
then H.n is nonnegative by A52;
hence H.n is without-infty by MESFUNC5:12;
for x be set st x in dom(H.n) holds (H.n).x < +infty
proof
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
let x be set;
A58: L.n = E /\ eq_dom(F.n1,+infty) by A50;
dom L = NAT by FUNCT_2:def 1;
then
A59: L.n in rng L by A58,FUNCT_1:3;
assume x in dom(H.n);
then
A60: x in dom((F.n)|E1) by A52;
then
A61: x in E1 by RELAT_1:57;
A62: x in dom(F.n) by A60,RELAT_1:57;
assume
A63: (H.n).x >= +infty;
(H.n).x = ((F.n)|E1).x by A52;
then (H.n).x = (F.n).x by A61,FUNCT_1:49;
then (F.n).x = +infty by A63,XXREAL_0:4;
then x in eq_dom(F.n,+infty) by A62,MESFUNC1:def 15;
then x in L.n by A54,A61,A58,XBOOLE_0:def 4;
then x in union E0 by A59,TARSKI:def 4;
hence contradiction by A61,XBOOLE_0:def 5;
end;
hence thesis by MESFUNC5:11;
end;
for n,m be Nat holds dom(H.n) = dom(H.m)
proof
let n,m be Nat;
dom(H.n) = E1 by A56;
hence thesis by A56;
end;
then reconsider
H as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2;
defpred G[Nat,set,set] means $3 = H.($1+1) - H.($1);
A64: for n being Nat for x being set ex y being set st G[n,x,y ];
consider G being Function such that
A65: dom G = NAT & G.0 = H.0 & for n being Nat holds G[n,G
.n,G.(n+1)] from RECDEF_1:sch 1(A64);
A66: for n be Nat holds G.(n+1) = H.(n+1)-H.n
by A65;
now
defpred IND[Nat] means G.$1 is PartFunc of X,ExtREAL;
let f be object;
assume f in rng G;
then consider m be object such that
A67: m in dom G and
A68: f = G.m by FUNCT_1:def 3;
reconsider m as Nat by A65,A67;
A69: for n be Nat st IND[n] holds IND[n+1]
proof
let n be Nat;
assume IND[n];
G.(n+1) = H.(n+1) - H.n by A66;
hence thesis;
end;
A70: IND[ 0 ] by A65;
for n be Nat holds IND[n] from NAT_1:sch 2(A70,A69);
then G.m is PartFunc of X,ExtREAL;
hence f in PFuncs(X,ExtREAL) by A68,PARTFUN1:45;
end;
then rng G c= PFuncs(X,ExtREAL);
then reconsider G as Functional_Sequence of X,ExtREAL by A65,FUNCT_2:def 1
,RELSET_1:4;
A71: for n be Nat holds dom(G.n) = E1
proof
let n be Nat;
now
assume n <> 0;
then consider k be Nat such that
A72: n = k+1 by NAT_1:6;
A73: H.(k+1) is without-infty by A56;
A74: H.k is without+infty by A56;
G.(k+1) = H.(k+1) - H.k by A66;
then dom(G.(k+1)) = dom(H.(k+1)) /\ dom(H.k) by A73,A74,MESFUNC5:17;
then dom(G.(k+1)) = E1 /\ dom(H.k) by A56;
then dom(G.(k+1)) = E1 /\ E1 by A56;
hence thesis by A72;
end;
hence thesis by A56,A65;
end;
A75: for n,m be Nat holds dom(G.n) = dom(G.m)
proof
let n,m be Nat;
dom(G.n) = E1 by A71;
hence thesis by A71;
end;
A76: for n be Nat holds G.n is nonnegative
proof
let n be Nat;
A77: n <> 0 implies G.n is nonnegative
proof
assume n <> 0;
then consider k be Nat such that
A78: n = k + 1 by NAT_1:6;
A79: G.(k+1) = H.(k+1) - H.k by A66;
for x be object st x in dom(G.(k+1)) holds 0 <= (G.(k+1)).x
proof
let x be object;
assume
A80: x in dom(G.(k+1));
A81: dom(G.(k+1)) = E1 by A71;
(H.k).x = ((F.k)|E1).x by A52;
then
A82: (H.k).x = (F.k).x by A80,A81,FUNCT_1:49;
(H.(k+1)).x = ((F.(k+1))|E1).x by A52;
then
A83: (H.(k+1)).x = (F.(k+1)).x by A80,A81,FUNCT_1:49;
(F.k).x <= (F.(k+1)).x by A5,A54,A80,A81,NAT_1:11;
then (H.(k+1)).x - (H.k).x >= 0 by A83,A82,XXREAL_3:40;
hence thesis by A79,A80,MESFUNC1:def 4;
end;
hence thesis by A78,SUPINF_2:52;
end;
n = 0 implies G.n is nonnegative
proof
assume
A84: n = 0;
(F.n)|E1 is nonnegative by A8,MESFUNC5:15;
hence thesis by A52,A65,A84;
end;
hence thesis by A77;
end;
A85: for n1 be object st n1 in NAT holds H.n1 = (Partial_Sums G).n1
proof
defpred PH[Nat] means H.$1 = (Partial_Sums G).$1;
let n1 be object;
assume n1 in NAT;
then reconsider n = n1 as Nat;
A86: for k be Nat st PH[k] holds PH[k+1]
proof
let k be Nat;
A87: H.k is without+infty by A56;
A88: H.k is without-infty by A56;
A89: dom(G.(k+1)) = E1 by A71;
G.(k+1) is without-infty by A76,MESFUNC5:12;
then dom(G.(k+1) + H.k) = dom(G.(k+1)) /\ dom(H.k) by A88,MESFUNC5:16;
then dom(G.(k+1) + H.k) = E1 /\ E1 by A56,A89;
then
A90: dom(H.(k+1)) = dom(G.(k+1) + H.k) by A56;
A91: G.(k+1) = H.(k+1) - H.k by A66;
for x being Element of X st x in dom(H.(k+1)) holds (H.(k+1)).x
= (G.(k+1) + H.k).x
proof
let x be Element of X;
A92: (H.k).x <> +infty by A87;
(H.k).x <> -infty by A88;
then ( (H.(k+1)).x - (H.k).x ) + (H.k).x = (H.(k+1)).x - ( (H.k).x
- (H.k).x ) by A92,XXREAL_3:32;
then
( (H.(k+1)).x - (H.k).x ) + (H.k).x = (H.(k+1)).x - 0. by XXREAL_3:7;
then
A93: ( (H.(k+1)).x - (H.k).x ) + (H.k).x = (H.(k+1)).x by XXREAL_3:4;
assume
A94: x in dom(H.(k+1));
then x in E1 by A56;
then (H.(k+1)).x = (G.(k+1)).x + (H.k).x by A91,A89,A93,
MESFUNC1:def 4;
hence thesis by A90,A94,MESFUNC1:def 3;
end;
then
A95: H.(k+1) = G.(k+1) + H.k by A90,PARTFUN1:5;
assume PH[k];
hence thesis by A95,Def4;
end;
A96: PH[ 0 ] by A65,Def4;
for k be Nat holds PH[k] from NAT_1:sch 2(A96,A86);
then H.n = (Partial_Sums G).n;
hence thesis;
end;
then
A97: for n be Nat holds H.n = (Partial_Sums G).n & lim H = lim(
Partial_Sums G) by FUNCT_2:12;
reconsider G as with_the_same_dom Functional_Sequence of X,ExtREAL by A75,
MESFUNC8:def 2;
reconsider G as additive with_the_same_dom Functional_Sequence of X,
ExtREAL by A76,Th30;
A98: for k be Nat holds H.k is real-valued
proof
let k be Nat;
for x be Element of X st x in dom(H.k) holds |. (H.k).x .| < +infty
proof
let x be Element of X;
assume x in dom(H.k);
H.k is without+infty by A56;
then
A99: (H.k).x < +infty;
H.k is without-infty by A56;
then -infty < (H.k).x;
hence thesis by A99,EXTREAL1:40,XXREAL_0:4;
end;
hence thesis by MESFUNC2:def 1;
end;
A100: for n be Nat holds G.n is E1-measurable
proof
let n be Nat;
n <> 0 implies G.n is E1-measurable
proof
assume n <> 0;
then consider k be Nat such that
A101: n = k + 1 by NAT_1:6;
A102: E1 = dom(H.k) by A56;
A103: G.(k+1) = H.(k+1) - H.k by A66;
A104: H.k is real-valued by A98;
A105: H.k is E1-measurable by A1,A3,A55,A52,Th20,XBOOLE_1:36;
A106: H.(k+1) is real-valued by A98;
H.(k+1) is E1-measurable by A1,A3,A55,A52,Th20,XBOOLE_1:36;
hence thesis by A101,A105,A102,A106,A104,A103,MESFUNC2:11;
end;
hence thesis by A1,A3,A54,A55,A52,A65,Th20;
end;
A107: E1 = dom(G.0) by A56,A65;
for x be Element of X st x in E1 holds G#x is summable
proof
let x be Element of X;
assume
A108: x in E1;
E1 c= E by XBOOLE_1:36;
then F#x is convergent by A6,A108;
then H#x is convergent by A52,A108,Th12;
then (Partial_Sums G)#x is convergent by A85,FUNCT_2:12;
then Partial_Sums (G#x) is convergent by A107,A108,Th33;
hence thesis;
end;
then consider J be ExtREAL_sequence such that
A109: for n be Nat holds J.n = Integral(M,(G.n)|E1) and
J is summable and
A110: Integral(M,(lim(Partial_Sums G))|E1) = Sum J by A76,A107,A100,Th51;
for n be object st n in NAT holds I.n = (Partial_Sums J).n
proof
let n be object;
assume n in NAT;
then reconsider n1 = n as Element of NAT;
A111: for n be Nat holds J.n = Integral(M,G.n)
proof
let n be Nat;
dom(G.n) = E1 by A71;
then (G.n)|E1 = (G.n);
hence thesis by A109;
end;
E1 = dom(G.0) by A71;
then (Partial_Sums J).n1 = Integral(M,(Partial_Sums G).n1) by A76,A100
,A111,Th46;
then (Partial_Sums J).n1 = Integral(M,H.n1) by A85;
then (Partial_Sums J).n1 = Integral(M,(F.n1)|E1) by A52;
hence thesis by A53;
end;
then
A112: I = Partial_Sums J;
dom(lim(Partial_Sums G)) = dom(H.0) by A97,MESFUNC8:def 9;
then dom(lim(Partial_Sums G)) = E1 by A56;
then
A113: lim I = Integral(M,lim H) by A97,A110,A112;
take I;
A114: for x be Element of X st x in E1 holds F#x is convergent
proof
let x be Element of X;
A115: E1 c= E by XBOOLE_1:36;
assume x in E1;
hence thesis by A6,A115;
end;
A116: for n be Element of NAT st 0 <= n holds (M*L).n = 0
proof
let n be Element of NAT;
assume 0 <= n;
dom L = NAT by FUNCT_2:def 1;
then (M*L).n = M.(L.n) by FUNCT_1:13;
then (M*L).n = M.(E /\ eq_dom(F.n,+infty)) by A50;
hence thesis by A48;
end;
M*L is nonnegative by MEASURE2:1;
then SUM(M*L) = Ser(M*L).0 by A116,SUPINF_2:48;
then SUM(M*L) = (M*L).0 by SUPINF_2:def 11;
then SUM(M*L) = 0 by A116;
then M.(union E0) <= 0 by MEASURE2:11;
then
A117: M.(union E0) = 0 by SUPINF_2:51;
A118: for n be Nat holds I.n = Integral(M,F.n)
proof
let n be Nat;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
A119: I.n = Integral(M,(F.n1)|E1) by A53;
dom(F.n) = E by A1,A3;
hence thesis by A4,A117,A119,MESFUNC5:95;
end;
for n,m be Nat st m <= n holds I.m <= I.n
proof
let n,m be Nat;
A120: F.m is nonnegative by A8;
A121: dom(F.m) = E by A1,A3;
assume m <= n;
then
A122: for x be Element of X st x in dom(F.m) holds (F.m).x <= (F.n).x by A5
,A121;
A123: dom(F.n) = E by A1,A3;
A124: F.n is E-measurable by A4;
A125: F.n is nonnegative by A8;
F.m is E-measurable by A4;
then integral+(M,F.m) <= integral+(M,F.n) by A121,A123,A122,A120,A125
,A124,MESFUNC5:85;
then Integral(M,F.m) <= integral+(M,F.n) by A4,A121,A120,MESFUNC5:88;
then Integral(M,F.m) <= Integral(M,F.n) by A4,A123,A125,MESFUNC5:88;
then I.m <= Integral(M,F.n) by A118;
hence thesis by A118;
end;
then
A126: I is non-decreasing by RINFSUP2:7;
E = dom(lim F) by A1,MESFUNC8:def 9;
then
A127: Integral(M,lim F) = Integral(M,(lim F)|E1) by A7,A117,MESFUNC5:95;
E1 c= dom(F.0) by A1,XBOOLE_1:36;
hence thesis by A127,A52,A118,A126,A114,A113,Th19,RINFSUP2:37;
end;
end;