:: Fatou's Lemma and the {L}ebesgue's Convergence Theorem
:: by Noboru Endou , Keiko Narita and Yasunari Shidama
::
:: Received July 22, 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, MESFUNC8, SEQFUNC, MESFUNC5, SUBSET_1,
SUPINF_1, NAT_1, FUNCT_1, XXREAL_0, ORDINAL2, RELAT_1, XXREAL_2,
RINFSUP1, ARYTM_3, PBOOLE, PARTFUN1, PROB_1, MEASURE1, CARD_1, SUPINF_2,
MESFUNC1, VALUED_0, SEQ_2, ARYTM_1, TARSKI, REAL_1, INTEGRA5, VALUED_1,
COMPLEX1, RFUNCT_3, MESFUNC2, MESFUN10;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_3, EXTREAL1,
XCMPLX_0, XREAL_0, REAL_1, XXREAL_0, XXREAL_2, RELAT_1, FUNCT_1,
RELSET_1, DOMAIN_1, NAT_1, VALUED_0, FUNCT_2, PARTFUN1, PROB_1, SUPINF_1,
SUPINF_2, MEASURE1, MESFUNC1, MEASURE6, MESFUNC2, SEQFUNC, MESFUNC5,
MESFUNC8, RINFSUP2;
constructors REAL_1, DOMAIN_1, EXTREAL1, MESFUNC1, MEASURE6, MESFUNC2,
MESFUNC5, RINFSUP2, MESFUNC9, SUPINF_1, MESFUNC8, SEQFUNC, RELSET_1,
BINOP_2, NUMBERS;
registrations NAT_1, XREAL_0, MEMBERED, ORDINAL1, PARTFUN1, XBOOLE_0,
SUPINF_2, NUMBERS, XXREAL_0, MESFUNC8, RINFSUP2, VALUED_0, MEMBER_1,
RELSET_1, FUNCT_2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities RINFSUP2, XXREAL_3, MEMBER_1, SUPINF_2;
expansions MESFUNC1, MESFUNC5;
theorems TARSKI, PARTFUN1, FUNCT_1, SUPINF_2, EXTREAL1, MESFUNC1, XREAL_0,
XBOOLE_0, XBOOLE_1, MESFUNC2, XREAL_1, XXREAL_0, MESFUNC5, NAT_1,
RELAT_1, FUNCT_2, SEQFUNC, ORDINAL1, MESFUNC8, RINFSUP2, MESFUNC7,
MESFUNC9, NUMBERS, XXREAL_2, XXREAL_3;
schemes FUNCT_2, SEQFUNC, FUNCT_1;
begin :: Fatou's Lemma
reserve X for non empty set,
F for with_the_same_dom Functional_Sequence of X, ExtREAL,
seq,seq1,seq2 for ExtREAL_sequence,
x for Element of X,
a,r for R_eal,
n,m,k for Nat;
theorem Th1:
(for n be Nat holds seq1.n <= seq2.n) implies inf rng seq1 <= inf rng seq2
proof
assume
A1: for n be Nat holds seq1.n <= seq2.n;
now
let x be ExtReal;
A2: now
let n be Element of NAT;
dom seq1 = NAT by FUNCT_2:def 1;
then
A3: seq1.n in rng seq1 by FUNCT_1:def 3;
A4: seq1.n <= seq2.n by A1;
inf rng seq1 is LowerBound of rng seq1 by XXREAL_2:def 4;
then inf rng seq1 <= seq1.n by A3,XXREAL_2:def 2;
hence inf rng seq1 <= seq2.n by A4,XXREAL_0:2;
end;
assume x in rng seq2;
then ex z be object st z in dom seq2 & x=seq2.z by FUNCT_1:def 3;
hence inf rng seq1 <= x by A2;
end;
then inf rng seq1 is LowerBound of rng seq2 by XXREAL_2:def 2;
hence thesis by XXREAL_2:def 4;
end;
theorem Th2:
(for n be Nat holds seq1.n <= seq2.n) implies (
inferior_realsequence seq1).k <= (inferior_realsequence seq2).k & (
superior_realsequence seq1).k <= (superior_realsequence seq2).k
proof
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
assume
A1: for n be Nat holds seq1.n <= seq2.n;
A2: now
let n be Nat;
A3: (seq2^\k1).n = seq2.(n+k) by NAT_1:def 3;
(seq1^\k1).n = seq1.(n+k) by NAT_1:def 3;
hence (seq1^\k1).n <= (seq2^\k1).n by A1,A3;
end;
then sup(seq1^\k1) <= sup(seq2^\k1) by MESFUNC5:55;
then
A4: (superior_realsequence seq1).k <= sup(seq2^\k1) by RINFSUP2:27;
inf(seq1^\k1) <= inf(seq2^\k1) by A2,Th1;
then (inferior_realsequence seq1).k <= inf(seq2^\k1) by RINFSUP2:27;
hence thesis by A4,RINFSUP2:27;
end;
theorem Th3:
(for n be Nat holds seq1.n <= seq2.n) implies lim_inf seq1 <=
lim_inf seq2 & lim_sup seq1 <= lim_sup seq2
proof
assume for n be Nat holds seq1.n <= seq2.n;
then for n be Nat holds (inferior_realsequence seq1).n <= (
inferior_realsequence seq2).n & (superior_realsequence seq1).n <= (
superior_realsequence seq2).n by Th2;
hence thesis by Th1,MESFUNC5:55;
end;
theorem Th4:
(for n be Nat holds seq.n >= a) implies inf seq >= a
proof
assume
A1: for n be Nat holds seq.n >= a;
now
let x be ExtReal;
assume x in rng seq;
then ex z be object st z in dom seq & x = seq.z by FUNCT_1:def 3;
hence x >= a by A1;
end;
then a is LowerBound of rng seq by XXREAL_2:def 2;
hence thesis by XXREAL_2:def 4;
end;
theorem Th5:
(for n be Nat holds seq.n <= a) implies sup seq <= a
proof
assume
A1: for n be Nat holds seq.n <= a;
now
let x be ExtReal;
assume x in rng seq;
then ex z be object st z in dom seq & x = seq.z by FUNCT_1:def 3;
hence x <= a by A1;
end;
then a is UpperBound of rng seq by XXREAL_2:def 1;
hence thesis by XXREAL_2:def 3;
end;
theorem Th6:
for n be Element of NAT st x in dom inf(F^\n) holds (inf(F^\n)).x
=inf((F#x)^\n)
proof
let n be Element of NAT;
now
reconsider g=F as sequence of PFuncs(X,ExtREAL);
let k be Element of NAT;
((F^\n)#x).k =((F^\n).k).x by MESFUNC5:def 13;
then ((F^\n)#x).k = (g.(n+k)).x by NAT_1:def 3;
then ((F^\n)#x).k =(F#x).(n+k) by MESFUNC5:def 13;
hence ((F^\n)#x).k = ((F#x)^\n).k by NAT_1:def 3;
end;
then
A1: (F^\n)#x = (F#x)^\n by FUNCT_2:63;
assume x in dom inf(F^\n);
hence thesis by A1,MESFUNC8:def 3;
end;
reserve S for SigmaField of X,
M for sigma_Measure of S,
E for Element of S;
::$N Fatou's Lemma
theorem Th7:
E = dom(F.0) & (for n holds F.n is nonnegative & F.n
is E-measurable) implies ex I be ExtREAL_sequence st (for n holds I.n =
Integral(M,F.n)) & Integral(M,lim_inf F) <= lim_inf I
proof
assume that
A1: E = dom(F.0) and
A2: for n holds F.n is nonnegative & F.n is E-measurable;
set H = inferior_realsequence F;
deffunc G(Element of NAT) = inf(F^\$1);
consider G be Function such that
A3: dom G = NAT & for n be Element of NAT holds G.n = G(n) from FUNCT_1:
sch 4;
now
let n be Nat;
n in NAT by ORDINAL1:def 12;
then G.n = inf(F^\n) by A3;
hence G.n is PartFunc of X,ExtREAL;
end;
then reconsider G as Functional_Sequence of X,ExtREAL by A3,SEQFUNC:1;
A4: for n be Element of NAT holds G.n = (inferior_realsequence F).n
proof
let n be Element of NAT;
(inferior_realsequence F).n = inf(F^\n) by MESFUNC8:8;
hence thesis by A3;
end;
then
A5: G = inferior_realsequence F by FUNCT_2:63;
reconsider G as with_the_same_dom Functional_Sequence of X,ExtREAL by A4,
FUNCT_2:63;
A6: dom(H.0) = dom(G.0) by A4;
A7: for n,m be Nat, x be Element of X st n <= m & x in E holds (G.n).x <= (G
.m).x & (G#x).n <= (G#x).m
proof
let n,m be Nat, x be Element of X;
reconsider n1=n, m1=m as Element of NAT by ORDINAL1:def 12;
assume that
A8: n <= m and
A9: x in E;
H#x = inferior_realsequence(F#x) by A1,A9,MESFUNC8:7;
then (H#x).n1 <= (H#x).m1 by A8,RINFSUP2:7;
then (H.n).x <= (H#x).m by MESFUNC5:def 13;
hence (G.n).x <= (G.m).x by A5,MESFUNC5:def 13;
then (G#x).n <= (G.m).x by MESFUNC5:def 13;
hence thesis by MESFUNC5:def 13;
end;
A10: now
let x be Element of X;
assume x in E;
then
for n,m be Nat st m <= n holds (G#x).m <= (G#x).n by A7;
then G#x is non-decreasing by RINFSUP2:7;
hence G#x is convergent by RINFSUP2:37;
end;
deffunc I(Element of NAT) = Integral(M,F.$1);
consider I be sequence of ExtREAL such that
A11: for n be Element of NAT holds I.n = I(n) from FUNCT_2:sch 4;
A12: for n be Nat holds G.n is E-measurable by A1,A2,A5,MESFUNC8:20;
A13: dom(H.0) = dom(F.0) by MESFUNC8:def 5;
then
A14: dom lim G = E by A1,A6,MESFUNC8:def 9;
for x be object st x in dom(G.0) holds 0 <= (G.0).x
proof
let x be object;
assume
A15: x in dom(G.0);
then reconsider x as Element of X;
A16: now
let n be Nat;
F.n is nonnegative by A2;
then 0 <= (F.n).x by SUPINF_2:51;
then 0 <= (F#x).(0+n) by MESFUNC5:def 13;
hence 0. <= ((F#x)^\0).n by NAT_1:def 3;
end;
(F^\0).0 = F.(0+0) by NAT_1:def 3;
then dom inf(F^\0) = dom(F.0) by MESFUNC8:def 3;
then (inf(F^\0)).x =inf((F#x)^\0) by A13,A6,A15,Th6;
then (G.0).x = inf((F#x)^\0) by A3;
hence thesis by A16,Th4;
end;
then
A17: G.0 is nonnegative by SUPINF_2:52;
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 A7;
then consider J be ExtREAL_sequence such that
A18: for n be Nat holds J.n = Integral(M,G.n) and
A19: J is convergent and
A20: Integral(M,lim G) = lim J by A1,A13,A6,A17,A12,A10,MESFUNC9:52;
reconsider I as ExtREAL_sequence;
for n be Nat holds J.n <= I.n
proof
let n be Nat;
A21: dom(F.n) = E by A1,MESFUNC8:def 2;
A22: F.n is nonnegative by A2;
A23: n is Element of NAT by ORDINAL1:def 12;
A24: now
let x be Element of X;
assume
A25: x in dom(G.n);
(inferior_realsequence(F#x)).n <= (F#x).n by RINFSUP2:8;
then (H.n).x <= (F#x).n by A5,A25,MESFUNC8:def 5;
then (H.n).x <= (F.n).x by MESFUNC5:def 13;
hence (G.n).x <= (F.n).x by A4,A23;
end;
A26: F.n is E-measurable by A2;
A27: G.n is E-measurable by A1,A2,A5,MESFUNC8:20;
A28: dom(G.n) = E by A1,A13,A6,MESFUNC8:def 2;
A29: now
let x be object;
assume
A30: x in dom(G.n);
0 <= (G.0).x by A17,SUPINF_2:51;
hence 0 <= (G.n).x by A7,A28,A30;
end;
then G.n is nonnegative by SUPINF_2:52;
then integral+(M,G.n) <= integral+(M,F.n) by A21,A28,A26,A27,A22,A24,
MESFUNC5:85;
then Integral(M,G.n) <= integral+(M,F.n) by A28,A27,A29,MESFUNC5:88
,SUPINF_2:52;
then
A31: Integral(M,G.n) <= Integral(M,F.n) by A21,A26,A22,MESFUNC5:88;
I.n = Integral(M,F.n) by A11,A23;
hence thesis by A18,A31;
end;
then lim_inf J <= lim_inf I by Th3;
then
A32: lim J <= lim_inf I by A19,RINFSUP2:41;
A33: dom sup G = E by A1,A13,A6,MESFUNC8:def 4;
now
let x be Element of X;
assume
A34: x in dom lim G;
then
for n,m be Nat st m <= n holds (G#x).m <= (G#x).n by A7,A14;
then G#x is non-decreasing by RINFSUP2:7;
then
A35: lim(G#x) = sup(G#x) by RINFSUP2:37;
(sup G).x = sup(G#x) by A14,A33,A34,MESFUNC8:def 4;
hence (lim G).x = (sup G).x by A34,A35,MESFUNC8:def 9;
end;
then
A36: lim G = sup G by A14,A33,PARTFUN1:5;
take I;
for n be Nat holds I.n = Integral(M,F.n)
proof
let n be Nat;
n is Element of NAT by ORDINAL1:def 12;
hence thesis by A11;
end;
hence thesis by A5,A20,A36,A32,MESFUNC8:11;
end;
begin :: Lebesgue's Convergence Theorem
theorem Th8:
for Y being non empty Subset of ExtREAL, r be R_eal st r in REAL
holds sup({r} + Y) = sup {r} + sup Y
proof
let Y be non empty Subset of ExtREAL;
let r be R_eal;
set X = {r};
assume
A1: r in REAL;
set W = X+Y;
A2: -r <> -infty by A1,XXREAL_3:23;
A3: -r <> +infty by A1,XXREAL_3:23;
now
let z be object;
assume z in -X + W;
then consider x,y be R_eal such that
A4: z = x + y and
A5: x in -X and
A6: y in W;
consider x1,y1 be R_eal such that
A7: y = x1 + y1 and
A8: x1 in X and
A9: y1 in Y by A6;
-x in --X by A5;
then -x in X;
then -x = r by TARSKI:def 1;
then z = -r + (r + y1) by A4,A8,A7,TARSKI:def 1;
then z = (-r + r) + y1 by A1,A3,A2,XXREAL_3:29;
then z = 0. + y1 by XXREAL_3:7;
hence z in Y by A9,XXREAL_3:4;
end;
then
A10: -X + W c= Y by TARSKI:def 3;
A11: r in X by TARSKI:def 1;
now
let z be object;
assume
A12: z in Y;
then reconsider y = z as Element of ExtREAL;
r + y - r = (-r + r) + y by A1,A3,A2,XXREAL_3:29;
then r + y - r = 0. + y by XXREAL_3:7;
then
A13: y = r + y - r by XXREAL_3:4;
A14: -r in -X by A11;
r + y in W by A11,A12;
hence z in -X + W by A14,A13;
end;
then Y c= -X + W by TARSKI:def 3;
then Y = -X + W by A10,XBOOLE_0:def 10;
then sup Y <= sup W + sup -X by SUPINF_2:8;
then sup Y <= sup(X+Y) + -inf X by SUPINF_2:15;
then sup Y <= sup(X+Y) -r by XXREAL_2:13;
then r + sup Y <= sup(X+Y) by A1,XXREAL_3:57;
then
A15: sup X + sup Y <= sup(X+Y) by XXREAL_2:11;
sup(X + Y) <= sup X + sup Y by SUPINF_2:8;
hence thesis by A15,XXREAL_0:1;
end;
theorem Th9:
for Y being non empty Subset of ExtREAL, r be R_eal st r in REAL
holds inf({r} + Y) = inf {r} + inf Y
proof
let Y be non empty Subset of ExtREAL;
let r be R_eal;
set X = {r};
assume
A1: r in REAL;
set W = X+Y;
set Z = -X;
A2: -r <> -infty by A1,XXREAL_3:23;
A3: -r <> +infty by A1,XXREAL_3:23;
now
let z be object;
assume z in Z + W;
then consider x,y be R_eal such that
A4: z = x + y and
A5: x in Z and
A6: y in W;
consider x1,y1 be R_eal such that
A7: y = x1 + y1 and
A8: x1 in X and
A9: y1 in Y by A6;
-x in -Z by A5;
then -x in X;
then -x = r by TARSKI:def 1;
then z = -r + (r + y1) by A4,A8,A7,TARSKI:def 1;
then z = (-r + r) + y1 by A1,A3,A2,XXREAL_3:29;
then z = 0. + y1 by XXREAL_3:7;
hence z in Y by A9,XXREAL_3:4;
end;
then
A10: Z + W c= Y by TARSKI:def 3;
A11: r in X by TARSKI:def 1;
now
let z be object;
assume
A12: z in Y;
then reconsider y = z as Element of ExtREAL;
r + y - r = (-r + r) + y by A1,A3,A2,XXREAL_3:29;
then r + y - r = 0. + y by XXREAL_3:7;
then
A13: y = r + y - r by XXREAL_3:4;
A14: -r in Z by A11;
r + y in W by A11,A12;
hence z in Z + W by A14,A13;
end;
then Y c= Z + W by TARSKI:def 3;
then Y = Z + W by A10,XBOOLE_0:def 10;
then inf Y >= inf W + inf Z by SUPINF_2:9;
then inf Y >= inf(X+Y) + -sup X by SUPINF_2:14;
then inf Y >= inf(X+Y) -r by XXREAL_2:11;
then r + inf Y >= inf(X+Y) by A1,XXREAL_3:52;
then
A15: inf X + inf Y >= inf(X+Y) by XXREAL_2:13;
inf(X + Y) >= inf X + inf Y by SUPINF_2:9;
hence thesis by A15,XXREAL_0:1;
end;
theorem Th10:
r in REAL & (for n be Nat holds seq1.n = r + seq2.n) implies
lim_inf seq1 = r + lim_inf seq2 & lim_sup seq1 = r + lim_sup seq2
proof
assume that
A1: r in REAL and
A2: for n be Nat holds seq1.n = r + seq2.n;
reconsider R1 = rng inferior_realsequence seq1, R2 = rng
inferior_realsequence seq2, P1 = rng superior_realsequence seq1, P2 = rng
superior_realsequence seq2 as non empty Subset of ExtREAL;
now
let z be object;
assume z in {r} + R2;
then consider z2,z3 be R_eal such that
A3: z = z2 + z3 and
A4: z2 in {r} and
A5: z3 in R2;
consider n be object such that
A6: n in NAT and
A7: (inferior_realsequence seq2).n = z3 by A5,FUNCT_2:11;
reconsider n as Element of NAT by A6;
consider Y2 be non empty Subset of ExtREAL such that
A8: Y2 = {seq2.k where k is Nat: n <= k} and
A9: z3 = inf Y2 by A7,RINFSUP2:def 6;
consider Y1 be non empty Subset of ExtREAL such that
A10: Y1 = {seq1.k where k is Nat : n <= k} and
A11: (inferior_realsequence seq1).n = inf Y1 by RINFSUP2:def 6;
now
let w be object;
A12: r in {r} by TARSKI:def 1;
assume w in Y1;
then consider k1 be Nat such that
A13: w = seq1.k1 and
A14: n <= k1 by A10;
reconsider w1=w as R_eal by A13;
A15: seq2.k1 in Y2 by A8,A14;
w1 = r + seq2.k1 by A2,A13;
hence w in {r} + Y2 by A12,A15;
end;
then
A16: Y1 c= {r} + Y2 by TARSKI:def 3;
now
let w be object;
assume w in {r} + Y2;
then consider w1,w2 be R_eal such that
A17: w = w1 + w2 and
A18: w1 in {r} and
A19: w2 in Y2;
consider k2 be Nat such that
A20: w2 = seq2.k2 and
A21: n <= k2 by A8,A19;
w1 = r by A18,TARSKI:def 1;
then w = seq1.k2 by A2,A17,A20;
hence w in Y1 by A10,A21;
end;
then {r} + Y2 c= Y1 by TARSKI:def 3;
then Y1 = {r} + Y2 by A16,XBOOLE_0:def 10;
then inf Y1 = inf{r} + inf Y2 by A1,Th9;
then inf Y1 = r + inf Y2 by XXREAL_2:13;
then z = (inferior_realsequence seq1).n by A4,A3,A9,A11,TARSKI:def 1;
hence z in R1 by FUNCT_2:4;
end;
then
A22: {r} + R2 c= R1 by TARSKI:def 3;
now
let z be object;
assume z in {r} + P2;
then consider z2,z3 be R_eal such that
A23: z = z2 + z3 and
A24: z2 in {r} and
A25: z3 in P2;
consider n be object such that
A26: n in NAT and
A27: (superior_realsequence seq2).n = z3 by A25,FUNCT_2:11;
reconsider n as Element of NAT by A26;
consider Y2 be non empty Subset of ExtREAL such that
A28: Y2 = {seq2.k where k is Nat : n <= k} and
A29: z3 = sup Y2 by A27,RINFSUP2:def 7;
consider Y1 be non empty Subset of ExtREAL such that
A30: Y1 = {seq1.k where k is Nat : n <= k} and
A31: (superior_realsequence seq1).n = sup Y1 by RINFSUP2:def 7;
now
let w be object;
A32: r in {r} by TARSKI:def 1;
assume w in Y1;
then consider k1 be Nat such that
A33: w = seq1.k1 and
A34: n <= k1 by A30;
reconsider w1=w as R_eal by A33;
A35: seq2.k1 in Y2 by A28,A34;
w1 = r + seq2.k1 by A2,A33;
hence w in {r} + Y2 by A32,A35;
end;
then
A36: Y1 c= {r} + Y2 by TARSKI:def 3;
now
let w be object;
assume w in {r} + Y2;
then consider w1,w2 be R_eal such that
A37: w = w1 + w2 and
A38: w1 in {r} and
A39: w2 in Y2;
consider k2 be Nat such that
A40: w2 = seq2.k2 and
A41: n <= k2 by A28,A39;
w1 = r by A38,TARSKI:def 1;
then w = seq1.k2 by A2,A37,A40;
hence w in Y1 by A30,A41;
end;
then {r} + Y2 c= Y1 by TARSKI:def 3;
then Y1 = {r} + Y2 by A36,XBOOLE_0:def 10;
then sup Y1 = sup{r} + sup Y2 by A1,Th8;
then sup Y1 = r + sup Y2 by XXREAL_2:11;
then z = (superior_realsequence seq1).n by A24,A23,A29,A31,TARSKI:def 1;
hence z in P1 by FUNCT_2:4;
end;
then
A42: {r} + P2 c= P1 by TARSKI:def 3;
now
let z be object;
assume z in R1;
then consider n be object such that
A43: n in NAT and
A44: (inferior_realsequence seq1).n = z by FUNCT_2:11;
reconsider n as Element of NAT by A43;
consider Y1 be non empty Subset of ExtREAL such that
A45: Y1 = {seq1.k where k is Nat : n <= k} and
A46: z = inf Y1 by A44,RINFSUP2:def 6;
consider Y2 be non empty Subset of ExtREAL such that
A47: Y2 = {seq2.k where k is Nat : n <= k} and
A48: (inferior_realsequence seq2).n = inf Y2 by RINFSUP2:def 6;
now
let w be object;
A49: r in {r} by TARSKI:def 1;
assume w in Y1;
then consider k1 be Nat such that
A50: w = seq1.k1 and
A51: n <= k1 by A45;
reconsider w1=w as R_eal by A50;
A52: seq2.k1 in Y2 by A47,A51;
w1 = r + seq2.k1 by A2,A50;
hence w in {r} + Y2 by A49,A52;
end;
then
A53: Y1 c= {r} + Y2 by TARSKI:def 3;
now
let w be object;
assume w in {r} + Y2;
then consider w1,w2 be R_eal such that
A54: w = w1 + w2 and
A55: w1 in {r} and
A56: w2 in Y2;
consider k2 be Nat such that
A57: w2 = seq2.k2 and
A58: n <= k2 by A47,A56;
w1 = r by A55,TARSKI:def 1;
then w = seq1.k2 by A2,A54,A57;
hence w in Y1 by A45,A58;
end;
then {r} + Y2 c= Y1 by TARSKI:def 3;
then Y1 = {r} + Y2 by A53,XBOOLE_0:def 10;
then inf Y1 = inf{r} + inf Y2 by A1,Th9;
then
A59: inf Y1 = r + inf Y2 by XXREAL_2:13;
A60: (inferior_realsequence seq2).n in R2 by FUNCT_2:4;
r in {r} by TARSKI:def 1;
hence z in {r} + R2 by A46,A48,A59,A60;
end;
then R1 c= {r} + R2 by TARSKI:def 3;
then R1 = {r} + R2 by A22,XBOOLE_0:def 10;
then sup R1 = sup {r} + sup R2 by A1,Th8;
hence lim_inf seq1 = r + lim_inf seq2 by XXREAL_2:11;
now
let z be object;
assume z in P1;
then consider n be object such that
A61: n in NAT and
A62: (superior_realsequence seq1).n = z by FUNCT_2:11;
reconsider n as Element of NAT by A61;
consider Y1 be non empty Subset of ExtREAL such that
A63: Y1 = {seq1.k where k is Nat : n <= k} and
A64: z = sup Y1 by A62,RINFSUP2:def 7;
consider Y2 be non empty Subset of ExtREAL such that
A65: Y2 = {seq2.k where k is Nat : n <= k} and
A66: (superior_realsequence seq2).n = sup Y2 by RINFSUP2:def 7;
now
let w be object;
A67: r in {r} by TARSKI:def 1;
assume w in Y1;
then consider k1 be Nat such that
A68: w = seq1.k1 and
A69: n <= k1 by A63;
reconsider w1=w as R_eal by A68;
A70: seq2.k1 in Y2 by A65,A69;
w1 = r + seq2.k1 by A2,A68;
hence w in {r} + Y2 by A67,A70;
end;
then
A71: Y1 c= {r} + Y2 by TARSKI:def 3;
now
let w be object;
assume w in {r} + Y2;
then consider w1,w2 be R_eal such that
A72: w = w1 + w2 and
A73: w1 in {r} and
A74: w2 in Y2;
consider k2 be Nat such that
A75: w2 = seq2.k2 and
A76: n <= k2 by A65,A74;
w1 = r by A73,TARSKI:def 1;
then w = seq1.k2 by A2,A72,A75;
hence w in Y1 by A63,A76;
end;
then {r} + Y2 c= Y1 by TARSKI:def 3;
then Y1 = {r} + Y2 by A71,XBOOLE_0:def 10;
then sup Y1 = sup{r} + sup Y2 by A1,Th8;
then
A77: sup Y1 = r + sup Y2 by XXREAL_2:11;
A78: (superior_realsequence seq2).n in P2 by FUNCT_2:4;
r in {r} by TARSKI:def 1;
hence z in {r} + P2 by A64,A66,A77,A78;
end;
then P1 c= {r} + P2 by TARSKI:def 3;
then P1 = {r} + P2 by A42,XBOOLE_0:def 10;
then inf P1 = inf{r} + inf P2 by A1,Th9;
hence thesis by XXREAL_2:13;
end;
reserve F1,F2 for Functional_Sequence of X,ExtREAL,
f,g,P for PartFunc of X, ExtREAL;
theorem Th11:
dom(F1.0) = dom(F2.0) & F1 is with_the_same_dom & f"{+infty} =
{} & f"{-infty} = {} & (for n be Nat holds F1.n = f + F2.n) implies lim_inf F1
= f + lim_inf F2 & lim_sup F1 = f + lim_sup F2
proof
assume that
A1: dom(F1.0) = dom(F2.0) and
A2: F1 is with_the_same_dom and
A3: f"{+infty} = {} and
A4: f"{-infty} = {} and
A5: for n be Nat holds F1.n = f + F2.n;
A6: F1.0 = f + F2.0 by A5;
A7: dom(f + F2.0) = (dom f /\ dom(F2.0))\((f"{-infty} /\ (F2.0)"{+infty}) \/
(f"{+infty} /\ (F2.0)"{-infty})) by MESFUNC1:def 3;
A8: dom(f + lim_sup F2) = (dom f /\ dom(lim_sup F2))\((f"{-infty} /\ (
lim_sup F2)"{+infty}) \/ (f"{+infty} /\ (lim_sup F2)"{-infty})) by
MESFUNC1:def 3;
then
A9: dom(f + lim_sup F2) = dom f /\ dom(F2.0) by A3,A4,MESFUNC8:def 8;
then
A10: dom(lim_sup F1) = dom(f + lim_sup F2) by A3,A4,A6,A7,MESFUNC8:def 8;
A11: dom(f + lim_inf F2) = (dom f /\ dom(lim_inf F2))\((f"{-infty} /\ (
lim_inf F2)"{+infty}) \/ (f"{+infty} /\ (lim_inf F2)"{-infty})) by
MESFUNC1:def 3;
then
A12: dom(f + lim_inf F2) = dom f /\ dom(F2.0) by A3,A4,MESFUNC8:def 7;
then
A13: dom(lim_inf F1) = dom(f + lim_inf F2) by A3,A4,A6,A7,MESFUNC8:def 7;
A14: dom(lim_inf F2) = dom(F2.0) by MESFUNC8:def 7;
A15: dom(lim_inf F1) = dom(F1.0) by MESFUNC8:def 7;
for x be Element of X st x in dom(lim_inf F1) holds (lim_inf F1).x = (f
+ lim_inf F2).x
proof
let x be Element of X;
assume
A16: x in dom(lim_inf F1);
then
A17: (lim_inf F1).x = lim_inf(F1#x) by MESFUNC8:def 7;
A18: for n be Nat holds (F1#x).n = f.x + (F2#x).n
proof
let n be Nat;
F1.n = f + F2.n by A5;
then dom(f + F2.n) = dom(F1.0) by A2,MESFUNC8:def 2;
then
A19: x in dom(f + F2.n) by A16,MESFUNC8:def 7;
(F1.n).x = (f + F2.n).x by A5;
then (F1.n).x = f.x + (F2.n).x by A19,MESFUNC1:def 3;
then (F1#x).n = f.x + (F2.n).x by MESFUNC5:def 13;
hence thesis by MESFUNC5:def 13;
end;
A20: dom(f + lim_inf F2) c= dom f by A3,A4,A11,XBOOLE_1:17;
then not f.x in {-infty} by A4,A13,A16,FUNCT_1:def 7;
then
A21: f.x <> -infty by TARSKI:def 1;
not f.x in {+infty} by A3,A13,A16,A20,FUNCT_1:def 7;
then f.x <> +infty by TARSKI:def 1;
then
A22: f.x in REAL by A21,XXREAL_0:14;
x in dom(f + lim_inf F2) by A3,A4,A6,A7,A12,A16,MESFUNC8:def 7;
then
A23: (f + lim_inf F2).x = f.x + (lim_inf F2).x by MESFUNC1:def 3;
(lim_inf F2).x = lim_inf(F2#x) by A1,A15,A14,A16,MESFUNC8:def 7;
hence thesis by A22,A18,A17,A23,Th10;
end;
hence lim_inf F1 = f + lim_inf F2 by A13,PARTFUN1:5;
A24: dom(lim_sup F1) = dom(F1.0) by MESFUNC8:def 8;
A25: dom(lim_sup F2) = dom(F2.0) by MESFUNC8:def 8;
for x be Element of X st x in dom(lim_sup F1) holds (lim_sup F1).x = (f
+ lim_sup F2).x
proof
let x be Element of X;
assume
A26: x in dom(lim_sup F1);
then
A27: (lim_sup F1).x = lim_sup(F1#x) by MESFUNC8:def 8;
A28: for n be Nat holds (F1#x).n = f.x + (F2#x).n
proof
let n be Nat;
F1.n = f + F2.n by A5;
then
A29: dom(f + F2.n) = dom(F1.0) by A2,MESFUNC8:def 2;
(F1.n).x = (f + F2.n).x by A5;
then (F1.n).x = f.x + (F2.n).x by A24,A26,A29,MESFUNC1:def 3;
then (F1#x).n = f.x + (F2.n).x by MESFUNC5:def 13;
hence thesis by MESFUNC5:def 13;
end;
A30: dom(f + lim_sup F2) c= dom f by A3,A4,A8,XBOOLE_1:17;
then not f.x in {-infty} by A4,A10,A26,FUNCT_1:def 7;
then
A31: f.x <> -infty by TARSKI:def 1;
not f.x in {+infty} by A3,A10,A26,A30,FUNCT_1:def 7;
then f.x <> +infty by TARSKI:def 1;
then
A32: f.x in REAL by A31,XXREAL_0:14;
x in dom(f + lim_sup F2) by A3,A4,A6,A7,A9,A26,MESFUNC8:def 8;
then
A33: (f + lim_sup F2).x = f.x + (lim_sup F2).x by MESFUNC1:def 3;
(lim_sup F2).x = lim_sup(F2#x) by A1,A24,A25,A26,MESFUNC8:def 8;
hence thesis by A32,A28,A27,A33,Th10;
end;
hence thesis by A10,PARTFUN1:5;
end;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
theorem Th12:
f is_integrable_on M & g is_integrable_on M implies f-g is_integrable_on M
proof
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M;
(-jj)(#)g is_integrable_on M by A2,MESFUNC5:110;
then -g is_integrable_on M by MESFUNC2:9;
then f+(-g) is_integrable_on M by A1,MESFUNC5:108;
hence thesis by MESFUNC2:8;
end;
theorem Th13:
f is_integrable_on M & g is_integrable_on M implies ex E be
Element of S st E = dom f /\ dom g & Integral(M,f-g)=Integral(M,f|E)+Integral(M
,(-g)|E)
proof
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M;
(-jj)(#)g is_integrable_on M by A2,MESFUNC5:110;
then -g is_integrable_on M by MESFUNC2:9;
then consider E be Element of S such that
A3: E = dom f /\ dom(-g) and
A4: Integral(M,f+(-g))= Integral(M,f|E)+Integral(M,(-g)|E) by A1,MESFUNC5:109;
A5: dom g = dom(-g) by MESFUNC1:def 7;
Integral(M,f-g)= Integral(M,f|E)+Integral(M,(-g)|E) by A4,MESFUNC2:8;
hence thesis by A3,A5;
end;
theorem Th14:
(for n be Nat holds seq1.n = -seq2.n) implies lim_inf seq2 = -
lim_sup seq1 & lim_sup seq2 = -lim_inf seq1
proof
assume
A1: for n be Nat holds seq1.n = -seq2.n;
now
let z be object;
assume z in rng (inferior_realsequence seq2);
then consider n be object such that
A2: n in dom (inferior_realsequence seq2) and
A3: z = (inferior_realsequence seq2).n by FUNCT_1:def 3;
reconsider n as Element of NAT by A2;
consider R2 be non empty Subset of ExtREAL such that
A4: R2 = {seq2.k where k is Nat : n <= k} and
A5: z = inf R2 by A3,RINFSUP2:def 6;
reconsider z2 = z as Element of ExtREAL by A3, XXREAL_0:def 1;
set R1 = {seq1.k where k is Nat : n <= k};
reconsider R1 as non empty Subset of ExtREAL by RINFSUP2:5;
set z1 = -z2;
A6: ex K1 be non empty Subset of ExtREAL st K1 = {seq1.k where k is
Nat: n <= k} & (superior_realsequence seq1).n = sup K1 by
RINFSUP2:def 7;
now
let x be object;
assume x in R1;
then consider k be Nat such that
A7: x = seq1.k and
A8: n <= k;
reconsider x1=x as Element of ExtREAL by A7;
-x1 = -(-seq2.k) by A1,A7;
then -x1 in {seq2.k2 where k2 is Nat : n <= k2} by A8;
then -(-x1) in -R2 by A4;
hence x in -R2;
end;
then
A9: R1 c= -R2 by TARSKI:def 3;
now
let x be object;
assume x in -R2;
then consider y be R_eal such that
A10: x = -y and
A11: y in R2;
consider k be Nat such that
A12: y = seq2.k and
A13: n <= k by A4,A11;
seq1.k = -seq2.k by A1;
hence x in R1 by A10,A12,A13;
end;
then -R2 c= R1 by TARSKI:def 3;
then -R2 = R1 by A9,XBOOLE_0:def 10;
then (superior_realsequence seq1).n = z1 by A5,A6,SUPINF_2:15;
then
A14: z1 in rng(superior_realsequence seq1) by FUNCT_2:4;
z2 = -z1;
hence z in -rng(superior_realsequence seq1) by A14;
end;
then
A15: rng (inferior_realsequence seq2) c= -(rng (superior_realsequence seq1))
by TARSKI:def 3;
now
let z be object;
assume z in rng (superior_realsequence seq2);
then consider n be object such that
A16: n in dom (superior_realsequence seq2) and
A17: z = (superior_realsequence seq2).n by FUNCT_1:def 3;
reconsider n as Element of NAT by A16;
consider R2 be non empty Subset of ExtREAL such that
A18: R2 = {seq2.k where k is Nat : n <= k} and
A19: z = sup R2 by A17,RINFSUP2:def 7;
reconsider z2 = z as Element of ExtREAL by A17,XXREAL_0:def 1;
set R1 = {seq1.k where k is Nat : n <= k};
reconsider R1 as non empty Subset of ExtREAL by RINFSUP2:5;
set z1 = -z2;
A20: ex K1 be non empty Subset of ExtREAL st K1 = {seq1.k where k is
Nat: n <= k} & (inferior_realsequence seq1).n = inf K1 by
RINFSUP2:def 6;
now
let x be object;
assume x in R1;
then consider k be Nat such that
A21: x = seq1.k and
A22: n <= k;
reconsider x1=x as Element of ExtREAL by A21;
-x1 = -(-seq2.k) by A1,A21;
then -x1 in {seq2.k2 where k2 is Nat : n <= k2} by A22;
then -(-x1) in -R2 by A18;
hence x in -R2;
end;
then
A23: R1 c= -R2 by TARSKI:def 3;
now
let x be object;
assume x in -R2;
then consider y be R_eal such that
A24: x = -y and
A25: y in R2;
consider k be Nat such that
A26: y = seq2.k and
A27: n <= k by A18,A25;
seq1.k = -seq2.k by A1;
hence x in R1 by A24,A26,A27;
end;
then -R2 c= R1 by TARSKI:def 3;
then -R2 = R1 by A23,XBOOLE_0:def 10;
then (inferior_realsequence seq1).n = z1 by A19,A20,SUPINF_2:14;
then
A28: z1 in rng(inferior_realsequence seq1) by FUNCT_2:4;
z2 = -z1;
hence z in -rng(inferior_realsequence seq1) by A28;
end;
then
A29: rng (superior_realsequence seq2) c= -(rng (inferior_realsequence seq1))
by TARSKI:def 3;
now
let z be object;
assume z in -(rng (superior_realsequence seq1));
then consider t be R_eal such that
A30: z = -t and
A31: t in rng (superior_realsequence seq1);
consider n be object such that
A32: n in dom (superior_realsequence seq1) and
A33: t = (superior_realsequence seq1).n by A31,FUNCT_1:def 3;
reconsider n as Element of NAT by A32;
consider R1 be non empty Subset of ExtREAL such that
A34: R1 = {seq1.k where k is Nat : n <= k} and
A35: t = sup R1 by A33,RINFSUP2:def 7;
reconsider z1 = z as Element of ExtREAL by A30;
set R2 = {seq2.k where k is Nat : n <= k};
reconsider R2 as non empty Subset of ExtREAL by RINFSUP2:5;
A36: ex K2 be non empty Subset of ExtREAL st K2 = {seq2.k where k is
Nat: n <= k} & (inferior_realsequence seq2).n = inf K2 by
RINFSUP2:def 6;
now
let x be object;
assume x in R2;
then consider k be Nat such that
A37: x = seq2.k and
A38: n <= k;
reconsider x1=x as Element of ExtREAL by A37;
-x1 = -(-seq1.k) by A1,A37;
then -x1 in {seq1.k2 where k2 is Nat : n <= k2} by A38;
then -(-x1) in -R1 by A34;
hence x in -R1;
end;
then
A39: R2 c= -R1 by TARSKI:def 3;
now
let x be object;
assume x in -R1;
then consider y be R_eal such that
A40: x = -y and
A41: y in R1;
consider k be Nat such that
A42: y = seq1.k and
A43: n <= k by A34,A41;
seq1.k = -seq2.k by A1;
hence x in R2 by A40,A42,A43;
end;
then -R1 c= R2 by TARSKI:def 3;
then -R1 = R2 by A39,XBOOLE_0:def 10;
then (inferior_realsequence seq2).n = z1 by A30,A35,A36,SUPINF_2:14;
hence z in rng (inferior_realsequence seq2) by FUNCT_2:4;
end;
then
-(rng (superior_realsequence seq1)) c= rng (inferior_realsequence seq2)
by TARSKI:def 3;
then rng (inferior_realsequence seq2) = -(rng (superior_realsequence seq1))
by A15,XBOOLE_0:def 10;
hence lim_inf seq2 = - lim_sup seq1 by SUPINF_2:15;
now
let z be object;
assume z in -(rng (inferior_realsequence seq1));
then consider t be R_eal such that
A44: z = -t and
A45: t in rng (inferior_realsequence seq1);
consider n be object such that
A46: n in dom (inferior_realsequence seq1) and
A47: t = (inferior_realsequence seq1).n by A45,FUNCT_1:def 3;
reconsider n as Element of NAT by A46;
consider R1 be non empty Subset of ExtREAL such that
A48: R1 = {seq1.k where k is Nat : n <= k} and
A49: t = inf R1 by A47,RINFSUP2:def 6;
reconsider z1 = z as Element of ExtREAL by A44;
set R2 = {seq2.k where k is Nat : n <= k};
reconsider R2 as non empty Subset of ExtREAL by RINFSUP2:5;
A50: ex K2 be non empty Subset of ExtREAL st K2 = {seq2.k where k is
Nat: n <= k} & (superior_realsequence seq2).n = sup K2 by
RINFSUP2:def 7;
now
let x be object;
assume x in R2;
then consider k be Nat such that
A51: x = seq2.k and
A52: n <= k;
reconsider x1=x as Element of ExtREAL by A51;
seq1.k = -seq2.k by A1;
then -x1 in R1 by A48,A51,A52;
then -(-x1) in -R1;
hence x in -R1;
end;
then
A53: R2 c= -R1 by TARSKI:def 3;
now
let x be object;
assume x in -R1;
then consider y be R_eal such that
A54: x = -y and
A55: y in R1;
consider k be Nat such that
A56: y = seq1.k and
A57: n <= k by A48,A55;
seq1.k = -seq2.k by A1;
hence x in R2 by A54,A56,A57;
end;
then -R1 c= R2 by TARSKI:def 3;
then -R1 = R2 by A53,XBOOLE_0:def 10;
then (superior_realsequence seq2).n = z1 by A44,A49,A50,SUPINF_2:15;
hence z in rng (superior_realsequence seq2) by FUNCT_2:4;
end;
then -(rng (inferior_realsequence seq1)) c= rng (superior_realsequence seq2
) by TARSKI:def 3;
then rng (superior_realsequence seq2) = -(rng (inferior_realsequence seq1))
by A29,XBOOLE_0:def 10;
hence thesis by SUPINF_2:14;
end;
theorem Th15:
dom(F1.0) = dom(F2.0) & F1 is with_the_same_dom & (for n be Nat
holds F1.n = - F2.n) implies lim_inf F1 = -lim_sup F2 & lim_sup F1 = -lim_inf
F2
proof
assume that
A1: dom(F1.0) = dom(F2.0) and
A2: F1 is with_the_same_dom and
A3: for n be Nat holds F1.n = - F2.n;
A4: dom lim_inf F1 = dom(F1.0) by MESFUNC8:def 7;
A5: dom lim_sup F2 = dom(F2.0) by MESFUNC8:def 8;
A6: now
let x be Element of X;
assume
A7: x in dom(F1.0);
let n be Nat;
dom(F1.n) = dom(F1.0) by A2,MESFUNC8:def 2;
then
A8: x in dom(-F2.n) by A3,A7;
(F1.n).x = (-F2.n).x by A3;
then (F1.n).x = -(F2.n).x by A8,MESFUNC1:def 7;
then (F1#x).n = -(F2.n).x by MESFUNC5:def 13;
hence (F2#x).n = -(F1#x).n by MESFUNC5:def 13;
end;
A9: now
let x be Element of X;
assume
A10: x in dom lim_inf F1;
then
A11: (lim_inf F1).x = lim_inf(F1#x) by MESFUNC8:def 7;
x in dom(-lim_sup F2) by A1,A4,A5,A10,MESFUNC1:def 7;
then
A12: (-lim_sup F2).x = -(lim_sup F2).x by MESFUNC1:def 7;
A13: for n be Nat holds (F2#x).n = -(F1#x).n by A4,A6,A10;
(lim_sup F2).x = lim_sup(F2#x) by A1,A4,A5,A10,MESFUNC8:def 8;
hence (lim_inf F1).x = (-lim_sup F2).x by A13,A11,A12,Th14;
end;
dom(-lim_sup F2) = dom lim_sup F2 by MESFUNC1:def 7;
hence lim_inf F1 = -lim_sup F2 by A1,A4,A5,A9,PARTFUN1:5;
A14: dom lim_sup F1 = dom(F1.0) by MESFUNC8:def 8;
A15: dom lim_inf F2 = dom(F2.0) by MESFUNC8:def 7;
A16: for x be Element of X st x in dom lim_sup F1 holds (lim_sup F1).x = (-
lim_inf F2).x
proof
let x be Element of X;
assume
A17: x in dom lim_sup F1;
then
A18: (lim_sup F1).x = lim_sup(F1#x) by MESFUNC8:def 8;
x in dom(-lim_inf F2) by A1,A14,A15,A17,MESFUNC1:def 7;
then
A19: (-lim_inf F2).x = -(lim_inf F2).x by MESFUNC1:def 7;
A20: for n be Nat holds (F2#x).n = -(F1#x).n by A14,A6,A17;
(lim_inf F2).x = lim_inf(F2#x) by A1,A14,A15,A17,MESFUNC8:def 7;
hence thesis by A20,A18,A19,Th14;
end;
dom(-lim_inf F2) = dom lim_inf F2 by MESFUNC1:def 7;
hence thesis by A1,A14,A15,A16,PARTFUN1:5;
end;
theorem Th16:
E = dom(F.0) & E = dom P & (for n be Nat holds F.n
is E-measurable) & P is_integrable_on M & (for x be Element of X, n be Nat
st x in E holds (|. F.n .|).x <= P.x) implies (for n be Nat holds |. F.n .|
is_integrable_on M) & |. lim_inf F .| is_integrable_on M & |. lim_sup F .|
is_integrable_on M
proof
assume that
A1: E = dom(F.0) and
A2: E = dom P and
A3: for n be Nat holds F.n is E-measurable and
A4: P is_integrable_on M and
A5: for x be Element of X, n be Nat st x in E holds (|. F.n .|).x <= P.x;
A6: (lim_inf F) is E-measurable by A1,A3,MESFUNC8:24;
hereby
let n be Nat;
A7: F.n is E-measurable by A3;
A8: E = dom(F.n) by A1,MESFUNC8:def 2;
now
let x be Element of X;
assume
A9: x in dom(F.n);
then
A10: x in dom(|. F.n .|) by MESFUNC1:def 10;
(|. F.n .|).x <= P.x by A5,A8,A9;
hence |. (F.n).x .| <= P.x by A10,MESFUNC1:def 10;
end;
then F.n is_integrable_on M by A2,A4,A8,A7,MESFUNC5:102;
hence |. F.n .| is_integrable_on M by MESFUNC5:100;
end;
A11: E = dom(lim_inf F) by A1,MESFUNC8:def 7;
A12: (lim_sup F) is E-measurable by A1,A3,MESFUNC8:23;
A13: for x be Element of X, k be Nat st x in E holds -(P.x) <= (F#x).k & (F#x
).k <= P.x
proof
let x be Element of X, k be Nat;
assume
A14: x in E;
then x in dom(F.k) by A1,MESFUNC8:def 2;
then
A15: x in dom(|.(F.k).|) by MESFUNC1:def 10;
(|. F.k .|).x <= P.x by A5,A14;
then
A16: |. (F.k).x .| <= P.x by A15,MESFUNC1:def 10;
then
A17: (F.k).x <= P.x by EXTREAL1:23;
-(P.x) <= (F.k).x by A16,EXTREAL1:23;
hence thesis by A17,MESFUNC5:def 13;
end;
now
let x be Element of X;
assume
A18: x in dom(lim_inf F);
then
A19: x in E by A1,MESFUNC8:def 7;
for k be Nat holds (inferior_realsequence(F#x)).k <= P.x
proof
let k be Nat;
reconsider k1=k as Nat;
A20: (inferior_realsequence(F#x)).k1 <= (F#x).k1 by RINFSUP2:8;
(F#x).k <= P.x by A13,A19;
hence thesis by A20,XXREAL_0:2;
end;
then lim_inf(F#x) <= P.x by Th5;
then
A21: (lim_inf F).x <= P.x by A18,MESFUNC8:def 7;
now
let y be ExtReal;
assume y in rng(F#x);
then ex k be object st k in dom(F#x) & y = (F#x).k by FUNCT_1:def 3;
hence -(P.x) <= y by A13,A19;
end;
then -(P.x) is LowerBound of rng(F#x) by XXREAL_2:def 2;
then -(P.x) <= inf(F#x) by XXREAL_2:def 4;
then -(P.x) <= inf((F#x)^\0) by NAT_1:47;
then
A22: -(P.x) <= (inferior_realsequence(F#x)).0 by RINFSUP2:27;
(inferior_realsequence(F#x)).0 <= sup inferior_realsequence(F#x) by
RINFSUP2:23;
then -(P.x) <= lim_inf(F#x) by A22,XXREAL_0:2;
then -(P.x) <= (lim_inf F).x by A18,MESFUNC8:def 7;
hence |. (lim_inf F).x .| <= P.x by A21,EXTREAL1:23;
end;
then lim_inf F is_integrable_on M by A2,A4,A11,A6,MESFUNC5:102;
hence |. lim_inf F .| is_integrable_on M by MESFUNC5:100;
A23: E = dom(lim_sup F) by A1,MESFUNC8:def 8;
now
let x be Element of X;
assume
A24: x in dom(lim_sup F);
for k be Nat holds (superior_realsequence(F#x)).k >= -(P.x)
proof
let k be Nat;
reconsider k1=k as Nat;
A25: (superior_realsequence(F#x)).k1 >= (F#x).k1 by RINFSUP2:8;
(F#x).k >= -(P.x) by A23,A13,A24;
hence thesis by A25,XXREAL_0:2;
end;
then lim_sup(F#x) >= -(P.x) by Th4;
then
A26: (lim_sup F).x >= -(P.x) by A24,MESFUNC8:def 8;
now
let y be ExtReal;
assume y in rng(F#x);
then ex k be object st k in dom(F#x) & y = (F#x).k by FUNCT_1:def 3;
hence P.x >= y by A23,A13,A24;
end;
then P.x is UpperBound of rng(F#x) by XXREAL_2:def 1;
then P.x >= sup rng(F#x) by XXREAL_2:def 3;
then P.x >= sup((F#x)^\0) by NAT_1:47;
then
A27: P.x >= (superior_realsequence(F#x)).0 by RINFSUP2:27;
(superior_realsequence(F#x)).0 >= inf superior_realsequence(F#x) by
RINFSUP2:23;
then P.x >= lim_sup(F#x) by A27,XXREAL_0:2;
then P.x >= (lim_sup F).x by A24,MESFUNC8:def 8;
hence |. (lim_sup F).x .| <= P.x by A26,EXTREAL1:23;
end;
then lim_sup F is_integrable_on M by A2,A4,A23,A12,MESFUNC5:102;
hence thesis by MESFUNC5:100;
end;
Lm1: E = dom(F.0) & E = dom P & (for n be Nat holds F.n is E-measurable) &
P is_integrable_on M & P is nonnegative & (for x be Element of X, n be Nat st x
in E holds (|. F.n .|).x <= P.x) & eq_dom(P,+infty) = {} implies ex I be
ExtREAL_sequence st (for n be Nat holds I.n = Integral(M,F.n)) & lim_inf I >=
Integral(M,lim_inf F) & lim_sup I <= Integral(M,lim_sup F) & ( (for x be
Element of X st x in E holds F#x is convergent) implies I is convergent & lim I
= Integral(M,lim F) )
proof
assume that
A1: E = dom(F.0) and
A2: E = dom P and
A3: for n be Nat holds F.n is E-measurable and
A4: P is_integrable_on M and
A5: P is nonnegative and
A6: for x be Element of X, n be Nat st x in E holds (|. F.n .|).x <= P.x and
A7: eq_dom(P,+infty) = {};
A8: E = dom(lim_inf F) by A1,MESFUNC8:def 7;
then
A9: (lim_inf F)|E = lim_inf F by RELAT_1:68;
deffunc G(Nat) = P + F.$1;
consider G be Function such that
A10: dom G = NAT & for n be Element of NAT holds G.n = G(n) from FUNCT_1
:sch 4;
A11: for x be Element of X, k be Nat st x in E holds -(P.x) <= (F#x).k & (F#x
).k <= P.x
proof
let x be Element of X, k be Nat;
assume
A12: x in E;
then x in dom(F.k) by A1,MESFUNC8:def 2;
then
A13: x in dom |.(F.k).| by MESFUNC1:def 10;
(|. F.k .|).x <= P.x by A6,A12;
then
A14: |. (F.k).x .| <= P.x by A13,MESFUNC1:def 10;
then
A15: (F.k).x <= P.x by EXTREAL1:23;
-(P.x) <= (F.k).x by A14,EXTREAL1:23;
hence thesis by A15,MESFUNC5:def 13;
end;
A16: now
let x be Element of X;
assume
A17: x in dom lim_inf F;
now
let k be Nat;
A18: (inferior_realsequence(F#x)).k <= (F#x).k by RINFSUP2:8;
(F#x).k <= P.x by A8,A11,A17;
hence (inferior_realsequence(F#x)).k <= P.x by A18,XXREAL_0:2;
end;
then lim_inf(F#x) <= P.x by Th5;
then
A19: (lim_inf F).x <= P.x by A17,MESFUNC8:def 7;
now
let y be ExtReal;
assume y in rng(F#x);
then ex k be object st k in dom(F#x) & y = (F#x).k by FUNCT_1:def 3;
hence -(P.x) <= y by A8,A11,A17;
end;
then -(P.x) is LowerBound of rng(F#x) by XXREAL_2:def 2;
then -(P.x) <= inf rng(F#x) by XXREAL_2:def 4;
then -(P.x) <= inf((F#x)^\0) by NAT_1:47;
then
A20: -(P.x) <= (inferior_realsequence(F#x)).0 by RINFSUP2:27;
(inferior_realsequence(F#x)).0 <= sup inferior_realsequence(F#x) by
RINFSUP2:23;
then -(P.x) <= lim_inf(F#x) by A20,XXREAL_0:2;
then -(P.x) <= (lim_inf F).x by A17,MESFUNC8:def 7;
hence |. (lim_inf F).x .| <= P.x by A19,EXTREAL1:23;
end;
lim_inf F is E-measurable by A1,A3,MESFUNC8:24;
then lim_inf F is_integrable_on M by A2,A4,A8,A16,MESFUNC5:102;
then
A21: ex E3 be Element of S st E3 = dom P /\ dom(lim_inf F) & Integral(M,P +
lim_inf F) = Integral(M,P|E3) + Integral(M,(lim_inf F)|E3) by A4,MESFUNC5:109
;
A22: P|E = P by A2,RELAT_1:68;
A23: Integral(M,P) < +infty by A4,MESFUNC5:96;
-infty < Integral(M,P) by A4,MESFUNC5:96;
then
A24: Integral(M,P) is Element of REAL by A23,XXREAL_0:14;
now
let x be object;
assume x in P"{-infty};
then
A25: P.x in {-infty} by FUNCT_1:def 7;
0 <= P.x by A5,SUPINF_2:51;
hence contradiction by A25,TARSKI:def 1;
end;
then
A26: P"{-infty} = {} by XBOOLE_0:def 1;
A27: now
let n be Nat;
n in NAT by ORDINAL1:def 12;
then G.n = P + F.n by A10;
hence G.n is PartFunc of X,ExtREAL;
end;
A28: now
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence G.n = P + F.n by A10;
end;
reconsider G as Functional_Sequence of X,ExtREAL by A10,A27,SEQFUNC:1;
A29: P"{+infty} = {} by A7,MESFUNC5:30;
A30: for n be Nat holds dom(G.n) = E
proof
let n be Nat;
dom(G.n) = dom(P + F.n) by A28;
then
A31: dom(G.n) = (dom P /\ dom(F.n))\((P"{-infty} /\ (F.n)"{+infty}) \/ (P"
{+infty} /\ (F.n)"{-infty})) by MESFUNC1:def 3;
dom(F.n) = E by A1,MESFUNC8:def 2;
hence thesis by A2,A29,A26,A31;
end;
A32: now
let n,m be Nat;
thus dom(G.n) = E by A30
.= dom(G.m) by A30;
end;
deffunc H(Nat) = P - F.$1;
consider H be Function such that
A33: dom H = NAT & for n be Element of NAT holds H.n = H(n) from
FUNCT_1:sch 4;
reconsider G as with_the_same_dom Functional_Sequence of X,ExtREAL by A32,
MESFUNC8:def 2;
A34: dom(G.0) = dom(F.0) by A1,A30;
A35: for n be Nat holds F.n is_integrable_on M
proof
let n be Nat;
A36: E = dom(F.n) by A1,MESFUNC8:def 2;
A37: now
let x be Element of X;
assume
A38: x in dom(F.n);
then
A39: x in dom(|. F.n .|) by MESFUNC1:def 10;
(|. F.n .|).x <= P.x by A6,A36,A38;
hence |. (F.n).x .| <= P.x by A39,MESFUNC1:def 10;
end;
F.n is E-measurable by A3;
hence thesis by A2,A4,A36,A37,MESFUNC5:102;
end;
A40: now
let n be Nat;
A41: G.n = P + F.n by A28;
now
let x be object;
assume
A42: x in dom(P+(F.n));
then reconsider x1=x as Element of X;
x in E by A30,A41,A42;
then -(P.x) <= (F#x1).n by A11;
then
A43: -P.x <= (F.n).x by MESFUNC5:def 13;
-P.x + P.x = 0 by XXREAL_3:7;
then 0 <= (F.n).x + P.x by A43,XXREAL_3:36;
hence 0 <= (P+(F.n)).x by A42,MESFUNC1:def 3;
end;
hence G.n is nonnegative by A41,SUPINF_2:52;
F.n is_integrable_on M by A35;
then G.n is_integrable_on M by A4,A41,MESFUNC5:108;
then consider E1 be Element of S such that
AB: E1 = dom(G.n) & G.n is E1-measurable;
for r being Real holds E /\ less_dom(G.n,r) in S
proof
let r be Real;
AC: E1 /\ less_dom(G.n,r) in S by AB;
E = E1 by A30,AB;
hence thesis by AC;
end;
hence G.n is E-measurable;
end;
E = dom(G.0) by A30;
then consider IG be ExtREAL_sequence such that
A44: for n be Nat holds IG.n = Integral(M,G.n) and
A45: Integral(M,lim_inf G) <= lim_inf IG by A40,Th7;
A46: Integral(M,P) < +infty by A4,MESFUNC5:96;
deffunc I(Nat) = Integral(M,F.$1);
consider I be sequence of ExtREAL such that
A47: for n be Element of NAT holds I.n = I(n) from FUNCT_2:sch 4;
reconsider I as ExtREAL_sequence;
A48: -infty < Integral(M,P) by A4,MESFUNC5:96;
A49: for n be Nat holds I.n = Integral(M,F.n) & I.n in REAL
proof
let n be Nat;
n in NAT by ORDINAL1:def 12;
then
A50: I.n = Integral(M,F.n) by A47;
A51: F.n is_integrable_on M by A35;
then
A52: Integral(M,F.n) < +infty by MESFUNC5:96;
-infty < Integral(M,F.n) by A51,MESFUNC5:96;
hence thesis by A50,A52,XXREAL_0:14;
end;
now
let n be Nat;
A53: G.n=P+(F.n) by A28;
F.n is_integrable_on M by A35;
then
A54: ex E2 be Element of S st E2 = dom P /\ dom(F.n) & Integral(M,G.n) =
Integral(M,P|E2) + Integral(M,(F.n)|E2) by A4,A53,MESFUNC5:109;
A55: P|E = P by A2,RELAT_1:68;
A56: dom(F.n) = E by A1,MESFUNC8:def 2;
then (F.n)|E = F.n by RELAT_1:68;
then Integral(M,G.n) = Integral(M,P) + I.n by A2,A49,A54,A56,A55;
hence IG.n = Integral(M,P) + I.n by A44;
end;
then lim_inf IG = Integral(M,P) + lim_inf I by A24,Th10;
then Integral(M,P) + Integral(M,lim_inf F) <= Integral(M,P) + lim_inf I
by A2,A8,A28,A29,A26,A45,A21,A22,A9,A34,Th11;
then Integral(M,lim_inf F) <= lim_inf I + Integral(M,P) - Integral(M,P) by
A48,A46,XXREAL_3:56;
then Integral(M,lim_inf F) <= lim_inf I + (Integral(M,P) - Integral(M,P))
by A48,A46,XXREAL_3:30;
then Integral(M,lim_inf F) <= lim_inf I + 0. by XXREAL_3:7;
then
A57: Integral(M,lim_inf F) <= lim_inf I by XXREAL_3:4;
A58: now
let n be Nat;
A59: n in NAT by ORDINAL1:def 12;
H.n = P - F.n by A33,A59;
hence H.n is PartFunc of X,ExtREAL;
end;
A60: now
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence H.n = P - F.n by A33;
end;
A61: E = dom(lim_sup F) by A1,MESFUNC8:def 8;
A62: now
let x be Element of X;
assume
A63: x in dom lim_sup F;
for k be Nat holds (superior_realsequence(F#x)).k >= -(P.x)
proof
let k be Nat;
A64: (superior_realsequence(F#x)).k >= (F#x).k by RINFSUP2:8;
(F#x).k >= -(P.x) by A61,A11,A63;
hence thesis by A64,XXREAL_0:2;
end;
then lim_sup(F#x) >= -(P.x) by Th4;
then
A65: (lim_sup F).x >= -(P.x) by A63,MESFUNC8:def 8;
now
let y be ExtReal;
assume y in rng(F#x);
then ex k be object st k in dom(F#x) & y = (F#x).k by FUNCT_1:def 3;
hence P.x >= y by A61,A11,A63;
end;
then P.x is UpperBound of rng(F#x) by XXREAL_2:def 1;
then P.x >= sup rng(F#x) by XXREAL_2:def 3;
then P.x >= sup((F#x)^\0) by NAT_1:47;
then
A66: P.x >= (superior_realsequence(F#x)).0 by RINFSUP2:27;
(superior_realsequence(F#x)).0 >= inf superior_realsequence(F#x) by
RINFSUP2:23;
then P.x >= lim_sup(F#x) by A66,XXREAL_0:2;
then P.x >= (lim_sup F).x by A63,MESFUNC8:def 8;
hence |. (lim_sup F).x .| <= P.x by A65,EXTREAL1:23;
end;
lim_sup F is E-measurable by A1,A3,MESFUNC8:23;
then
A67: lim_sup F is_integrable_on M by A2,A4,A61,A62,MESFUNC5:102;
then
A68: ex E6 be Element of S st E6 = dom P /\ dom lim_sup F & Integral(M,P -
lim_sup F) = Integral(M,P|E6) + Integral(M,(-lim_sup F)|E6) by A4,Th13;
set E1 = Integral(M,lim_sup F);
A69: E1 < +infty by A67,MESFUNC5:96;
-infty < E1 by A67,MESFUNC5:96;
then reconsider e1 = E1 as Element of REAL by A69,XXREAL_0:14;
A70: -E1 = -e1 by SUPINF_2:2;
A71: P|E = P by A2,RELAT_1:68;
deffunc F1(Nat) = - F.$1;
consider F1 be Function such that
A72: dom F1 = NAT & for n be Element of NAT holds F1.n = F1(n) from
FUNCT_1:sch 4;
reconsider H as Functional_Sequence of X,ExtREAL
by A33,A58,SEQFUNC:1;
A73: now
let n be Nat;
A74: dom(H.n) = dom(P - F.n) by A60;
dom(F.n) = E by A1,MESFUNC8:def 2;
then dom(H.n) = (E /\ E)\(({} /\ (F.n)"{+infty}) \/ ({} /\ (F.n)"{-infty}
)) by A2,A29,A26,A74,MESFUNC1:def 4;
hence dom(H.n) = E;
end;
now
let n,m be Nat;
thus dom(H.n) = E by A73
.= dom(H.m) by A73;
end;
then reconsider H as with_the_same_dom Functional_Sequence of X,ExtREAL by
MESFUNC8:def 2;
A75: -infty < Integral(M,P) by A4,MESFUNC5:96;
A76: now
let n be Nat;
A77: H.n = P - F.n by A60;
now
let x be Element of X;
assume x in dom(F.n);
then x in E by A1,MESFUNC8:def 2;
then (F#x).n <= P.x by A11;
hence (F.n).x <= P.x by MESFUNC5:def 13;
end;
hence H.n is nonnegative by A77,MESFUNC7:1;
F.n is_integrable_on M by A35;
then H.n is_integrable_on M by A4,A77,Th12;
then consider E4 be Element of S such that
AA: E4 = dom(H.n) & H.n is E4-measurable;
E4 = E by AA,A73;
hence H.n is E-measurable by AA;
end;
E = dom(H.0) by A73;
then consider IH be ExtREAL_sequence such that
A78: for n be Nat holds IH.n = Integral(M,H.n) and
A79: Integral(M,lim_inf H) <= lim_inf IH by A76,Th7;
A80: Integral(M,P) < +infty by A4,MESFUNC5:96;
now
let n be Nat;
A81: n in NAT by ORDINAL1:def 12;
F1.n = -F.n by A72,A81;
hence F1.n is PartFunc of X,ExtREAL;
end;
then reconsider F1 as Functional_Sequence of X,ExtREAL
by A72,SEQFUNC:1;
A82: now
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence F1.n = -F.n by A72;
end;
now
let n,m be Nat;
F1.m = -F.m by A82;
then
A83: dom(F1.m) = dom(F.m) by MESFUNC1:def 7;
F1.n = -F.n by A82;
then dom(F1.n) = dom(F.n) by MESFUNC1:def 7;
hence dom(F1.n) = dom(F1.m) by A83,MESFUNC8:def 2;
end;
then reconsider F1 as with_the_same_dom Functional_Sequence of X,ExtREAL by
MESFUNC8:def 2;
A84: Integral(M,-lim_sup F) = Integral(M,(-1)(#)lim_sup F) by MESFUNC2:9;
A85: now
let n be Nat;
H.n = P - F.n by A60;
then H.n = P + (- F.n) by MESFUNC2:8;
hence H.n = P + F1.n by A82;
end;
F1.0 = -F.0 by A82;
then
A86: dom(F1.0) = dom(F.0) by MESFUNC1:def 7;
then dom(F1.0) = dom(H.0) by A1,A73;
then lim_inf H = P + lim_inf F1 by A29,A26,A85,Th11;
then lim_inf H = P + -lim_sup F by A82,A86,Th15;
then
A87: lim_inf H = P - lim_sup F by MESFUNC2:8;
E = dom lim_sup F by A1,MESFUNC8:def 8;
then E = dom(-lim_sup F) by MESFUNC1:def 7;
then
A88: (-lim_sup F)|E = -lim_sup F by RELAT_1:68;
deffunc I1(Nat) = - I.$1;
consider I1 be sequence of ExtREAL such that
A89: for n be Element of NAT holds I1.n = I1(n) from FUNCT_2:sch 4;
reconsider I1 as ExtREAL_sequence;
A90: now
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence I1.n = -I.n by A89;
end;
then
A91: -lim_inf I1 = lim_sup I by Th14;
now
let n be Nat;
A92: F.n is_integrable_on M by A35;
Integral(M,-F.n) = Integral(M,(-1)(#)F.n) by MESFUNC2:9;
then
A93: Integral(M,(-F.n)) = (-jj)*Integral(M,F.n) by A92,MESFUNC5:110;
A94: dom(F.n) = E by A1,MESFUNC8:def 2;
then E = dom(-F.n) by MESFUNC1:def 7;
then
A95: (-F.n)|E = -(F.n) by RELAT_1:68;
H.n = P - F.n by A60;
then
A96: ex E5 be Element of S st E5 = dom P /\ dom(F.n) & Integral(M,H.n) =
Integral(M,P|E5) + Integral(M,(-F.n)|E5) by A4,A92,Th13;
reconsider In = I.n as Element of REAL by A49;
A97: (-1)*I.n = (-1)*In by EXTREAL1:1;
A98: -I.n = -In by SUPINF_2:2;
P|E = P by A2,RELAT_1:68;
then Integral(M,H.n) = Integral(M,P) + -I.n by A2,A49,A96,A94,A95,A93,A97
,A98;
then IH.n = Integral(M,P) + -I.n by A78;
hence IH.n = Integral(M,P) + I1.n by A90;
end;
then lim_inf IH = Integral(M,P) + lim_inf I1 by A24,Th10;
then Integral(M,P)+ (-jj)*Integral(M,lim_sup F) <= Integral(M,P) + -
lim_sup I by A2,A61,A79,A91,A87,A67,A68,A71,A88,A84,MESFUNC5:110;
then (-1)*Integral(M,lim_sup F) <= -lim_sup I + Integral(M,P) -
Integral(M,P) by A75,A80,XXREAL_3:56;
then (-1)*Integral(M,lim_sup F) <= -lim_sup I + (Integral(M,P) -
Integral(M,P)) by A75,A80,XXREAL_3:30;
then
A99: (-1)*Integral(M,lim_sup F) <= -lim_sup I + 0. by XXREAL_3:7;
(-1)*E1 = (-1)*e1 by EXTREAL1:1;
then -Integral(M,lim_sup F) <= -lim_sup I by A99,A70,XXREAL_3:4;
then
A100: Integral(M,lim_sup F) >= lim_sup I by XXREAL_3:38;
now
A101: lim_inf I <= lim_sup I by RINFSUP2:39;
A102: dom lim F = dom(F.0) by MESFUNC8:def 9;
assume
A103: for x be Element of X st x in E holds F#x is convergent;
A104: for x be Element of X st x in dom(lim F) holds (lim F).x = (lim_inf F).x
proof
let x be Element of X;
assume
A105: x in dom(lim F);
then F#x is convergent by A1,A103,A102;
hence thesis by A105,MESFUNC8:14;
end;
A106: for x be Element of X st x in dom lim F holds (lim F).x = (lim_sup F ).x
proof
let x be Element of X;
assume
A107: x in dom lim F;
then F#x is convergent by A1,A103,A102;
hence thesis by A107,MESFUNC8:14;
end;
A108: dom lim F = dom lim_sup F by A102,MESFUNC8:def 8;
then
A109: lim F = lim_sup F by A106,PARTFUN1:5;
A110: dom lim F = dom lim_inf F by A102,MESFUNC8:def 7;
then Integral(M,lim F) <= lim_inf I by A57,A104,PARTFUN1:5;
then lim_sup I <= lim_inf I by A100,A109,XXREAL_0:2;
then lim_inf I = lim_sup I by A101,XXREAL_0:1;
hence
A111: I is convergent by RINFSUP2:40;
then lim I = lim_sup I by RINFSUP2:41;
then
A112: lim I <= Integral(M,lim F) by A100,A108,A106,PARTFUN1:5;
lim I = lim_inf I by A111,RINFSUP2:41;
then Integral(M,lim F) <= lim I by A57,A110,A104,PARTFUN1:5;
hence lim I = Integral(M,lim F) by A112,XXREAL_0:1;
end;
hence thesis by A49,A57,A100;
end;
:: Lebesgue's Convergence theorem
theorem Th17:
E = dom(F.0) & E = dom P & (for n be Nat holds F.n
is E-measurable) & P is_integrable_on M & P is nonnegative & (for x be
Element of X, n be Nat st x in E holds (|. F.n .|).x <= P.x) implies ex I be
ExtREAL_sequence st (for n be Nat holds I.n = Integral(M,F.n)) & lim_inf I >=
Integral(M,lim_inf F) & lim_sup I <= Integral(M,lim_sup F) & ( (for x be
Element of X st x in E holds F#x is convergent) implies I is convergent & lim I
= Integral(M,lim F) )
proof
assume that
A1: E = dom(F.0) and
A2: E = dom P and
A3: for n be Nat holds F.n is E-measurable and
A4: P is_integrable_on M and
A5: P is nonnegative and
A6: for x be Element of X, n be Nat st x in E holds (|. F.n .|).x <= P.x;
for x be object st x in eq_dom(P,+infty) holds x in E by A2,MESFUNC1:def 15;
then eq_dom(P,+infty) c= E by TARSKI:def 3;
then
A7: eq_dom(P,+infty) = E /\ eq_dom(P,+infty) by XBOOLE_1:28;
ex A be Element of S st A = dom P & P is A-measurable by A4;
then reconsider E0 = eq_dom(P,+infty) as Element of S by A2,A7,MESFUNC1:33;
reconsider E1 = E \ E0 as Element of S;
deffunc F1(Nat) = (F.$1)|E1;
consider F1 be Functional_Sequence of X,ExtREAL such that
A8: for n be Nat holds F1.n = F1(n) from SEQFUNC:sch 1;
A9: now
let n be Nat;
dom(F.n) = E by A1,MESFUNC8:def 2;
then dom((F.n)|E1) = E1 by RELAT_1:62,XBOOLE_1:36;
hence dom(F1.n) = E1 by A8;
end;
then
A10: E1 = dom(F1.0);
now
let n,m be Nat;
thus dom(F1.n) = E1 by A9
.= dom(F1.m) by A9;
end;
then reconsider F1 as with_the_same_dom Functional_Sequence of X,ExtREAL by
MESFUNC8:def 2;
set P1 = P|E1;
A11: P1 is nonnegative by A5,MESFUNC5:15;
A12: E1 c= E by XBOOLE_1:36;
A13: now
let x be Element of X, n be Nat;
assume
A14: x in E1;
then
A15: P1.x = P.x by FUNCT_1:49;
x in E by A12,A14;
then x in dom(F.n) by A1,MESFUNC8:def 2;
then x in dom(|. F.n .|) by MESFUNC1:def 10;
then
A16: (|. F.n .|).x = |. (F.n).x .| by MESFUNC1:def 10;
E1 = dom(F1.n) by A9;
then
A17: E1 = dom(|. F1.n .|) by MESFUNC1:def 10;
F1.n = (F.n)|E1 by A8;
then (F1.n).x = (F.n).x by A14,FUNCT_1:49;
then (|. F.n .|).x = (|. F1.n .|).x by A14,A16,A17,MESFUNC1:def 10;
hence (|. F1.n .|).x <= P1.x by A6,A12,A14,A15;
end;
A18: dom(lim F) = dom(F.0) by MESFUNC8:def 9;
then
A19: dom(lim F) = dom(lim_inf F) by MESFUNC8:def 7;
A20: dom(lim_inf F) = E by A1,MESFUNC8:def 7;
A21: now
let x be Element of X;
assume
A22: x in dom(lim_inf F1);
then
A23: x in E1 by A10,MESFUNC8:def 7;
now
let n be Element of NAT;
((F.n)|E1).x = (F.n).x by A23,FUNCT_1:49;
then (F1.n).x = (F.n).x by A8;
then (F1#x).n = (F.n).x by MESFUNC5:def 13;
hence (F1#x).n = (F#x).n by MESFUNC5:def 13;
end;
then
A24: F1#x = F#x by FUNCT_2:63;
E1 = dom(lim_inf F1) by A10,MESFUNC8:def 7;
then lim_inf(F#x) = (lim_inf F).x by A12,A20,A22,MESFUNC8:def 7;
then (lim_inf F1).x = (lim_inf F).x by A22,A24,MESFUNC8:def 7;
hence ((lim_inf F)|(E\E0)).x = (lim_inf F1).x by A23,FUNCT_1:49;
end;
E1 = dom((lim_inf F)|(E\E0)) by A20,RELAT_1:62,XBOOLE_1:36;
then dom((lim_inf F)|(E\E0)) = dom(lim_inf F1) by A10,MESFUNC8:def 7;
then
A25: (lim_inf F)|(E\E0) = lim_inf F1 by A21,PARTFUN1:5;
A26: dom(lim_sup F) = E by A1,MESFUNC8:def 8;
A27: now
let x be Element of X;
assume
A28: x in dom(lim_sup F1);
then
A29: x in E1 by A10,MESFUNC8:def 8;
now
let n be Element of NAT;
((F.n)|E1).x = (F.n).x by A29,FUNCT_1:49;
then (F1.n).x = (F.n).x by A8;
then (F1#x).n = (F.n).x by MESFUNC5:def 13;
hence (F1#x).n = (F#x).n by MESFUNC5:def 13;
end;
then
A30: F1#x = F#x by FUNCT_2:63;
E1 = dom(lim_sup F1) by A10,MESFUNC8:def 8;
then lim_sup(F#x) = (lim_sup F).x by A12,A26,A28,MESFUNC8:def 8;
then (lim_sup F1).x = (lim_sup F).x by A28,A30,MESFUNC8:def 8;
hence ((lim_sup F)|(E\E0)).x = (lim_sup F1).x by A29,FUNCT_1:49;
end;
E1 = dom((lim_sup F)|(E\E0)) by A26,RELAT_1:62,XBOOLE_1:36;
then dom((lim_sup F)|(E\E0)) = dom(lim_sup F1) by A10,MESFUNC8:def 8;
then
A31: (lim_sup F)|(E\E0) = lim_sup F1 by A27,PARTFUN1:5;
A32: dom(P|E1) = E1 by A2,RELAT_1:62,XBOOLE_1:36;
A33: now
assume eq_dom(P1,+infty) <> {};
then consider x be object such that
A34: x in eq_dom(P1,+infty) by XBOOLE_0:def 1;
reconsider x as Element of X by A34;
P1.x = +infty by A34,MESFUNC1:def 15;
then consider y be R_eal such that
A35: y = P1.x and
A36: +infty = y;
A37: x in E1 by A32,A34,MESFUNC1:def 15;
then y = P.x by A35,FUNCT_1:49;
then x in eq_dom(P,+infty) by A2,A12,A36,A37,MESFUNC1:def 15;
hence contradiction by A37,XBOOLE_0:def 5;
end;
A38: for n be Nat holds F1.n is E1-measurable
proof
let n be Nat;
dom(F.n) = E by A1,MESFUNC8:def 2;
then
A39: E1 = dom(F.n) /\ E1 by XBOOLE_1:28,36;
F.n is E-measurable by A3;
then F.n is E1-measurable by MESFUNC1:30,XBOOLE_1:36;
then (F.n)|E1 is E1-measurable by A39,MESFUNC5:42;
hence thesis by A8;
end;
P1 is_integrable_on M by A4,MESFUNC5:112;
then consider I be ExtREAL_sequence such that
A40: for n be Nat holds I.n = Integral(M,F1.n) and
A41: lim_inf I >= Integral(M,lim_inf F1) and
A42: lim_sup I <= Integral(M,lim_sup F1) and
(for x be Element of X st x in E1 holds F1#x is convergent) implies I is
convergent & lim I = Integral(M,lim F1) by A32,A10,A11,A13,A38,A33,Lm1;
P"{+infty} = E0 by MESFUNC5:30;
then
A43: M.E0 = 0 by A4,MESFUNC5:105;
A44: for n be Nat holds I.n = Integral(M,F.n)
proof
let n be Nat;
A45: E = dom(F.n) by A1,MESFUNC8:def 2;
A46: F.n is E-measurable by A3;
|. F.n .| is_integrable_on M by A1,A2,A3,A4,A6,Th16;
then F.n is_integrable_on M by A45,A46,MESFUNC5:100;
then
Integral(M,F.n) = Integral(M,(F.n)|E0) + Integral(M,(F.n)|E1) by A45,
MESFUNC5:99;
then
A47: Integral(M,F.n) = 0. + Integral(M,(F.n)|E1) by A3,A43,A45,MESFUNC5:94;
I.n = Integral(M,F1.n) by A40;
then I.n = Integral(M,(F.n)|E1) by A8;
hence thesis by A47,XXREAL_3:4;
end;
lim_inf F is E-measurable by A1,A3,MESFUNC8:24;
then
A48: Integral(M,(lim_inf F)|(E\E0)) = Integral(M,lim_inf F) by A43,A20,
MESFUNC5:95;
lim_sup F is E-measurable by A1,A3,MESFUNC8:23;
then
A49: Integral(M,(lim_sup F)|(E\E0)) = Integral(M,lim_sup F) by A43,A26,
MESFUNC5:95;
A50: dom(lim F) = dom(lim_sup F) by A18,MESFUNC8:def 8;
now
assume
A51: for x be Element of X st x in E holds F#x is convergent;
A52: for x be Element of X st x in dom(lim F) holds (lim F).x = (lim_inf F).x
proof
let x be Element of X;
assume
A53: x in dom(lim F);
then F#x is convergent by A1,A18,A51;
hence thesis by A53,MESFUNC8:14;
end;
then
A54: lim F = lim_inf F by A19,PARTFUN1:5;
A55: lim_inf I <= lim_sup I by RINFSUP2:39;
A56: for x be Element of X st x in dom(lim F) holds (lim F).x = (lim_sup F).x
proof
let x be Element of X;
assume
A57: x in dom(lim F);
then F#x is convergent by A1,A18,A51;
hence thesis by A57,MESFUNC8:14;
end;
then lim F = lim_sup F by A50,PARTFUN1:5;
then lim_sup I <= lim_inf I by A41,A42,A25,A31,A54,XXREAL_0:2;
then lim_inf I = lim_sup I by A55,XXREAL_0:1;
hence
A58: I is convergent by RINFSUP2:40;
then lim I = lim_sup I by RINFSUP2:41;
then
A59: lim I <= Integral(M,lim F) by A42,A49,A31,A50,A56,PARTFUN1:5;
lim I = lim_inf I by A58,RINFSUP2:41;
then Integral(M,lim F) <= lim I by A41,A48,A25,A19,A52,PARTFUN1:5;
hence lim I = Integral(M,lim F) by A59,XXREAL_0:1;
end;
hence thesis by A41,A42,A44,A48,A49,A25,A31;
end;
theorem
E = dom(F.0) & (for n holds F.n is nonnegative & F.n is E-measurable
) & (for x,n,m st x in E & n <= m holds (F.n).x >= (F.m).x) & Integral(M,(F.0)
|E) < +infty implies ex I be ExtREAL_sequence st (for n be Nat holds I.n =
Integral(M,F.n)) & I is convergent & lim I = Integral(M,lim F)
proof
assume that
A1: E = dom(F.0) and
A2: for n holds F.n is nonnegative & F.n is E-measurable and
A3: for x,n,m st x in E & n <= m holds (F.n).x >= (F.m).x and
A4: Integral(M,(F.0)|E) < +infty;
A5: F.0 is nonnegative by A2;
A6: dom(F.0) = dom(|. F.0 .|) by MESFUNC1:def 10;
A7: for x be Element of X st x in dom(F.0) holds (F.0).x = |. F.0 .|.x
proof
let x be Element of X;
0 <= (F.0).x by A5,SUPINF_2:51;
then
A8: |.(F.0).x.| = (F.0).x by EXTREAL1:def 1;
assume x in dom(F.0);
hence thesis by A6,A8,MESFUNC1:def 10;
end;
A9: F.0 is E-measurable by A2;
then Integral(M,F.0) = integral+(M,F.0) by A1,A5,MESFUNC5:88;
then integral+(M,F.0) < +infty by A1,A4,RELAT_1:68;
then
A10: integral+(M,|. F.0 .|) < +infty by A6,A7,PARTFUN1:5;
A11: max+(F.0) is E-measurable by A2,MESFUNC2:25;
for x be object st x in dom max-(F.0) holds 0. <= (max-(F.0)).x
by MESFUNC2:13;
then
A12: max-(F.0) is nonnegative by SUPINF_2:52;
A13: for x be Element of X, n be Nat st x in E holds (|. F.n .|).x <= (F.0). x
proof
let x be Element of X, n be Nat;
assume
A14: x in E;
F.n is nonnegative by A2;
then 0 <= (F.n).x by SUPINF_2:51;
then |.(F.n).x.| = (F.n).x by EXTREAL1:def 1;
then
A15: |.(F.n).x.| <= (F.0).x by A3,A14;
dom(F.n) = dom(|. F.n .|) by MESFUNC1:def 10;
then x in dom(|. F.n .|) by A1,A14,MESFUNC8:def 2;
hence thesis by A15,MESFUNC1:def 10;
end;
A16: for x be Element of X st x in E holds F#x is convergent
proof
let x be Element of X;
assume
A17: x in E;
now
let n,m be Nat;
assume m <= n;
then (F.n).x <= (F.m).x by A3,A17;
then (F#x).n <= (F.m).x by MESFUNC5:def 13;
hence (F#x).n <= (F#x).m by MESFUNC5:def 13;
end;
then F#x is non-increasing by RINFSUP2:7;
hence thesis by RINFSUP2:36;
end;
A18: dom max+(F.0) = dom(F.0) by MESFUNC2:def 2;
then
A19: max+(F.0)|E = max+(F.0) by A1,RELAT_1:68;
for x be object st x in dom max+(F.0) holds 0. <= (max+(F.0)).x
by MESFUNC2:12;
then
A20: max+(F.0) is nonnegative by SUPINF_2:52;
then
A21: dom(max+(F.0) + max-(F.0)) = dom max+(F.0) /\ dom max-(F.0) by A12,
MESFUNC5:22;
A22: dom max-(F.0) = dom(F.0) by MESFUNC2:def 3;
then
A23: max-(F.0)|E = max-(F.0) by A1,RELAT_1:68;
max-(F.0) is E-measurable by A1,A2,MESFUNC2:26;
then ex C be Element of S st C = dom(max+(F.0) + max-(F.0)) & integral+(M,
max+(F.0) + max-(F.0)) = integral+(M,max+(F.0)|C) + integral+(M,max-(F.0)|C)
by A1,A18,A22,A20,A12,A11,MESFUNC5:78;
then
A24: integral+(M,max+(F.0)) + integral+(M,max-(F.0)) < +infty by A1,A18,A22,A21
,A19,A23,A10,MESFUNC2:24;
0 <= integral+(M,max-(F.0)) by A1,A9,A22,A12,MESFUNC2:26,MESFUNC5:79;
then integral+(M,max+(F.0)) <> +infty by A24,XXREAL_3:def 2;
then
A25: integral+(M,max+(F.0)) < +infty by XXREAL_0:4;
0 <= integral+(M,max+(F.0)) by A1,A9,A18,A20,MESFUNC2:25,MESFUNC5:79;
then integral+(M,max-(F.0)) <> +infty by A24,XXREAL_3:def 2;
then integral+(M,max-(F.0)) < +infty by XXREAL_0:4;
then F.0 is_integrable_on M by A1,A9,A25;
then
ex I be ExtREAL_sequence st ( for n be Nat holds I.n = Integral(M,F.n))&
lim_inf I >= Integral(M,lim_inf F) & lim_sup I <= Integral( M,lim_sup F) &( (
for x be Element of X st x in E holds F#x is convergent) implies I is
convergent & lim I = Integral(M,lim F)) by A1,A2,A13,Th17;
hence thesis by A16;
end;
definition
let X be set, F be Functional_Sequence of X,ExtREAL;
attr F is uniformly_bounded means
ex K be Real st for n be Nat
, x be set st x in dom(F.0) holds |. (F.n).x .| <= K;
end;
::$N Lebesgue's Bounded Convergence Theorem
theorem
M.E < +infty & E = dom(F.0) & (for n be Nat holds F.n is E-measurable
) & F is uniformly_bounded & (for x be Element of X st x in E holds F#x is
convergent) implies (for n be Nat holds F.n is_integrable_on M) & lim F
is_integrable_on M & ex I be ExtREAL_sequence st (for n be Nat holds I.n =
Integral(M,F.n)) & I is convergent & lim I = Integral(M,lim F)
proof
assume that
A1: M.E < +infty and
A2: E = dom(F.0) and
A3: for n be Nat holds F.n is E-measurable and
A4: F is uniformly_bounded and
A5: for x be Element of X st x in E holds F#x is convergent;
consider K1 be Real such that
A6: for n be Nat, x be set st x in dom(F.0) holds |. (F.n).x .| <= K1 by A4;
set K = max(K1,1);
K in REAL by XREAL_0:def 1;
then consider h be PartFunc of X,ExtREAL such that
A7: h is_simple_func_in S and
A8: dom h = E and
A9: for x be object st x in E holds h.x = K by MESFUNC5:41,NUMBERS:31;
A10: dom h = dom |.h.| by MESFUNC1:def 10;
A11: K > 0 by XXREAL_0:30;
then
A12: K * +infty = +infty by XXREAL_3:def 5;
for x be object st x in E holds h.x >= 0. by A11,A9;
then
A13: h is nonnegative by A8,SUPINF_2:52;
then
A14: Integral(M,h) = integral'(M,h) by A7,MESFUNC5:89;
A15: integral'(M,h) = K * M.(dom h) by A11,A8,A9,MESFUNC5:104;
A16: for x be Element of X st x in dom h holds h.x = |.h.|.x
proof
let x be Element of X;
assume x in dom h;
then
A17: x in dom |.h.| by MESFUNC1:def 10;
0 <= h.x by A13,SUPINF_2:51;
then |. h.x .| = h.x by EXTREAL1:def 1;
hence thesis by A17,MESFUNC1:def 10;
end;
Integral(M,h) = integral+(M,h) by A7,A13,MESFUNC5:89;
then integral+(M,h) < +infty by A1,A11,A8,A15,A12,A14,XXREAL_3:72;
then
A18: integral+(M,|.h.|) < +infty by A10,A16,PARTFUN1:5;
A19: dom max+h = dom h by MESFUNC2:def 2;
then
A20: max+h|E = max+h by A8,RELAT_1:68;
A21: max+h is E-measurable by A7,MESFUNC2:25,34;
for x be object st x in dom max-h holds 0. <= (max-h).x by MESFUNC2:13;
then
A22: max-h is nonnegative by SUPINF_2:52;
A23: K >= K1 by XXREAL_0:25;
A24: for n be Nat, x be set st x in dom(F.0) holds |. (F.n).x .| <= K
proof
let n be Nat, x be set;
assume x in dom(F.0);
then |. (F.n).x .| <= K1 by A6;
hence thesis by A23,XXREAL_0:2;
end;
A25: for x be Element of X, n be Nat st x in E holds (|. F.n .|).x <= h.x
proof
let x be Element of X, n be Nat;
assume
A26: x in E;
dom(F.n) = dom(|.(F.n).|) by MESFUNC1:def 10;
then x in dom(|.(F.n).|) by A2,A26,MESFUNC8:def 2;
then
A27: |. F.n .|.x = |. (F.n).x .| by MESFUNC1:def 10;
|. (F.n).x .| <= K by A2,A24,A26;
hence thesis by A9,A26,A27;
end;
for x be object st x in dom max+h holds 0. <= (max+h).x by MESFUNC2:12;
then
A28: max+h is nonnegative by SUPINF_2:52;
then
A29: dom(max+h + max-h) = dom max+h /\ dom max-h by A22,MESFUNC5:22;
A30: dom max-h = dom h by MESFUNC2:def 3;
then
A31: max-h|E = max-h by A8,RELAT_1:68;
max-h is E-measurable by A7,A8,MESFUNC2:26,34;
then ex C be Element of S st C = dom(max+h + max-h) & integral+(M,max+h +
max-h) = integral+(M,max+h|C) + integral+(M,max-h|C) by A8,A19,A30,A21,A28
,A22,MESFUNC5:78;
then
A32: integral+(M,max+h) + integral+(M,max-h) < +infty by A8,A19,A30,A29,A20,A31
,A18,MESFUNC2:24;
A33: for x be Element of X st x in dom(lim F) holds (lim F).x = (lim_inf F). x
proof
let x be Element of X;
assume
A34: x in dom(lim F);
then x in E by A2,MESFUNC8:def 9;
then F#x is convergent by A5;
hence thesis by A34,MESFUNC8:14;
end;
A35: dom(lim_inf F) = dom (F.0) by MESFUNC8:def 7;
A36: h is E-measurable by A7,MESFUNC2:34;
then 0 <= integral+(M,max-h) by A8,A30,A22,MESFUNC2:26,MESFUNC5:79;
then integral+(M,max+h) <> +infty by A32,XXREAL_3:def 2;
then
A37: integral+(M,max+h) < +infty by XXREAL_0:4;
0 <= integral+(M,max+h) by A8,A36,A19,A28,MESFUNC2:25,MESFUNC5:79;
then integral+(M,max-h) <> +infty by A32,XXREAL_3:def 2;
then integral+(M,max-h) < +infty by XXREAL_0:4;
then
A38: h is_integrable_on M by A8,A36,A37;
then
A39: ex I be ExtREAL_sequence st (for n be Nat holds I.n = Integral(M,F.n))
& lim_inf I >= Integral(M,lim_inf F) & lim_sup I <= Integral(M,lim_sup F) & ( (
for x be Element of X st x in E holds F#x is convergent) implies I is
convergent & lim I = Integral(M,lim F) ) by A2,A3,A8,A13,A25,Th17;
A40: now
let n be Nat;
A41: E = dom(F.n) by A2,MESFUNC8:def 2;
A42: F.n is E-measurable by A3;
|. F.n .| is_integrable_on M by A2,A3,A8,A38,A25,Th16;
hence F.n is_integrable_on M by A41,A42,MESFUNC5:100;
end;
A43: |. lim_inf F .| is_integrable_on M by A2,A3,A8,A38,A25,Th16;
dom(lim F) = dom (F.0) by MESFUNC8:def 9;
then
A44: lim F = lim_inf F by A35,A33,PARTFUN1:5;
then lim F is E-measurable by A2,A3,MESFUNC8:24;
hence thesis by A2,A5,A43,A40,A35,A44,A39,MESFUNC5:100;
end;
definition
let X be set, F be Functional_Sequence of X,ExtREAL, f be PartFunc of X,
ExtREAL;
pred F is_uniformly_convergent_to f means
F is with_the_same_dom &
dom(F.0) = dom f & for e be Real st e>0 ex N be Nat st for n be Nat, x
be set st n >= N & x in dom(F.0) holds |. (F.n).x - f.x .| < e;
end;
theorem Th20:
F1 is_uniformly_convergent_to f implies for x be Element of X st
x in dom(F1.0) holds F1#x is convergent & lim(F1#x) = f.x
proof
assume
A1: F1 is_uniformly_convergent_to f;
let x be Element of X;
assume
A2: x in dom(F1.0);
per cases by XXREAL_0:14;
suppose
f.x in REAL;
then reconsider g=f.x as Real;
A3: now
let e be Real;
assume 0 < e;
then consider N be Nat such that
A4: for n be Nat, x be set st n >= N & x in dom(F1.0) holds |. (F1.n
).x - f.x .| < e by A1;
take N;
hereby
let m be Nat;
assume N <= m;
then |. (F1.m).x - f.x .| < e by A2,A4;
hence |. (F1#x).m - g .| < e by MESFUNC5:def 13;
end;
end;
then
A5: F1#x is convergent_to_finite_number;
then F1#x is convergent;
hence thesis by A3,A5,MESFUNC5:def 12;
end;
suppose
A6: f.x = +infty;
now
let e be Real;
assume 0 < e;
then consider N be Nat such that
A7: for n be Nat, x be set st n >= N & x in dom(F1.0) holds |. (F1.
n).x - f.x .| < e by A1;
take N;
hereby
let n be Nat;
assume n >= N;
then |. (F1.n).x - f.x .| < e by A2,A7;
then
A8: |. -( (F1.n).x - f.x ) .| < e by EXTREAL1:29;
(F1.n).x = (F1#x).n by MESFUNC5:def 13;
then -( (F1#x).n - f.x ) < e by A8,EXTREAL1:21;
then f.x - (F1#x).n < e by XXREAL_3:26;
then (F1#x).n = +infty by A6,XXREAL_3:54;
hence e <= (F1#x).n by XXREAL_0:3;
end;
end;
then
A9: F1#x is convergent_to_+infty;
then F1#x is convergent;
hence thesis by A6,A9,MESFUNC5:def 12;
end;
suppose
A10: f.x = -infty;
now
let e be Real;
assume e < 0;
then -0 < -e by XREAL_1:24;
then consider N be Nat such that
A11: for n be Nat, x be set st n >= N & x in dom(F1.0) holds |. (F1.
n).x - f.x .| < -e by A1;
take N;
hereby
let n be Nat;
assume n >= N;
then
A12: |. (F1.n).x - f.x .| < -e by A2,A11;
(F1.n).x = (F1#x).n by MESFUNC5:def 13;
then (F1#x).n - f.x < -e by A12,EXTREAL1:21;
then (F1#x).n = -infty by A10,XXREAL_3:54;
hence e >= (F1#x).n by XXREAL_0:5;
end;
end;
then
A13: F1#x is convergent_to_-infty;
then F1#x is convergent;
hence thesis by A10,A13,MESFUNC5:def 12;
end;
end;
theorem
M.E < +infty & E = dom(F.0) & (for n be Nat holds F.n is_integrable_on
M) & F is_uniformly_convergent_to f implies f is_integrable_on M & ex I be
ExtREAL_sequence st (for n be Nat holds I.n = Integral(M,F.n)) & I is
convergent & lim I = Integral(M,f)
proof
assume that
A1: M.E < +infty and
A2: E = dom(F.0) and
A3: for n be Nat holds F.n is_integrable_on M and
A4: F is_uniformly_convergent_to f;
reconsider e = 1/2 as Real;
consider N be Nat such that
A5: for n be Nat, x be set st n >= N & x in dom(F.0)
holds |. (F.n).x - f.x .| < e by A4;
reconsider N1=N as Nat;
consider h be PartFunc of X,ExtREAL such that
A6: h is_simple_func_in S and
A7: dom h = E and
A8: for x be object st x in E holds h.x=1. by MESFUNC5:41;
A9: max-h is E-measurable by A6,A7,MESFUNC2:26,34;
for x be object st x in E holds h.x >= 0. by A8;
then
A10: h is nonnegative by A7,SUPINF_2:52;
then
A11: Integral(M,h) = integral'(M,h) by A6,MESFUNC5:89;
set AFN = |. F.N .|;
A12: dom(F.N) = dom AFN by MESFUNC1:def 10;
now
let x be object;
assume x in dom AFN;
then AFN.x = |. (F.N).x .| by MESFUNC1:def 10;
hence 0 <= AFN.x by EXTREAL1:14;
end;
then
A13: AFN is nonnegative by SUPINF_2:52;
then
A14: dom(AFN + h) = dom AFN /\ dom h by A10,MESFUNC5:22;
A15: for x be set st x in dom(F.0) holds |. (F.N).x - f.x .| < 1/2 by A5;
A16: now
let x be set, n be Nat;
assume that
A17: n >= N and
A18: x in dom(F.0);
A19: |. (F.n).x - f.x .| < jj/2 by A5,A17,A18;
A20: |. (F.N).x - f.x .| < jj/2 by A5,A18;
A21: now
A22: |. (F.n).x - f.x .| < 1 by A19,XXREAL_0:2;
then
A23: (F.n).x - f.x < 1. by EXTREAL1:21;
A24: |. (F.N).x - f.x .| < 1 by A20,XXREAL_0:2;
then
A25: -1. < (F.N).x - f.x by EXTREAL1:21;
A26: (F.N).x - f.x < 1. by A24,EXTREAL1:21;
assume
A27: f.x = +infty or f.x = -infty;
-1. < (F.n).x - f.x by A22,EXTREAL1:21;
then (F.n).x = +infty & (F.N).x = +infty or (F.n).x = -infty & (F.N).x
= -infty by A27,A25,A23,A26,XXREAL_3:53,54;
hence |. (F.n).x .| <= |. (F.N).x .| + 1. by EXTREAL1:30,XXREAL_3:52;
end;
dom(AFN + h) = dom AFN /\ dom h by A10,A13,MESFUNC5:22;
then dom(AFN + h) = E /\ E by A2,A7,A12,MESFUNC8:def 2;
then AFN.x + h.x = (AFN + h).x by A2,A18,MESFUNC1:def 3;
then
A28: AFN.x + 1. = (AFN + h).x by A2,A8,A18;
dom(F.n) = E by A2,MESFUNC8:def 2;
then
A29: x in dom |. F.n .| by A2,A18,MESFUNC1:def 10;
A30: now
A31: 0 <= |. (F.n).x - f.x .| by EXTREAL1:14;
A32: jj/2 in REAL by XREAL_0:def 1;
then |. (F.n).x - f.x .| < +infty by A19,XXREAL_0:2,9;
then reconsider a = |. (F.n).x - f.x .| as Element of REAL
by A31,XXREAL_0:14;
|. f.x - (F.N).x .| < jj/2 by A20,MESFUNC5:1;
then
A33: |. f.x - (F.N).x .| < +infty by XXREAL_0:2,9,A32;
0 <= |. f.x - (F.N).x .| by EXTREAL1:14;
then reconsider b = |. f.x - (F.N).x .| as Element of REAL
by A33,XXREAL_0:14;
assume
A34: f.x in REAL;
A35: now
assume (F.N).x = +infty or (F.N).x = -infty;
then (F.N).x - f.x = +infty or (F.N).x - f.x = -infty by A34,
XXREAL_3:13,14;
then jj < |. (F.N).x - f.x .| by EXTREAL1:30,XXREAL_0:9;
hence contradiction by A15,A18,XXREAL_0:2;
end;
A36: now
assume (F.n).x = +infty or (F.n).x = -infty;
then (F.n).x - f.x = +infty or (F.n).x - f.x = -infty by A34,
XXREAL_3:13,14;
hence contradiction by A19,EXTREAL1:30,XXREAL_0:9,A32;
end;
then (F.n).x in REAL by XXREAL_0:14;
then
A37: |. (F.n).x .| - |. (F.N).x .| <= |. (F.n).x - (F.N).x .| by EXTREAL1:31;
b <= 1/2 by A20,MESFUNC5:1;
then a + b < 1/2 + 1/2 by A19,XREAL_1:8;
then
A38: |. (F.n).x - f.x .| + |. f.x - (F.N).x .| < 1 by SUPINF_2:1;
-f.x + f.x = 0. by XXREAL_3:7;
then (F.n).x - (F.N).x = (F.n).x + (-f.x + f.x) - (F.N).x by XXREAL_3:4;
then (F.n).x - (F.N).x = (F.n).x + -f.x + f.x - (F.N).x by A34,A36,
XXREAL_3:29;
then (F.n).x - (F.N).x = (F.n).x - f.x + (f.x - (F.N).x) by A34,A35,
XXREAL_3:30;
then |. (F.n).x - (F.N).x .| <= |. (F.n).x - f.x .| + |. f.x - (F.N).x
.| by EXTREAL1:24;
then |. (F.n).x - (F.N).x .| < 1 by A38,XXREAL_0:2;
then |. (F.n).x .| - |. (F.N).x .| <= 1. by A37,XXREAL_0:2;
hence |. (F.n).x .| <= |. (F.N).x .| + 1. by XXREAL_3:52;
end;
x in dom AFN by A12,A18,MESFUNC8:def 2;
then |. (F.n).x .| <= AFN.x + 1. by A30,A21,MESFUNC1:def 10,XXREAL_0:14;
hence (|. F.n .|).x <= (AFN + h).x by A28,A29,MESFUNC1:def 10;
end;
A39: for x be Element of X, n be Nat st x in E holds (|.(F^\N1).n.|).x <= (
AFN + h).x
proof
let x be Element of X, n be Nat;
A40: (F^\N1).n = F.(n+N) by NAT_1:def 3;
assume x in E;
hence thesis by A2,A16,A40,NAT_1:11;
end;
A41: max+h is E-measurable by A6,MESFUNC2:25,34;
for x be object st x in dom max-h holds 0. <= (max-h).x by MESFUNC2:13;
then
A42: max-h is nonnegative by SUPINF_2:52;
A43: for n be Nat holds F.n is E-measurable
proof
let n be Nat;
F.n is_integrable_on M by A3;
then consider A be Element of S such that
AA: A = dom(F.n) & (F.n) is A-measurable;
for r being Real holds E /\ less_dom(F.n,r) in S
proof
let r be Real;
E = dom (F.n) by A2,MESFUNC8:def 2; then
E = A by AA;
hence thesis by AA;
end;
hence thesis;
end;
(F^\N1).0 = F.(0+N) by NAT_1:def 3;
then
A45: dom((F^\N1).0) = E by A2,MESFUNC8:def 2;
A46: now
let x be Element of X;
assume x in dom f;
then
A47: x in dom(F.0) by A4;
then
A48: x in dom(lim F) by MESFUNC8:def 9;
lim(F#x) = f.x by A4,A47,Th20;
hence (lim F).x = f.x by A48,MESFUNC8:def 9;
end;
dom f = dom(F.0) by A4;
then dom(lim F) = dom f by MESFUNC8:def 9;
then
A49: lim F = f by A46,PARTFUN1:5;
F.N is_integrable_on M by A3; then
A51: AFN is_integrable_on M by MESFUNC5:100;
deffunc I(Nat) = Integral(M,F.$1);
A52: 1 * +infty = +infty by XXREAL_3:def 5;
A53: now
let x be Element of X;
assume x in dom h;
then
A54: x in dom(|.h.|) by MESFUNC1:def 10;
0 <= h.x by A10,SUPINF_2:51;
then |. h.x .| = h.x by EXTREAL1:def 1;
hence |.h.|.x = h.x by A54,MESFUNC1:def 10;
end;
dom h = dom(|.h.|) by MESFUNC1:def 10;
then
A55: h = |.h.| by A53,PARTFUN1:5;
Integral(M,h) = integral+(M,h) by A6,A10,MESFUNC5:89;
then integral+(M,h) = jj * M.(dom h) by A7,A8,A11,MESFUNC5:104;
then
A56: integral+(M,|.h.|) < +infty by A1,A7,A55,A52,XXREAL_3:72;
A57: for n be Nat holds (F^\N1).n is E-measurable
proof
let n be Nat;
(F^\N1).n = F.(n+N) by NAT_1:def 3;
hence thesis by A43;
end;
A58: for x be Element of X st x in E holds (F^\N1)#x is convergent & lim(F#x
) = lim((F^\N1)#x)
proof
let x be Element of X;
A59: now
let n be Element of NAT;
((F^\N1)#x).n = ((F^\N1).n).x by MESFUNC5:def 13;
then ((F^\N1)#x).n = (F.(n+N)).x by NAT_1:def 3;
then ((F^\N1)#x).n = (F#x).(n+N) by MESFUNC5:def 13;
hence ((F^\N1)#x).n = ((F#x)^\N1).n by NAT_1:def 3;
end;
assume x in E;
then
A60: F#x is convergent by A2,A4,Th20;
then (F#x)^\N1 is convergent by RINFSUP2:21;
hence (F^\N1)#x is convergent by A59,FUNCT_2:63;
lim(F#x) = lim((F#x)^\N1) by A60,RINFSUP2:21;
hence thesis by A59,FUNCT_2:63;
end;
then for x be Element of X st x in E holds (F^\N1)#x is convergent;
then
A61: lim(F^\N1) is E-measurable by A57,A45,MESFUNC8:25;
dom(lim(F^\N1)) = E by A45,MESFUNC8:def 9;
then
A62: dom(lim F) = dom(lim(F^\N1)) by A2,MESFUNC8:def 9;
A63: now
let x be Element of X;
assume
A64: x in dom(lim F);
then x in E by A2,MESFUNC8:def 9;
then
A65: lim(F#x) = lim((F^\N1)#x) by A58;
lim((F^\N1)#x) = (lim (F^\N1)).x by A62,A64,MESFUNC8:def 9;
hence (lim F).x = (lim (F^\N1)).x by A64,A65,MESFUNC8:def 9;
end;
A66: dom max-h = dom h by MESFUNC2:def 3;
then
A67: max-h|E = max-h by A7,RELAT_1:68;
A68: dom max+h = dom h by MESFUNC2:def 2;
then
A69: max+h|E = max+h by A7,RELAT_1:68;
for x be object st x in dom max+h holds 0. <= (max+h).x by MESFUNC2:12;
then
A70: max+h is nonnegative by SUPINF_2:52;
then dom(max+h + max-h) = dom max+h /\ dom max-h by A42,MESFUNC5:22;
then
ex C be Element of S st C = E & integral+(M,max+h + max-h) = integral+(
M,max+h|C) + integral+(M,max-h|C) by A7,A41,A9,A70,A42,A68,A66,MESFUNC5:78;
then
A71: integral+(M,|.h.|) = integral+(M,max+h) + integral+(M,max-h) by A69,A67,
MESFUNC2:24;
A72: h is E-measurable by A6,MESFUNC2:34;
then 0 <= integral+(M,max-h) by A7,A42,A66,MESFUNC2:26,MESFUNC5:79;
then integral+(M,max+h) <> +infty by A71,A56,XXREAL_3:def 2;
then
A73: integral+(M,max+h) < +infty by XXREAL_0:4;
0 <= integral+(M,max+h) by A7,A72,A70,A68,MESFUNC2:25,MESFUNC5:79;
then integral+(M,max-h) <> +infty by A71,A56,XXREAL_3:def 2;
then integral+(M,max-h) < +infty by XXREAL_0:4;
then h is_integrable_on M by A7,A72,A73;
then
A74: AFN + h is_integrable_on M by A51,MESFUNC5:108;
A75: E = dom AFN by A2,A12,MESFUNC8:def 2;
then
A76: |. lim_inf(F^\N1) .| is_integrable_on M by A7,A74,A14,A39,A57,A45,Th16;
AFN + h is nonnegative by A10,A13,MESFUNC5:22;
then consider J be ExtREAL_sequence such that
A77: for n be Nat holds J.n = Integral(M,(F^\N1).n) and
lim_inf J >= Integral(M,lim_inf (F^\N1)) and
lim_sup J <= Integral(M,lim_sup (F^\N1)) and
A78: (for x be Element of X st x in E holds (F^\N1)#x is convergent)
implies J is convergent & lim J = Integral(M,lim (F^\N1)) by A7,A74,A14,A75
,A39,A57,A45,Th17;
consider I be sequence of ExtREAL such that
A79: for n be Element of NAT holds I.n = I(n) from FUNCT_2:sch 4;
reconsider I as ExtREAL_sequence;
A80: dom lim_inf(F^\N1) = dom((F^\N1).0) by MESFUNC8:def 7;
A81: now
let x be Element of X;
assume
A82: x in dom(lim(F^\N1));
then x in E by A45,MESFUNC8:def 9;
then (F^\N1)#x is convergent by A58;
hence (lim(F^\N1)).x = (lim_inf(F^\N1)).x by A82,MESFUNC8:14;
end;
dom lim(F^\N1) = dom((F^\N1).0) by MESFUNC8:def 9;
then lim(F^\N1) = lim_inf(F^\N1) by A80,A81,PARTFUN1:5;
then
A83: lim(F^\N1) is_integrable_on M by A45,A76,A80,A61,MESFUNC5:100;
A84: for n be Nat holds I.n = Integral(M,F.n)
proof
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A79;
end;
now
let n be Element of NAT;
A85: (F^\N1).n = F.(n+N) by NAT_1:def 3;
A86: (I^\N1).n = I.(n+N) by NAT_1:def 3;
reconsider nn=n+N as Element of NAT by ORDINAL1:def 12;
thus J.n = Integral(M,(F^\N1).n) by A77
.= I.nn by A79,A85
.= (I^\N1).n by A86;
end;
then
A87: J = I^\N1 by FUNCT_2:63;
then
A88: I is convergent by A58,A78,RINFSUP2:17;
lim I = lim J by A58,A78,A87,RINFSUP2:17;
then lim I = Integral(M,lim F) by A58,A62,A63,A78,PARTFUN1:5;
hence thesis by A49,A62,A63,A83,A84,A88,PARTFUN1:5;
end;