:: Lebesgue's Convergence Theorem of Complex-Valued Function
:: by Keiko Narita , Noboru Endou and Yasunari Shidama
::
:: Received March 17, 2009
:: Copyright (c) 2009-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, PROB_1, MEASURE1, SUBSET_1, SEQFUNC, SEQ_1,
PARTFUN1, NAT_1, REALSET1, FUNCT_1, RELAT_1, PBOOLE, SEQ_2, MEASURE6,
MESFUNC5, MESFUNC8, TARSKI, CARD_1, ORDINAL2, MESFUNC1, SERIES_1,
ARYTM_3, XXREAL_0, MSSUBFAM, SETFAM_1, CARD_3, MESFUNC2, INTEGRA5,
COMPLEX1, COMSEQ_1, XCMPLX_0, VALUED_1, ARYTM_1, RINFSUP1, XXREAL_2,
SUPINF_2, VALUED_0, MESFUN10, REAL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS,
XCMPLX_0, XREAL_0, XXREAL_3,
COMPLEX1, REAL_1, XXREAL_0, RELAT_1, VALUED_1, FUNCT_1, RELSET_1,
FUNCT_2, PARTFUN1, NAT_1, PROB_1, SETFAM_1, SUPINF_2, MESFUNC9, SEQ_1,
SEQ_2, SEQFUNC, SERIES_1, MEASURE1, EXTREAL1, MESFUNC1, MEASURE6,
MESFUNC2, MESFUNC6, MESFUN6C, MESFUN10, MESFUNC8, MESFUN7C, MESFUNC5,
COMSEQ_1, COMSEQ_2, COMSEQ_3, RINFSUP2, XXREAL_2;
constructors REAL_1, EXTREAL1, SUPINF_1, MESFUNC9, MESFUN10, SEQFUNC,
COMSEQ_2, COMSEQ_3, MESFUNC1, MEASURE6, MESFUNC2, MESFUNC5, MESFUNC6,
MESFUN6C, MESFUN7C, RINFSUP2, RELSET_1;
registrations XREAL_0, MEMBERED, ORDINAL1, PARTFUN1, COMSEQ_3, FUNCT_2,
XBOOLE_0, NUMBERS, XXREAL_0, XCMPLX_0, MESFUNC8, VALUED_0, MESFUN7C,
RELSET_1, XXREAL_3;
requirements NUMERALS, REAL, BOOLE, SUBSET;
definitions FUNCT_2, MESFUNC8;
equalities MESFUNC5, SERIES_1, VALUED_1, RINFSUP2, MESFUN7C, MESFUNC6;
expansions FUNCT_2, MESFUNC5, SERIES_1, MESFUN7C, MESFUNC6, MESFUNC8;
theorems TARSKI, PARTFUN1, FUNCT_1, EXTREAL1, MESFUNC1, XBOOLE_0, MESFUNC2,
XXREAL_0, MESFUNC5, NAT_1, RELAT_1, FUNCT_2, COMPLEX1, MESFUN10,
XCMPLX_0, MESFUNC6, SEQFUNC, ORDINAL1, MESFUNC8, RINFSUP2, RELSET_1,
MESFUN7C, SERIES_1, VALUED_1, COMSEQ_3, MESFUN6C, XXREAL_2, MESFUNC9;
schemes FUNCT_2, NAT_1, RECDEF_1, SEQFUNC;
begin :: Partial Sums of Real-valued Functional Sequences
reserve X for non empty set,
S for SigmaField of X,
M for sigma_Measure of S,
E for Element of S,
F for Functional_Sequence of X,REAL,
f for PartFunc of X,REAL,
seq for Real_Sequence,
n,m for Nat,
x for Element of X,
z,D for set;
definition
let X,Y be set, F be Functional_Sequence of X,Y;
let D be set;
func F||D -> Functional_Sequence of X,Y means
:Def1:
for n being Nat holds it.n = (F.n)|D;
existence
proof
deffunc F(Nat) = (F.$1)|D;
ex G being Functional_Sequence of X,Y st for n being Nat holds G.n = F
(n) from SEQFUNC:sch 1;
hence thesis;
end;
uniqueness
proof
let A, B be Functional_Sequence of X,Y such that
A1: for n being Nat holds A.n = (F.n)|D and
A2: for n being Nat holds B.n = (F.n)|D;
let x be Element of NAT;
thus A.x = (F.x)|D by A1
.= B.x by A2;
end;
end;
theorem Th1:
x in D & F#x is convergent implies (F||D)#x is convergent
proof
set G = F||D;
assume
A1: x in D;
A2: (R_EAL G)#x = G#x by MESFUN7C:1;
assume F#x is convergent;
then R_EAL(F#x) is convergent_to_finite_number by RINFSUP2:14;
then
A3: (R_EAL F)#x is convergent_to_finite_number by MESFUN7C:1;
for n be Nat holds (R_EAL G).n = ((R_EAL F).n)|D by Def1;
then (R_EAL G)#x is convergent_to_finite_number by A1,A3,MESFUNC9:12;
hence thesis by A2,RINFSUP2:15;
end;
theorem Th2:
for X,Y,D be set, F be Functional_Sequence of X,Y st F is
with_the_same_dom holds F||D is with_the_same_dom
proof
let X,Y,D be set, F be Functional_Sequence of X,Y;
assume
A1: F is with_the_same_dom;
let n,m be Nat;
set G = F||D;
G.m = (F.m)|D by Def1;
then
A2: dom(G.m) = dom(F.m) /\ D by RELAT_1:61;
G.n = (F.n)|D by Def1;
then dom(G.n) = dom(F.n) /\ D by RELAT_1:61;
hence dom(G.n) = dom(G.m) by A1,A2;
end;
theorem Th3:
D c= dom(F.0) & (for x be Element of X st x in D holds F#x is
convergent) implies (lim F)|D = lim (F||D)
proof
set G = F||D;
assume that
A1: D c= dom(F.0) and
A2: for x be Element of X st x in D holds F#x is convergent;
A3: for x be Element of X st x in D holds (R_EAL F)#x is convergent
proof
let x be Element of X;
assume x in D;
then
A4: F#x is convergent by A2;
(R_EAL F)#x = F#x by MESFUN7C:1;
hence (R_EAL F)#x is convergent by A4,RINFSUP2:14;
end;
for n be Nat holds (R_EAL G).n = ((R_EAL F).n)|D by Def1;
hence (lim F)|D = lim G by A1,A3,MESFUNC9:19;
end;
theorem Th4:
F is with_the_same_dom & E c= dom(F.0) & (for m be Nat holds F.m
is E-measurable) implies (F||E).n is E-measurable
proof
set G = F||E;
assume
A1: F is with_the_same_dom & E c= dom(F.0);
assume
A2: for m be Nat holds F.m is E-measurable;
for m be Nat holds (R_EAL F).m is E-measurable & (R_EAL G).m = ((
R_EAL F).m)|E
proof
let m be Nat;
F.m is E-measurable by A2;
then R_EAL(F.m) is E-measurable;
hence (R_EAL F).m is E-measurable;
thus (R_EAL G).m = ((R_EAL F).m)|E by Def1;
end;
then R_EAL(G.n) is E-measurable by A1,MESFUNC9:20;
hence G.n is E-measurable;
end;
reserve i for Element of NAT;
theorem Th5:
Partial_Sums R_EAL seq = R_EAL(Partial_Sums seq)
proof
defpred P[Nat] means (Partial_Sums(R_EAL seq)).$1 = (R_EAL
Partial_Sums(seq)).$1;
A1: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k];
then
(Partial_Sums(R_EAL seq)).(k+1) = Partial_Sums(seq).k + seq
.(k+1) by MESFUNC9:def 1
.=Partial_Sums(seq).k + seq.(k+1);
hence thesis by SERIES_1:def 1;
end;
(Partial_Sums(R_EAL seq)).0 = seq.0 by MESFUNC9:def 1;
then
A2: P[ 0 ] by SERIES_1:def 1;
for i being Nat holds P[i] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
theorem Th6:
(for x be Element of X st x in E holds F#x is summable) implies
for x be Element of X st x in E holds (F||E)#x is summable
proof
set G = F||E;
assume
A1: for x be Element of X st x in E holds F#x is summable;
let x be Element of X;
assume
A2: x in E;
for n be Element of NAT holds (F#x).n = (G#x).n
proof
let n be Element of NAT;
(F#x).n = (F.n).x by SEQFUNC:def 10;
then (F#x).n = ((F.n)|E).x by A2,FUNCT_1:49;
then (F#x).n = (G.n).x by Def1;
hence (F#x).n = (G#x).n by SEQFUNC:def 10;
end;
then
A3: Partial_Sums(F#x) = Partial_Sums(G#x) by FUNCT_2:63;
F#x is summable by A1,A2;
then Partial_Sums(F#x) is convergent;
hence G#x is summable by A3;
end;
definition
let X be non empty set, F be Functional_Sequence of X,REAL;
func Partial_Sums F -> Functional_Sequence of X,REAL means
:Def2:
it.0 = F.0 & for n be Nat holds it.(n+1) = it.n + F.(n+1);
existence
proof
defpred P[Nat,set,set] means (not $2 is PartFunc of X,REAL & $3
= F.$1) or ($2 is PartFunc of X,REAL & for F2 be PartFunc of X,REAL st F2 = $2
holds $3 = F2 + F.($1+1));
A1: for n being Nat for x being set ex y being set st P[n,x,y]
proof
let n be Nat;
let x be set;
now
assume x is PartFunc of X,REAL;
then reconsider G2 = x as PartFunc of X,REAL;
take y = G2 + F.(n+1);
thus not x is PartFunc of X,REAL & y = F.n or (x is PartFunc of X,REAL
& for F2 be PartFunc of X,REAL st F2 = x holds y = F2 + F.(n+1));
end;
hence thesis;
end;
consider IT being Function such that
A2: dom IT = NAT & IT.0 = F.0 & for n being Nat holds P[n,
IT.n,IT.(n+1)] from RECDEF_1:sch 1(A1);
now
defpred IND[Nat] means IT.$1 is PartFunc of X,REAL;
let f be object;
assume f in rng IT;
then consider m be object such that
A3: m in dom IT and
A4: f = IT.m by FUNCT_1:def 3;
reconsider m as Element of NAT by A2,A3;
A5: for n be Nat st IND[n] holds IND[n+1]
proof
let n be Nat;
assume IND[n];
then reconsider F2 = IT.n as PartFunc of X,REAL;
IT.(n+1) = F2 + F.(n+1) by A2;
hence IND[n+1];
end;
A6: IND[ 0 ] by A2;
for n be Nat holds IND[n] from NAT_1:sch 2(A6,A5);
then IT.m is PartFunc of X,REAL;
hence f in PFuncs(X,REAL) by A4,PARTFUN1:45;
end;
then rng IT c= PFuncs(X,REAL) by TARSKI:def 3;
then reconsider IT as Functional_Sequence of X,REAL by A2,FUNCT_2:def 1
,RELSET_1:4;
take IT;
thus thesis by A2;
end;
uniqueness
proof
let PS1,PS2 be Functional_Sequence of X,REAL;
assume that
A7: PS1.0 = F.0 and
A8: for n be Nat holds PS1.(n+1) = PS1.n + F.(n+1) and
A9: PS2.0 = F.0 and
A10: for n be Nat holds PS2.(n+1) = PS2.n + F.(n+1);
defpred IND[Nat] means PS1.$1 = PS2.$1;
A11: for n be Nat st IND[n] holds IND[n+1]
proof
let n be Nat;
assume
A12: IND[n];
PS1.(n+1) = PS1.n + F.(n+1) by A8;
hence PS1.(n+1) = PS2.(n+1) by A10,A12;
end;
A13: IND[ 0 ] by A7,A9;
for n be Nat holds IND[n] from NAT_1:sch 2(A13,A11);
then for m be Element of NAT holds PS1.m = PS2.m;
hence thesis;
end;
end;
theorem Th7:
Partial_Sums R_EAL F = R_EAL(Partial_Sums F)
proof
defpred P[Nat] means (Partial_Sums(R_EAL F)).$1 = (R_EAL
Partial_Sums F).$1;
A1: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k];
then
(Partial_Sums(R_EAL F)).(k+1) =R_EAL((Partial_Sums F).k) +R_EAL(F.(k+1
)) by MESFUNC9:def 4
.=R_EAL((Partial_Sums F).k + F.(k+1)) by MESFUNC6:23;
hence thesis by Def2;
end;
(Partial_Sums(R_EAL F)).0 = (R_EAL F).0 by MESFUNC9:def 4
.= R_EAL(Partial_Sums(F).0) by Def2;
then
A2: P[ 0 ];
for i being Nat holds P[i] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
theorem Th8:
z in dom((Partial_Sums F).n) & m <= n implies z in dom((
Partial_Sums F).m) & z in dom(F.m)
proof
(Partial_Sums F).n = (R_EAL(Partial_Sums F)).n;
then
A1: (Partial_Sums F).n = (Partial_Sums R_EAL F).n by Th7;
(Partial_Sums R_EAL F).m = (R_EAL(Partial_Sums F)).m by Th7;
hence thesis by A1,MESFUNC9:22;
end;
theorem Th9:
R_EAL F is additive
proof
now
let n,m be Nat;
assume n <> m;
let x be set;
assume x in dom((R_EAL F).n) /\ dom((R_EAL F).m);
(R_EAL F).n = R_EAL(F.n);
hence ((R_EAL F).n).x <> +infty or ((R_EAL F).m).x <> -infty;
end;
hence thesis by MESFUNC9:def 5;
end;
theorem Th10:
dom((Partial_Sums F).n) = meet{dom(F.k) where k is Element of NAT : k <= n}
proof
dom((Partial_Sums R_EAL F).n) = meet{dom((R_EAL F).k) where k is Element
of NAT : k <= n} & (Partial_Sums R_EAL F).n = (R_EAL(Partial_Sums F)).n by Th7
,Th9,MESFUNC9:28;
hence thesis;
end;
theorem Th11:
F is with_the_same_dom implies dom((Partial_Sums F).n) = dom(F.0 )
proof
assume F is with_the_same_dom;
then dom((Partial_Sums R_EAL F).n) = dom((R_EAL F).0) by Th9,MESFUNC9:29;
then dom((R_EAL(Partial_Sums F)).n) = dom((R_EAL F).0) by Th7;
hence thesis;
end;
theorem Th12:
F is with_the_same_dom & D c= dom(F.0) & x in D implies (
Partial_Sums(F#x)).n = ((Partial_Sums F)#x).n
proof
assume F is with_the_same_dom & D c= dom(F.0) & x in D;
then (Partial_Sums((R_EAL F)#x)).n = ((Partial_Sums(R_EAL F))#x).n by Th9,
MESFUNC9:32;
then (Partial_Sums(R_EAL(F#x))).n = ((Partial_Sums(R_EAL F))#x).n by
MESFUN7C:1;
then (R_EAL(Partial_Sums(F#x))).n = ((Partial_Sums(R_EAL F))#x).n by Th5;
then ((Partial_Sums(F#x)).n) = ((R_EAL(Partial_Sums F))#x).n by Th7;
hence thesis by MESFUN7C:1;
end;
theorem Th13:
F is with_the_same_dom & D c= dom(F.0) & x in D implies (
Partial_Sums(F#x) is convergent iff (Partial_Sums F)#x is convergent )
proof
assume
A1: F is with_the_same_dom & D c= dom(F.0) & x in D;
A2: R_EAL(F#x) = (R_EAL F)#x by MESFUN7C:1;
Partial_Sums R_EAL F = R_EAL(Partial_Sums F) by Th7;
then
A3: (Partial_Sums(R_EAL F))#x= (Partial_Sums F)#x by MESFUN7C:1;
A4: Partial_Sums(F#x) = R_EAL(Partial_Sums(F#x))
.= Partial_Sums(R_EAL(F#x)) by Th5;
A5: R_EAL F is additive by Th9;
hereby
assume Partial_Sums(F#x) is convergent;
then Partial_Sums(R_EAL(F#x)) is convergent_to_finite_number by A4,
RINFSUP2:14;
then
(Partial_Sums(R_EAL F))#x is convergent_to_finite_number by A1,A5,A2,
MESFUNC9:33;
hence (Partial_Sums F)#x is convergent by A3,RINFSUP2:15;
end;
assume (Partial_Sums F)#x is convergent;
then (Partial_Sums(R_EAL F))#x is convergent_to_finite_number by A3,
RINFSUP2:14;
then Partial_Sums((R_EAL F)#x) is convergent_to_finite_number by A1,A5,
MESFUNC9:33;
hence Partial_Sums(F#x) is convergent by A4,A2,RINFSUP2:15;
end;
theorem Th14:
F is with_the_same_dom & dom f c= dom(F.0) & x in dom f & f.x =
Sum(F#x) implies f.x = lim((Partial_Sums F)#x)
proof
assume that
A1: F is with_the_same_dom & dom f c= dom(F.0) & x in dom f and
A2: f.x = Sum(F#x);
A3: dom Partial_Sums(F#x) = NAT & dom ((Partial_Sums F)#x) = NAT by
FUNCT_2:def 1;
for n be object st n in NAT
holds (Partial_Sums(F#x)).n = ((Partial_Sums F)#x).n by A1,Th12;
hence f.x = lim((Partial_Sums F)#x) by A2,A3,FUNCT_1:2;
end;
theorem Th15:
(for m be Nat holds F.m is_simple_func_in S) implies (
Partial_Sums F).n is_simple_func_in S
proof
assume
A1: for m be Nat holds F.m is_simple_func_in S;
for m be Nat holds (R_EAL F).m is_simple_func_in S
proof
let m be Nat;
F.m is_simple_func_in S by A1;
then R_EAL(F.m) is_simple_func_in S by MESFUNC6:49;
hence (R_EAL F).m is_simple_func_in S;
end;
then (Partial_Sums R_EAL F).n is_simple_func_in S by MESFUNC9:35;
then (R_EAL(Partial_Sums F)).n is_simple_func_in S by Th7;
then R_EAL((Partial_Sums F).n) is_simple_func_in S;
hence (Partial_Sums F).n is_simple_func_in S by MESFUNC6:49;
end;
theorem Th16:
(for n be Nat holds F.n is E-measurable) implies (
Partial_Sums F).m is E-measurable
proof
set PF = Partial_Sums F;
defpred P[Nat] means PF.$1 is E-measurable;
assume
A1: for n be Nat holds F.n is E-measurable;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A3: P[k];
F.(k+1) is E-measurable by A1;
then PF.k + F.(k+1) is E-measurable by A3,MESFUNC6:26;
hence thesis by Def2;
end;
PF.0 = F.0 by Def2;
then
A4: P[ 0 ] by A1;
for k being Nat holds P[k] from NAT_1:sch 2(A4,A2);
hence (Partial_Sums F).m is E-measurable;
end;
theorem Th17:
for X be non empty set, F be Functional_Sequence of X,REAL st F
is with_the_same_dom holds Partial_Sums F is with_the_same_dom
proof
let X be non empty set, F be Functional_Sequence of X,REAL;
assume
A1: F is with_the_same_dom;
let n,m be Nat;
dom((Partial_Sums F).n) = dom(F.0) by A1,Th11;
hence dom((Partial_Sums F).n) = dom((Partial_Sums F).m) by A1,Th11;
end;
theorem Th18:
dom(F.0) = E & F is with_the_same_dom & (for n be Nat holds (
Partial_Sums F).n is E-measurable) & (for x be Element of X st x in E holds
F#x is summable) implies lim(Partial_Sums F) is E-measurable
proof
assume that
A1: dom(F.0) = E & F is with_the_same_dom and
A2: for n be Nat holds (Partial_Sums F).n is E-measurable and
A3: for x be Element of X st x in E holds F#x is summable;
A4: now
let x be Element of X;
assume
A5: x in E;
then F#x is summable by A3;
then Partial_Sums(F#x) is convergent;
hence (Partial_Sums F)#x is convergent by A1,A5,Th13;
end;
dom((Partial_Sums F).0) = E & Partial_Sums F is with_the_same_dom
Functional_Sequence of X,REAL by A1,Th11,Th17;
hence thesis by A2,A4,MESFUN7C:21;
end;
theorem Th19:
(for n be Nat holds F.n is_integrable_on M) implies for m be Nat
holds (Partial_Sums F).m is_integrable_on M
proof
assume
A1: for n be Nat holds F.n is_integrable_on M;
let m be Nat;
for n be Nat holds (R_EAL F).n is_integrable_on M
proof
let n be Nat;
F.n is_integrable_on M by A1;
then R_EAL(F.n) is_integrable_on M;
hence (R_EAL F).n is_integrable_on M;
end;
then (Partial_Sums R_EAL F).m is_integrable_on M by MESFUNC9:45;
then ((R_EAL(Partial_Sums F)).m) is_integrable_on M by Th7;
then (R_EAL((Partial_Sums F).m)) is_integrable_on M;
hence (Partial_Sums F).m is_integrable_on M;
end;
begin :: Partial Sums of Complex-valued Functional Sequences
reserve F for Functional_Sequence of X,COMPLEX,
f for PartFunc of X,COMPLEX,
A for set;
theorem Th20:
(Re f)|A = Re(f|A) & (Im f)|A = Im(f|A)
proof
dom((Re f)|A) = (dom Re f) /\ A by RELAT_1:61
.= dom f /\ A by COMSEQ_3:def 3;
then
A1: dom((Re f)|A) = dom(f|A) by RELAT_1:61
.= dom Re(f|A) by COMSEQ_3:def 3;
now
let x be object;
assume
A2: x in dom(Re(f)|A);
then
A3: x in dom Re(f) /\ A by RELAT_1:61;
then
A4: x in dom Re f by XBOOLE_0:def 4;
A5: x in A by A3,XBOOLE_0:def 4;
thus Re(f|A).x = Re((f|A).x) by A1,A2,COMSEQ_3:def 3
.= Re(f.x) by A5,FUNCT_1:49
.= (Re f).x by A4,COMSEQ_3:def 3
.= ((Re f)|A).x by A5,FUNCT_1:49;
end;
hence (Re f)|A = Re(f|A) by A1,FUNCT_1:2;
dom((Im f)|A) = dom Im f /\ A by RELAT_1:61;
then dom((Im f)|A) = dom f /\ A by COMSEQ_3:def 4;
then
A6: dom((Im f)|A) = dom(f|A) by RELAT_1:61
.= dom Im(f|A) by COMSEQ_3:def 4;
now
let x be object;
assume
A7: x in dom(Im(f)|A);
then
A8: x in dom Im f /\ A by RELAT_1:61;
then
A9: x in dom Im f by XBOOLE_0:def 4;
A10: x in A by A8,XBOOLE_0:def 4;
thus Im(f|A).x = Im((f|A).x) by A6,A7,COMSEQ_3:def 4
.= Im(f.x) by A10,FUNCT_1:49
.= (Im f).x by A9,COMSEQ_3:def 4
.= ((Im f)|A).x by A10,FUNCT_1:49;
end;
hence (Im f)|A = Im(f|A) by A6,FUNCT_1:2;
end;
Lm1: for n be Nat holds (Re (F||D)).n = ((Re F).n)|D & (Im (F||D)).n = ((Im F)
.n)|D
proof
set G = F||D;
let n be Nat;
Re((F.n)|D) = (Re(F.n))|D by Th20;
then
A1: Re((F.n)|D) = ((Re F).n)|D by MESFUN7C:24;
Im((F.n)|D) = (Im(F.n))|D by Th20;
then
A2: Im((F.n)|D) = ((Im F).n)|D by MESFUN7C:24;
Re(G.n) = (Re G).n & Im(G.n) = (Im G).n by MESFUN7C:24;
hence (Re G).n = ((Re F).n)|D & (Im G).n = ((Im F).n)|D by A1,A2,Def1;
end;
theorem Th21:
Re (F||D) = (Re F)||D
proof
let n be Element of NAT;
(Re (F||D)).n = ((Re F).n)|D by Lm1;
hence thesis by Def1;
end;
theorem Th22:
Im (F||D) = (Im F)||D
proof
let n be Element of NAT;
(Im (F||D)).n = ((Im F).n)|D by Lm1;
hence thesis by Def1;
end;
theorem Th23:
F is with_the_same_dom & D c= dom(F.0) & x in D implies (F#x is
convergent implies (F||D)#x is convergent)
proof
set G = F||D;
assume that
A1: F is with_the_same_dom and
A2: D c= dom(F.0) and
A3: x in D;
Re G = (Re F)||D by Th21;
then
A4: (Re F)#x is convergent implies (Re G)#x is convergent by A3,Th1;
dom((Re F).0) = dom(F.0) by MESFUN7C:def 11;
then dom(((Re F).0)|D) = D by A2,RELAT_1:62;
then dom((Re G).0) = D by Lm1;
then
A5: dom(G.0) = D by MESFUN7C:def 11;
G is with_the_same_dom by A1,Th2;
then
A6: (Re G)#x = Re(G#x) & (Im G)#x = Im(G#x) by A3,A5,MESFUN7C:23;
Im G = (Im F)||D by Th22;
then
A7: (Im F)#x is convergent implies (Im G)#x is convergent by A3,Th1;
(Re F)#x = Re(F#x) & (Im F)#x = Im(F#x) by A1,A2,A3,MESFUN7C:23;
hence thesis by A4,A7,A6,COMSEQ_3:42;
end;
theorem Th24:
F is with_the_same_dom iff Re F is with_the_same_dom
proof
thus F is with_the_same_dom implies Re F is with_the_same_dom;
assume
A1: Re F is with_the_same_dom;
now
let n,m be Nat;
dom((Re F).n) = dom(F.n) & dom((Re F).m) = dom(F.m) by MESFUN7C:def 11;
hence dom(F.n) = dom(F.m) by A1;
end;
hence F is with_the_same_dom;
end;
theorem Th25:
Re F is with_the_same_dom iff Im F is with_the_same_dom
proof
hereby
assume Re F is with_the_same_dom;
then
F is with_the_same_dom by Th24;
then for n,m being Nat holds dom((Im F).n) = dom((Im F).m)
by MESFUN7C:def 12,MESFUNC8:def 2;
hence Im F is with_the_same_dom;
end;
assume
A1: Im F is with_the_same_dom;
now
let n,m be Nat;
dom((Im F).n) = dom(F.n) & dom((Im F).m) = dom(F.m) by MESFUN7C:def 12;
hence dom(F.n) = dom(F.m) by A1;
end;
then F is with_the_same_dom;
hence Re F is with_the_same_dom;
end;
theorem
F is with_the_same_dom & D = dom(F.0) & (for x be Element of X st x in
D holds F#x is convergent) implies (lim F)|D = lim (F||D)
proof
set G = F||D;
assume that
A1: F is with_the_same_dom and
A2: D = dom(F.0) and
A3: for x be Element of X st x in D holds F#x is convergent;
A4: Re G = (Re F)||D by Th21;
A5: now
let x be Element of X;
dom((F.0)|D) = D by A2,RELAT_1:62;
then
A6: dom(G.0) = D by Def1;
assume
A7: x in dom(G.0);
then F#x is convergent by A3,A6;
hence G#x is convergent by A1,A2,A7,A6,Th23;
end;
A8: for x be Element of X st x in D holds (Re F)#x is convergent
proof
let x be Element of X;
assume
A9: x in D;
then F#x is convergent Complex_Sequence by A3;
then Re(F#x) is convergent;
hence (Re F)#x is convergent by A1,A2,A9,MESFUN7C:23;
end;
D c= dom((Re F).0) by A2,MESFUN7C:def 11;
then (lim Re F)|D = lim Re G by A4,A8,Th3;
then
A10: (Re lim F)|D = lim Re G by A1,A2,A3,MESFUN7C:25;
A11: G is with_the_same_dom by A1,Th2;
then lim Re G = Re(lim G) by A5,MESFUN7C:25;
then
A12: Re((lim F)|D) = Re(lim G) by A10,Th20;
A13: for x be Element of X st x in D holds (Im F)#x is convergent
proof
let x be Element of X;
assume
A14: x in D;
then F#x is convergent Complex_Sequence by A3;
then Im(F#x) is convergent;
hence (Im F)#x is convergent by A1,A2,A14,MESFUN7C:23;
end;
A15: Im G = (Im F)||D by Th22;
D c= dom((Im F).0) by A2,MESFUN7C:def 12;
then (lim Im F)|D = lim Im G by A15,A13,Th3;
then
A16: (Im lim F)|D = lim Im G by A1,A2,A3,MESFUN7C:25;
lim Im G = Im(lim G) by A11,A5,MESFUN7C:25;
then
A17: Im((lim F)|D) = Im(lim G) by A16,Th20;
thus lim G = Re(lim G) + <i>(#)(Im(lim G)) by MESFUN6C:8
.= (lim F)|D by A12,A17,MESFUN6C:8;
end;
theorem
F is with_the_same_dom & E c= dom(F.0) & (for m be Nat holds F.m
is E-measurable) implies (F||E).n is E-measurable
proof
set G = F||E;
A1: Re G = (Re F)||E by Th21;
A2: Im G = (Im F)||E by Th22;
assume F is with_the_same_dom;
then
A3: Re F is with_the_same_dom;
then
A4: Im F is with_the_same_dom by Th25;
assume
A5: E c= dom(F.0);
assume
A6: for m be Nat holds F.m is E-measurable;
A7: for m be Nat holds (Re F).m is E-measurable & (Im F).m
is E-measurable
proof
let m be Nat;
F.m is E-measurable by A6;
then Re(F.m) is E-measurable & Im(F.m) is E-measurable by
MESFUN6C:def 1;
hence thesis by MESFUN7C:24;
end;
E c= dom((Im F).0) by A5,MESFUN7C:def 12;
then (Im G).n is E-measurable by A4,A2,A7,Th4;
then
A8: Im(G.n) is E-measurable by MESFUN7C:24;
E c= dom((Re F).0) by A5,MESFUN7C:def 11;
then (Re G).n is E-measurable by A3,A1,A7,Th4;
then Re(G.n) is E-measurable by MESFUN7C:24;
hence thesis by A8,MESFUN6C:def 1;
end;
theorem
E c= dom(F.0) & F is with_the_same_dom & (for x be Element of X st x
in E holds F#x is summable) implies for x be Element of X st x in E holds (F||E
)#x is summable
proof
set G = F||E;
assume that
A1: E c= dom(F.0) and
A2: F is with_the_same_dom and
A3: for x be Element of X st x in E holds F#x is summable;
A4: G is with_the_same_dom by A2,Th2;
A5: for x be Element of X st x in E holds (Im F)#x is summable
proof
let x be Element of X;
assume
A6: x in E;
then F#x is summable by A3;
then Im(F#x) is summable;
hence (Im F)#x is summable by A1,A2,A6,MESFUN7C:23;
end;
A7: for x be Element of X st x in E holds (Re F)#x is summable
proof
let x be Element of X;
assume
A8: x in E;
then F#x is summable by A3;
then Re(F#x) is summable;
hence (Re F)#x is summable by A1,A2,A8,MESFUN7C:23;
end;
hereby
let x be Element of X;
assume
A9: x in E;
G.0= (F.0)|E by Def1;
then
A10: x in dom(G.0) by A1,A9,RELAT_1:62;
Im G = (Im F)||E by Th22;
then (Im G)#x is summable by A5,A9,Th6;
then
A11: Im(G#x) is summable by A4,A10,MESFUN7C:23;
Re G = (Re F)||E by Th21;
then (Re G)#x is summable by A7,A9,Th6;
then Re(G#x) is summable by A4,A10,MESFUN7C:23;
hence G#x is summable by A11,COMSEQ_3:57;
end;
end;
definition
let X be non empty set, F be Functional_Sequence of X,COMPLEX;
func Partial_Sums F -> Functional_Sequence of X,COMPLEX means
:Def3:
it.0 = F.0 & for n be Nat holds it.(n+1) = it.n + F.(n+1);
existence
proof
defpred P[Nat,set,set] means (not $2 is PartFunc of X,COMPLEX &
$3 = F.$1) or ($2 is PartFunc of X,COMPLEX & for F2 be PartFunc of X,COMPLEX st
F2 = $2 holds $3 = F2 + F.($1+1));
A1: for n being Nat, x being set ex y being set st P[n,x,y]
proof
let n be Nat;
let x be set;
now
assume x is PartFunc of X,COMPLEX;
then reconsider G2 = x as PartFunc of X,COMPLEX;
take y = G2 + F.(n+1);
thus not x is PartFunc of X,COMPLEX & y = F.n or (x is PartFunc of X,
COMPLEX & for F2 be PartFunc of X,COMPLEX st F2 = x holds y = F2 + F.(n+1));
end;
hence thesis;
end;
consider IT being Function such that
A2: dom IT = NAT & IT.0 = F.0 & for n being Nat holds P[n,
IT.n,IT.(n+1)] from RECDEF_1:sch 1(A1);
now
defpred IND[Nat] means IT.$1 is PartFunc of X,COMPLEX;
let f be object;
assume f in rng IT;
then consider m be object such that
A3: m in dom IT and
A4: f = IT.m by FUNCT_1:def 3;
reconsider m as Element of NAT by A2,A3;
A5: for n be Nat st IND[n] holds IND[n+1]
proof
let n be Nat;
assume IND[n];
then reconsider F2 = IT.n as PartFunc of X,COMPLEX;
IT.(n+1) = F2 + F.(n+1) by A2;
hence IND[n+1];
end;
A6: IND[ 0 ] by A2;
for n be Nat holds IND[n] from NAT_1:sch 2(A6,A5);
then IT.m is PartFunc of X,COMPLEX;
hence f in PFuncs(X,COMPLEX) by A4,PARTFUN1:45;
end;
then rng IT c= PFuncs(X,COMPLEX) by TARSKI:def 3;
then reconsider IT as Functional_Sequence of X,COMPLEX by A2,FUNCT_2:def 1
,RELSET_1:4;
take IT;
thus thesis by A2;
end;
uniqueness
proof
let PS1,PS2 be Functional_Sequence of X,COMPLEX;
assume that
A7: PS1.0 = F.0 and
A8: for n be Nat holds PS1.(n+1) = PS1.n + F.(n+1) and
A9: PS2.0 = F.0 and
A10: for n be Nat holds PS2.(n+1) = PS2.n + F.(n+1);
defpred IND[Nat] means PS1.$1 = PS2.$1;
A11: for n be Nat st IND[n] holds IND[n+1]
proof
let n be Nat;
assume
A12: IND[n];
PS1.(n+1) = PS1.n + F.(n+1) by A8;
hence PS1.(n+1) = PS2.(n+1) by A10,A12;
end;
A13: IND[ 0 ] by A7,A9;
for n be Nat holds IND[n] from NAT_1:sch 2(A13,A11);
then for m be Element of NAT holds PS1.m = PS2.m;
hence thesis;
end;
end;
theorem Th29:
Partial_Sums Re F = Re Partial_Sums F & Partial_Sums Im F = Im Partial_Sums F
proof
defpred P[Nat] means
Partial_Sums(Re F).$1 = (Re Partial_Sums F).$1;
defpred R[Nat] means
Partial_Sums(Im F).$1 = (Im Partial_Sums F).$1;
A1: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume P[k];
then Partial_Sums(Re F).(k+1) =(Re Partial_Sums F).k + Re F.(k+1) by Def2
.=(Re Partial_Sums F).k +Re(F.(k+1)) by MESFUN7C:24
.=Re((Partial_Sums F).k) +Re(F.(k+1)) by MESFUN7C:24
.=Re((Partial_Sums F).k + F.(k+1)) by MESFUN6C:5
.=Re((Partial_Sums F).(k+1)) by Def3;
hence thesis by MESFUN7C:24;
end;
A2: for k be Nat st R[k] holds R[k+1]
proof
let k be Nat;
assume R[k];
then Partial_Sums(Im F).(k+1) = (Im Partial_Sums F).k + Im F.(k+1) by Def2
.=(Im Partial_Sums F).k +Im(F.(k+1)) by MESFUN7C:24
.=Im((Partial_Sums F).k) +Im(F.(k+1)) by MESFUN7C:24
.=Im((Partial_Sums F).k + F.(k+1)) by MESFUN6C:5
.=Im((Partial_Sums F).(k+1)) by Def3;
hence thesis by MESFUN7C:24;
end;
Partial_Sums(Im F).0 = Im F.0 by Def2
.= Im(F.0) by MESFUN7C:24
.= Im((Partial_Sums F).0) by Def3;
then
A3: R[ 0 ] by MESFUN7C:24;
A4: for i being Nat holds R[i] from NAT_1:sch 2(A3,A2);
Partial_Sums(Re F).0 = Re F.0 by Def2
.= Re(F.0) by MESFUN7C:24
.= Re(Partial_Sums F.0) by Def3;
then
A5: P[ 0 ] by MESFUN7C:24;
for i being Nat holds P[i] from NAT_1:sch 2(A5,A1);
hence thesis by A4;
end;
theorem
z in dom((Partial_Sums F).n) & m <= n implies z in dom((Partial_Sums F
).m) & z in dom(F.m)
proof
assume
A1: z in dom((Partial_Sums F).n) & m <= n;
A2: dom((Partial_Sums F).n) = dom((Re(Partial_Sums F)).n) by MESFUN7C:def 11
.= dom((Partial_Sums Re F).n) by Th29;
dom((Partial_Sums Re F).m) = dom((Re(Partial_Sums F)).m) by Th29
.= dom((Partial_Sums F).m) by MESFUN7C:def 11;
hence z in dom((Partial_Sums F).m) by A1,A2,Th8;
z in dom((Re F).m) by A1,A2,Th8;
hence z in dom(F.m) by MESFUN7C:def 11;
end;
theorem
dom((Partial_Sums F).n) = meet{dom(F.k) where k is Element of NAT : k <= n}
proof
now
let A be object;
assume A in {dom((Re F).k) where k is Element of NAT : k <= n};
then consider i be Element of NAT such that
A1: A = dom((Re F).i) and
A2: i <= n;
A = dom(F.i) by A1,MESFUN7C:def 11;
hence A in {dom(F.k) where k is Element of NAT : k <= n} by A2;
end;
then
A3: {dom((Re F).k) where k is Element of NAT : k <= n} c= {dom(F.k) where k
is Element of NAT : k <= n} by TARSKI:def 3;
now
let A be object;
assume A in {dom(F.k) where k is Element of NAT : k <= n};
then consider i be Element of NAT such that
A4: A = dom(F.i) and
A5: i <= n;
A = dom((Re F).i) by A4,MESFUN7C:def 11;
hence A in {dom((Re F).k) where k is Element of NAT : k <= n} by A5;
end;
then
A6: {dom(F.k) where k is Element of NAT : k <= n} c= {dom((Re F).k) where k
is Element of NAT : k <= n} by TARSKI:def 3;
dom((Partial_Sums Re F).n) = dom((Re(Partial_Sums F)).n) by Th29;
then
A7: dom((Partial_Sums Re F).n) = dom((Partial_Sums F).n) by MESFUN7C:def 11;
dom((Partial_Sums Re F).n) = meet{dom((Re F).k) where k is Element of NAT
: k <= n} by Th10;
hence thesis by A7,A3,A6,XBOOLE_0:def 10;
end;
theorem Th32:
F is with_the_same_dom implies dom((Partial_Sums F).n) = dom(F.0 )
proof
assume F is with_the_same_dom;
then Re F is with_the_same_dom;
then dom((Partial_Sums Re F).n) = dom((Re F).0) by Th11;
then dom((Partial_Sums Re F).n) = dom(F.0) by MESFUN7C:def 11;
then dom((Re Partial_Sums F).n) = dom(F.0) by Th29;
hence dom((Partial_Sums F).n) = dom(F.0) by MESFUN7C:def 11;
end;
theorem
F is with_the_same_dom & D c= dom(F.0) & x in D implies (Partial_Sums(
F#x)).n = ((Partial_Sums F)#x).n
proof
assume that
A1: F is with_the_same_dom and
A2: D c= dom(F.0) and
A3: x in D;
A4: D c= dom((Im F).0) by A2,MESFUN7C:def 12;
dom((Partial_Sums F).n) = dom(F.0) by A1,Th32;
then
A5: x in dom((Partial_Sums F).n) by A2,A3;
then
A6: x in dom Re((Partial_Sums F).n) by COMSEQ_3:def 3;
A7: Re F is with_the_same_dom by A1;
then Im F is with_the_same_dom by Th25;
then
A8: (Partial_Sums((Im F)#x)).n = ((Partial_Sums Im F)#x).n by A3,A4,Th12;
D c= dom((Re F).0) by A2,MESFUN7C:def 11;
then
A9: (Partial_Sums((Re F)#x)).n = ((Partial_Sums Re F)#x).n by A3,A7,Th12;
A10: Re((Partial_Sums(F#x)).n) = (Re(Partial_Sums(F#x))).n by COMSEQ_3:def 5
.= (Partial_Sums Re(F#x)).n by COMSEQ_3:26
.= (Partial_Sums((Re F)#x)).n by A1,A2,A3,MESFUN7C:23
.= ((Partial_Sums Re F).n).x by A9,SEQFUNC:def 10
.= ((Re(Partial_Sums F)).n).x by Th29
.= (Re((Partial_Sums F).n)).x by MESFUN7C:24
.= Re(((Partial_Sums F).n).x) by A6,COMSEQ_3:def 3
.= Re(((Partial_Sums F)#x).n) by MESFUN7C:def 9;
A11: x in dom Im((Partial_Sums F).n) by A5,COMSEQ_3:def 4;
A12: Im((Partial_Sums(F#x)).n) = (Im(Partial_Sums(F#x))).n by
COMSEQ_3:def 6
.= (Partial_Sums Im(F#x)).n by COMSEQ_3:26
.= (Partial_Sums((Im F)#x)).n by A1,A2,A3,MESFUN7C:23
.= ((Partial_Sums Im F).n).x by A8,SEQFUNC:def 10
.= ((Im(Partial_Sums F)).n).x by Th29
.= (Im((Partial_Sums F).n)).x by MESFUN7C:24
.= Im(((Partial_Sums F).n).x) by A11,COMSEQ_3:def 4
.= Im(((Partial_Sums F)#x).n) by MESFUN7C:def 9;
thus (Partial_Sums(F#x)).n = Re((Partial_Sums(F#x)).n) + ( Im((Partial_Sums(
F#x)).n) )*<i> by COMPLEX1:13
.= ((Partial_Sums F)#x).n by A10,A12,COMPLEX1:13;
end;
theorem Th34:
F is with_the_same_dom implies Partial_Sums F is with_the_same_dom
proof
assume F is with_the_same_dom;
then Re F is with_the_same_dom;
then Partial_Sums Re F is with_the_same_dom by Th17;
then Re(Partial_Sums F) is with_the_same_dom by Th29;
hence Partial_Sums F is with_the_same_dom by Th24;
end;
theorem Th35:
F is with_the_same_dom & D c= dom(F.0) & x in D implies (
Partial_Sums(F#x) is convergent iff (Partial_Sums F)#x is convergent )
proof
assume that
A1: F is with_the_same_dom and
A2: D c= dom(F.0) and
A3: x in D;
A4: D c= dom((Re F).0) by A2,MESFUN7C:def 11;
A5: D c= dom((Im F).0) by A2,MESFUN7C:def 12;
A6: dom((Partial_Sums F).0) = dom(F.0) & Partial_Sums F is with_the_same_dom
by A1,Th32,Th34;
A7: Re F is with_the_same_dom by A1;
then
A8: Im F is with_the_same_dom by Th25;
hereby
assume
A9: Partial_Sums(F#x) is convergent;
then Im(Partial_Sums(F#x)) is convergent;
then Partial_Sums Im(F#x) is convergent by COMSEQ_3:26;
then Partial_Sums((Im F)#x) is convergent by A1,A2,A3,MESFUN7C:23;
then (Partial_Sums Im F)#x is convergent by A3,A8,A5,Th13;
then (Im(Partial_Sums F))#x is convergent by Th29;
then
A10: Im((Partial_Sums F)#x) is convergent by A2,A3,A6,MESFUN7C:23;
Re(Partial_Sums(F#x)) is convergent by A9;
then Partial_Sums Re(F#x) is convergent by COMSEQ_3:26;
then Partial_Sums((Re F)#x) is convergent by A1,A2,A3,MESFUN7C:23;
then (Partial_Sums Re F)#x is convergent by A3,A7,A4,Th13;
then (Re(Partial_Sums F))#x is convergent by Th29;
then Re((Partial_Sums F)#x) is convergent by A2,A3,A6,MESFUN7C:23;
hence (Partial_Sums F)#x is convergent by A10,COMSEQ_3:42;
end;
assume
A11: (Partial_Sums F)#x is convergent;
then Im((Partial_Sums F)#x) is convergent;
then
A12: (Im(Partial_Sums F))#x is convergent by A2,A3,A6,MESFUN7C:23;
A13: (Im F)#x = Im(F#x) by A1,A2,A3,MESFUN7C:23;
Re((Partial_Sums F)#x) is convergent by A11;
then
A14: (Re(Partial_Sums F))#x is convergent by A2,A3,A6,MESFUN7C:23;
Partial_Sums((Im F)#x) is convergent iff (Partial_Sums Im F)#x is
convergent by A3,A8,A5,Th13;
then
A15: Im(Partial_Sums(F#x)) is convergent by A12,A13,Th29,COMSEQ_3:26;
A16: (Re F)#x = Re(F#x) by A1,A2,A3,MESFUN7C:23;
Partial_Sums((Re F)#x) is convergent iff (Partial_Sums Re F)#x is
convergent by A3,A7,A4,Th13;
then Re(Partial_Sums(F#x)) is convergent by A14,A16,Th29,COMSEQ_3:26;
hence Partial_Sums(F#x) is convergent by A15,COMSEQ_3:42;
end;
theorem
F is with_the_same_dom & dom f c= dom(F.0) & x in dom f & F#x is
summable & f.x = Sum(F#x) implies f.x = lim((Partial_Sums F)#x)
proof
assume that
A1: F is with_the_same_dom and
A2: dom f c= dom(F.0) and
A3: x in dom f and
A4: F#x is summable and
A5: f.x = Sum(F#x);
dom Re f = dom f by COMSEQ_3:def 3;
then
A6: dom Re f c= dom((Re F).0) by A2,MESFUN7C:def 11;
Partial_Sums(F#x) is convergent by A4;
then (Partial_Sums F)#x is convergent by A1,A2,A3,Th35;
then
A7: lim(Re((Partial_Sums F)#x)) = Re(lim((Partial_Sums F)#x)) & lim(Im((
Partial_Sums F)#x)) = Im(lim((Partial_Sums F)#x)) by COMSEQ_3:41;
dom Im f = dom f by COMSEQ_3:def 4;
then
A8: dom Im f c= dom((Im F).0) by A2,MESFUN7C:def 12;
A9: x in dom Im f by A3,COMSEQ_3:def 4;
then
A10: (Im f).x = Im(f.x) by COMSEQ_3:def 4;
A11: Partial_Sums F is with_the_same_dom & dom((Partial_Sums F).0) = dom(F.0
) by A1,Th32,Th34;
then (Re(Partial_Sums F))#x = Re((Partial_Sums F)#x) by A2,A3,MESFUN7C:23;
then
A12: lim((Partial_Sums Re F)#x) = lim(Re((Partial_Sums F)#x)) by Th29;
(Im(Partial_Sums F))#x = Im((Partial_Sums F)#x) by A2,A3,A11,MESFUN7C:23;
then
A13: lim((Partial_Sums Im F)#x) = lim(Im((Partial_Sums F)#x)) by Th29;
A14: x in dom Re f by A3,COMSEQ_3:def 3;
then
A15: (Re f).x = Re(f.x) by COMSEQ_3:def 3;
A16: Re F is with_the_same_dom by A1;
then
A17: Im F is with_the_same_dom by Th25;
Re(F#x) = (Re F)#x & Im(F#x) = (Im F)#x by A1,A2,A3,MESFUN7C:23;
then
A18: Sum(F#x) = Sum((Re F)#x) + Sum((Im F)#x)*<i> by A4,COMSEQ_3:53;
then Re(Sum(F#x)) = Sum((Re F)#x) by COMPLEX1:12;
then (Re f).x = Sum((Re F)#x) by A5,A14,COMSEQ_3:def 3;
then
A19: (Re f).x = lim((Partial_Sums Re F)#x) by A16,A6,A14,Th14;
Im(Sum(F#x)) = Sum((Im F)#x) by A18,COMPLEX1:12;
then (Im f).x = Sum((Im F)#x) by A5,A9,COMSEQ_3:def 4;
then
A20: (Im f).x = lim((Partial_Sums Im F)#x) by A17,A8,A9,Th14;
thus f.x = Re(f.x) + Im(f.x)*<i> by COMPLEX1:13
.= lim((Partial_Sums F)#x) by A15,A10,A19,A20,A7,A12,A13,COMPLEX1:13;
end;
theorem
(for m be Nat holds F.m is_simple_func_in S) implies (Partial_Sums F).
n is_simple_func_in S
proof
assume
A1: for m be Nat holds F.m is_simple_func_in S;
for m be Nat holds (Im F).m is_simple_func_in S
proof
let m be Nat;
F.m is_simple_func_in S by A1;
then Im(F.m) is_simple_func_in S by MESFUN7C:43;
hence (Im F).m is_simple_func_in S by MESFUN7C:24;
end;
then (Partial_Sums Im F).n is_simple_func_in S by Th15;
then (Im(Partial_Sums F)).n is_simple_func_in S by Th29;
then
A2: Im((Partial_Sums F).n) is_simple_func_in S by MESFUN7C:24;
for m be Nat holds (Re F).m is_simple_func_in S
proof
let m be Nat;
F.m is_simple_func_in S by A1;
then Re(F.m) is_simple_func_in S by MESFUN7C:43;
hence (Re F).m is_simple_func_in S by MESFUN7C:24;
end;
then (Partial_Sums Re F).n is_simple_func_in S by Th15;
then (Re(Partial_Sums F)).n is_simple_func_in S by Th29;
then Re((Partial_Sums F).n) is_simple_func_in S by MESFUN7C:24;
hence (Partial_Sums F).n is_simple_func_in S by A2,MESFUN7C:43;
end;
Lm2: (for n be Nat holds F.n is E-measurable) implies (Re F).m
is E-measurable & (Im F).m is E-measurable
proof
assume for n be Nat holds F.n is E-measurable;
then F.m is E-measurable;
then Re(F.m) is E-measurable & Im(F.m) is E-measurable by
MESFUN6C:def 1;
hence (Re F).m is E-measurable & (Im F).m is E-measurable by
MESFUN7C:24;
end;
theorem
(for n be Nat holds F.n is E-measurable) implies (Partial_Sums F).m
is E-measurable
proof
assume
A1: for n be Nat holds F.n is E-measurable;
then for n be Nat holds (Im F).n is E-measurable by Lm2;
then (Partial_Sums Im F).m is E-measurable by Th16;
then (Im(Partial_Sums F)).m is E-measurable by Th29;
then
A2: Im((Partial_Sums F).m) is E-measurable by MESFUN7C:24;
for n be Nat holds (Re F).n is E-measurable by A1,Lm2;
then (Partial_Sums Re F).m is E-measurable by Th16;
then (Re(Partial_Sums F)).m is E-measurable by Th29;
then Re((Partial_Sums F).m) is E-measurable by MESFUN7C:24;
hence (Partial_Sums F).m is E-measurable by A2,MESFUN6C:def 1;
end;
theorem
dom(F.0) = E & F is with_the_same_dom & (for n be Nat holds (
Partial_Sums F).n is E-measurable) & (for x be Element of X st x in E holds
F#x is summable) implies lim(Partial_Sums F) is E-measurable
proof
assume that
A1: dom(F.0) = E and
A2: F is with_the_same_dom and
A3: for n be Nat holds (Partial_Sums F).n is E-measurable and
A4: for x be Element of X st x in E holds F#x is summable;
A5: dom((Im F).0) = E by A1,MESFUN7C:def 12;
A6: for x be Element of X st x in dom((Partial_Sums F).0) holds (
Partial_Sums F)#x is convergent
proof
let x be Element of X;
assume
A7: x in dom((Partial_Sums F).0);
A8: dom((Partial_Sums F).0) = dom(F.0) by A2,Th32;
then F#x is summable by A1,A4,A7;
then Partial_Sums (F#x) is convergent;
hence (Partial_Sums F)#x is convergent by A2,A7,A8,Th35;
end;
A9: for n be Nat holds (Partial_Sums Im F).n is E-measurable
proof
let n be Nat;
(Partial_Sums F).n is E-measurable by A3;
then Im((Partial_Sums F).n) is E-measurable by MESFUN6C:def 1;
then (Im(Partial_Sums F)).n is E-measurable by MESFUN7C:24;
hence (Partial_Sums Im F).n is E-measurable by Th29;
end;
A10: for x be Element of X st x in E holds (Im F)#x is summable
proof
let x be Element of X;
assume
A11: x in E;
then F#x is summable by A4;
then Im(F#x) is summable;
hence (Im F)#x is summable by A1,A2,A11,MESFUN7C:23;
end;
A12: Re F is with_the_same_dom by A2;
then Im F is with_the_same_dom by Th25;
then lim(Partial_Sums Im F) is E-measurable by A5,A9,A10,Th18;
then
A13: lim(Im(Partial_Sums F)) is E-measurable by Th29;
A14: for x be Element of X st x in E holds (Re F)#x is summable
proof
let x be Element of X;
assume
A15: x in E;
then F#x is summable by A4;
then Re(F#x) is summable;
hence (Re F)#x is summable by A1,A2,A15,MESFUN7C:23;
end;
A16: for n be Nat holds (Partial_Sums Re F).n is E-measurable
proof
let n be Nat;
(Partial_Sums F).n is E-measurable by A3;
then Re((Partial_Sums F).n) is E-measurable by MESFUN6C:def 1;
then (Re(Partial_Sums F)).n is E-measurable by MESFUN7C:24;
hence (Partial_Sums Re F).n is E-measurable by Th29;
end;
A17: Partial_Sums F is with_the_same_dom by A2,Th34;
then lim(Im(Partial_Sums F)) = R_EAL Im(lim(Partial_Sums F)) by A6,
MESFUN7C:25;
then
A18: Im(lim(Partial_Sums F)) is E-measurable by A13;
dom((Re F).0) = E by A1,MESFUN7C:def 11;
then lim(Partial_Sums Re F) is E-measurable by A12,A16,A14,Th18;
then
A19: lim(Re(Partial_Sums F)) is E-measurable by Th29;
lim(Re(Partial_Sums F)) = R_EAL Re(lim(Partial_Sums F)) by A6,A17,MESFUN7C:25
;
then Re(lim(Partial_Sums F)) is E-measurable by A19;
hence lim(Partial_Sums F) is E-measurable by A18,MESFUN6C:def 1;
end;
theorem
(for n be Nat holds F.n is_integrable_on M) implies for m be Nat holds
(Partial_Sums F).m is_integrable_on M
proof
assume
A1: for n be Nat holds F.n is_integrable_on M;
A2: for n be Nat holds (Im F).n is_integrable_on M
proof
let n be Nat;
F.n is_integrable_on M by A1;
then Im(F.n) is_integrable_on M by MESFUN6C:def 2;
hence (Im F).n is_integrable_on M by MESFUN7C:24;
end;
A3: for n be Nat holds (Re F).n is_integrable_on M
proof
let n be Nat;
F.n is_integrable_on M by A1;
then Re(F.n) is_integrable_on M by MESFUN6C:def 2;
hence (Re F).n is_integrable_on M by MESFUN7C:24;
end;
thus for m be Nat holds (Partial_Sums F).m is_integrable_on M
proof
let m be Nat;
(Partial_Sums Im F).m is_integrable_on M by A2,Th19;
then (Im(Partial_Sums F)).m is_integrable_on M by Th29;
then
A4: Im((Partial_Sums F).m) is_integrable_on M by MESFUN7C:24;
(Partial_Sums Re F).m is_integrable_on M by A3,Th19;
then (Re(Partial_Sums F)).m is_integrable_on M by Th29;
then Re((Partial_Sums F).m) is_integrable_on M by MESFUN7C:24;
hence (Partial_Sums F).m is_integrable_on M by A4,MESFUN6C:def 2;
end;
end;
begin :: Selected Properties of Complex-valued Simple Functions
reserve f,g for PartFunc of X,COMPLEX,
A for Element of S;
theorem
f is_simple_func_in S implies f is A-measurable
proof
assume
A1: f is_simple_func_in S;
then Im f is_simple_func_in S by MESFUN7C:43;
then
A2: Im f is A-measurable by MESFUNC6:50;
Re f is_simple_func_in S by A1,MESFUN7C:43;
then Re f is A-measurable by MESFUNC6:50;
hence f is A-measurable by A2,MESFUN6C:def 1;
end;
theorem
f is_simple_func_in S implies f|A is_simple_func_in S
proof
assume
A1: f is_simple_func_in S;
then Im f is_simple_func_in S by MESFUN7C:43;
then R_EAL Im f is_simple_func_in S by MESFUNC6:49;
then R_EAL((Im f)|A) is_simple_func_in S by MESFUNC5:34;
then (Im f)|A is_simple_func_in S by MESFUNC6:49;
then
A2: Im(f|A) is_simple_func_in S by MESFUN6C:7;
Re f is_simple_func_in S by A1,MESFUN7C:43;
then R_EAL Re f is_simple_func_in S by MESFUNC6:49;
then R_EAL((Re f)|A) is_simple_func_in S by MESFUNC5:34;
then (Re f)|A is_simple_func_in S by MESFUNC6:49;
then Re(f|A) is_simple_func_in S by MESFUN6C:7;
hence f|A is_simple_func_in S by A2,MESFUN7C:43;
end;
theorem
f is_simple_func_in S implies dom f is Element of S
by MESFUNC2:31;
theorem
f is_simple_func_in S & g is_simple_func_in S implies f+g is_simple_func_in S
proof
assume
A1: f is_simple_func_in S & g is_simple_func_in S;
then Im f is_simple_func_in S & Im g is_simple_func_in S by MESFUN7C:43;
then Im f + Im g is_simple_func_in S by MESFUNC6:72;
then
A2: Im(f+g) is_simple_func_in S by MESFUN6C:5;
Re f is_simple_func_in S & Re g is_simple_func_in S by A1,MESFUN7C:43;
then Re f + Re g is_simple_func_in S by MESFUNC6:72;
then Re(f+g) is_simple_func_in S by MESFUN6C:5;
hence thesis by A2,MESFUN7C:43;
end;
theorem
for c be Complex st f is_simple_func_in S holds c(#)f
is_simple_func_in S
proof
let c be Complex;
assume
A1: f is_simple_func_in S;
then
A2: Re f is_simple_func_in S by MESFUN7C:43;
then
A3: (Im c)(#)(Re f) is_simple_func_in S by MESFUNC6:73;
A4: Im f is_simple_func_in S by A1,MESFUN7C:43;
then (Im c)(#)(Im f) is_simple_func_in S by MESFUNC6:73;
then (-1)(#)((Im c)(#)(Im f)) is_simple_func_in S by MESFUNC6:73;
then
A5: R_EAL( -(Im c)(#)(Im f) ) is_simple_func_in S by MESFUNC6:49;
(Re c)(#)(Re f) is_simple_func_in S by A2,MESFUNC6:73;
then R_EAL( (Re c)(#)(Re f) ) is_simple_func_in S by MESFUNC6:49;
then R_EAL( (Re c)(#)(Re f) ) + R_EAL( -(Im c)(#)(Im f) ) is_simple_func_in
S by A5,MESFUNC5:38;
then R_EAL((Re c)(#)(Re f) - (Im c)(#)(Im f)) is_simple_func_in S by
MESFUNC6:23;
then (Re c)(#)(Re f) - (Im c)(#)(Im f) is_simple_func_in S by MESFUNC6:49;
then
A6: Re(c(#)f) is_simple_func_in S by MESFUN6C:3;
(Re c)(#)(Im f) is_simple_func_in S by A4,MESFUNC6:73;
then (Im c)(#)(Re f) + (Re c)(#)(Im f) is_simple_func_in S by A3,MESFUNC6:72;
then Im(c(#)f) is_simple_func_in S by MESFUN6C:3;
hence thesis by A6,MESFUN7C:43;
end;
begin :: Lebesgue's Convergence theorem of Complex-valued Function
reserve F for with_the_same_dom Functional_Sequence of X,ExtREAL,
P for PartFunc of X,ExtREAL;
theorem Th46:
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) & (for x be Element of X st x in E holds
F#x is convergent) implies lim 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 and
A6: for x be Element of X st x in E holds F#x is convergent;
A7: E = dom lim_sup F by A1,MESFUNC8:def 8;
A8: 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
A9: x in E;
then x in dom(F.k) by A1,MESFUNC8:def 2;
then
A10: x in dom |.(F.k).| by MESFUNC1:def 10;
(|. F.k .|).x <= P.x by A5,A9;
then |. (F.k).x .| <= P.x by A10,MESFUNC1:def 10;
then -(P.x) <= (F.k).x & (F.k).x <= P.x by EXTREAL1:23;
hence -(P.x) <= (F#x).k & (F#x).k <= P.x by MESFUNC5:def 13;
end;
A11: now
let x be Element of X;
assume
A12: x in dom lim_sup F;
for k be Nat holds (superior_realsequence(F#x)).k >= -(P.x)
proof
let k be Nat;
A13: (superior_realsequence(F#x)).k >= (F#x).k by RINFSUP2:8;
(F#x).k >= -(P.x) by A7,A8,A12;
hence (superior_realsequence(F#x)).k >= -(P.x) by A13,XXREAL_0:2;
end;
then lim_sup(F#x) >= -(P.x) by MESFUN10:4;
then
A14: (lim_sup F).x >= -(P.x) by A12,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 A7,A8,A12;
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
A15: 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 A15,XXREAL_0:2;
then P.x >= (lim_sup F).x by A12,MESFUNC8:def 8;
hence |. (lim_sup F).x .| <= P.x by A14,EXTREAL1:23;
end;
A16: now
let x be Element of X;
assume
A17: x in dom lim F;
then x in E by A1,MESFUNC8:def 9;
then F#x is convergent by A6;
hence (lim F).x = (lim_sup F).x by A17,MESFUNC8:14;
end;
A18: lim_sup F is E-measurable by A1,A3,MESFUNC8:23;
E = dom lim F by A1,MESFUNC8:def 9;
then lim F = lim_sup F by A7,A16,PARTFUN1:5;
hence lim F is_integrable_on M by A2,A4,A7,A18,A11,MESFUNC5:102;
end;
reserve F for with_the_same_dom Functional_Sequence of X,REAL,
f,P for PartFunc of X,REAL;
theorem Th47:
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) & (for x be Element of X st x in E holds
F#x is convergent) implies lim 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 E-measurable and
A3: P is_integrable_on M and
A4: for x be Element of X, n be Nat st x in E holds (|. F.n .|).x <= P.x and
A5: for x be Element of X st x in E holds F#x is convergent;
A6: for n be Nat holds (R_EAL F).n is E-measurable
proof
let n be Nat;
F.n is E-measurable by A2;
then R_EAL (F.n) is E-measurable;
hence (R_EAL F).n is E-measurable;
end;
A7: for x be Element of X st x in E holds (R_EAL F)#x is convergent
proof
let x be Element of X;
assume x in E;
then
A8: F#x is convergent by A5;
(R_EAL F)#x = F#x by MESFUN7C:1;
hence (R_EAL F)#x is convergent by A8,RINFSUP2:14;
end;
A9: for x be Element of X, n be Nat st x in E holds (|. (R_EAL F).n .|).x <=
(R_EAL P).x
proof
let x be Element of X, n be Nat;
A10: R_EAL |. F.n .| = |. R_EAL (F.n) .| by MESFUNC6:1;
assume x in E;
hence (|. (R_EAL F).n .|).x <= (R_EAL P).x by A4,A10;
end;
R_EAL P is_integrable_on M by A3;
hence lim F is_integrable_on M by A1,A6,A9,A7,Th46;
end;
:: Lebesgue's Convergence theorem
theorem Th48:
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 ex I be Real_Sequence st (for n
be Nat holds I.n = Integral(M,F.n)) & ( (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: for x be Element of X, n be Nat st x in E holds (|. F.n .|).x <= P.x;
A6: R_EAL P is_integrable_on M by A4;
A7: for x be Element of X, n be Nat st x in E holds (|. (R_EAL F).n .|).x <=
(R_EAL P).x
proof
let x be Element of X, n be Nat;
A8: R_EAL |. F.n .| = |. R_EAL (F.n) .| by MESFUNC6:1;
assume x in E;
hence (|. (R_EAL F).n .|).x <= (R_EAL P).x by A5,A8;
end;
A9: for n be Nat holds (R_EAL F).n is E-measurable
proof
let n be Nat;
F.n is E-measurable by A3;
then R_EAL (F.n) is E-measurable;
hence (R_EAL F).n is E-measurable;
end;
now
let x be object;
assume
A10: x in dom P;
then x in dom|. F.0 .| by A1,A2,VALUED_1:def 11;
then (|. F.0 .|).x = |. (F.0).x qua Complex .| by VALUED_1:def 11;
then |. (F.0).x qua Complex .| <= P.x by A2,A5,A10;
hence 0<= P.x by COMPLEX1:46;
end;
then P is nonnegative by MESFUNC6:52;
then consider J be ExtREAL_sequence such that
A11: for n be Nat holds J.n = Integral(M,(R_EAL F).n) and
lim_inf J >= Integral(M,lim_inf(R_EAL F)) and
lim_sup J <= Integral(M,lim_sup(R_EAL F)) and
A12: (for x be Element of X st x in E holds (R_EAL F)#x is convergent)
implies J is convergent & lim J = Integral(M,lim(R_EAL F)) by A1,A2,A9,A6,A7,
MESFUN10:17;
A13: Integral(M,R_EAL P) < +infty by A6,MESFUNC5:96;
for n be Nat holds |. J.n .| < +infty
proof
let n be Nat;
A14: E = dom((R_EAL F).n) & (R_EAL F).n is E-measurable by A1,A9,
MESFUNC8:def 2;
|. (R_EAL F).n .| is_integrable_on M by A1,A2,A9,A6,A7,MESFUN10:16;
then (R_EAL F).n is_integrable_on M by A14,MESFUNC5:100;
then
A15: |. Integral(M,(R_EAL F).n) .| <= Integral(M,|. (R_EAL F).n .|) by
MESFUNC5:101;
for x be Element of X st x in dom((R_EAL F).n) holds |. ((R_EAL F).n)
.x .| <= (R_EAL P).x
proof
let x be Element of X;
assume
A16: x in dom((R_EAL F).n);
then x in E by A1,MESFUNC8:def 2;
then
A17: (|. (R_EAL F).n .|).x <= (R_EAL P).x by A7;
x in dom |. (R_EAL F).n .| by A16,MESFUNC1:def 10;
hence |. ((R_EAL F).n).x .| <= (R_EAL P).x by A17,MESFUNC1:def 10;
end;
then Integral(M,|. (R_EAL F).n .|) <= Integral(M,R_EAL P) by A2,A6,A14,
MESFUNC5:102;
then |. Integral(M,(R_EAL F).n) .| <= Integral(M,R_EAL P) by A15,XXREAL_0:2
;
then |. Integral(M,(R_EAL F).n) .| < +infty by A13,XXREAL_0:2;
hence |. J.n .| < +infty by A11;
end;
then for n be Element of NAT st n in dom J holds |. J.n .| < +infty;
then J is real-valued by MESFUNC2:def 1;
then reconsider I=J as Real_Sequence by RINFSUP2:6;
(for x be Element of X st x in E holds F#x is convergent) implies J is
convergent_to_finite_number & lim J = Integral(M,lim F)
proof
assume
A18: for x be Element of X st x in E holds F#x is convergent;
A19: now
let x be Element of X;
assume x in E;
then
A20: F#x is convergent by A18;
F#x = (R_EAL F)#x by MESFUN7C:1;
hence (R_EAL F)#x is convergent by A20,RINFSUP2:14;
end;
lim F is_integrable_on M by A1,A2,A3,A4,A5,A18,Th47;
then
A21: -infty < Integral(M,lim F) & Integral(M,lim F) < +infty by MESFUNC5:96;
J is convergent implies J is convergent_to_finite_number
by A12,A19,A21,MESFUNC5:def 12;
hence thesis by A12,A19;
end;
then
A22: (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 RINFSUP2:15;
for n be Nat holds I.n = Integral(M,F.n) by A11;
hence thesis by A22;
end;
definition
let X be set, F be Functional_Sequence of X,REAL;
attr F is uniformly_bounded means
ex K be Real st for n be Nat
, x be Element of X st x in dom(F.0)
holds |. (F.n).x qua Complex .| <= K;
end;
:: Lebesgue's Bounded Convergence Theorem
theorem Th49:
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 & E = dom(F.0) and
A2: for n be Nat holds F.n is E-measurable and
A3: F is uniformly_bounded and
A4: for x be Element of X st x in E holds F#x is convergent;
consider K be Real such that
A5: for n be Nat, x be Element of X st x in dom(F.0)
holds |. (F.n).x qua Complex .|
<= K by A3;
A6: for x be Element of X st x in E holds (R_EAL F)#x is convergent
proof
let x be Element of X;
assume x in E;
then
A7: F#x is convergent by A4;
(R_EAL F)#x = F#x by MESFUN7C:1;
hence (R_EAL F)#x is convergent by A7,RINFSUP2:14;
end;
for n be Nat, x be set st x in dom((R_EAL F).0)
holds |. ((R_EAL F).n).x.| <= K
proof
let n be Nat, x be set;
A8: |. (F.n).x qua Complex .| = |. (F.n).x .| by MESFUNC6:43;
assume x in dom((R_EAL F).0);
hence |. ((R_EAL F).n).x .| <= K by A5,A8;
end;
then
A9: R_EAL F is uniformly_bounded by MESFUN10:def 1;
A10: for n be Nat holds (R_EAL F).n is E-measurable
proof
let n be Nat;
F.n is E-measurable by A2;
then R_EAL(F.n) is E-measurable;
hence (R_EAL F).n is E-measurable;
end;
then consider I be ExtREAL_sequence such that
A11: for n be Nat holds I.n = Integral(M,(R_EAL F).n) and
A12: I is convergent & lim I = Integral(M,lim (R_EAL F)) by A1,A9,A6,
MESFUN10:19;
for n be Nat holds I.n = Integral(M,F.n) by A11;
hence thesis by A1,A10,A9,A6,A12,MESFUN10:19;
end;
definition
let X be set, F be Functional_Sequence of X,REAL, f be PartFunc of X,REAL;
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 Element of X st n >= N & x in dom(F.0)
holds |. (F.n).x - f.x qua Complex .| < e;
end;
theorem Th50:
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 (R_EAL F).n is_integrable_on M
proof
let n be Nat;
F.n is_integrable_on M by A2;
then R_EAL(F.n) is_integrable_on M;
hence (R_EAL F).n is_integrable_on M;
end;
A5: 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((R_EAL F).0) holds |. ((R_EAL F).n).x - (R_EAL f).x .| < e
proof
let e be Real;
assume e>0;
then consider N be Nat such that
A6: for n be Nat, x be Element of X st n >= N & x in dom(F.0) holds
|. (F.n).x - f.x qua Complex .| < e by A3;
now
let n be Nat, x be set;
assume n >= N & x in dom((R_EAL F).0);
then
A7: |. (F.n).x - f.x qua Complex .| < e by A6;
|. (F.n).x - f.x qua Complex .|
= |. ((F.n).x - f.x) .| by MESFUNC6:43;
hence |. ((R_EAL F).n).x - (R_EAL f).x .| < e by A7;
end;
hence thesis;
end;
dom((R_EAL F).0) = dom R_EAL f by A3;
then
A8: R_EAL F is_uniformly_convergent_to R_EAL f by A5,MESFUN10:def 2;
then
A9: R_EAL f is_integrable_on M by A1,A4,MESFUN10:21;
consider I be ExtREAL_sequence such that
A10: for n be Nat holds I.n = Integral(M,(R_EAL F).n) and
A11: I is convergent & lim I = Integral(M,R_EAL f) by A1,A4,A8,MESFUN10:21;
for n be Nat holds I.n = Integral(M,F.n) by A10;
hence thesis by A9,A11;
end;
reserve F for with_the_same_dom Functional_Sequence of X,COMPLEX,
f for PartFunc of X,COMPLEX;
theorem Th51:
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) & (for x be Element of X st x in E holds
F#x is convergent) implies lim 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 and
A6: for x be Element of X st x in E holds F#x is convergent;
A7: for n be Nat holds (Re F).n is E-measurable & (Im F).n
is E-measurable by A3,Lm2;
for x be Element of X, n be Nat st x in E holds (|. (Re F).n .|).x <= P
.x & (|. (Im F).n .|).x <= P.x
proof
let x be Element of X, n be Nat;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
Re((F#x).n1) = (Re(F#x)).n1 by COMSEQ_3:def 5;
then
A8: |. (Re(F#x)).n qua Complex .|
<= |. (F#x).n qua Complex .| by COMSEQ_3:13;
Im((F#x).n1) = (Im(F#x)).n1 by COMSEQ_3:def 6;
then
A9: |. (Im(F#x)).n qua Complex .|
<= |. (F#x).n qua Complex .| by COMSEQ_3:13;
assume
A10: x in E;
then (|. F.n .|).x <= P.x by A5;
then |.(F.n).x .| <= P.x by VALUED_1:18;
then
A11: |. (F#x).n .| <= P.x by MESFUN7C:def 9;
(Im F)#x = Im(F#x) by A1,A10,MESFUN7C:23;
then |. ((Im F)#x).n1 qua Complex .| <= P.x by A11,A9,XXREAL_0:2;
then
A12: |. ((Im F).n1).x qua Complex .| <= P.x by SEQFUNC:def 10;
(Re F)#x = Re(F#x) by A1,A10,MESFUN7C:23;
then |. ((Re F)#x).n1 qua Complex .| <= P.x by A11,A8,XXREAL_0:2;
then |. ((Re F).n1).x qua Complex .| <= P.x by SEQFUNC:def 10;
hence (|. (Re F).n.|).x <= P.x &
(|. (Im F).n .|).x <= P.x by A12,
VALUED_1:18;
end;
then
A13: for x be Element of X, n be Nat holds (x in E implies (|. (Re F).n .|).x
<= P.x) & (x in E implies (|. (Im F).n .|).x <= P.x);
A14: for x be Element of X st x in E holds (Re F)#x is convergent & (Im F)#x
is convergent
proof
let x be Element of X;
assume
A15: x in E;
then F#x is convergent Complex_Sequence by A6;
then Re(F#x) is convergent & Im(F#x) is convergent;
hence (Re F)#x is convergent & (Im F)#x is convergent by A1,A15,MESFUN7C:23
;
end;
then
A16: for x be Element of X st x in E holds (Im F)#x is convergent;
E = dom((Im F).0) by A1,MESFUN7C:def 12;
then lim Im F is_integrable_on M by A2,A4,A7,A13,A16,Th47;
then R_EAL(Im lim F) is_integrable_on M by A1,A6,MESFUN7C:25;
then
A17: Im lim F is_integrable_on M;
A18: for x be Element of X st x in E holds (Re F)#x is convergent by A14;
E = dom((Re F).0) by A1,MESFUN7C:def 11;
then lim Re F is_integrable_on M by A2,A4,A7,A13,A18,Th47;
then R_EAL(Re lim F) is_integrable_on M by A1,A6,MESFUN7C:25;
then Re lim F is_integrable_on M;
hence lim F is_integrable_on M by A17,MESFUN6C:def 2;
end;
:: Lebesgue's Convergence theorem
theorem
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 ex I be Complex_Sequence st (for n be Nat holds I.n =
Integral(M,F.n)) & ( (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: for x be Element of X, n be Nat st x in E holds (|. F.n .|).x <= P.x;
A6: E = dom((Re F).0) by A1,MESFUN7C:def 11;
A7: for n be Nat holds (Re F).n is E-measurable & (Im F).n
is E-measurable by A3,Lm2;
A8: for x be Element of X, n be Nat st x in E holds (|. (Re F).n .|).x <= P.
x & (|. (Im F).n .|).x <= P.x
proof
let x be Element of X, n be Nat;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
Re((F#x).n1) = (Re(F#x)).n1 by COMSEQ_3:def 5;
then
A9: |. (Re(F#x)).n qua Complex .| <= |. (F#x).n .| by COMSEQ_3:13;
Im((F#x).n1) = (Im(F#x)).n1 by COMSEQ_3:def 6;
then
A10: |. (Im(F#x)).n qua Complex .| <= |. (F#x).n .| by COMSEQ_3:13;
assume
A11: x in E;
then (|. F.n .|).x <= P.x by A5;
then |.(F.n).x .| <= P.x by VALUED_1:18;
then
A12: |. (F#x).n .| <= P.x by MESFUN7C:def 9;
(Im F)#x = Im(F#x) by A1,A11,MESFUN7C:23;
then
A13: |. ((Im F)#x).n1 qua Complex .| <= P.x by A12,A10,XXREAL_0:2;
(Re F)#x = Re(F#x) by A1,A11,MESFUN7C:23;
then |. ((Re F)#x).n qua Complex .| <= P.x by A12,A9,XXREAL_0:2;
then
A14: |. ((Re F).n).x qua Complex .| <= P.x by SEQFUNC:def 10;
|. ((Im F).n).x qua Complex .| <= P.x by A13,SEQFUNC:def 10;
hence (|. (Re F).n .|).x <= P.x &
(|. (Im F).n .|).x <= P.x by A14,
VALUED_1:18;
end;
then
for x be Element of X, n be Nat st x in E holds (|. (Re F).n .|).x <= P .x;
then consider A be Real_Sequence such that
A15: for n be Nat holds A.n = Integral(M,(Re F).n) and
A16: (for x be Element of X st x in E holds (Re F)#x is convergent)
implies A is convergent & lim A = Integral(M,lim Re F) by A2,A4,A6,A7,Th48;
defpred P[Element of NAT,set] means $2 = Integral(M,F.$1);
A17: for n being Element of NAT ex y being Element of COMPLEX st P[n,y]
proof
let n be Element of NAT;
Integral(M,F.n) is Element of COMPLEX by XCMPLX_0:def 2;
hence thesis;
end;
consider I be sequence of COMPLEX such that
A18: for n be Element of NAT holds P[n,I.n] from FUNCT_2:sch 3(A17);
reconsider I as Complex_Sequence;
A19: E = dom((Im F).0) by A1,MESFUN7C:def 12;
for x be Element of X, n be Nat st x in E holds (|. (Im F).n .|).x <= P
.x by A8;
then consider B be Real_Sequence such that
A20: for n be Nat holds B.n = Integral(M,(Im F).n) and
A21: (for x be Element of X st x in E holds (Im F)#x is convergent)
implies B is convergent & lim B = Integral(M,lim Im F) by A2,A4,A19,A7,Th48;
A22: for n be Nat holds (Re F).n is_integrable_on M & (Im F).n
is_integrable_on M
proof
let n be Nat;
A23: now
let x be Element of X;
assume x in dom((Re F).n);
then x in E by A6,MESFUNC8:def 2;
then (|. (Re F).n .|).x <= P.x by A8;
hence |. ((Re F).n).x qua Complex .| <= P.x by VALUED_1:18;
end;
A24: now
let x be Element of X;
assume x in dom((Im F).n);
then x in E by A19,MESFUNC8:def 2;
then (|. (Im F).n .|).x <= P.x by A8;
hence |. ((Im F).n).x qua Complex .| <= P.x by VALUED_1:18;
end;
A25: (Re F).n is E-measurable & (Im F).n is E-measurable by A3,Lm2;
dom((Re F).n) = E & dom((Im F).n) = E by A6,A19,MESFUNC8:def 2;
hence (Re F).n is_integrable_on M & (Im F).n is_integrable_on M by A2,A4
,A23,A24,A25,MESFUNC6:96;
end;
A26: now
let n1 be set;
assume n1 in NAT;
then reconsider n=n1 as Element of NAT;
A27: (Re I).n = Re(I.n) & (Im I).n = Im(I.n) by COMSEQ_3:def 5,def 6;
A28: (Im F).n = Im(F.n) by MESFUN7C:24;
then
A29: Im(F.n) is_integrable_on M by A22;
A30: (Re F).n = Re(F.n) by MESFUN7C:24;
then Re(F.n) is_integrable_on M by A22;
then F.n is_integrable_on M by A29,MESFUN6C:def 2;
then consider RF,IF be Real such that
A31: RF = Integral(M,Re(F.n)) & IF = Integral(M,Im(F.n)) and
A32: Integral(M,F.n) = RF + IF * <i> by MESFUN6C:def 3;
I.n1 = Integral(M,F.n) by A18;
then Re(I.n1) = RF & Im(I.n1) = IF by A32,COMPLEX1:12;
hence (Re I).n1 = A.n1 & (Im I).n1 = B.n1 by A15,A20,A30,A28,A31,A27;
end;
then for x be object st x in NAT holds (Re I).x = A.x;
then
A33: Re I = A;
take I;
hereby
let n be Nat;
n is Element of NAT by ORDINAL1:def 12;
hence I.n = Integral(M,F.n) by A18;
end;
for x be object st x in NAT holds (Im I).x = B.x by A26;
then
A34: Im I = B;
hereby
assume
A35: for x be Element of X st x in E holds F#x is convergent;
then
A36: Integral(M,lim Im F) = Integral(M,Im lim F) by A1,MESFUN7C:25;
A37: lim F is_integrable_on M & Integral(M,lim Re F) = Integral(M,Re lim F
) by A1,A2,A3,A4,A5,A35,Th51,MESFUN7C:25;
A38: now
let x be Element of X such that
A39: x in E;
F#x is convergent Complex_Sequence by A35,A39;
then Re(F#x) is convergent & Im(F#x) is convergent;
hence (Re F)#x is convergent & (Im F)#x is convergent by A1,A39,
MESFUN7C:23;
end;
hence I is convergent by A16,A21,A33,A34,COMSEQ_3:42;
for n be Nat holds (Re I).n = Re(I.n) & (Im I).n = Im(I.n)
by COMSEQ_3:def 5,def 6;
then lim I = lim Re I + (lim Im I) * <i> by A16,A21,A33,A34,A38,COMSEQ_3:39
;
hence lim I = Integral(M,lim F) by A16,A21,A33,A34,A38,A37,A36,
MESFUN6C:def 3;
end;
end;
definition
let X be set, F be Functional_Sequence of X,COMPLEX;
attr F is uniformly_bounded means
ex K be Real st for n be Nat
, x be Element of X 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 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 Complex_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 K be Real such that
A6: for n be Nat, x be Element of X st x in dom(F.0) holds |. (F.n).x .|
<= K by A4;
A7: for x be Element of X st x in E holds (Re F)#x is convergent
proof
let x be Element of X;
assume
A8: x in E;
then F#x is convergent Complex_Sequence by A5;
then Re(F#x) is convergent;
hence (Re F)#x is convergent by A2,A8,MESFUN7C:23;
end;
for n be Nat, x be Element of X st x in dom((Im F).0)
holds |. ((Im F). n).x qua Complex .| <= K
proof
let n be Nat, x be Element of X;
assume x in dom((Im F).0);
then
A9: x in E by A2,MESFUN7C:def 12;
then |. (F.n).x .| <= K by A2,A6;
then
A10: |. (F#x).n .| <= K by MESFUN7C:def 9;
Im((F#x).n) = (Im(F#x)).n by COMSEQ_3:def 6;
then Im((F#x).n) = ((Im F)#x).n by A2,A9,MESFUN7C:23;
then |. ((Im F)#x).n qua Complex .| <= |. (F#x).n .| by COMSEQ_3:13;
then |. ((Im F)#x).n qua Complex .| <= K by A10,XXREAL_0:2;
hence thesis by SEQFUNC:def 10;
end;
then
A11: Im F is uniformly_bounded;
A12: for x be Element of X st x in E holds (Im F)#x is convergent
proof
let x be Element of X;
assume
A13: x in E;
then F#x is convergent Complex_Sequence by A5;
then Im(F#x) is convergent;
hence (Im F)#x is convergent by A2,A13,MESFUN7C:23;
end;
defpred P[Element of NAT,set] means $2 = Integral(M,F.$1);
A14: for n being Element of NAT ex y being Element of COMPLEX st P[n,y]
proof
let n being Element of NAT;
take Integral(M,F.n);
thus thesis by XCMPLX_0:def 2,TARSKI:1;
end;
consider I be sequence of COMPLEX such that
A15: for n be Element of NAT holds P[n,I.n] from FUNCT_2:sch 3(A14);
reconsider I as Complex_Sequence;
A16: for n be Nat holds (Re F).n is E-measurable & (Im F).n
is E-measurable by A3,Lm2;
for n be Nat, x be Element of X st x in dom((Re F).0)
holds |. ((Re F).n).x qua Complex .| <= K
proof
let n be Nat, x be Element of X;
assume x in dom((Re F).0);
then
A17: x in E by A2,MESFUN7C:def 11;
then |. (F.n).x .| <= K by A2,A6;
then
A18: |. (F#x).n .| <= K by MESFUN7C:def 9;
Re((F#x).n) = (Re(F#x)).n by COMSEQ_3:def 5;
then Re((F#x).n) = ((Re F)#x).n by A2,A17,MESFUN7C:23;
then |. ((Re F)#x).n qua Complex .| <= |. (F#x).n .| by COMSEQ_3:13;
then |. ((Re F)#x).n qua Complex .| <= K by A18,XXREAL_0:2;
hence |. ((Re F).n).x qua Complex .| <= K by SEQFUNC:def 10;
end;
then
A19: Re F is uniformly_bounded;
A20: E = dom((Im F).0) by A2,MESFUN7C:def 12;
then consider B be ExtREAL_sequence such that
A21: for n be Nat holds B.n = Integral(M,(Im F).n) and
A22: B is convergent and
A23: lim B = Integral(M,lim Im F) by A1,A16,A12,A11,Th49;
A24: lim Im F is_integrable_on M by A1,A20,A16,A12,A11,Th49;
then R_EAL Im lim F is_integrable_on M by A2,A5,MESFUN7C:25;
then
A25: Im lim F is_integrable_on M;
A26: E = dom((Re F).0) by A2,MESFUN7C:def 11;
then consider A be ExtREAL_sequence such that
A27: for n be Nat holds A.n = Integral(M,(Re F).n) and
A28: A is convergent and
A29: lim A = Integral(M,lim Re F) by A1,A16,A7,A19,Th49;
thus
A30: for n be Nat holds F.n is_integrable_on M
proof
let n be Nat;
(Im F).n = Im(F.n) by MESFUN7C:24;
then
A31: Im(F.n) is_integrable_on M by A1,A20,A16,A12,A11,Th49;
(Re F).n = Re(F.n) by MESFUN7C:24;
then Re(F.n) is_integrable_on M by A1,A26,A16,A7,A19,Th49;
hence F.n is_integrable_on M by A31,MESFUN6C:def 2;
end;
A32: for n1 be set st n1 in NAT holds (R_EAL Re I).n1 = A.n1 & (R_EAL Im I).
n1 = B.n1
proof
let n1 be set;
assume n1 in NAT;
then reconsider n=n1 as Element of NAT;
A33: I.n1 = Integral(M,F.n) by A15;
F.n is_integrable_on M by A30;
then consider RF,IF be Real such that
A34: RF = Integral(M,Re(F.n)) and
A35: IF = Integral(M,Im(F.n)) and
A36: Integral(M,F.n) = RF + IF * <i> by MESFUN6C:def 3;
(Re I).n = Re(I.n) by COMSEQ_3:def 5;
then (Re F).n = Re(F.n) & (Re I).n1 = RF by A36,A33,COMPLEX1:12,MESFUN7C:24
;
hence (R_EAL Re I).n1 = A.n1 by A27,A34;
(Im I).n = Im(I.n) by COMSEQ_3:def 6;
then (Im F).n = Im(F.n) & (Im I).n1 = IF by A36,A33,COMPLEX1:12,MESFUN7C:24
;
hence (R_EAL Im I).n1 = B.n1 by A21,A35;
end;
then for n1 be object st n1 in NAT holds (R_EAL Im I).n1 = B.n1;
then
A37: Im I = B;
A38: -infty < Integral(M,lim Im F) & Integral(M,lim Im F) < +infty by A24,
MESFUNC5:96;
A39: B is convergent implies B is convergent_to_finite_number
by A23,A38,MESFUNC5:def 12;
then
A40: lim Im I = Integral(M,lim Im F) by A22,A23,A37,RINFSUP2:15;
A41: Im I is convergent by A22,A37,A39,RINFSUP2:15;
A42: lim Re F is_integrable_on M by A1,A26,A16,A7,A19,Th49;
then R_EAL Re lim F is_integrable_on M by A2,A5,MESFUN7C:25;
then Re lim F is_integrable_on M;
hence
A43: lim F is_integrable_on M by A25,MESFUN6C:def 2;
take I;
for n1 be object st n1 in NAT holds (R_EAL Re I).n1 = A.n1 by A32;
then
A44: Re I = A;
thus for n be Nat holds I.n = Integral(M,F.n)
proof
let n be Nat;
A45: (Re I).n = Re(I.n) & (Im I).n = Im(I.n) by COMSEQ_3:def 5,def 6;
(Re F).n = Re(F.n) by MESFUN7C:24;
then
A46: (Re I).n = Integral(M,Re(F.n)) by A27,A44;
(Im F).n = Im(F.n) by MESFUN7C:24;
then
A47: (Im I).n = Integral(M,Im(F.n)) by A21,A37;
I.n = Re(I.n) + Im(I.n)*<i> & F.n is_integrable_on M by A30,COMPLEX1:13;
hence I.n = Integral(M,F.n) by A45,A46,A47,MESFUN6C:def 3;
end;
A48: -infty < Integral(M,lim Re F) & Integral(M,lim Re F) < +infty by A42,
MESFUNC5:96;
A49: A is convergent implies A is convergent_to_finite_number
by A29,A48,MESFUNC5:def 12;
then
A50: Re I is convergent by A28,A44,RINFSUP2:15;
hence I is convergent by A41,COMSEQ_3:42;
for n be Nat holds (Re I).n = Re(I.n) & (Im I).n = Im(I.n)
by COMSEQ_3:def 5,def 6;
then
A51: lim I = lim Re I + (lim Im I) * <i> by A50,A41,COMSEQ_3:39;
A52: Integral(M,lim Re F) = Integral(M,Re lim F) & Integral(M,lim Im F) =
Integral(M,Im lim F) by A2,A5,MESFUN7C:25;
lim Re I = Integral(M,lim Re F) by A28,A29,A44,A49,RINFSUP2:15;
hence lim I = Integral(M,lim F) by A43,A40,A51,A52,MESFUN6C:def 3;
end;
definition
let X be set, F be Functional_Sequence of X,COMPLEX, f be PartFunc of X,
COMPLEX;
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 Element of X st n >= N & x in dom(F.0) holds |. (F.n).x - f.x .| < e;
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
Complex_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;
A5: for n be Nat holds (Im F).n is_integrable_on M
proof
let n be Nat;
F.n is_integrable_on M by A3;
then Im(F.n) is_integrable_on M by MESFUN6C:def 2;
hence (Im F).n is_integrable_on M by MESFUN7C:24;
end;
A6: dom(F.0) = dom f by A4;
A7: for e be Real st e>0 ex N be Nat st for n be Nat, x be Element
of X st n >= N & x in dom((Im F).0)
holds |. ((Im F).n).x - (Im f).x qua Complex .| < e
proof
let e be Real;
assume e>0;
then consider N be Nat such that
A8: for n be Nat, x be Element of X st n >= N & x in dom(F.0) holds
|. (F.n).x - f.x .| < e by A4;
for n be Nat, x be Element of X st n >= N & x in dom((Im F).0) holds
|. ((Im F).n).x - (Im f).x qua Complex .| < e
proof
let n be Nat, x be Element of X;
assume that
A9: n >= N and
A10: x in dom((Im F).0);
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
A11: x in dom(F.0) by A10,MESFUN7C:def 12;
then |. (F.n).x - f.x .| < e by A8,A9;
then
A12: |. (F#x).n - f.x .| < e by MESFUN7C:def 9;
A13: Im((F#x).n - f.x) = Im((F#x).n) - Im(f.x) by COMPLEX1:19;
A14: |. Im((F#x).n) - Im(f.x) qua Complex .|
<= |. (F#x).n - f.x .| by A13,COMSEQ_3:13;
x in dom Im f by A6,A11,COMSEQ_3:def 4;
then
A15: Im(f.x) = (Im f).x by COMSEQ_3:def 4;
Im((F#x).n1) = (Im(F#x)).n by COMSEQ_3:def 6
.= ((Im F)#x).n1 by A11,MESFUN7C:23
.= ((Im F).n).x by SEQFUNC:def 10;
hence |. ((Im F).n).x - (Im f).x qua Complex .|
< e by A12,A14,A15,XXREAL_0:2;
end;
hence thesis;
end;
dom((Im F).0) = dom f by A6,MESFUN7C:def 12;
then dom((Im F).0) = dom Im f by COMSEQ_3:def 4;
then
A16: Im F is_uniformly_convergent_to Im f by A7;
A17: for e be Real st e>0 ex N be Nat st for n be Nat, x be Element
of X st n >= N & x in dom((Re F).0)
holds |. ((Re F).n).x - (Re f).x qua Complex .| < e
proof
let e be Real;
assume e>0;
then consider N be Nat such that
A18: for n be Nat, x be Element of X st n >= N & x in dom(F.0) holds
|. (F.n).x - f.x .| < e by A4;
for n be Nat, x be Element of X st n >= N & x in dom((Re F).0) holds
|. ((Re F).n).x - (Re f).x qua Complex .| < e
proof
let n be Nat, x be Element of X;
assume that
A19: n >= N and
A20: x in dom((Re F).0);
A21: x in dom(F.0) by A20,MESFUN7C:def 11;
A22: Re((F#x).n - f.x) = Re((F#x).n) - Re(f.x) by COMPLEX1:19;
(F.n).x = (F#x).n by MESFUN7C:def 9;
then
A23: |. (F#x).n - f.x .| < e by A18,A19,A21;
x in dom Re f by A6,A21,COMSEQ_3:def 3;
then
A24: Re(f.x) = (Re f).x by COMSEQ_3:def 3;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
A25: |. Re((F#x).n) - Re(f.x) qua Complex .|
<= |. (F#x).n - f.x .| by A22,COMSEQ_3:13;
Re((F#x).n) = (Re(F#x)).n1 by COMSEQ_3:def 5
.= ((Re F)#x).n by A21,MESFUN7C:23
.= ((Re F).n1).x by SEQFUNC:def 10;
hence |. ((Re F).n).x - (Re f).x qua Complex .| < e
by A23,A25,A24,XXREAL_0:2;
end;
hence thesis;
end;
dom((Re F).0) = dom f by A6,MESFUN7C:def 11;
then dom((Re F).0) = dom Re f by COMSEQ_3:def 3;
then
A26: Re F is_uniformly_convergent_to Re f by A17;
defpred P[Element of NAT,set] means $2 = Integral(M,F.$1);
A27: for n being Element of NAT ex y being Element of COMPLEX st P[n,y]
proof
let n being Element of NAT;
Integral(M,F.n) is Element of COMPLEX by XCMPLX_0:def 2;
hence thesis;
end;
consider I be sequence of COMPLEX such that
A28: for n be Element of NAT holds P[n,I.n] from FUNCT_2:sch 3(A27);
A29: for n be Nat holds (Re F).n is_integrable_on M
proof
let n be Nat;
F.n is_integrable_on M by A3;
then Re(F.n) is_integrable_on M by MESFUN6C:def 2;
hence (Re F).n is_integrable_on M by MESFUN7C:24;
end;
A30: E = dom((Im F).0) by A2,MESFUN7C:def 12;
then
A31: Im f is_integrable_on M by A1,A5,A16,Th50;
A32: E = dom((Re F).0) by A2,MESFUN7C:def 11;
then consider A be ExtREAL_sequence such that
A33: for n be Nat holds A.n = Integral(M,(Re F).n) and
A34: A is convergent and
A35: lim A = Integral(M,Re f) by A1,A29,A26,Th50;
A36: Re f is_integrable_on M by A1,A32,A29,A26,Th50;
hence
A37: f is_integrable_on M by A31,MESFUN6C:def 2;
reconsider I as Complex_Sequence;
consider B be ExtREAL_sequence such that
A38: for n be Nat holds B.n = Integral(M,(Im F).n) and
A39: B is convergent and
A40: lim B = Integral(M,Im f) by A1,A30,A5,A16,Th50;
A41: now
let n1 be set;
assume n1 in NAT;
then reconsider n=n1 as Element of NAT;
A42: (Re F).n = Re(F.n) & (Im F).n = Im(F.n) by MESFUN7C:24;
F.n is_integrable_on M by A3;
then consider RF,IF be Real such that
A43: RF = Integral(M,Re(F.n)) & IF = Integral(M,Im(F.n)) and
A44: Integral(M,F.n) = RF + IF * <i> by MESFUN6C:def 3;
A45: (Re I).n = Re(I.n) & (Im I).n = Im(I.n) by COMSEQ_3:def 5,def 6;
I.n1 = Integral(M,F.n) by A28;
then Re(I.n1) = RF & Im(I.n1) = IF by A44,COMPLEX1:12;
hence (R_EAL Re I).n1 = A.n1 & (R_EAL Im I).n1 = B.n1 by A33,A38,A42,A45
,A43;
end;
then for x be object st x in NAT holds (R_EAL Im I).x = B.x;
then
A46: Im I = B;
A47: -infty < Integral(M,Im f) & Integral(M,Im f) < +infty by A31,MESFUNC6:90;
A48: B is convergent implies B is convergent_to_finite_number
by A40,A47,MESFUNC5:def 12;
then
A49: lim Im I = Integral(M,Im f) by A39,A40,A46,RINFSUP2:15;
A50: Im I is convergent by A39,A46,A48,RINFSUP2:15;
take I;
for x be object st x in NAT holds (R_EAL Re I).x = A.x by A41;
then
A51: Re I = A;
thus for n be Nat holds I.n = Integral(M,F.n)
proof
let n be Nat;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
(Re I).n1 = Re(I.n1) & (Im I).n1 = Im(I.n1) by COMSEQ_3:def 5,def 6;
then
A52: I.n = ((Re I).n) + ((Im I).n) * <i> by COMPLEX1:13;
(Re F).n = Re(F.n) by MESFUN7C:24;
then
A53: (Re I).n = Integral(M,Re(F.n)) by A33,A51;
(Im F).n = Im(F.n) by MESFUN7C:24;
then
A54: (Im I).n = Integral(M,Im(F.n)) by A38,A46;
F.n is_integrable_on M by A3;
hence I.n = Integral(M,F.n) by A52,A53,A54,MESFUN6C:def 3;
end;
A55: -infty < Integral(M,Re f) & Integral(M,Re f) < +infty by A36,MESFUNC6:90;
A56: A is convergent implies A is convergent_to_finite_number
by A35,A55,MESFUNC5:def 12;
then
A57: Re I is convergent by A34,A51,RINFSUP2:15;
hence I is convergent by A50,COMSEQ_3:42;
for n be Nat holds (Re I).n = Re(I.n) & (Im I).n = Im(I.n)
by COMSEQ_3:def 5,def 6;
then
A58: lim I = lim (Re I) + lim (Im I) * <i> by A57,A50,COMSEQ_3:39;
lim Re I = Integral(M,Re f) by A34,A35,A51,A56,RINFSUP2:15;
hence lim I = Integral(M,f) by A37,A49,A58,MESFUN6C:def 3;
end;