:: 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 Association of Mizar Users
environ
vocabularies PARTFUN1, MEASURE1, RELAT_1, FUNCT_1, ORDINAL2, COMPLEX1, SEQ_1,
SEQ_2, MEASURE6, BOOLE, ARYTM, ARYTM_1, MESFUNC1, ARYTM_3, RLVECT_1,
GROUP_1, PROB_1, INTEGRA1, MESFUNC2, MESFUNC5, SUPINF_1, SUPINF_2,
SEQFUNC, TDGROUP, RFUNCT_3, MESFUNC8, SEQM_3, RINFSUP1, MESFUN10,
XXREAL_2, SQUARE_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, XXREAL_0, XXREAL_2, RELAT_1, FUNCT_1, RELSET_1, DOMAIN_1, SEQM_3,
FUNCT_2, PARTFUN1, NAT_1, PROB_1, SUPINF_1, SUPINF_2, KURATO_2, MEASURE1,
EXTREAL1, MESFUNC1, MEASURE6, MESFUNC2, SEQFUNC, MESFUNC5, MESFUNC8,
RINFSUP2;
constructors REAL_1, DOMAIN_1, NAT_1, KURATO_2, EXTREAL1, MESFUNC1, MEASURE6,
MESFUNC2, MESFUNC5, RINFSUP2, EXTREAL2, XXREAL_2, MESFUNC9, SUPINF_1;
registrations SUPINF_1, NAT_1, XREAL_0, MEMBERED, ORDINAL1, PARTFUN1,
MEASURE1, RELAT_1, XBOOLE_0, SUPINF_2, NUMBERS, XXREAL_0, MESFUNC8,
RINFSUP2, VALUED_0, XXREAL_2, FINSET_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions SUPINF_2, MESFUNC1, MEASURE6, XXREAL_0, MESFUNC8, RINFSUP2;
theorems TARSKI, PARTFUN1, FUNCT_1, SUPINF_2, EXTREAL1, EXTREAL2, MESFUNC1,
XREAL_0, XBOOLE_0, XBOOLE_1, MESFUNC2, XREAL_1, XXREAL_0, MESFUNC5,
NAT_1, RELAT_1, FUNCT_2, SEQFUNC, ORDINAL1, MESFUNC8, RINFSUP2, KURATO_2,
MESFUNC7, MESFUNC9, NUMBERS, XXREAL_2;
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 Th61a:
(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 ext-real number;
assume x in rng seq2; then
A2: ex z be set st z in dom seq2 & x=seq2.z by FUNCT_1:def 5;
now let n be Element of NAT;
A3: inf rng seq1 is LowerBound of rng seq1 by XXREAL_2:def 4;
dom seq1 = NAT by FUNCT_2:def 1; then
seq1.n in rng seq1 by FUNCT_1:def 5; then
A4: inf rng seq1 <= seq1.n by A3,XXREAL_2:def 2;
seq1.n <= seq2.n by A1;
hence inf rng seq1 <= seq2.n by A4,XXREAL_0:2;
end;
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 limseq1b:
(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
assume A1: for n be Nat holds seq1.n <= seq2.n;
reconsider k1 = k as Element of NAT by ORDINAL1:def 13;
now let n be Nat;
n is Element of NAT by ORDINAL1:def 13; then
(seq1^\k1).n = seq1.(n+k) & (seq2^\k1).n = seq2.(n+k)
by KURATO_2:def 2;
hence (seq1^\k1).n <= (seq2^\k1).n by A1;
end; then
inf(seq1^\k1) <= inf(seq2^\k1) &
sup(seq1^\k1) <= sup(seq2^\k1) by Th61a,MESFUNC5:61; then
(inferior_realsequence seq1).k <= inf(seq2^\k1) &
(superior_realsequence seq1).k <= sup(seq2^\k1) by RINFSUP2:27;
hence thesis by RINFSUP2:27;
end;
theorem limseq1:
(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 limseq1b;
hence thesis by Th61a,MESFUNC5:61;
end;
theorem Th63a:
(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 ext-real number;
assume x in rng seq; then
consider z be set such that
A2: z in dom seq and
A3: x = seq.z by FUNCT_1:def 5;
thus x >= a by A1,A3,A2;
end; then
a is LowerBound of rng seq by XXREAL_2:def 2;
hence thesis by XXREAL_2:def 4;
end;
theorem Th63b:
(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 ext-real number;
assume x in rng seq; then
consider z be set such that
A2: z in dom seq and
A3: x = seq.z by FUNCT_1:def 5;
thus x <= a by A1,A2,A3;
end; then
a is UpperBound of rng seq by XXREAL_2:def 1;
hence thesis by XXREAL_2:def 3;
end;
theorem inferiorf1a:
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;
assume A1: x in dom inf(F^\n);
now let k be Element of NAT;
reconsider g=F as Function of NAT,PFuncs(X,ExtREAL);
((F^\n)#x).k =((F^\n).k).x by MESFUNC5:def 13; then
((F^\n)#x).k = (g.(n+k)).x by KURATO_2:def 2; then
((F^\n)#x).k =(F#x).(n+k) by MESFUNC5:def 13;
hence ((F^\n)#x).k = ((F#x)^\n).k by KURATO_2:def 2;
end; then
(F^\n)#x = (F#x)^\n by FUNCT_2:113;
hence (inf(F^\n)).x =inf((F#x)^\n) by MESFUNC8:def 3,A1;
end;
reserve S for SigmaField of X,
M for sigma_Measure of S,
E for Element of S;
:: Fatou's Lemma
theorem Th135:
E = dom(F.0) &
(for n holds F.n is nonnegative & F.n is_measurable_on E) 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_measurable_on E;
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 Element of NAT;
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 SEQFUNC:2;
set H = inferior_realsequence F;
reconsider G as with_the_same_dom Functional_Sequence of X,ExtREAL
by A4,SEQFUNC:2;
A6:dom(H.0) = dom(F.0) & dom(H.0) = dom(G.0) by A4,MESFUNC8:def 5;
for x be set st x in dom(G.0) holds 0 <= (G.0).x
proof
let x be set;
assume P11: x in dom(G.0); then
reconsider x as Element of X;
P12:now let n be Nat;
F.n is nonnegative by A2; then
0 <= (F.n).x by SUPINF_2:70; then
0 <= (F#x).(0+n) by MESFUNC5:def 13;
hence 0. <= ((F#x)^\0).n by KURATO_2:def 2;
end;
(F^\0).0 = F.(0+0) by KURATO_2:def 2; then
dom inf(F^\0) = dom(F.0) by MESFUNC8:def 3; then
(inf(F^\0)).x =inf((F#x)^\0) by P11,A6,inferiorf1a;
then (G.0).x = inf((F#x)^\0) by A3;
hence thesis by P12,Th63a;
end; then
P1:G.0 is nonnegative by SUPINF_2:71;
P2:for n be Nat holds G.n is_measurable_on E by A1,A2,A5,MESFUNC8:20;
P3: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 13;
assume P31: n <= m & x in E; then
H#x = inferior_realsequence(F#x) by A1,MESFUNC8:7; then
(H#x).n1 <= (H#x).m1 by P31,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 (G#x).n <= (G#x).m by MESFUNC5:def 13;
end; then
PP: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;
now let x be Element of X;
assume x in E; then
for n,m be Element of NAT st m <= n holds (G#x).m <= (G#x).n by P3; then
G#x is non-decreasing by RINFSUP2:7;
hence G#x is convergent by RINFSUP2:37;
end; then
consider J be ExtREAL_sequence such that
P4: (for n be Nat holds J.n = Integral(M,G.n)) &
J is convergent & Integral(M,lim G) = lim J
by A1,A6,P1,P2,PP,MESFUNC9:52;
deffunc I(Element of NAT) = Integral(M,F.$1);
consider I be Function of NAT,ExtREAL such that
P5: for n be Element of NAT holds I.n = I(n) from FUNCT_2:sch 4;
reconsider I as ExtREAL_sequence;
take I;
P6:for n be Nat holds I.n = Integral(M,F.n)
proof
let n be Nat;
n is Element of NAT by ORDINAL1:def 13;
hence I.n = Integral(M,F.n) by P5;
end;
P7:dom lim G = E & dom sup G = E by A1,A6,MESFUNC8:def 4,def 10;
now let x be Element of X;
assume P81: x in dom lim G; then
for n,m be Element of NAT st m <= n holds (G#x).m <= (G#x).n by P7,P3; then
G#x is non-decreasing by RINFSUP2:7; then
P82:lim(G#x) = sup(G#x) by RINFSUP2:37;
(sup G).x = sup(G#x) by P81,P7,MESFUNC8:def 4;
hence (lim G).x = (sup G).x by P82,P81,MESFUNC8:def 10;
end; then
P8:lim G = sup G by P7,PARTFUN1:34;
for n be Nat holds J.n <= I.n
proof
let n be Nat;
Q1: dom(F.n) = E & dom(G.n) = E by A1,A6,MESFUNC8:def 2;
Q2: F.n is_measurable_on E & G.n is_measurable_on E by A1,A2,A5,MESFUNC8:20;
Q3: F.n is nonnegative by A2;
q4: now let x be set;
assume Q41: x in dom(G.n);
0 <= (G.0).x by P1,SUPINF_2:70;
hence 0 <= (G.n).x by Q41,Q1,P3;
end; then
Q4: G.n is nonnegative by SUPINF_2:71;
Q0: n is Element of NAT by ORDINAL1:def 13; then
Q5: I.n = Integral(M,F.n) by P5;
now let x be Element of X;
assume P01:x in dom(G.n);
(inferior_realsequence(F#x)).n <= (F#x).n by Q0,RINFSUP2:8; then
(H.n).x <= (F#x).n by P01,A5,MESFUNC8:def 5; then
(H.n).x <= (F.n).x by MESFUNC5:def 13;
hence (G.n).x <= (F.n).x by A4,Q0;
end; then
integral+(M,G.n) <= integral+(M,F.n) by Q1,Q2,Q3,Q4,MESFUNC5:91; then
Integral(M,G.n) <= integral+(M,F.n)
by Q1,Q2,q4,MESFUNC5:94,SUPINF_2:71; then
Integral(M,G.n) <= Integral(M,F.n) by Q1,Q2,Q3,MESFUNC5:94;
hence J.n <= I.n by Q5,P4;
end; then
lim_inf J <= lim_inf I by limseq1; then
lim J <= lim_inf I by P4,RINFSUP2:41;
hence thesis by P6,P4,P8,A5,MESFUNC8:11;
end;
begin :: Lebesgue's Convergence Theorem
theorem SUPINF226a:
for X,Y being non empty Subset of ExtREAL, r be R_eal st
X = {r} & r in REAL holds sup(X + Y) = sup X + sup Y
proof
let X,Y be non empty Subset of ExtREAL;
let r be R_eal;
assume that
A1: X = {r} and
A2: r in REAL;
A5:sup(X + Y) <= sup X + sup Y by SUPINF_2:26;
set W = X+Y;
A8:-r <> +infty & -r <> -infty by A2,EXTREAL1:4;
A61:r in X by A1,TARSKI:def 1;
now let z be set;
assume A60: z in Y; then
reconsider y = z as Element of ExtREAL;
A62:r + y in W by A61,A60,SUPINF_2:def 5;
A63:-r in -X by A61,SUPINF_2:def 6;
r + y - r = (-r + r) + y by A2,A8,EXTREAL1:8; then
r + y - r = 0. + y by EXTREAL1:9; then
y = r + y - r by SUPINF_2:18;
hence z in -X + W by A62,A63,SUPINF_2:def 5;
end; then
A64:Y c= -X + W by TARSKI:def 3;
now let z be set;
assume z in -X + W; then
consider x,y be R_eal such that
A65: x in -X & y in W & z = x + y by SUPINF_2:def 5;
-x in --X by A65,SUPINF_2:23; then
-x in X by SUPINF_2:22; then
A66:-x = r by A1,TARSKI:def 1;
consider x1,y1 be R_eal such that
A67: x1 in X & y1 in Y & y = x1 + y1 by A65,SUPINF_2:def 5;
z = -r + (r + y1) by A65,A66,A1,A67,TARSKI:def 1; then
z = (-r + r) + y1 by A2,A8,EXTREAL1:8; then
z = 0. + y1 by EXTREAL1:9;
hence z in Y by A67,SUPINF_2:18;
end; then
-X + W c= Y by TARSKI:def 3; then
A6:Y = -X + W by A64,XBOOLE_0:def 10;
sup Y <= sup W + sup -X by A6,SUPINF_2:26; then
sup Y <= sup(X+Y) + -inf X by SUPINF_2:33; then
sup Y <= sup(X+Y) -r by A1,XXREAL_2:13; then
r + sup Y <= sup(X+Y) by A2,EXTREAL2:32; then
sup X + sup Y <= sup(X+Y) by A1,XXREAL_2:11;
hence sup(X+Y) = sup X + sup Y by A5,XXREAL_0:1;
end;
theorem SUPINF227a:
for X,Y being non empty Subset of ExtREAL, r be R_eal st
X = {r} & r in REAL holds inf(X + Y) = inf X + inf Y
proof
let X,Y be non empty Subset of ExtREAL;
let r be R_eal;
assume that
A1: X = {r} and
A2: r in REAL;
A5:inf(X + Y) >= inf X + inf Y by SUPINF_2:27;
set Z = -X;
set W = X+Y;
A8:-r <> +infty & -r <> -infty by A2,EXTREAL1:4;
A61:r in X by A1,TARSKI:def 1;
now let z be set;
assume A60: z in Y; then
reconsider y = z as Element of ExtREAL;
A62:r + y in W by A61,A60,SUPINF_2:def 5;
A63:-r in Z by A61,SUPINF_2:def 6;
r + y - r = (-r + r) + y by A2,A8,EXTREAL1:8; then
r + y - r = 0. + y by EXTREAL1:9; then
y = r + y - r by SUPINF_2:18;
hence z in Z + W by A62,A63,SUPINF_2:def 5;
end; then
A64:Y c= Z + W by TARSKI:def 3;
now let z be set;
assume z in Z + W; then
consider x,y be R_eal such that
A65: x in Z & y in W & z = x + y by SUPINF_2:def 5;
-x in -Z by A65,SUPINF_2:23; then
-x in X by SUPINF_2:22; then
A66:-x = r by A1,TARSKI:def 1;
consider x1,y1 be R_eal such that
A67: x1 in X & y1 in Y & y = x1 + y1 by A65,SUPINF_2:def 5;
z = -r + (r + y1) by A65,A66,A1,A67,TARSKI:def 1; then
z = (-r + r) + y1 by A2,A8,EXTREAL1:8; then
z = 0. + y1 by EXTREAL1:9;
hence z in Y by A67,SUPINF_2:18;
end; then
Z + W c= Y by TARSKI:def 3; then
A6:Y = Z + W by A64,XBOOLE_0:def 10;
inf Y >= inf W + inf Z by A6,SUPINF_2:27; then
inf Y >= inf(X+Y) + -sup X by SUPINF_2:32; then
inf Y >= inf(X+Y) -r by A1,XXREAL_2:11; then
r + inf Y >= inf(X+Y) by A2,EXTREAL2:27; then
inf X + inf Y >= inf(X+Y) by A1,XXREAL_2:13;
hence inf(X+Y) = inf X + inf Y by A5,XXREAL_0:1;
end;
theorem limseq2:
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
A0: r in REAL and
A1: 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 set;
assume z in R1; then
consider n be set such that
B1: n in NAT & (inferior_realsequence seq1).n = z by FUNCT_2:17;
reconsider n as Element of NAT by B1;
consider Y1 be non empty Subset of ExtREAL such that
B2: Y1 = {seq1.k where k is Element of NAT : n <= k} &
z = inf Y1 by B1,RINFSUP2:def 6;
consider Y2 be non empty Subset of ExtREAL such that
B21: Y2 = {seq2.k where k is Element of NAT : n <= k} &
(inferior_realsequence seq2).n = inf Y2 by RINFSUP2:def 6;
now let w be set;
assume w in Y1; then
consider k1 be Element of NAT such that
B3: w = seq1.k1 & n <= k1 by B2;
reconsider w1=w as R_eal by B3;
B4: w1 = r + seq2.k1 by A1,B3;
r in {r} & seq2.k1 in Y2 by TARSKI:def 1,B3,B21;
hence w in {r} + Y2 by B4,SUPINF_2:def 5;
end; then
B6: Y1 c= {r} + Y2 by TARSKI:def 3;
now let w be set;
assume w in {r} + Y2; then
consider w1,w2 be R_eal such that
B7: w1 in {r} & w2 in Y2 & w = w1 + w2 by SUPINF_2:def 5;
consider k2 be Element of NAT such that
B8: w2 = seq2.k2 & n <= k2 by B21,B7;
w1 = r by B7,TARSKI:def 1; then
w = seq1.k2 by A1,B7,B8;
hence w in Y1 by B2,B8;
end; then
{r} + Y2 c= Y1 by TARSKI:def 3; then
Y1 = {r} + Y2 by B6,XBOOLE_0:def 10; then
inf Y1 = inf{r} + inf Y2 by A0,SUPINF227a; then
B9: inf Y1 = r + inf Y2 by XXREAL_2:13;
r in {r} &
(inferior_realsequence seq2).n in R2 by TARSKI:def 1,FUNCT_2:6;
hence z in {r} + R2 by B9,B2,B21,SUPINF_2:def 5;
end; then
B9:R1 c= {r} + R2 by TARSKI:def 3;
now let z be set;
assume z in {r} + R2; then
consider z2,z3 be R_eal such that
C2: z2 in {r} & z3 in R2 & z = z2 + z3 by SUPINF_2:def 5;
consider n be set such that
C3: n in NAT & (inferior_realsequence seq2).n = z3 by C2,FUNCT_2:17;
reconsider n as Element of NAT by C3;
consider Y2 be non empty Subset of ExtREAL such that
C4: Y2 = {seq2.k where k is Element of NAT : n <= k} &
z3 = inf Y2 by C3,RINFSUP2:def 6;
consider Y1 be non empty Subset of ExtREAL such that
C5: Y1 = {seq1.k where k is Element of NAT : n <= k} &
(inferior_realsequence seq1).n = inf Y1 by RINFSUP2:def 6;
now let w be set;
assume w in Y1; then
consider k1 be Element of NAT such that
B3: w = seq1.k1 & n <= k1 by C5;
reconsider w1=w as R_eal by B3;
B4: w1 = r + seq2.k1 by A1,B3;
r in {r} & seq2.k1 in Y2 by TARSKI:def 1,B3,C4;
hence w in {r} + Y2 by B4,SUPINF_2:def 5;
end; then
B6: Y1 c= {r} + Y2 by TARSKI:def 3;
now let w be set;
assume w in {r} + Y2; then
consider w1,w2 be R_eal such that
B7: w1 in {r} & w2 in Y2 & w = w1 + w2 by SUPINF_2:def 5;
consider k2 be Element of NAT such that
B8: w2 = seq2.k2 & n <= k2 by C4,B7;
w1 = r by B7,TARSKI:def 1; then
w = seq1.k2 by A1,B7,B8;
hence w in Y1 by C5,B8;
end; then
{r} + Y2 c= Y1 by TARSKI:def 3; then
Y1 = {r} + Y2 by B6,XBOOLE_0:def 10; then
inf Y1 = inf{r} + inf Y2 by A0,SUPINF227a; then
inf Y1 = r + inf Y2 by XXREAL_2:13; then
z = (inferior_realsequence seq1).n by C2,C4,C5,TARSKI:def 1;
hence z in R1 by FUNCT_2:6;
end; then
{r} + R2 c= R1 by TARSKI:def 3; then
R1 = {r} + R2 by B9,XBOOLE_0:def 10; then
sup R1 = sup {r} + sup R2 by A0,SUPINF226a;
hence lim_inf seq1 = r + lim_inf seq2 by XXREAL_2:11;
now let z be set;
assume z in P1; then
consider n be set such that
B1: n in NAT & (superior_realsequence seq1).n = z by FUNCT_2:17;
reconsider n as Element of NAT by B1;
consider Y1 be non empty Subset of ExtREAL such that
B2: Y1 = {seq1.k where k is Element of NAT : n <= k} &
z = sup Y1 by B1,RINFSUP2:def 7;
consider Y2 be non empty Subset of ExtREAL such that
B21: Y2 = {seq2.k where k is Element of NAT : n <= k} &
(superior_realsequence seq2).n = sup Y2 by RINFSUP2:def 7;
now let w be set;
assume w in Y1; then
consider k1 be Element of NAT such that
B3: w = seq1.k1 & n <= k1 by B2;
reconsider w1=w as R_eal by B3;
B4: w1 = r + seq2.k1 by A1,B3;
r in {r} & seq2.k1 in Y2 by TARSKI:def 1,B3,B21;
hence w in {r} + Y2 by B4,SUPINF_2:def 5;
end; then
B6: Y1 c= {r} + Y2 by TARSKI:def 3;
now let w be set;
assume w in {r} + Y2; then
consider w1,w2 be R_eal such that
B7: w1 in {r} & w2 in Y2 & w = w1 + w2 by SUPINF_2:def 5;
consider k2 be Element of NAT such that
B8: w2 = seq2.k2 & n <= k2 by B21,B7;
w1 = r by B7,TARSKI:def 1; then
w = seq1.k2 by A1,B7,B8;
hence w in Y1 by B2,B8;
end; then
{r} + Y2 c= Y1 by TARSKI:def 3; then
Y1 = {r} + Y2 by B6,XBOOLE_0:def 10; then
sup Y1 = sup{r} + sup Y2 by A0,SUPINF226a; then
B9: sup Y1 = r + sup Y2 by XXREAL_2:11;
r in {r} &
(superior_realsequence seq2).n in P2 by TARSKI:def 1,FUNCT_2:6;
hence z in {r} + P2 by B9,B2,B21,SUPINF_2:def 5;
end; then
B9:P1 c= {r} + P2 by TARSKI:def 3;
now let z be set;
assume z in {r} + P2; then
consider z2,z3 be R_eal such that
C2: z2 in {r} & z3 in P2 & z = z2 + z3 by SUPINF_2:def 5;
consider n be set such that
C3: n in NAT & (superior_realsequence seq2).n = z3 by C2,FUNCT_2:17;
reconsider n as Element of NAT by C3;
consider Y2 be non empty Subset of ExtREAL such that
C4: Y2 = {seq2.k where k is Element of NAT : n <= k} &
z3 = sup Y2 by C3,RINFSUP2:def 7;
consider Y1 be non empty Subset of ExtREAL such that
C5: Y1 = {seq1.k where k is Element of NAT : n <= k} &
(superior_realsequence seq1).n = sup Y1 by RINFSUP2:def 7;
now let w be set;
assume w in Y1; then
consider k1 be Element of NAT such that
B3: w = seq1.k1 & n <= k1 by C5;
reconsider w1=w as R_eal by B3;
B4: w1 = r + seq2.k1 by A1,B3;
r in {r} & seq2.k1 in Y2 by TARSKI:def 1,B3,C4;
hence w in {r} + Y2 by B4,SUPINF_2:def 5;
end; then
B6: Y1 c= {r} + Y2 by TARSKI:def 3;
now let w be set;
assume w in {r} + Y2; then
consider w1,w2 be R_eal such that
B7: w1 in {r} & w2 in Y2 & w = w1 + w2 by SUPINF_2:def 5;
consider k2 be Element of NAT such that
B8: w2 = seq2.k2 & n <= k2 by C4,B7;
w1 = r by B7,TARSKI:def 1; then
w = seq1.k2 by A1,B7,B8;
hence w in Y1 by C5,B8;
end; then
{r} + Y2 c= Y1 by TARSKI:def 3; then
Y1 = {r} + Y2 by B6,XBOOLE_0:def 10; then
sup Y1 = sup{r} + sup Y2 by A0,SUPINF226a; then
sup Y1 = r + sup Y2 by XXREAL_2:11; then
z = (superior_realsequence seq1).n by C2,TARSKI:def 1,C4,C5;
hence z in P1 by FUNCT_2:6;
end; then
{r} + P2 c= P1 by TARSKI:def 3; then
P1 = {r} + P2 by B9,XBOOLE_0:def 10; then
inf P1 = inf{r} + inf P2 by A0,SUPINF227a;
hence lim_sup seq1 = r + lim_sup seq2 by XXREAL_2:13;
end;
reserve F1,F2 for Functional_Sequence of X,ExtREAL,
f,g,P for PartFunc of X,ExtREAL;
theorem limfunc2:
dom(F1.0) = dom(F2.0) & F1 is with_the_same_dom & F2 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
A0: dom(F1.0) = dom(F2.0) &
F1 is with_the_same_dom & F2 is with_the_same_dom and
A1: f"{+infty} = {} & f"{-infty} = {} and
A2: for n be Nat holds F1.n = f + F2.n;
A3:F1.0 = f + F2.0 by A2;
A4:dom(f + F2.0) = (dom f /\ dom(F2.0))\((f"{-infty} /\ (F2.0)"{+infty}) \/
(f"{+infty} /\ (F2.0)"{-infty})) by MESFUNC1:def 3;
A5:dom(lim_inf F1) = dom(F1.0) & dom(lim_inf F2) = dom(F2.0) by MESFUNC8:def 8;
A6: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
Z7:dom(f + lim_inf F2) = dom f /\ dom(F2.0) by A1,MESFUNC8:def 8; then
A7:dom(lim_inf F1) = dom(f + lim_inf F2) by A3,A4,A1,MESFUNC8:def 8;
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 P01: x in dom(lim_inf F1);
R02:dom(f + lim_inf F2) c= dom f by A6,A1,XBOOLE_1:17; then
not f.x in {+infty} by A1,P01,A7,FUNCT_1:def 13; then
R04:f.x <> +infty by TARSKI:def 1;
not f.x in {-infty} by A1,R02,P01,A7,FUNCT_1:def 13; then
f.x <> -infty by TARSKI:def 1; then
RR: f.x is Real by R04,EXTREAL1:1;
P07:for n be Nat holds (F1#x).n = f.x + (F2#x).n
proof
let n be Nat;
F1.n = f + F2.n by A2; then
dom(f + F2.n) = dom(F1.0) by A0,MESFUNC8:def 2; then
P06: x in dom(f + F2.n) by P01,MESFUNC8:def 8;
(F1.n).x = (f + F2.n).x by A2; then
(F1.n).x = f.x + (F2.n).x by P06,MESFUNC1:def 3; then
(F1#x).n = f.x + (F2.n).x by MESFUNC5:def 13;
hence (F1#x).n = f.x + (F2#x).n by MESFUNC5:def 13;
end;
P08:(lim_inf F1).x = lim_inf(F1#x) &
(lim_inf F2).x = lim_inf(F2#x) by P01,A5,A0,MESFUNC8:def 8;
x in dom(f + lim_inf F2) by P01,Z7,A4,A1,A3,MESFUNC8:def 8; then
(f + lim_inf F2).x = f.x + (lim_inf F2).x by MESFUNC1:def 3;
hence (lim_inf F1).x = (f + lim_inf F2).x by P07,P08,RR,limseq2;
end;
hence lim_inf F1 = f + lim_inf F2 by A7,PARTFUN1:34;
B5:dom(lim_sup F1) = dom(F1.0) & dom(lim_sup F2) = dom(F2.0) by MESFUNC8:def 9;
BB: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
B6:dom(f + lim_sup F2) = dom f /\ dom(F2.0) by A1,MESFUNC8:def 9; then
B7:dom(lim_sup F1) = dom(f + lim_sup F2) by A3,A4,A1,MESFUNC8:def 9;
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 Q01: x in dom(lim_sup F1);
R02:dom(f + lim_sup F2) c= dom f by A1,BB,XBOOLE_1:17; then
not f.x in {+infty} by A1,B7,Q01,FUNCT_1:def 13; then
R04:f.x <> +infty by TARSKI:def 1;
not f.x in {-infty} by A1,B7,Q01,R02,FUNCT_1:def 13; then
f.x <> -infty by TARSKI:def 1; then
RR: f.x is Real by R04,EXTREAL1:1;
Q07:for n be Nat holds (F1#x).n = f.x + (F2#x).n
proof
let n be Nat;
F1.n = f + F2.n by A2; then
Q06: dom(f + F2.n) = dom(F1.0) by A0,MESFUNC8:def 2;
(F1.n).x = (f + F2.n).x by A2; then
(F1.n).x = f.x + (F2.n).x by Q06,Q01,B5,MESFUNC1:def 3; then
(F1#x).n = f.x + (F2.n).x by MESFUNC5:def 13;
hence (F1#x).n = f.x + (F2#x).n by MESFUNC5:def 13;
end;
Q08:(lim_sup F1).x = lim_sup(F1#x) &
(lim_sup F2).x = lim_sup(F2#x) by Q01,B5,A0,MESFUNC8:def 9;
x in dom(f + lim_sup F2) by Q01,B6,A4,A1,A3,MESFUNC8:def 9; then
(f + lim_sup F2).x = f.x + (lim_sup F2).x by MESFUNC1:def 3;
hence (lim_sup F1).x = (f + lim_sup F2).x by Q07,Q08,RR,limseq2;
end;
hence lim_sup F1 = f + lim_sup F2 by B7,PARTFUN1:34;
end;
theorem subseq1:
seq^\0 = seq
proof
now let n be Element of NAT;
(seq^\0).n = seq.(n+0) by KURATO_2:def 2;
hence (seq^\0).n = seq.n;
end;
hence seq^\0 = seq by FUNCT_2:113;
end;
theorem Th114a:
f is_integrable_on M & g is_integrable_on M implies f-g is_integrable_on M
proof
assume A1: f is_integrable_on M & g is_integrable_on M; then
(-1)(#)g is_integrable_on M by MESFUNC5:116; then
-g is_integrable_on M by MESFUNC2:11; then
f+(-g) is_integrable_on M by A1,MESFUNC5:114;
hence f-g is_integrable_on M by MESFUNC2:9;
end;
theorem Th115a:
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
A1: f is_integrable_on M & g is_integrable_on M; then
(-1)(#)g is_integrable_on M by MESFUNC5:116; then
-g is_integrable_on M by MESFUNC2:11; then
consider E be Element of S such that
A2: E = dom f /\ dom(-g) &
Integral(M,f+(-g))= Integral(M,f|E)+Integral(M,(-g)|E)
by A1,MESFUNC5:115;
A3:dom g = dom(-g) by MESFUNC1:def 7;
Integral(M,f-g)= Integral(M,f|E)+Integral(M,(-g)|E) by A2,MESFUNC2:9;
hence thesis by A2,A3;
end;
theorem supinfa:
(for n be Nat holds seq1.n = -seq2.n) implies
lim_inf seq2 = -lim_sup seq1 & lim_sup seq2 = -lim_inf seq1
proof
assume A0: for n be Nat holds seq1.n = -seq2.n;
now let z be set;
assume z in rng (inferior_realsequence seq2); then
consider n be set such that
A21: n in dom (inferior_realsequence seq2) &
z = (inferior_realsequence seq2).n by FUNCT_1:def 5;
reconsider z2 = z as Element of ExtREAL by A21;
reconsider n as Element of NAT by A21;
consider R2 be non empty Subset of ExtREAL such that
A22: R2 = {seq2.k where k is Element of NAT : n <= k} &
z = inf R2 by A21,RINFSUP2:def 6;
set R1 = {seq1.k where k is Element of NAT : n <= k};
reconsider R1 as non empty Subset of ExtREAL by RINFSUP2:5;
set z1 = -z2;
A25:z2 = -z1;
now let x be set;
assume x in -R2; then
consider y be R_eal such that
P01: y in R2 & x = -y by SUPINF_2:def 6;
consider k be Element of NAT such that
P02: y = seq2.k & n <= k by P01,A22;
seq1.k = -seq2.k by A0;
hence x in R1 by P01,P02;
end; then
R01:-R2 c= R1 by TARSKI:def 3;
now let x be set;
assume x in R1; then
consider k be Element of NAT such that
P01: x = seq1.k & n <= k;
reconsider x1=x as Element of ExtREAL by P01;
-x1 = -(-seq2.k) by A0,P01; then
-x1 in {seq2.k2 where k2 is Element of NAT : n <= k2} by P01; then
-(-x1) in -R2 by A22,SUPINF_2:23;
hence x in -R2;
end; then
R1 c= -R2 by TARSKI:def 3; then
A23:-R2 = R1 by R01,XBOOLE_0:def 10;
ex K1 be non empty Subset of ExtREAL st
K1 = {seq1.k where k is Element of NAT: n <= k} &
(superior_realsequence seq1).n = sup K1 by RINFSUP2:def 7; then
(superior_realsequence seq1).n = z1 by A22,A23,SUPINF_2:33; then
z1 in rng(superior_realsequence seq1) by FUNCT_2:6;
hence z in -rng(superior_realsequence seq1) by A25,SUPINF_2:def 6;
end; then
A26:rng (inferior_realsequence seq2) c= -(rng (superior_realsequence seq1))
by TARSKI:def 3;
now let z be set;
assume z in -(rng (superior_realsequence seq1)); then
consider t be R_eal such that
B20: t in rng (superior_realsequence seq1) & z = -t by SUPINF_2:def 6;
consider n be set such that
B21: n in dom (superior_realsequence seq1) &
t = (superior_realsequence seq1).n by B20,FUNCT_1:def 5;
reconsider z1 = z as Element of ExtREAL by B20;
reconsider n as Element of NAT by B21;
consider R1 be non empty Subset of ExtREAL such that
B22: R1 = {seq1.k where k is Element of NAT : n <= k} &
t = sup R1 by B21,RINFSUP2:def 7;
set R2 = {seq2.k where k is Element of NAT : n <= k};
reconsider R2 as non empty Subset of ExtREAL by RINFSUP2:5;
now let x be set;
assume x in -R1; then
consider y be R_eal such that
P01: y in R1 & x = -y by SUPINF_2:def 6;
consider k be Element of NAT such that
P02: y = seq1.k & n <= k by P01,B22;
seq1.k = -seq2.k by A0;
hence x in R2 by P01,P02;
end; then
R02:-R1 c= R2 by TARSKI:def 3;
now let x be set;
assume x in R2; then
consider k be Element of NAT such that
P01: x = seq2.k & n <= k;
reconsider x1=x as Element of ExtREAL by P01;
-x1 = -(-seq1.k) by A0,P01; then
-x1 in {seq1.k2 where k2 is Element of NAT : n <= k2} by P01; then
-(-x1) in -R1 by B22,SUPINF_2:23;
hence x in -R1;
end; then
R2 c= -R1 by TARSKI:def 3; then
B23:-R1 = R2 by R02,XBOOLE_0:def 10;
ex K2 be non empty Subset of ExtREAL st
K2 = {seq2.k where k is Element of NAT: n <= k} &
(inferior_realsequence seq2).n = inf K2 by RINFSUP2:def 6; then
(inferior_realsequence seq2).n = z1 by B23,B20,B22,SUPINF_2:32;
hence z in rng (inferior_realsequence seq2) by FUNCT_2:6;
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 A26,XBOOLE_0:def 10;
hence lim_inf seq2 = - lim_sup seq1 by SUPINF_2:33;
now let z be set;
assume z in rng (superior_realsequence seq2); then
consider n be set such that
A31: n in dom (superior_realsequence seq2) &
z = (superior_realsequence seq2).n by FUNCT_1:def 5;
reconsider z2 = z as Element of ExtREAL by A31;
reconsider n as Element of NAT by A31;
consider R2 be non empty Subset of ExtREAL such that
A32: R2 = {seq2.k where k is Element of NAT : n <= k} &
z = sup R2 by A31,RINFSUP2:def 7;
set R1 = {seq1.k where k is Element of NAT : n <= k};
reconsider R1 as non empty Subset of ExtREAL by RINFSUP2:5;
set z1 = -z2;
A35:z2 = -z1;
now let x be set;
assume x in -R2; then
consider y be R_eal such that
P01: y in R2 & x = -y by SUPINF_2:def 6;
consider k be Element of NAT such that
P02: y = seq2.k & n <= k by P01,A32;
seq1.k = -seq2.k by A0;
hence x in R1 by P01,P02;
end; then
R01:-R2 c= R1 by TARSKI:def 3;
now let x be set;
assume x in R1; then
consider k be Element of NAT such that
P01: x = seq1.k & n <= k;
reconsider x1=x as Element of ExtREAL by P01;
-x1 = -(-seq2.k) by P01,A0; then
-x1 in {seq2.k2 where k2 is Element of NAT : n <= k2} by P01; then
-(-x1) in -R2 by A32,SUPINF_2:23;
hence x in -R2;
end; then
R1 c= -R2 by TARSKI:def 3; then
A33:-R2 = R1 by R01,XBOOLE_0:def 10;
ex K1 be non empty Subset of ExtREAL st
K1 = {seq1.k where k is Element of NAT: n <= k} &
(inferior_realsequence seq1).n = inf K1 by RINFSUP2:def 6; then
(inferior_realsequence seq1).n = z1 by A32,A33,SUPINF_2:32; then
z1 in rng(inferior_realsequence seq1) by FUNCT_2:6;
hence z in -rng(inferior_realsequence seq1) by A35,SUPINF_2:def 6;
end; then
A36:rng (superior_realsequence seq2) c= -(rng (inferior_realsequence seq1))
by TARSKI:def 3;
now let z be set;
assume z in -(rng (inferior_realsequence seq1)); then
consider t be R_eal such that
B30: t in rng (inferior_realsequence seq1) & z = -t by SUPINF_2:def 6;
consider n be set such that
B31: n in dom (inferior_realsequence seq1) &
t = (inferior_realsequence seq1).n by B30,FUNCT_1:def 5;
reconsider z1 = z as Element of ExtREAL by B30;
reconsider n as Element of NAT by B31;
consider R1 be non empty Subset of ExtREAL such that
B32: R1 = {seq1.k where k is Element of NAT : n <= k} &
t = inf R1 by B31,RINFSUP2:def 6;
set R2 = {seq2.k where k is Element of NAT : n <= k};
reconsider R2 as non empty Subset of ExtREAL by RINFSUP2:5;
now let x be set;
assume x in -R1; then
consider y be R_eal such that
P01: y in R1 & x = -y by SUPINF_2:def 6;
consider k be Element of NAT such that
P02: y = seq1.k & n <= k by P01,B32;
seq1.k = -seq2.k by A0;
hence x in R2 by P01,P02;
end; then
R02:-R1 c= R2 by TARSKI:def 3;
now let x be set;
assume x in R2; then
consider k be Element of NAT such that
P01: x = seq2.k & n <= k;
reconsider x1=x as Element of ExtREAL by P01;
seq1.k = -seq2.k by A0; then
-x1 in R1 by P01,B32; then
-(-x1) in -R1 by SUPINF_2:23;
hence x in -R1;
end; then
R2 c= -R1 by TARSKI:def 3; then
B33:-R1 = R2 by R02,XBOOLE_0:def 10;
ex K2 be non empty Subset of ExtREAL st
K2 = {seq2.k where k is Element of NAT: n <= k} &
(superior_realsequence seq2).n = sup K2 by RINFSUP2:def 7; then
(superior_realsequence seq2).n = z1 by B33,B30,B32,SUPINF_2:33;
hence z in rng (superior_realsequence seq2) by FUNCT_2:6;
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 A36,XBOOLE_0:def 10;
hence lim_sup seq2 = -lim_inf seq1 by SUPINF_2:32;
end;
theorem supinfb:
dom(F1.0) = dom(F2.0) & F1 is with_the_same_dom & F2 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) &
F1 is with_the_same_dom & F2 is with_the_same_dom and
A2: for n be Nat holds F1.n = - F2.n;
A3:dom lim_inf F1 = dom(F1.0) & dom lim_sup F2 = dom(F2.0) &
dom lim_sup F1 = dom(F1.0) & dom lim_inf F2 = dom(F2.0)
by MESFUNC8:def 8,def 9;
A5:dom(-lim_sup F2) = dom lim_sup F2 by MESFUNC1:def 7;
A6:now let x be Element of X;
assume A61: x in dom(F1.0);
let n be Nat;
dom(F1.n) = dom(F1.0) by A1,MESFUNC8:def 2; then
A62:x in dom(-F2.n) by A61,A2;
(F1.n).x = (-F2.n).x by A2; then
(F1.n).x = -(F2.n).x by A62,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;
now let x be Element of X;
assume P01: x in dom lim_inf F1; then
P07:for n be Nat holds (F2#x).n = -(F1#x).n by A3,A6;
P08:(lim_inf F1).x = lim_inf(F1#x) &
(lim_sup F2).x = lim_sup(F2#x) by P01,A3,A1,MESFUNC8:def 8,def 9;
x in dom(-lim_sup F2) by P01,A3,A1,MESFUNC1:def 7; then
(-lim_sup F2).x = -(lim_sup F2).x by MESFUNC1:def 7;
hence (lim_inf F1).x = (-lim_sup F2).x by P08,P07,supinfa;
end;
hence lim_inf F1 = -lim_sup F2 by A5,A3,A1,PARTFUN1:34;
B5:dom(-lim_inf F2) = dom lim_inf F2 by MESFUNC1:def 7;
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 Q01: x in dom lim_sup F1; then
Q07:for n be Nat holds (F2#x).n = -(F1#x).n by A3,A6;
Q08:(lim_sup F1).x = lim_sup(F1#x) &
(lim_inf F2).x = lim_inf(F2#x) by Q01,A1,A3,MESFUNC8:def 8,def 9;
x in dom(-lim_inf F2) by Q01,A1,A3,MESFUNC1:def 7; then
(-lim_inf F2).x = -(lim_inf F2).x by MESFUNC1:def 7;
hence (lim_sup F1).x = (-lim_inf F2).x by Q08,Q07,supinfa;
end;
hence lim_sup F1 = -lim_inf F2 by A1,A3,B5,PARTFUN1:34;
end;
theorem Th136z:
E = dom(F.0) & E = dom P & (for n be Nat holds F.n is_measurable_on E) &
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
(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) & E = dom P and
A2: for n be Nat holds F.n is_measurable_on E and
A3: P is_integrable_on M & P is nonnegative and
A4: for x be Element of X, n be Nat st x in E holds (|. F.n .|).x <= P.x;
hereby let n be Nat;
B1: E = dom(F.n) & F.n is_measurable_on E by A1,A2,MESFUNC8:def 2;
now let x be Element of X;
assume B2: x in dom(F.n); then
B3: x in dom(|. F.n .|) by MESFUNC1:def 10;
(|. F.n .|).x <= P.x by B1,B2,A4;
hence |. (F.n).x .| <= P.x by B3,MESFUNC1:def 10;
end; then
F.n is_integrable_on M by B1,A1,A3,MESFUNC5:108;
hence |. F.n .| is_integrable_on M by B1,MESFUNC5:106;
end;
C0:E = dom(lim_inf F) & E = dom(lim_sup F) by A1,MESFUNC8:def 8,def 9;
C1:(lim_inf F) is_measurable_on E & (lim_sup F) is_measurable_on E
by A1,A2,MESFUNC8:23,24;
C2: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 C3: x in E; then
x in dom(F.k) by A1,MESFUNC8:def 2; then
C4: x in dom(|.(F.k).|) by MESFUNC1:def 10;
(|. F.k .|).x <= P.x by A4,C3; then
|. (F.k).x .| <= P.x by C4,MESFUNC1:def 10; then
-(P.x) <= (F.k).x & (F.k).x <= P.x by EXTREAL2:60;
hence -(P.x) <= (F#x).k & (F#x).k <= P.x by MESFUNC5:def 13;
end;
now let x be Element of X;
assume D2: x in dom(lim_inf F); then
D3: x in E by A1,MESFUNC8:def 8;
for k be Nat holds (inferior_realsequence(F#x)).k <= P.x
proof
let k be Nat;
reconsider k1=k as Element of NAT by ORDINAL1:def 13;
D4: (inferior_realsequence(F#x)).k1 <= (F#x).k1 by RINFSUP2:8;
(F#x).k <= P.x by C2,D3;
hence (inferior_realsequence(F#x)).k <= P.x by D4,XXREAL_0:2;
end; then
lim_inf(F#x) <= P.x by Th63b; then
D5: (lim_inf F).x <= P.x by D2,MESFUNC8:def 8;
now let y be ext-real number;
assume y in rng(F#x); then
consider k be set such that
D6: k in dom(F#x) & y = (F#x).k by FUNCT_1:def 5;
thus -(P.x) <= y by D6,C2,D3;
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 subseq1; then
D7: -(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 D7,XXREAL_0:2; then
-(P.x) <= (lim_inf F).x by D2,MESFUNC8:def 8;
hence |. (lim_inf F).x .| <= P.x by D5,EXTREAL2:60;
end; then
lim_inf F is_integrable_on M by C0,C1,A1,A3,MESFUNC5:108;
hence |. lim_inf F .| is_integrable_on M by C0,C1,MESFUNC5:106;
now let x be Element of X;
assume D12: 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 Element of NAT by ORDINAL1:def 13;
D14: (superior_realsequence(F#x)).k1 >= (F#x).k1 by RINFSUP2:8;
(F#x).k >= -(P.x) by C2,D12,C0;
hence (superior_realsequence(F#x)).k >= -(P.x) by D14,XXREAL_0:2;
end; then
lim_sup(F#x) >= -(P.x) by Th63a; then
D15:(lim_sup F).x >= -(P.x) by D12,MESFUNC8:def 9;
now let y be ext-real number;
assume y in rng(F#x); then
consider k be set such that
D16: k in dom(F#x) & y = (F#x).k by FUNCT_1:def 5;
thus P.x >= y by D16,C2,D12,C0;
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 subseq1; then
D17: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 D17,XXREAL_0:2; then
P.x >= (lim_sup F).x by D12,MESFUNC8:def 9;
hence |. (lim_sup F).x .| <= P.x by D15,EXTREAL2:60;
end; then
lim_sup F is_integrable_on M by C0,C1,A1,A3,MESFUNC5:108;
hence |. lim_sup F .| is_integrable_on M by C0,C1,MESFUNC5:106;
end;
Th136:
E = dom(F.0) & E = dom P & (for n be Nat holds F.n is_measurable_on E) &
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) & E = dom P and
A2: for n be Nat holds F.n is_measurable_on E and
A3: P is_integrable_on M & P is nonnegative and
A4: for x be Element of X, n be Nat st x in E holds (|. F.n .|).x <= P.x and
A5: eq_dom(P,+infty) = {};
A6:for n be Nat holds F.n is_integrable_on M
proof
let n be Nat;
A61:E = dom(F.n) & F.n is_measurable_on E by A1,A2,MESFUNC8:def 2;
now let x be Element of X;
assume x in dom(F.n); then
x in dom(|. F.n .|) & (|. F.n .|).x <= P.x by A61,A4,MESFUNC1:def 10;
hence |. (F.n).x .| <= P.x by MESFUNC1:def 10;
end;
hence F.n is_integrable_on M by A61,A1,A3,MESFUNC5:108;
end;
A7:E = dom(lim_inf F) & E = dom(lim_sup F) by A1,MESFUNC8:def 8,def 9;
A8:lim_inf F is_measurable_on E & lim_sup F is_measurable_on E
by A1,A2,MESFUNC8:23,24;
A9: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 A91: x in E; then
x in dom(F.k) by A1,MESFUNC8:def 2; then
A92:x in dom |.(F.k).| by MESFUNC1:def 10;
(|. F.k .|).x <= P.x by A4,A91; then
|. (F.k).x .| <= P.x by A92,MESFUNC1:def 10; then
-(P.x) <= (F.k).x & (F.k).x <= P.x by EXTREAL2:60;
hence -(P.x) <= (F#x).k & (F#x).k <= P.x by MESFUNC5:def 13;
end;
deffunc I(Element of NAT) = Integral(M,F.$1);
consider I be Function of NAT,ExtREAL such that
B1: for n be Element of NAT holds I.n = I(n) from FUNCT_2:sch 4;
reconsider I as ExtREAL_sequence;
B2:for n be Nat holds I.n = Integral(M,F.n) & I.n is Real
proof
let n be Nat;
n is Element of NAT by ORDINAL1:def 13; then
B21:I.n = Integral(M,F.n) by B1;
F.n is_integrable_on M by A6; then
-infty < Integral(M,F.n) & Integral(M,F.n) < +infty by MESFUNC5:102;
hence thesis by B21,EXTREAL1:1;
end;
deffunc G(Element of NAT) = P + F.$1;
consider G be Function such that
B3: dom G = NAT & for n be Element of NAT holds G.n = G(n) from FUNCT_1:sch 4;
B8:now let n be Nat;
n is Element of NAT by ORDINAL1:def 13;
hence G.n = P + F.n by B3;
end;
now let n be Element of NAT;
G.n = P + F.n by B3;
hence G.n is PartFunc of X,ExtREAL;
end; then
reconsider G as Functional_Sequence of X,ExtREAL by B3,SEQFUNC:1;
B4:P"{+infty} = {} by A5,MESFUNC5:36;
now let x be set;
assume x in P"{-infty}; then
B51:x in dom P & P.x in {-infty} by FUNCT_1:def 13;
-infty < 0 & 0 <= P.x by A3,SUPINF_2:70;
hence contradiction by B51,TARSKI:def 1;
end; then
B5:P"{-infty} = {} by XBOOLE_0:def 1;
B6:for n be Nat holds dom(G.n) = E
proof
let n be natural number;
B61:dom(F.n) = E by A1,MESFUNC8:def 2;
dom(G.n) = dom(P + F.n) by B8; then
dom(G.n) =
(dom P /\ dom(F.n))\((P"{-infty} /\ (F.n)"{+infty}) \/ (P"{+infty} /\
(F.n)"{-infty})) by MESFUNC1:def 3;
hence dom(G.n) = E by B4,B5,B61,A1;
end;
now let n,m be natural number;
thus dom(G.n) = E by B6 .= dom(G.m) by B6;
end; then
reconsider G as with_the_same_dom Functional_Sequence of X,ExtREAL
by MESFUNC8:def 2;
B7:E = dom(G.0) by B6;
now let n be Nat;
C10:G.n = P + F.n by B8;
now let x be set;
assume C11: x in dom(P+(F.n)); then
reconsider x1=x as Element of X;
x in E by C11,C10,B6; then
-(P.x) <= (F#x1).n by A9; then
C12: -P.x <= (F.n).x by MESFUNC5:def 13;
-P.x + P.x = P.x - P.x; then
-P.x + P.x = 0 by EXTREAL2:13; then
0 <= (F.n).x + P.x by C12,SUPINF_2:14;
hence 0 <= (P+(F.n)).x by C11,MESFUNC1:def 3;
end;
hence G.n is nonnegative by C10,SUPINF_2:71;
F.n is_integrable_on M by A6; then
G.n is_integrable_on M by C10,A3,MESFUNC5:114; then
ex E1 be Element of S st
E1 = dom(G.n) & G.n is_measurable_on E1 by MESFUNC5:def 17;
hence G.n is_measurable_on E by B6;
end; then
consider IG be ExtREAL_sequence such that
C1: (for n be Nat holds IG.n = Integral(M,G.n)) &
Integral(M,lim_inf G) <= lim_inf IG by B7,Th135;
-infty < Integral(M,P) & Integral(M,P) < +infty by A3,MESFUNC5:102; then
C2:Integral(M,P) is Real by EXTREAL1:1;
now let n be Nat;
F.n is_integrable_on M & G.n=P+(F.n) by A6,B8; then
C31: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 A3,MESFUNC5:115;
C32:dom(F.n) = E by A1,MESFUNC8:def 2; then
P|E = P & (F.n)|E = F.n by A1,RELAT_1:97; then
Integral(M,G.n) = Integral(M,P) + I.n by A1,C31,C32,B2;
hence IG.n = Integral(M,P) + I.n by C1;
end; then
C3:lim_inf IG = Integral(M,P) + lim_inf I by C2,limseq2;
now let x be Element of X;
assume C41: x in dom lim_inf F;
now let k be Nat;
k is Element of NAT by ORDINAL1:def 13; then
(inferior_realsequence(F#x)).k <= (F#x).k & (F#x).k <= P.x
by A9,C41,A7,RINFSUP2:8;
hence (inferior_realsequence(F#x)).k <= P.x by XXREAL_0:2;
end; then
lim_inf(F#x) <= P.x by Th63b; then
C42:(lim_inf F).x <= P.x by C41,MESFUNC8:def 8;
now let y be ext-real number;
assume y in rng(F#x); then
consider k be set such that
C43: k in dom(F#x) & y = (F#x).k by FUNCT_1:def 5;
thus -(P.x) <= y by C43,A9,C41,A7;
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 subseq1; then
C44:-(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 C44,XXREAL_0:2; then
-(P.x) <= (lim_inf F).x by C41,MESFUNC8:def 8;
hence |. (lim_inf F).x .| <= P.x by C42,EXTREAL2:60;
end; then
lim_inf F is_integrable_on M by A7,A8,A1,A3,MESFUNC5:108; then
C4: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 A3,MESFUNC5:115;
C5:-infty < Integral(M,P) & Integral(M,P) < +infty by A3,MESFUNC5:102;
P|E = P & (lim_inf F)|E = lim_inf F & dom(G.0) = dom(F.0)
by A1,A7,B6,RELAT_1:97; then
Integral(M,P) + Integral(M,lim_inf F) <= Integral(M,P) + lim_inf I
by B8,C3,A1,A7,C4,C1,B4,B5,limfunc2; then
Integral(M,lim_inf F) <= lim_inf I + Integral(M,P) - Integral(M,P)
by C5,EXTREAL2:31; then
Integral(M,lim_inf F) <= lim_inf I + (Integral(M,P) - Integral(M,P))
by C5,EXTREAL1:11; then
Integral(M,lim_inf F) <= lim_inf I + 0. by EXTREAL1:9; then
C6:Integral(M,lim_inf F) <= lim_inf I by SUPINF_2:18;
deffunc H(Element of NAT) = P - F.$1;
consider H be Function such that
D1: dom H = NAT & for n be Element of NAT holds H.n = H(n) from FUNCT_1:sch 4;
D2:now let n be Nat;
n is Element of NAT by ORDINAL1:def 13;
hence H.n = P - F.n by D1;
end;
now let n be Element of NAT;
H.n = P - F.n by D1;
hence H.n is PartFunc of X,ExtREAL;
end; then
reconsider H as Functional_Sequence of X,ExtREAL by D1,SEQFUNC:1;
D3:now let n be natural number;
dom(F.n) = E & dom(H.n) = dom(P - F.n) by D2,A1,MESFUNC8:def 2; then
dom(H.n) = (E /\ E)\(({} /\ (F.n)"{+infty}) \/ ({} /\ (F.n)"{-infty}))
by A1,B4,B5,MESFUNC1:def 4;
hence dom(H.n) = E;
end;
now let n,m be natural number;
thus dom(H.n) = E by D3 .= dom(H.m) by D3;
end; then
reconsider H as with_the_same_dom Functional_Sequence of X,ExtREAL
by MESFUNC8:def 2;
D4:now let n be Nat;
D41:H.n = P - F.n by D2;
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 A9;
hence (F.n).x <= P.x by MESFUNC5:def 13;
end;
hence H.n is nonnegative by D41,MESFUNC7:1;
F.n is_integrable_on M by A6; then
H.n is_integrable_on M by D41,A3,Th114a; then
ex E4 be Element of S st
E4 = dom(H.n) & H.n is_measurable_on E4 by MESFUNC5:def 17;
hence H.n is_measurable_on E by D3;
end;
E = dom(H.0) by D3; then
consider IH be ExtREAL_sequence such that
D5: (for n be Nat holds IH.n = Integral(M,H.n)) &
Integral(M,lim_inf H) <= lim_inf IH by D4,Th135;
deffunc I1(Element of NAT) = - I.$1;
consider I1 be Function of NAT,ExtREAL such that
D6: for n be Element of NAT holds I1.n = I1(n) from FUNCT_2:sch 4;
reconsider I1 as ExtREAL_sequence;
D7:now let n be Nat;
n is Element of NAT by ORDINAL1:def 13;
hence I1.n = -I.n by D6;
end; then
D8:-lim_inf I1 = lim_sup I by supinfa;
now let n be Nat;
D91:F.n is_integrable_on M & H.n = P - F.n by D2,A6; then
D92: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 A3,Th115a;
D93:dom(F.n) = E by A1,MESFUNC8:def 2; then
E = dom(-F.n) by MESFUNC1:def 7; then
D94:P|E = P & (-F.n)|E = -(F.n) by A1,RELAT_1:97;
Integral(M,-F.n) = Integral(M,(-1)(#)F.n) by MESFUNC2:11; then
D95:Integral(M,(-F.n)) = R_EAL (-1)*Integral(M,F.n) by D91,MESFUNC5:116;
reconsider In = I.n as Real by B2;
R_EAL (-1)*I.n = (-1)*In & -I.n = -In by SUPINF_2:3,EXTREAL1:13; then
Integral(M,H.n) = Integral(M,P) + -I.n by A1,B2,D92,D93,D94,D95; then
IH.n = Integral(M,P) + -I.n by D5;
hence IH.n = Integral(M,P) + I1.n by D7;
end; then
D9:lim_inf IH = Integral(M,P) + lim_inf I1 by C2,limseq2;
deffunc F1(Element of NAT) = - F.$1;
consider F1 be Function such that
E1: dom F1 = NAT &
for n be Element of NAT holds F1.n = F1(n) from FUNCT_1:sch 4;
now let n be Element of NAT;
F1.n = -F.n by E1;
hence F1.n is PartFunc of X,ExtREAL;
end; then
reconsider F1 as Functional_Sequence of X,ExtREAL by E1,SEQFUNC:1;
E2:now let n be Nat;
n is Element of NAT by ORDINAL1:def 13;
hence F1.n = -F.n by E1;
end;
now let n,m be natural number;
F1.n = -F.n & F1.m = -F.m by E2; then
dom(F1.n) = dom(F.n) & dom(F1.m) = dom(F.m) by MESFUNC1:def 7;
hence dom(F1.n) = dom(F1.m) by MESFUNC8:def 2;
end; then
reconsider F1 as with_the_same_dom Functional_Sequence of X,ExtREAL
by MESFUNC8:def 2;
E3:now let n be Nat;
H.n = P - F.n by D2; then
H.n = P + (- F.n) by MESFUNC2:9;
hence H.n = P + F1.n by E2;
end;
F1.0 = -F.0 by E2; then
E4:dom(F1.0) = dom(F.0) by MESFUNC1:def 7; then
dom(F1.0) = dom(H.0) by A1,D3; then
lim_inf H = P + lim_inf F1 by E3,B4,B5,limfunc2; then
lim_inf H = P + -lim_sup F by E4,E2,supinfb; then
E5:lim_inf H = P - lim_sup F by MESFUNC2:9;
now let x be Element of X;
assume E61: x in dom lim_sup F;
for k be Nat holds (superior_realsequence(F#x)).k >= -(P.x)
proof
let k be Nat;
k is Element of NAT by ORDINAL1:def 13; then
(superior_realsequence(F#x)).k >= (F#x).k & (F#x).k >= -(P.x)
by A9,E61,A7,RINFSUP2:8;
hence (superior_realsequence(F#x)).k >= -(P.x) by XXREAL_0:2;
end; then
lim_sup(F#x) >= -(P.x) by Th63a; then
E62:(lim_sup F).x >= -(P.x) by E61,MESFUNC8:def 9;
now let y be ext-real number;
assume y in rng(F#x); then
consider k be set such that
E63: k in dom(F#x) & y = (F#x).k by FUNCT_1:def 5;
thus P.x >= y by E63,A9,E61,A7;
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 subseq1; then
E64: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 E64,XXREAL_0:2; then
P.x >= (lim_sup F).x by E61,MESFUNC8:def 9;
hence |. (lim_sup F).x .| <= P.x by E62,EXTREAL2:60;
end; then
E6:lim_sup F is_integrable_on M by A7,A8,A1,A3,MESFUNC5:108; then
E7: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 A3,Th115a;
E8:-infty < Integral(M,P) & Integral(M,P) < +infty by A3,MESFUNC5:102;
E = dom lim_sup F by A1,MESFUNC8:def 9; then
E = dom(-lim_sup F) by MESFUNC1:def 7; then
E9:P|E = P & (-lim_sup F)|E = -lim_sup F by A1,RELAT_1:97;
Integral(M,-lim_sup F) = Integral(M,(-1)(#)lim_sup F) by MESFUNC2:11; then
Integral(M,P)+ R_EAL(-1)*Integral(M,lim_sup F) <= Integral(M,P) + -lim_sup I
by D5,D9,D8,A1,A7,E5,E6,E7,E9,MESFUNC5:116; then
R_EAL(-1)*Integral(M,lim_sup F)
<= -lim_sup I + Integral(M,P) - Integral(M,P) by E8,EXTREAL2:31; then
R_EAL (-1)*Integral(M,lim_sup F)
<= -lim_sup I + (Integral(M,P) - Integral(M,P)) by E8,EXTREAL1:11; then
F1:R_EAL (-1)*Integral(M,lim_sup F) <= -lim_sup I + 0. by EXTREAL1:9;
set E1 = Integral(M,lim_sup F);
-infty < E1 & E1 < +infty by E6,MESFUNC5:102; then
reconsider e1 = E1 as Real by EXTREAL1:1;
R_EAL (-1)*E1 = (-1)*e1 & -E1 = -e1 by EXTREAL1:13,SUPINF_2:3; then
-Integral(M,lim_sup F) <= -lim_sup I by F1,SUPINF_2:18; then
F2:Integral(M,lim_sup F) >= lim_sup I by SUPINF_2:16;
now assume L1:for x be Element of X st x in E holds F#x is convergent;
L2: dom lim F = dom(F.0) by MESFUNC8:def 10; then
L3: dom lim F = dom lim_sup F & dom lim F = dom lim_inf F
by MESFUNC8:def 8,def 9;
L4: 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 L31: x in dom lim F; then
x in dom(F.0) & F#x is convergent by L1,L2,A1;
hence (lim F).x = (lim_sup F).x by L31,MESFUNC8:14;
end; then
L5: lim F = lim_sup F by L3,PARTFUN1:34;
L6: 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 L51: x in dom(lim F); then
x in dom(F.0) & F#x is convergent by L1,L2,A1;
hence (lim F).x = (lim_inf F).x by L51,MESFUNC8:14;
end; then
Integral(M,lim F) <= lim_inf I by C6,L3,PARTFUN1:34; then
L7: lim_sup I <= lim_inf I by L5,F2,XXREAL_0:2;
lim_inf I <= lim_sup I by RINFSUP2:39; then
lim_inf I = lim_sup I by L7,XXREAL_0:1;
hence I is convergent by RINFSUP2:40; then
lim I = lim_inf I & lim I = lim_sup I by RINFSUP2:41; then
Integral(M,lim F) <= lim I & lim I <= Integral(M,lim F)
by L4,L6,C6,F2,L3,PARTFUN1:34;
hence lim I = Integral(M,lim F) by XXREAL_0:1;
end;
hence thesis by B2,C6,F2;
end;
:: Lebesgue's Convergence theorem
theorem Th136x:
E = dom(F.0) & E = dom P & (for n be Nat holds F.n is_measurable_on E) &
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) & E = dom P &
(for n be Nat holds F.n is_measurable_on E) &
P is_integrable_on M & P is nonnegative and
A3: for x be Element of X, n be Nat st x in E holds (|. F.n .|).x <= P.x;
A4:ex A be Element of S st A = dom P & P is_measurable_on A
by A1,MESFUNC5:def 17; then
A5:P is_measurable_on E by A1;
for x be set st x in eq_dom(P,+infty) holds x in E
by A1,MESFUNC1:def 16; then
eq_dom(P,+infty) c= E by TARSKI:def 3; then
eq_dom(P,+infty) = E /\ eq_dom(P,+infty) by XBOOLE_1:28; then
reconsider E0 = eq_dom(P,+infty) as Element of S by A1,A4,MESFUNC1:37;
reconsider E1 = E \ E0 as Element of S;
P"{+infty} = E0 by MESFUNC5:36; then
A6:M.E0 = 0 by A1,MESFUNC5:111;
A7:E1 c= E by XBOOLE_1:36;
A8:dom(P|E1) = E1 by A1,RELAT_1:91,XBOOLE_1:36;
set P1 = P|E1;
deffunc F1(Nat) = (F.$1)|E1;
consider F1 be Functional_Sequence of X,ExtREAL such that
B1: for n be Nat holds F1.n = F1(n) from SEQFUNC:sch 1;
B2:now let n be Nat;
dom(F.n) = E by A1,MESFUNC8:def 2; then
dom((F.n)|E1) = E1 by XBOOLE_1:36,RELAT_1:91;
hence dom(F1.n) = E1 by B1;
end; then
B3:E1 = dom(F1.0);
now let n,m be Nat;
thus dom(F1.n) = E1 by B2 .= dom(F1.m) by B2;
end; then
reconsider F1 as with_the_same_dom Functional_Sequence of X,ExtREAL
by MESFUNC8:def 2;
P is_measurable_on E1 by A5,XBOOLE_1:36,MESFUNC1:34; then
B4:P1 is_integrable_on M by A1,MESFUNC5:118;
B5:P1 is nonnegative by A1,MESFUNC5:21;
B6:now let x be Element of X, n be Nat;
assume B61: x in E1;
F1.n = (F.n)|E1 by B1; then
B62:(F1.n).x = (F.n).x & P1.x = P.x by B61,FUNCT_1:72;
x in E by A7,B61; then
x in dom(F.n) by A1,MESFUNC8:def 2; then
x in dom(|. F.n .|) by MESFUNC1:def 10; then
B63:(|. F.n .|).x = |. (F.n).x .| by MESFUNC1:def 10;
E1 = dom(F1.n) by B2; then
E1 = dom(|. F1.n .|) by MESFUNC1:def 10; then
(|. F.n .|).x = (|. F1.n .|).x by B61,B62,B63,MESFUNC1:def 10;
hence (|. F1.n .|).x <= P1.x by B61,A7,A3,B62;
end;
B7:for n be Nat holds F1.n is_measurable_on E1
proof
let n be Nat;
F.n is_measurable_on E by A1; then
B71:F.n is_measurable_on E1 by XBOOLE_1:36,MESFUNC1:34;
dom(F.n) = E by A1,MESFUNC8:def 2; then
E1 = dom(F.n) /\ E1 by XBOOLE_1:28,36; then
(F.n)|E1 is_measurable_on E1 by B71,MESFUNC5:48;
hence F1.n is_measurable_on E1 by B1;
end;
now assume eq_dom(P1,+infty) <> {}; then
consider x be set such that
B81: x in eq_dom(P1,+infty) by XBOOLE_0:def 1;
reconsider x as Element of X by B81;
x in dom P1 & P1.x = +infty by B81,MESFUNC1:def 16; then
consider y be R_eal such that
B82: y = P1.x & +infty = y;
B83:x in E1 by A8,B81,MESFUNC1:def 16; then
x in dom P & y = P.x & +infty = y by A7,A1,B82,FUNCT_1:72; then
x in eq_dom(P,+infty) by MESFUNC1:def 16;
hence contradiction by B83,XBOOLE_0:def 4;
end; then
consider I be ExtREAL_sequence such that
B9: (for n be Nat holds I.n = Integral(M,F1.n)) &
lim_inf I >= Integral(M,lim_inf F1) &
lim_sup I <= Integral(M,lim_sup F1) &
( (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 B3,A8,B4,B5,B6,B7,Th136;
C1:for n be Nat holds I.n = Integral(M,F.n)
proof
let n be Nat;
C11:E = dom(F.n) & F.n is_measurable_on E by A1,MESFUNC8:def 2;
I.n = Integral(M,F1.n) by B9; then
C12:I.n = Integral(M,(F.n)|E1) by B1;
|. F.n .| is_integrable_on M by A1,A3,Th136z; then
F.n is_integrable_on M & E1 = dom(F.n) \ E0 by C11,MESFUNC5:106; then
Integral(M,F.n) = Integral(M,(F.n)|E0) + Integral(M,(F.n)|E1)
by MESFUNC5:105; then
Integral(M,F.n) = 0. + Integral(M,(F.n)|E1) by C11,A6,MESFUNC5:100;
hence I.n = Integral(M,F.n) by C12,SUPINF_2:18;
end;
C2:dom(lim_inf F) = E & lim_inf F is_measurable_on E &
dom(lim_sup F) = E & lim_sup F is_measurable_on E
by A1,MESFUNC8:def 8,def 9,23,24; then
C3:Integral(M,(lim_inf F)|(E\E0)) = Integral(M,lim_inf F) &
Integral(M,(lim_sup F)|(E\E0)) = Integral(M,lim_sup F) by A6,MESFUNC5:101;
E1 = dom((lim_inf F)|(E\E0)) & E1 = dom((lim_sup F)|(E\E0))
by C2,XBOOLE_1:36,RELAT_1:91; then
C4:dom((lim_inf F)|(E\E0)) = dom(lim_inf F1) &
dom((lim_sup F)|(E\E0)) = dom(lim_sup F1) by B3,MESFUNC8:def 8,def 9;
now let x be Element of X;
assume C51: x in dom(lim_inf F1); then
C52:x in E1 by B3,MESFUNC8:def 8;
now let n be Element of NAT;
((F.n)|E1).x = (F.n).x by C52,FUNCT_1:72; then
(F1.n).x = (F.n).x by B1; then
(F1#x).n = (F.n).x by MESFUNC5:def 13;
hence (F1#x).n = (F#x).n by MESFUNC5:def 13;
end; then
C53:F1#x = F#x by FUNCT_2:113;
E1 = dom(lim_inf F1) by B3,MESFUNC8:def 8; then
lim_inf(F#x) = (lim_inf F).x by C51,A7,C2,MESFUNC8:def 8; then
(lim_inf F1).x = (lim_inf F).x by C53,C51,MESFUNC8:def 8;
hence ((lim_inf F)|(E\E0)).x = (lim_inf F1).x by C52,FUNCT_1:72;
end; then
C5:(lim_inf F)|(E\E0) = lim_inf F1 by C4,PARTFUN1:34;
now let x be Element of X;
assume C61: x in dom(lim_sup F1); then
C62:x in E1 by B3,MESFUNC8:def 9;
now let n be Element of NAT;
((F.n)|E1).x = (F.n).x by C62,FUNCT_1:72; then
(F1.n).x = (F.n).x by B1; then
(F1#x).n = (F.n).x by MESFUNC5:def 13;
hence (F1#x).n = (F#x).n by MESFUNC5:def 13;
end; then
C63:F1#x = F#x by FUNCT_2:113;
E1 = dom(lim_sup F1) by B3,MESFUNC8:def 9; then
lim_sup(F#x) = (lim_sup F).x by C61,A7,C2,MESFUNC8:def 9; then
(lim_sup F1).x = (lim_sup F).x by C63,C61,MESFUNC8:def 9;
hence ((lim_sup F)|(E\E0)).x = (lim_sup F1).x by C62,FUNCT_1:72;
end; then
C6:(lim_sup F)|(E\E0) = lim_sup F1 by C4,PARTFUN1:34;
L2:dom(lim F) = dom(F.0) by MESFUNC8:def 10; then
L3:dom(lim F) = dom(lim_sup F) & dom(lim F) = dom(lim_inf F)
by MESFUNC8:def 8,def 9;
now assume L1:for x be Element of X st x in E holds F#x is convergent;
L4: 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 L31: x in dom(lim F); then
x in dom(F.0) & F#x is convergent by L1,L2,A1;
hence (lim F).x = (lim_sup F).x by L31,MESFUNC8:14;
end; then
L5: lim F = lim_sup F by L3,PARTFUN1:34;
L6: 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 L51: x in dom(lim F); then
x in dom(F.0) & F#x is convergent by L1,L2,A1;
hence (lim F).x = (lim_inf F).x by L51,MESFUNC8:14;
end; then
lim F = lim_inf F by L3,PARTFUN1:34; then
L7: lim_sup I <= lim_inf I by L5,C6,B9,C5,XXREAL_0:2;
lim_inf I <= lim_sup I by RINFSUP2:39; then
lim_inf I = lim_sup I by L7,XXREAL_0:1;
hence I is convergent by RINFSUP2:40; then
lim I = lim_inf I & lim I = lim_sup I by RINFSUP2:41; then
Integral(M,lim F) <= lim I & lim I <= Integral(M,lim F)
by L4,L6,C5,C3,C6,B9,L3,PARTFUN1:34;
hence lim I = Integral(M,lim F) by XXREAL_0:1;
end;
hence thesis by C1,C5,C3,C6,B9;
end;
theorem
E = dom(F.0) &
(for n holds F.n is nonnegative & F.n is_measurable_on E) &
(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_measurable_on E 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 & F.0 is_measurable_on E 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;
assume A71: x in dom(F.0);
0 <= (F.0).x by A5,SUPINF_2:70; then
|.(F.0).x.| = (F.0).x by EXTREAL1:def 3;
hence |. F.0 .|.x = (F.0).x by A6,A71,MESFUNC1:def 10;
end;
A8:dom max+(F.0) = dom(F.0) & dom max-(F.0) = dom(F.0) by MESFUNC2:def 2,def 3;
(for x be set st x in dom max+(F.0) holds 0. <= (max+(F.0)).x) &
(for x be set st x in dom max-(F.0) holds 0. <= (max-(F.0)).x)
by MESFUNC2:14,15; then
A9:max+(F.0) is nonnegative & max-(F.0) is nonnegative by SUPINF_2:71;
B1:dom(max+(F.0) + max-(F.0)) = dom max+(F.0) /\ dom max-(F.0)
by A9,MESFUNC5:28;
B2:0 <= integral+(M,max+(F.0)) by A1,A8,A5,A9,MESFUNC2:27,MESFUNC5:85;
B3:0 <= integral+(M,max-(F.0)) by A1,A8,A5,A9,MESFUNC2:28,MESFUNC5:85;
max+(F.0) is_measurable_on E & max-(F.0) is_measurable_on E
by A1,A5,MESFUNC2:27,28; then
B4: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,A8,A9,MESFUNC5:84;
B5:max+(F.0)|E = max+(F.0) & max-(F.0)|E = max-(F.0) by A1,A8,RELAT_1:97;
Integral(M,F.0) = integral+(M,F.0) by A1,A5,MESFUNC5:94; then
integral+(M,F.0) < +infty by A4,A1,RELAT_1:97; then
integral+(M,|. F.0 .|) < +infty by A7,A6,PARTFUN1:34; then
integral+(M,max+(F.0)) + integral+(M,max-(F.0)) < +infty
by B5,B1,A1,A8,B4,MESFUNC2:26; then
integral+(M,max+(F.0)) <> +infty & integral+(M,max-(F.0)) <> +infty
by B2,B3,EXTREAL2:23; then
integral+(M,max+(F.0)) < +infty & integral+(M,max-(F.0)) < +infty
by XXREAL_0:4; then
C2:F.0 is_integrable_on M by A1,A5,MESFUNC5:def 17;
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 C31: x in E;
dom(F.n) = dom(|. F.n .|) by MESFUNC1:def 10; then
C32:x in dom(|. F.n .|) by C31,A1,MESFUNC8:def 2;
F.n is nonnegative by A2; then
0 <= (F.n).x by SUPINF_2:70; then
|.(F.n).x.| = (F.n).x by EXTREAL1:def 3; then
|.(F.n).x.| <= (F.0).x by C31,A3;
hence (|. F.n .|).x <= (F.0).x by C32,MESFUNC1:def 10;
end; then
consider I be ExtREAL_sequence such that
C4: (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,A5,C2,Th136x;
for x be Element of X st x in E holds F#x is convergent
proof
let x be Element of X;
assume C5: x in E;
now let n,m be Element of NAT;
assume m <= n; then
(F.n).x <= (F.m).x by C5,A3; 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 F#x is convergent by RINFSUP2:36;
end;
hence
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) by C4;
end;
definition let X be set, F be Functional_Sequence of X,ExtREAL;
attr F is uniformly_bounded means :DefUB:
ex K be real number st
for n be Nat, x be set st x in dom(F.0) holds |. (F.n).x .| <= K;
end;
:: Lebesgue's Bounded Convergence Theorem
theorem
M.E < +infty & E = dom(F.0) &
(for n be Nat holds F.n is_measurable_on E) &
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 & E = dom(F.0) and
A2: for n be Nat holds F.n is_measurable_on E and
A3: F is uniformly_bounded and
A4: for x be Element of X st x in E holds F#x is convergent;
consider K1 be real number such that
A5: for n be Nat, x be set st x in dom(F.0) holds |. (F.n).x .| <= K1
by A3,DefUB;
set K = max(K1,1);
X: K > 0 by XXREAL_0:30;
Y: K >= K1 by XXREAL_0:25;
X5: 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 A5;
hence thesis by Y,XXREAL_0:2;
end;
K in REAL by XREAL_0:def 1; then
consider h be PartFunc of X,ExtREAL such that
B1: h is_simple_func_in S & dom h = E &
for x be set st x in E holds h.x = K by MESFUNC5:47,NUMBERS:31;
for x be set st x in E holds h.x >= 0. by B1,X; then
B2:h is nonnegative by B1,SUPINF_2:71;
B3:h is_measurable_on E by B1,MESFUNC2:37;
K is Real by XREAL_0:def 1; then
B4:integral'(M,h) = R_EAL K * M.(dom h) by B1,MESFUNC5:110,X;
B5:R_EAL K * +infty = +infty by EXTREAL1:def 1,X;
B6:dom h = dom |.h.| by MESFUNC1:def 10;
B7: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
B71:x in dom |.h.| by MESFUNC1:def 10;
0 <= h.x by B2,SUPINF_2:70; then
|. h.x .| = h.x by EXTREAL1:def 3;
hence |.h.|.x = h.x by B71,MESFUNC1:def 10;
end;
B8:dom max+h = dom h & dom max-h = dom h by MESFUNC2:def 2,def 3;
B9:max+h is_measurable_on E & max-h is_measurable_on E
by B1,B3,MESFUNC2:27,28;
(for x be set st x in dom max+h holds 0. <= (max+h).x) &
(for x be set st x in dom max-h holds 0. <= (max-h).x)
by MESFUNC2:14,15; then
C1:max+h is nonnegative & max-h is nonnegative by SUPINF_2:71; then
C2:dom(max+h + max-h) = dom max+h /\ dom max-h by MESFUNC5:28;
C3:0 <= integral+(M,max+h) & 0 <= integral+(M,max-h)
by B1,B8,B9,C1,MESFUNC5:85;
C4: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 B1,B8,B9,C1,MESFUNC5:84;
C5:max+h|E = max+h & max-h|E = max-h by B1,B8,RELAT_1:97;
Integral(M,h) = integral+(M,h) & Integral(M,h) = integral'(M,h)
by B1,B2,MESFUNC5:95; then
integral+(M,h) < +infty by B5,B4,B1,A1,EXTREAL1:44,X; then
integral+(M,|.h.|) < +infty by B7,B6,PARTFUN1:34; then
integral+(M,max+h) + integral+(M,max-h) < +infty
by C5,C2,B1,B8,C4,MESFUNC2:26; then
integral+(M,max+h) <> +infty & integral+(M,max-h) <> +infty
by C3,EXTREAL2:23; then
integral+(M,max+h) < +infty & integral+(M,max-h) < +infty
by XXREAL_0:4; then
C6:h is_integrable_on M by B1,B3,MESFUNC5:def 17;
C7: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 C71: x in E; then
C72:|. (F.n).x .| <= K by A1,X5;
dom(F.n) = dom(|.(F.n).|) by MESFUNC1:def 10; then
x in dom(|.(F.n).|) by C71,A1,MESFUNC8:def 2; then
|. F.n .|.x = |. (F.n).x .| by MESFUNC1:def 10;
hence (|. F.n .|).x <= h.x by C72,C71,B1;
end; then
D1:(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 by A1,A2,B1,B2,C6,Th136z;
E1:now let n be Nat;
|. F.n .| is_integrable_on M & E = dom(F.n) &
F.n is_measurable_on E by A1,A2,B1,B2,C6,C7,Th136z,MESFUNC8:def 2;
hence F.n is_integrable_on M by MESFUNC5:106;
end;
E4:dom(lim_inf F) = dom (F.0) & dom(lim F) = dom (F.0)
by MESFUNC8:def 8,def 10;
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 E41: x in dom(lim F); then
x in E by A1,MESFUNC8:def 10; then
F#x is convergent by A4;
hence (lim F).x = (lim_inf F).x by E41,MESFUNC8:14;
end; then
E2:lim F = lim_inf F by E4,PARTFUN1:34; then
E3:lim F is_measurable_on E by A1,A2,MESFUNC8:24;
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,B1,B2,C6,C7,Th136x;
hence thesis by A4,E1,E2,E3,A1,E4,D1,MESFUNC5:106;
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 :DefUC:
F is with_the_same_dom &
dom(F.0) = dom f &
for e be real number 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 UCONV:
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 A0: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 number;
Q00:now let e be real number;
assume 0 < e; then
consider N be Nat such that
Q01: for n be Nat, x be set st n >= N & x in dom(F1.0) holds
|. (F1.n).x - f.x .| < e by A0,DefUC;
take N;
hereby let m be Nat;
assume N <= m; then
|. (F1.m).x - f.x .| < e by Q01,A2;
hence |. (F1#x).m - R_EAL g .| < e by MESFUNC5:def 13;
end;
end; then
L1: F1#x is convergent_to_finite_number by MESFUNC5:def 8; then
F1#x is convergent by MESFUNC5:def 11;
hence thesis by L1,Q00,MESFUNC5:def 12;
end;
suppose P2: f.x = +infty;
now let e be real number;
assume 0 < e; then
consider N be Nat such that
Q02: for n be Nat, x be set st n >= N & x in dom(F1.0) holds
|. (F1.n).x - f.x .| < e by A0,DefUC;
take N;
hereby let n be Nat;
assume n >= N; then
|. (F1.n).x - f.x .| < e by Q02,A2; then
P03: |. -( (F1.n).x - f.x ) .| < e by EXTREAL2:66;
(F1.n).x = (F1#x).n by MESFUNC5:def 13; then
-( (F1#x).n - f.x ) < R_EAL e by P03,EXTREAL2:58; then
f.x - (F1#x).n < R_EAL e by EXTREAL2:15; then
(F1#x).n = +infty by P2,EXTREAL2:29;
hence e <= (F1#x).n by XXREAL_0:3;
end;
end; then
L2: F1#x is convergent_to_+infty by MESFUNC5:def 9; then
F1#x is convergent by MESFUNC5:def 11;
hence thesis by L2,P2,MESFUNC5:def 12;
end;
suppose P3: f.x = -infty;
now let e be real number;
assume e < 0; then
-0 < -e by XREAL_1:26; then
consider N be Nat such that
Q03: for n be Nat, x be set st n >= N & x in dom(F1.0) holds
|. (F1.n).x - f.x .| < -e by A0,DefUC;
take N;
hereby let n be Nat;
assume n >= N; then
P03: |. (F1.n).x - f.x .| < -e by Q03,A2;
(F1.n).x = (F1#x).n by MESFUNC5:def 13; then
(F1#x).n - f.x < R_EAL -e by P03,EXTREAL2:58; then
(F1#x).n = -infty by P3,EXTREAL2:29;
hence e >= (F1#x).n by XXREAL_0:5;
end;
end; then
L3: F1#x is convergent_to_-infty by MESFUNC5:def 10; then
F1#x is convergent by MESFUNC5:def 11;
hence thesis by L3,P3,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 & E = dom(F.0) and
A2: (for n be Nat holds F.n is_integrable_on M) and
A3: F is_uniformly_convergent_to f;
A4:for n be Nat holds F.n is_measurable_on E
proof
let n be Nat;
F.n is_integrable_on M by A2; then
ex A be Element of S st A = dom(F.n) & (F.n) is_measurable_on A
by MESFUNC5:def 17;
hence F.n is_measurable_on E by A1,MESFUNC8:def 2;
end;
dom f = dom(F.0) by A3,DefUC; then
A5:dom(lim F) = dom f by MESFUNC8:def 10;
now let x be Element of X;
assume x in dom f; then
x in dom(F.0) by A3,DefUC; then
x in dom(lim F) & lim(F#x) = f.x by A3,UCONV,MESFUNC8:def 10;
hence (lim F).x = f.x by MESFUNC8:def 10;
end; then
A6:lim F = f by A5,PARTFUN1:34;
consider N be Nat such that
A7: for n be Nat, x be set st n >= N & x in dom(F.0) holds
|. (F.n).x - f.x .| < 1/2 by A3,DefUC;
A8:for x be set st x in dom(F.0) holds |. (F.N).x - f.x .| < 1/2 by A7;
consider h be PartFunc of X,ExtREAL such that
B1: h is_simple_func_in S & dom h = E &
(for x be set st x in E holds h.x=1.) by MESFUNC5:47;
for x be set st x in E holds h.x >= 0. by B1; then
B2:h is nonnegative by B1,SUPINF_2:71; then
Integral(M,h) = integral+(M,h) & Integral(M,h) = integral'(M,h)
by B1,MESFUNC5:95; then
B3:integral+(M,h) = R_EAL 1 * M.(dom h) by B1,MESFUNC5:110;
B4:dom h = dom(|.h.|) by MESFUNC1:def 10;
now let x be Element of X;
assume x in dom h; then
B41:x in dom(|.h.|) by MESFUNC1:def 10;
0 <= h.x by B2,SUPINF_2:70; then
|. h.x .| = h.x by EXTREAL1:def 3;
hence |.h.|.x = h.x by B41,MESFUNC1:def 10;
end; then
B5:h = |.h.| by B4,PARTFUN1:34;
B6:h is_measurable_on E by B1,MESFUNC2:37; then
B7:max+h is_measurable_on E & max-h is_measurable_on E by B1,MESFUNC2:27,28;
(for x be set st x in dom max+h holds 0. <= (max+h).x) &
(for x be set st x in dom max-h holds 0. <= (max-h).x)
by MESFUNC2:14,15; then
B8:max+h is nonnegative & max-h is nonnegative by SUPINF_2:71;
B9:dom max+h = dom h & dom max-h = dom h by MESFUNC2:def 2,def 3; then
C1:max+h|E = max+h & max-h|E = max-h by B1,RELAT_1:97;
dom(max+h + max-h) = dom max+h /\ dom max-h by B8,MESFUNC5:28; 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 B1,B9,B7,B8,MESFUNC5:84; then
C2:integral+(M,|.h.|) = integral+(M,max+h) + integral+(M,max-h)
by C1,MESFUNC2:26;
C3:0 <= integral+(M,max+h) & 0 <= integral+(M,max-h)
by B1,B9,B7,B8,MESFUNC5:85;
R_EAL 1 * +infty = +infty by EXTREAL1:def 1; then
integral+(M,|.h.|) < +infty by B1,B3,B5,A1,EXTREAL1:44; then
integral+(M,max+h) <> +infty & integral+(M,max-h) <> +infty
by C2,C3,EXTREAL2:23; then
integral+(M,max+h) < +infty & integral+(M,max-h) < +infty
by XXREAL_0:4; then
C4:h is_integrable_on M by B1,B6,MESFUNC5:def 17;
set AFN = |. F.N .|;
E = dom(F.N) & F.N is_integrable_on M & F.N is_measurable_on E
by A2,A4,A1,MESFUNC8:def 2; then
AFN is_integrable_on M by MESFUNC5:106; then
C5:AFN + h is_integrable_on M by C4,MESFUNC5:114;
now let x be set;
assume x in dom AFN; then
AFN.x = |. (F.N).x .| by MESFUNC1:def 10;
hence 0 <= AFN.x by EXTREAL2:51;
end; then
C6:AFN is nonnegative by SUPINF_2:71; then
C7:dom(AFN + h) = dom AFN /\ dom h & AFN + h is nonnegative by B2,MESFUNC5:28;
C9:dom(F.N) = dom AFN by MESFUNC1:def 10; then
C8:E = dom AFN by A1,MESFUNC8:def 2;
D1:now let x be set, n be Nat;
assume D11: n >= N & x in dom(F.0); then
D12:x in dom AFN by C9,MESFUNC8:def 2;
D13: |. (F.n).x - f.x .| < 1/2 & |. (F.N).x - f.x .| < 1/2 by D11,A7;
D14:now assume d: f.x in REAL;
D17: 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 d,SUPINF_2:6,7;
hence contradiction by D13,XXREAL_0:9,EXTREAL2:67;
end;
D18: 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 d,SUPINF_2:6,7; then
1. < |. (F.N).x - f.x .| by XXREAL_0:9,EXTREAL2:67;
hence contradiction by D11,A8,XXREAL_0:2;
end; then
D19: (F.n).x in REAL & (F.N).x in REAL by D17,XXREAL_0:14;
D21: |. (F.n).x - f.x .| < 1 & |. f.x - (F.N).x .| < 1/2
by D13,XXREAL_0:2,MESFUNC5:1; then
D22: |. f.x - (F.N).x .| < 1 by XXREAL_0:2;
0 <= |. (F.n).x - f.x .| by EXTREAL2:51; then
reconsider a = |. (F.n).x - f.x .| as Real by D21,EXTREAL2:20,EXTREAL1:1;
0 <= |. f.x - (F.N).x .| by EXTREAL2:51; then
reconsider b = |. f.x - (F.N).x .| as Real by D22,EXTREAL2:20,EXTREAL1:1;
-f.x + f.x = -(f.x - f.x) by EXTREAL2:15; then
-f.x + f.x = 0. by EXTREAL2:13; then
(F.n).x - (F.N).x = (F.n).x + (-f.x + f.x) - (F.N).x by SUPINF_2:18; then
(F.n).x - (F.N).x = (F.n).x + -f.x + f.x - (F.N).x
by d,D17,EXTREAL1:8; then
(F.n).x - (F.N).x = (F.n).x - f.x + (f.x - (F.N).x)
by d,D18,EXTREAL1:11; then
D23: |. (F.n).x - (F.N).x .| <= |. (F.n).x - f.x .| + |. f.x - (F.N).x .|
by D21,EXTREAL2:20,61,67;
a < 1/2 & b <= 1/2 by D13,MESFUNC5:1; then
a + b < 1/2 + 1/2 by XREAL_1:10; then
|. (F.n).x - f.x .| + |. f.x - (F.N).x .| < 1 by SUPINF_2:1; then
D24: |. (F.n).x - (F.N).x .| < 1 by D23,XXREAL_0:2;
|. (F.n).x .| - |. (F.N).x .| <= |. (F.n).x - (F.N).x .|
by D19,EXTREAL2:68; then
|. (F.n).x .| - |. (F.N).x .| <= 1. by D24,XXREAL_0:2;
hence |. (F.n).x .| <= |. (F.N).x .| + 1. by EXTREAL2:27;
end;
now assume D25: f.x = +infty or f.x = -infty;
|. (F.n).x - f.x .| < 1. & |. (F.N).x - f.x .| < 1.
by D13,XXREAL_0:2; then
-1. < (F.n).x - f.x & -1. < (F.N).x - f.x &
(F.n).x - f.x < 1. & (F.N).x - f.x < 1. by EXTREAL2:58; then
( (F.n).x = +infty & (F.N).x = +infty ) or
( (F.n).x = -infty & (F.N).x = -infty ) by D25,EXTREAL2:28,29;
hence |. (F.n).x .| <= |. (F.N).x .| + 1.
by EXTREAL2:67,27;
end; then
D26:|. (F.n).x .| <= AFN.x + 1. by D12,D14,XXREAL_0:14,MESFUNC1:def 10;
dom(AFN + h) = dom AFN /\ dom h by B2,C6,MESFUNC5:28; then
dom(AFN + h) = E /\ E by C9,A1,MESFUNC8:def 2,B1; then
AFN.x + h.x = (AFN + h).x by D11,A1,MESFUNC1:def 3; then
D27:AFN.x + 1. = (AFN + h).x by B1,D11,A1;
dom(F.n) = E by A1,MESFUNC8:def 2; then
x in dom |. F.n .| by D11,A1,MESFUNC1:def 10;
hence (|. F.n .|).x <= (AFN + h).x by D26,D27,MESFUNC1:def 10;
end;
reconsider N1=N as Element of NAT by ORDINAL1:def 13;
D3: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;
assume D31: x in E;
n is Element of NAT by ORDINAL1:def 13; then
(F^\N1).n = F.(n+N) by KURATO_2:def 2;
hence (|.(F^\N1).n.|).x <= (AFN + h).x by D31,A1,D1,NAT_1:11;
end;
D5:for n be Nat holds (F^\N1).n is_measurable_on E
proof
let n be Nat;
n is Element of NAT by ORDINAL1:def 13; then
(F^\N1).n = F.(n+N) by KURATO_2:def 2;
hence (F^\N1).n is_measurable_on E by A4;
end;
D6: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;
assume x in E; then
D61:F#x is convergent by A1,A3,UCONV;
D62: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 KURATO_2:def 2; then
((F^\N1)#x).n = (F#x).(n+N) by MESFUNC5:def 13;
hence ((F^\N1)#x).n = ((F#x)^\N1).n by KURATO_2:def 2;
end;
(F#x)^\N1 is convergent by D61,RINFSUP2:21;
hence (F^\N1)#x is convergent by D62,FUNCT_2:113;
lim(F#x) = lim((F#x)^\N1) by D61,RINFSUP2:21;
hence lim(F#x) = lim((F^\N1)#x) by D62,FUNCT_2:113;
end;
(F^\N1).0 = F.(0+N) by KURATO_2:def 2; then
D4:dom((F^\N1).0) = E by A1,MESFUNC8:def 2; then
dom(lim(F^\N1)) = E by MESFUNC8:def 10; then
D7:dom(lim F) = dom(lim(F^\N1)) by A1,MESFUNC8:def 10;
D8:now let x be Element of X;
assume D81:x in dom(lim F); then
D82:lim((F^\N1)#x) = (lim (F^\N1)).x by D7,MESFUNC8:def 10;
x in E by D81,A1,MESFUNC8:def 10; then
lim(F#x) = lim((F^\N1)#x) by D6;
hence (lim F).x = (lim (F^\N1)).x by D81,D82,MESFUNC8:def 10;
end;
consider J be ExtREAL_sequence such that
E1: ( for n be Nat holds J.n = Integral(M,(F^\N1).n) )&
lim_inf J >= Integral(M,lim_inf (F^\N1)) &
lim_sup J <= Integral(M,lim_sup (F^\N1)) &
( (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 D4,D5,B1,C5,C7,C8,D3,Th136x;
E2:|. lim_inf(F^\N1) .| is_integrable_on M by D4,D5,B1,C5,C7,C8,D3,Th136z;
E3:dom lim_inf(F^\N1) = dom((F^\N1).0) &
dom lim(F^\N1) = dom((F^\N1).0) by MESFUNC8:def 8,def 10;
now let x be Element of X;
assume P01: x in dom(lim(F^\N1)); then
x in E by D4,MESFUNC8:def 10; then
(F^\N1)#x is convergent by D6;
hence (lim(F^\N1)).x = (lim_inf(F^\N1)).x by P01, MESFUNC8:14;
end; then
E4:lim(F^\N1) = lim_inf(F^\N1) by E3,PARTFUN1:34;
for x be Element of X st x in E holds (F^\N1)#x is convergent by D6; then
lim(F^\N1) is_measurable_on E by D4,D5,MESFUNC8:25; then
E5:lim(F^\N1) is_integrable_on M by D4,E3,E4,E2,MESFUNC5:106;
deffunc I(Element of NAT) = Integral(M,F.$1);
consider I be Function of NAT,ExtREAL such that
E6: for n be Element of NAT holds I.n = I(n) from FUNCT_2:sch 4;
reconsider I as ExtREAL_sequence;
E7:for n be Nat holds I.n = Integral(M,F.n)
proof
let n be Nat;
n is Element of NAT by ORDINAL1:def 13;
hence I.n = Integral(M,F.n) by E6;
end;
now let n be Element of NAT;
E8: J.n = Integral(M,(F^\N1).n) by E1;
(F^\N1).n = F.(n+N) & (I^\N1).n = I.(n+N) by KURATO_2:def 2;
hence J.n = (I^\N1).n by E8,E6;
end; then
J = I^\N1 by FUNCT_2:113; then
I is convergent & lim I = lim J by E1,D6,RINFSUP2:17; then
I is convergent & lim I = Integral(M,lim F) by D6,E1,D8,D7,PARTFUN1:34;
hence 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) by E5,E7,A6,D8,D7,PARTFUN1:34;
end;