let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for F being Functional_Sequence of X,ExtREAL st E = dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is nonnegative & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )
let S be SigmaField of X; for M being sigma_Measure of S
for E being Element of S
for F being Functional_Sequence of X,ExtREAL st E = dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is nonnegative & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )
let M be sigma_Measure of S; for E being Element of S
for F being Functional_Sequence of X,ExtREAL st E = dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is nonnegative & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )
let E be Element of S; for F being Functional_Sequence of X,ExtREAL st E = dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is nonnegative & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
F # x is summable ) holds
ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )
let F be Functional_Sequence of X,ExtREAL; ( E = dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is nonnegative & F . n is E -measurable ) ) & ( for x being Element of X st x in E holds
F # x is summable ) implies ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I ) )
assume that
A1:
E = dom (F . 0)
and
A2:
F is additive
and
A3:
F is with_the_same_dom
and
A4:
for n being Nat holds
( F . n is nonnegative & F . n is E -measurable )
and
A5:
for x being Element of X st x in E holds
F # x is summable
; ex I being ExtREAL_sequence st
( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )
consider FF being sequence of (Funcs (NAT,(PFuncs (X,ExtREAL)))) such that
A6:
for n being Nat holds
( ( for m being Nat holds
( (FF . n) . m is_simple_func_in S & dom ((FF . n) . m) = dom (F . n) ) ) & ( for m being Nat holds (FF . n) . m is nonnegative ) & ( for j, k being Nat st j <= k holds
for x being Element of X st x in dom (F . n) holds
((FF . n) . j) . x <= ((FF . n) . k) . x ) & ( for x being Element of X st x in dom (F . n) holds
( (FF . n) # x is convergent & lim ((FF . n) # x) = (F . n) . x ) ) )
by A1, A3, A4, Th49;
defpred S1[ Element of NAT , Element of NAT , set ] means for n, m being Nat st n = $1 & m = $2 holds
$3 = (FF . n) . m;
A7:
for i1, j1 being Element of NAT ex F1 being Element of PFuncs (X,ExtREAL) st S1[i1,j1,F1]
proof
let i1,
j1 be
Element of
NAT ;
ex F1 being Element of PFuncs (X,ExtREAL) st S1[i1,j1,F1]
reconsider i =
i1,
j =
j1 as
Nat ;
reconsider F1 =
(FF . i) . j as
Element of
PFuncs (
X,
ExtREAL)
by PARTFUN1:45;
take
F1
;
S1[i1,j1,F1]
thus
S1[
i1,
j1,
F1]
;
verum
end;
consider FF2 being Function of [:NAT,NAT:],(PFuncs (X,ExtREAL)) such that
A8:
for i, j being Element of NAT holds S1[i,j,FF2 . (i,j)]
from BINOP_1:sch 3(A7);
deffunc H1( Nat) -> Element of bool [:X,ExtREAL:] = (Partial_Sums (ProjMap2 (FF2,$1))) . $1;
consider P being Functional_Sequence of X,ExtREAL such that
A9:
for k being Nat holds P . k = H1(k)
from SEQFUNC:sch 1();
A10:
for n being Nat holds
( ( for m being Nat holds
( dom ((ProjMap1 (FF2,n)) . m) = E & dom ((ProjMap2 (FF2,n)) . m) = E & (ProjMap1 (FF2,n)) . m is_simple_func_in S & (ProjMap2 (FF2,n)) . m is_simple_func_in S ) ) & ProjMap1 (FF2,n) is additive & ProjMap2 (FF2,n) is additive & ProjMap1 (FF2,n) is with_the_same_dom & ProjMap2 (FF2,n) is with_the_same_dom )
proof
let n be
Nat;
( ( for m being Nat holds
( dom ((ProjMap1 (FF2,n)) . m) = E & dom ((ProjMap2 (FF2,n)) . m) = E & (ProjMap1 (FF2,n)) . m is_simple_func_in S & (ProjMap2 (FF2,n)) . m is_simple_func_in S ) ) & ProjMap1 (FF2,n) is additive & ProjMap2 (FF2,n) is additive & ProjMap1 (FF2,n) is with_the_same_dom & ProjMap2 (FF2,n) is with_the_same_dom )
A11:
now for m being Nat holds
( dom ((ProjMap1 (FF2,n)) . m) = E & dom ((ProjMap2 (FF2,n)) . m) = E & (ProjMap1 (FF2,n)) . m is_simple_func_in S & (ProjMap2 (FF2,n)) . m is_simple_func_in S )let m be
Nat;
( dom ((ProjMap1 (FF2,n)) . m) = E & dom ((ProjMap2 (FF2,n)) . m) = E & (ProjMap1 (FF2,n)) . m is_simple_func_in S & (ProjMap2 (FF2,n)) . m is_simple_func_in S )reconsider n1 =
n,
m1 =
m as
Element of
NAT by ORDINAL1:def 12;
A12:
(ProjMap1 (FF2,n)) . m = FF2 . (
n,
m)
by Def8;
A13:
FF2 . (
n1,
m1)
= (FF . n1) . m
by A8;
A14:
dom (F . m1) = dom (F . 0)
by A3;
A15:
(ProjMap2 (FF2,n)) . m = FF2 . (
m,
n)
by Def9;
A16:
FF2 . (
m1,
n1)
= (FF . m1) . n
by A8;
dom (F . n1) = dom (F . m1)
by A3;
hence
(
dom ((ProjMap1 (FF2,n)) . m) = E &
dom ((ProjMap2 (FF2,n)) . m) = E )
by A1, A6, A12, A15, A13, A16, A14;
( (ProjMap1 (FF2,n)) . m is_simple_func_in S & (ProjMap2 (FF2,n)) . m is_simple_func_in S )thus
(
(ProjMap1 (FF2,n)) . m is_simple_func_in S &
(ProjMap2 (FF2,n)) . m is_simple_func_in S )
by A6, A12, A15, A13, A16;
verum end;
for
i1,
j1 being
Nat holds
(
dom ((ProjMap1 (FF2,n)) . i1) = dom ((ProjMap1 (FF2,n)) . j1) &
dom ((ProjMap2 (FF2,n)) . i1) = dom ((ProjMap2 (FF2,n)) . j1) )
proof
let i1,
j1 be
Nat;
( dom ((ProjMap1 (FF2,n)) . i1) = dom ((ProjMap1 (FF2,n)) . j1) & dom ((ProjMap2 (FF2,n)) . i1) = dom ((ProjMap2 (FF2,n)) . j1) )
A17:
dom ((ProjMap2 (FF2,n)) . i1) = E
by A11;
dom ((ProjMap1 (FF2,n)) . i1) = E
by A11;
hence
(
dom ((ProjMap1 (FF2,n)) . i1) = dom ((ProjMap1 (FF2,n)) . j1) &
dom ((ProjMap2 (FF2,n)) . i1) = dom ((ProjMap2 (FF2,n)) . j1) )
by A11, A17;
verum
end;
hence
( ( for
m being
Nat holds
(
dom ((ProjMap1 (FF2,n)) . m) = E &
dom ((ProjMap2 (FF2,n)) . m) = E &
(ProjMap1 (FF2,n)) . m is_simple_func_in S &
(ProjMap2 (FF2,n)) . m is_simple_func_in S ) ) &
ProjMap1 (
FF2,
n) is
additive &
ProjMap2 (
FF2,
n) is
additive &
ProjMap1 (
FF2,
n) is
with_the_same_dom &
ProjMap2 (
FF2,
n) is
with_the_same_dom )
by A11, Th35;
verum
end;
for n, m being Nat holds dom (P . n) = dom (P . m)
proof
let n,
m be
Nat;
dom (P . n) = dom (P . m)
A18:
ProjMap2 (
FF2,
n) is
with_the_same_dom
by A10;
A19:
dom (P . n) = dom ((Partial_Sums (ProjMap2 (FF2,n))) . n)
by A9;
ProjMap2 (
FF2,
n) is
additive
by A10;
then
dom (P . n) = dom ((ProjMap2 (FF2,n)) . 0)
by A18, A19, Th29;
then
dom (P . n) = E
by A10;
then A20:
dom (P . n) = dom ((ProjMap2 (FF2,m)) . 0)
by A10;
A21:
ProjMap2 (
FF2,
m) is
with_the_same_dom
by A10;
ProjMap2 (
FF2,
m) is
additive
by A10;
then
dom (P . n) = dom ((Partial_Sums (ProjMap2 (FF2,m))) . m)
by A21, A20, Th29;
hence
dom (P . n) = dom (P . m)
by A9;
verum
end;
then reconsider P = P as with_the_same_dom Functional_Sequence of X,ExtREAL by MESFUNC8:def 2;
dom (lim P) = dom (P . 0)
by MESFUNC8:def 9;
then
dom (lim P) = dom ((Partial_Sums (ProjMap2 (FF2,0))) . 0)
by A9;
then
dom (lim P) = dom ((ProjMap2 (FF2,0)) . 0)
by Def4;
then
dom (lim P) = dom (FF2 . (0,0))
by Def9;
then A22:
dom (lim P) = dom ((FF . 0) . 0)
by A8;
then A23:
dom (lim P) = dom (F . 0)
by A6;
A24:
for k, m being Nat
for x being Element of X st x in (dom (F . 0)) /\ (dom ((ProjMap2 (FF2,k)) . 0)) holds
((ProjMap2 (FF2,k)) . m) . x <= (F . m) . x
proof
let k,
m be
Nat;
for x being Element of X st x in (dom (F . 0)) /\ (dom ((ProjMap2 (FF2,k)) . 0)) holds
((ProjMap2 (FF2,k)) . m) . x <= (F . m) . xlet x be
Element of
X;
( x in (dom (F . 0)) /\ (dom ((ProjMap2 (FF2,k)) . 0)) implies ((ProjMap2 (FF2,k)) . m) . x <= (F . m) . x )
reconsider m1 =
m,
k1 =
k as
Element of
NAT by ORDINAL1:def 12;
assume
x in (dom (F . 0)) /\ (dom ((ProjMap2 (FF2,k)) . 0))
;
((ProjMap2 (FF2,k)) . m) . x <= (F . m) . x
then
x in dom (F . 0)
by XBOOLE_0:def 4;
then A25:
x in dom (F . m)
by A3;
(FF . m1) # x is
non-decreasing
then
lim ((FF . m1) # x) = sup ((FF . m1) # x)
by RINFSUP2:37;
then
((FF . m1) # x) . k1 <= lim ((FF . m1) # x)
by RINFSUP2:23;
then A30:
((FF . m1) # x) . k <= (F . m1) . x
by A6, A25;
(ProjMap2 (FF2,k)) . m = FF2 . (
m1,
k1)
by Def9;
then
(ProjMap2 (FF2,k)) . m = (FF . m) . k
by A8;
hence
((ProjMap2 (FF2,k)) . m) . x <= (F . m) . x
by A30, MESFUNC5:def 13;
verum
end;
A31:
for x being Element of X
for k being Element of NAT st x in dom (lim P) holds
(P # x) . k <= ((Partial_Sums F) # x) . k
proof
let x be
Element of
X;
for k being Element of NAT st x in dom (lim P) holds
(P # x) . k <= ((Partial_Sums F) # x) . klet k be
Element of
NAT ;
( x in dom (lim P) implies (P # x) . k <= ((Partial_Sums F) # x) . k )
assume A32:
x in dom (lim P)
;
(P # x) . k <= ((Partial_Sums F) # x) . k
dom ((ProjMap2 (FF2,k)) . 0) = E
by A10;
then A33:
x in (dom (F . 0)) /\ (dom ((ProjMap2 (FF2,k)) . 0))
by A1, A6, A22, A32;
A34:
ProjMap2 (
FF2,
k) is
with_the_same_dom
by A10;
(P # x) . k = (P . k) . x
by MESFUNC5:def 13;
then A35:
(P # x) . k = ((Partial_Sums (ProjMap2 (FF2,k))) . k) . x
by A9;
A36:
for
m being
Nat for
x being
Element of
X st
x in (dom (F . 0)) /\ (dom ((ProjMap2 (FF2,k)) . 0)) holds
((ProjMap2 (FF2,k)) . m) . x <= (F . m) . x
by A24;
ProjMap2 (
FF2,
k) is
additive
by A10;
then
((Partial_Sums (ProjMap2 (FF2,k))) . k) . x <= ((Partial_Sums F) . k) . x
by A2, A3, A33, A34, A36, Th42;
hence
(P # x) . k <= ((Partial_Sums F) # x) . k
by A35, MESFUNC5:def 13;
verum
end;
dom (lim (Partial_Sums F)) = dom ((Partial_Sums F) . 0)
by MESFUNC8:def 9;
then A37:
dom (lim (Partial_Sums F)) = E
by A1, Def4;
A38:
for n, m being Nat holds
( (ProjMap1 (FF2,n)) . m is nonnegative & (ProjMap2 (FF2,n)) . m is nonnegative )
proof
let n,
m be
Nat;
( (ProjMap1 (FF2,n)) . m is nonnegative & (ProjMap2 (FF2,n)) . m is nonnegative )
reconsider n1 =
n,
m1 =
m as
Element of
NAT by ORDINAL1:def 12;
(ProjMap1 (FF2,n)) . m = FF2 . (
n1,
m1)
by Def8;
then
(ProjMap1 (FF2,n)) . m = (FF . n) . m
by A8;
hence
(ProjMap1 (FF2,n)) . m is
nonnegative
by A6;
(ProjMap2 (FF2,n)) . m is nonnegative
(ProjMap2 (FF2,n)) . m = FF2 . (
m1,
n1)
by Def9;
then
(ProjMap2 (FF2,n)) . m = (FF . m) . n
by A8;
hence
(ProjMap2 (FF2,n)) . m is
nonnegative
by A6;
verum
end;
A39:
for n being Element of NAT
for x being Element of X st x in E holds
( (ProjMap1 (FF2,n)) # x is convergent & (F . n) . x = lim ((ProjMap1 (FF2,n)) # x) )
proof
let n be
Element of
NAT ;
for x being Element of X st x in E holds
( (ProjMap1 (FF2,n)) # x is convergent & (F . n) . x = lim ((ProjMap1 (FF2,n)) # x) )
reconsider n1 =
n as
Nat ;
let x be
Element of
X;
( x in E implies ( (ProjMap1 (FF2,n)) # x is convergent & (F . n) . x = lim ((ProjMap1 (FF2,n)) # x) ) )
assume A40:
x in E
;
( (ProjMap1 (FF2,n)) # x is convergent & (F . n) . x = lim ((ProjMap1 (FF2,n)) # x) )
for
k being
Nat ex
m being
Nat st
(
k <= m &
((ProjMap1 (FF2,n)) # x) . m > - 1 )
then A42:
not
(ProjMap1 (FF2,n)) # x is
convergent_to_-infty
;
A43:
E = dom (F . n1)
by A1, A3;
(ProjMap1 (FF2,n)) # x is
non-decreasing
proof
let i,
j be
ExtReal;
VALUED_0:def 15 ( not i in dom ((ProjMap1 (FF2,n)) # x) or not j in dom ((ProjMap1 (FF2,n)) # x) or not i <= j or ((ProjMap1 (FF2,n)) # x) . i <= ((ProjMap1 (FF2,n)) # x) . j )
assume that A44:
i in dom ((ProjMap1 (FF2,n)) # x)
and A45:
j in dom ((ProjMap1 (FF2,n)) # x)
and A46:
i <= j
;
((ProjMap1 (FF2,n)) # x) . i <= ((ProjMap1 (FF2,n)) # x) . j
reconsider i1 =
i,
j1 =
j as
Element of
NAT by A44, A45;
A47:
((ProjMap1 (FF2,n)) # x) . i1 = ((ProjMap1 (FF2,n)) . i1) . x
by MESFUNC5:def 13;
(ProjMap1 (FF2,n)) . i1 = FF2 . (
n,
i1)
by Def8;
then A48:
(ProjMap1 (FF2,n)) . i1 = (FF . n1) . i1
by A8;
A49:
((ProjMap1 (FF2,n)) # x) . j1 = ((ProjMap1 (FF2,n)) . j1) . x
by MESFUNC5:def 13;
A50:
(ProjMap1 (FF2,n)) . j1 = FF2 . (
n,
j1)
by Def8;
((FF . n1) . i1) . x <= ((FF . n1) . j1) . x
by A6, A43, A40, A46;
hence
((ProjMap1 (FF2,n)) # x) . i <= ((ProjMap1 (FF2,n)) # x) . j
by A8, A47, A49, A48, A50;
verum
end;
hence A51:
(ProjMap1 (FF2,n)) # x is
convergent
by RINFSUP2:37;
(F . n) . x = lim ((ProjMap1 (FF2,n)) # x)
per cases
( (ProjMap1 (FF2,n)) # x is convergent_to_finite_number or (ProjMap1 (FF2,n)) # x is convergent_to_+infty )
by A51, A42;
suppose A52:
(ProjMap1 (FF2,n)) # x is
convergent_to_finite_number
;
(F . n) . x = lim ((ProjMap1 (FF2,n)) # x)then A53:
not
(ProjMap1 (FF2,n)) # x is
convergent_to_-infty
by MESFUNC5:51;
not
(ProjMap1 (FF2,n)) # x is
convergent_to_+infty
by A52, MESFUNC5:50;
then consider lP being
Real such that A54:
lim ((ProjMap1 (FF2,n)) # x) = lP
and A55:
for
p being
Real st
0 < p holds
ex
nn being
Nat st
for
mm being
Nat st
nn <= mm holds
|.((((ProjMap1 (FF2,n)) # x) . mm) - (lim ((ProjMap1 (FF2,n)) # x))).| < p
and
(ProjMap1 (FF2,n)) # x is
convergent_to_finite_number
by A51, A53, MESFUNC5:def 12;
A56:
for
p being
Real st
0 < p holds
ex
nn being
Nat st
for
mm being
Nat st
nn <= mm holds
|.((((FF . n1) # x) . mm) - lP).| < p
proof
let p be
Real;
( 0 < p implies ex nn being Nat st
for mm being Nat st nn <= mm holds
|.((((FF . n1) # x) . mm) - lP).| < p )
assume
0 < p
;
ex nn being Nat st
for mm being Nat st nn <= mm holds
|.((((FF . n1) # x) . mm) - lP).| < p
then consider nn being
Nat such that A57:
for
mm being
Nat st
nn <= mm holds
|.((((ProjMap1 (FF2,n)) # x) . mm) - (lim ((ProjMap1 (FF2,n)) # x))).| < p
by A55;
take
nn
;
for mm being Nat st nn <= mm holds
|.((((FF . n1) # x) . mm) - lP).| < p
let mm be
Nat;
( nn <= mm implies |.((((FF . n1) # x) . mm) - lP).| < p )
assume A58:
nn <= mm
;
|.((((FF . n1) # x) . mm) - lP).| < p
reconsider mm1 =
mm as
Element of
NAT by ORDINAL1:def 12;
(ProjMap1 (FF2,n)) . mm = FF2 . (
n,
mm)
by Def8;
then A59:
(ProjMap1 (FF2,n)) . mm = (FF . n1) . mm1
by A8;
((ProjMap1 (FF2,n)) # x) . mm = ((ProjMap1 (FF2,n)) . mm) . x
by MESFUNC5:def 13;
then
((FF . n1) # x) . mm = ((ProjMap1 (FF2,n)) # x) . mm
by A59, MESFUNC5:def 13;
hence
|.((((FF . n1) # x) . mm) - lP).| < p
by A54, A57, A58;
verum
end; then A60:
(FF . n1) # x is
convergent_to_finite_number
;
reconsider lP =
lP as
R_eal by XXREAL_0:def 1;
(FF . n1) # x is
convergent
by A60;
then
lim ((FF . n1) # x) = lP
by A56, A60, MESFUNC5:def 12;
hence
(F . n) . x = lim ((ProjMap1 (FF2,n)) # x)
by A6, A43, A40, A54;
verum end; end;
end;
A67:
dom (lim (Partial_Sums F)) = dom ((Partial_Sums F) . 0)
by MESFUNC8:def 9;
then A68:
dom (lim (Partial_Sums F)) = E
by A1, Def4;
A69:
for n being Nat holds dom (P . n) = dom (lim (Partial_Sums F))
A72:
for n, m being Nat st n <= m holds
for i being Nat
for x being Element of X st x in E holds
((ProjMap2 (FF2,n)) . i) . x <= ((ProjMap2 (FF2,m)) . i) . x
proof
let n,
m be
Nat;
( n <= m implies for i being Nat
for x being Element of X st x in E holds
((ProjMap2 (FF2,n)) . i) . x <= ((ProjMap2 (FF2,m)) . i) . x )
assume A73:
n <= m
;
for i being Nat
for x being Element of X st x in E holds
((ProjMap2 (FF2,n)) . i) . x <= ((ProjMap2 (FF2,m)) . i) . x
let i be
Nat;
for x being Element of X st x in E holds
((ProjMap2 (FF2,n)) . i) . x <= ((ProjMap2 (FF2,m)) . i) . xlet x be
Element of
X;
( x in E implies ((ProjMap2 (FF2,n)) . i) . x <= ((ProjMap2 (FF2,m)) . i) . x )
reconsider i1 =
i,
n1 =
n,
m1 =
m as
Element of
NAT by ORDINAL1:def 12;
((ProjMap2 (FF2,n)) . i) . x = (FF2 . (i1,n1)) . x
by Def9;
then A74:
((ProjMap2 (FF2,n)) . i) . x = ((FF . i) . n) . x
by A8;
((ProjMap2 (FF2,m)) . i) . x = (FF2 . (i1,m1)) . x
by Def9;
then A75:
((ProjMap2 (FF2,m)) . i) . x = ((FF . i) . m) . x
by A8;
assume
x in E
;
((ProjMap2 (FF2,n)) . i) . x <= ((ProjMap2 (FF2,m)) . i) . x
then
x in dom (F . i)
by A1, A3;
hence
((ProjMap2 (FF2,n)) . i) . x <= ((ProjMap2 (FF2,m)) . i) . x
by A6, A73, A74, A75;
verum
end;
A76:
for n, m being Nat st n <= m holds
for i being Nat
for x being Element of X st x in E holds
((Partial_Sums (ProjMap2 (FF2,n))) . i) . x <= ((Partial_Sums (ProjMap2 (FF2,m))) . i) . x
proof
let n,
m be
Nat;
( n <= m implies for i being Nat
for x being Element of X st x in E holds
((Partial_Sums (ProjMap2 (FF2,n))) . i) . x <= ((Partial_Sums (ProjMap2 (FF2,m))) . i) . x )
A77:
ProjMap2 (
FF2,
n) is
with_the_same_dom
by A10;
A78:
ProjMap2 (
FF2,
m) is
additive
by A10;
assume A79:
n <= m
;
for i being Nat
for x being Element of X st x in E holds
((Partial_Sums (ProjMap2 (FF2,n))) . i) . x <= ((Partial_Sums (ProjMap2 (FF2,m))) . i) . x
A80:
for
i being
Nat for
x being
Element of
X st
x in (dom ((ProjMap2 (FF2,n)) . 0)) /\ (dom ((ProjMap2 (FF2,m)) . 0)) holds
((ProjMap2 (FF2,n)) . i) . x <= ((ProjMap2 (FF2,m)) . i) . x
proof
let i be
Nat;
for x being Element of X st x in (dom ((ProjMap2 (FF2,n)) . 0)) /\ (dom ((ProjMap2 (FF2,m)) . 0)) holds
((ProjMap2 (FF2,n)) . i) . x <= ((ProjMap2 (FF2,m)) . i) . xlet x be
Element of
X;
( x in (dom ((ProjMap2 (FF2,n)) . 0)) /\ (dom ((ProjMap2 (FF2,m)) . 0)) implies ((ProjMap2 (FF2,n)) . i) . x <= ((ProjMap2 (FF2,m)) . i) . x )
assume
x in (dom ((ProjMap2 (FF2,n)) . 0)) /\ (dom ((ProjMap2 (FF2,m)) . 0))
;
((ProjMap2 (FF2,n)) . i) . x <= ((ProjMap2 (FF2,m)) . i) . x
then
x in dom ((ProjMap2 (FF2,n)) . 0)
by XBOOLE_0:def 4;
then
x in E
by A10;
hence
((ProjMap2 (FF2,n)) . i) . x <= ((ProjMap2 (FF2,m)) . i) . x
by A72, A79;
verum
end;
let i be
Nat;
for x being Element of X st x in E holds
((Partial_Sums (ProjMap2 (FF2,n))) . i) . x <= ((Partial_Sums (ProjMap2 (FF2,m))) . i) . xlet x be
Element of
X;
( x in E implies ((Partial_Sums (ProjMap2 (FF2,n))) . i) . x <= ((Partial_Sums (ProjMap2 (FF2,m))) . i) . x )
assume A81:
x in E
;
((Partial_Sums (ProjMap2 (FF2,n))) . i) . x <= ((Partial_Sums (ProjMap2 (FF2,m))) . i) . x
then A82:
x in dom ((ProjMap2 (FF2,m)) . 0)
by A10;
x in dom ((ProjMap2 (FF2,n)) . 0)
by A10, A81;
then A83:
x in (dom ((ProjMap2 (FF2,n)) . 0)) /\ (dom ((ProjMap2 (FF2,m)) . 0))
by A82, XBOOLE_0:def 4;
A84:
ProjMap2 (
FF2,
m) is
with_the_same_dom
by A10;
ProjMap2 (
FF2,
n) is
additive
by A10;
hence
((Partial_Sums (ProjMap2 (FF2,n))) . i) . x <= ((Partial_Sums (ProjMap2 (FF2,m))) . i) . x
by A83, A77, A78, A84, A80, Th42;
verum
end;
A85:
for n, m being Nat st n <= m holds
for x being Element of X st x in E holds
(P . n) . x <= (P . m) . x
proof
let n,
m be
Nat;
( n <= m implies for x being Element of X st x in E holds
(P . n) . x <= (P . m) . x )
reconsider n1 =
n,
m1 =
m as
Element of
NAT by ORDINAL1:def 12;
assume A86:
n <= m
;
for x being Element of X st x in E holds
(P . n) . x <= (P . m) . x
let x be
Element of
X;
( x in E implies (P . n) . x <= (P . m) . x )
A87:
ProjMap2 (
FF2,
m) is
with_the_same_dom
by A10;
A88:
for
n being
Nat holds
(ProjMap2 (FF2,m)) . n is
nonnegative
by A38;
assume A89:
x in E
;
(P . n) . x <= (P . m) . x
then
x in dom ((ProjMap2 (FF2,m)) . 0)
by A10;
then
(Partial_Sums (ProjMap2 (FF2,m))) # x is
non-decreasing
by A87, A88, Th38;
then
((Partial_Sums (ProjMap2 (FF2,m))) # x) . n1 <= ((Partial_Sums (ProjMap2 (FF2,m))) # x) . m1
by A86, RINFSUP2:7;
then
((Partial_Sums (ProjMap2 (FF2,m))) . n) . x <= ((Partial_Sums (ProjMap2 (FF2,m))) # x) . m1
by MESFUNC5:def 13;
then
((Partial_Sums (ProjMap2 (FF2,m))) . n) . x <= ((Partial_Sums (ProjMap2 (FF2,m))) . m) . x
by MESFUNC5:def 13;
then A90:
((Partial_Sums (ProjMap2 (FF2,m))) . n) . x <= (P . m) . x
by A9;
((Partial_Sums (ProjMap2 (FF2,n))) . n) . x <= ((Partial_Sums (ProjMap2 (FF2,m))) . n) . x
by A76, A86, A89;
then
(P . n) . x <= ((Partial_Sums (ProjMap2 (FF2,m))) . n) . x
by A9;
hence
(P . n) . x <= (P . m) . x
by A90, XXREAL_0:2;
verum
end;
A91:
for x being Element of X st x in dom (lim P) holds
P # x is convergent
A93:
for x being Element of X st x in dom (lim P) holds
lim (P # x) = lim ((Partial_Sums F) # x)
proof
defpred S2[
Element of
NAT ,
Element of
NAT ,
set ]
means for
n,
m being
Nat st
n = $1 &
m = $2 holds
$3
= (Partial_Sums (ProjMap2 (FF2,n))) . m;
let x be
Element of
X;
( x in dom (lim P) implies lim (P # x) = lim ((Partial_Sums F) # x) )
A94:
for
i1,
j1 being
Element of
NAT ex
PP2 being
Element of
PFuncs (
X,
ExtREAL) st
S2[
i1,
j1,
PP2]
proof
let i1,
j1 be
Element of
NAT ;
ex PP2 being Element of PFuncs (X,ExtREAL) st S2[i1,j1,PP2]
reconsider i =
i1,
j =
j1 as
Nat ;
reconsider F1 =
(Partial_Sums (ProjMap2 (FF2,i))) . j as
Element of
PFuncs (
X,
ExtREAL)
by PARTFUN1:45;
take
F1
;
S2[i1,j1,F1]
thus
S2[
i1,
j1,
F1]
;
verum
end;
consider PP2 being
Function of
[:NAT,NAT:],
(PFuncs (X,ExtREAL)) such that A95:
for
i,
j being
Element of
NAT holds
S2[
i,
j,
PP2 . (
i,
j)]
from BINOP_1:sch 3(A94);
assume A96:
x in dom (lim P)
;
lim (P # x) = lim ((Partial_Sums F) # x)
then A97:
P # x is
convergent
by A91;
A98:
for
p,
n being
Element of
NAT holds
(ProjMap2 (PP2,n)) . p = (Partial_Sums (ProjMap2 (FF2,p))) . n
A99:
for
n being
Element of
NAT holds
(
(ProjMap2 (PP2,n)) # x is
convergent &
((ProjMap2 (PP2,n)) # x) ^\ n is
convergent &
lim ((ProjMap2 (PP2,n)) # x) = lim (((ProjMap2 (PP2,n)) # x) ^\ n) )
proof
let n be
Element of
NAT ;
( (ProjMap2 (PP2,n)) # x is convergent & ((ProjMap2 (PP2,n)) # x) ^\ n is convergent & lim ((ProjMap2 (PP2,n)) # x) = lim (((ProjMap2 (PP2,n)) # x) ^\ n) )
(ProjMap2 (PP2,n)) # x is
non-decreasing
proof
let j,
k be
ExtReal;
VALUED_0:def 15 ( not j in dom ((ProjMap2 (PP2,n)) # x) or not k in dom ((ProjMap2 (PP2,n)) # x) or not j <= k or ((ProjMap2 (PP2,n)) # x) . j <= ((ProjMap2 (PP2,n)) # x) . k )
assume that A100:
j in dom ((ProjMap2 (PP2,n)) # x)
and A101:
k in dom ((ProjMap2 (PP2,n)) # x)
and A102:
j <= k
;
((ProjMap2 (PP2,n)) # x) . j <= ((ProjMap2 (PP2,n)) # x) . k
reconsider j =
j,
k =
k as
Element of
NAT by A100, A101;
A103:
ProjMap2 (
FF2,
j) is
additive
by A10;
A104:
ProjMap2 (
FF2,
k) is
with_the_same_dom
by A10;
A105:
dom ((ProjMap2 (FF2,k)) . 0) = E
by A10;
((ProjMap2 (PP2,n)) # x) . k = ((ProjMap2 (PP2,n)) . k) . x
by MESFUNC5:def 13;
then A106:
((ProjMap2 (PP2,n)) # x) . k = ((Partial_Sums (ProjMap2 (FF2,k))) . n) . x
by A98;
A107:
ProjMap2 (
FF2,
k) is
additive
by A10;
((ProjMap2 (PP2,n)) # x) . j = ((ProjMap2 (PP2,n)) . j) . x
by MESFUNC5:def 13;
then A108:
((ProjMap2 (PP2,n)) # x) . j = ((Partial_Sums (ProjMap2 (FF2,j))) . n) . x
by A98;
A109:
ProjMap2 (
FF2,
j) is
with_the_same_dom
by A10;
A110:
dom ((ProjMap2 (FF2,j)) . 0) = E
by A10;
then
for
i being
Nat for
z being
Element of
X st
z in (dom ((ProjMap2 (FF2,j)) . 0)) /\ (dom ((ProjMap2 (FF2,k)) . 0)) holds
((ProjMap2 (FF2,j)) . i) . z <= ((ProjMap2 (FF2,k)) . i) . z
by A72, A102, A105;
hence
((ProjMap2 (PP2,n)) # x) . j <= ((ProjMap2 (PP2,n)) # x) . k
by A1, A23, A96, A108, A106, A103, A109, A107, A104, A110, A105, Th42;
verum
end;
hence
(ProjMap2 (PP2,n)) # x is
convergent
by RINFSUP2:37;
( ((ProjMap2 (PP2,n)) # x) ^\ n is convergent & lim ((ProjMap2 (PP2,n)) # x) = lim (((ProjMap2 (PP2,n)) # x) ^\ n) )
hence
(
((ProjMap2 (PP2,n)) # x) ^\ n is
convergent &
lim ((ProjMap2 (PP2,n)) # x) = lim (((ProjMap2 (PP2,n)) # x) ^\ n) )
by RINFSUP2:21;
verum
end;
A111:
for
n being
Nat holds
((Partial_Sums F) # x) . n <= lim (P # x)
proof
for
p being
object st
p in NAT holds
((ProjMap2 (PP2,0)) # x) . p = ((ProjMap1 (FF2,0)) # x) . p
proof
let p be
object ;
( p in NAT implies ((ProjMap2 (PP2,0)) # x) . p = ((ProjMap1 (FF2,0)) # x) . p )
assume
p in NAT
;
((ProjMap2 (PP2,0)) # x) . p = ((ProjMap1 (FF2,0)) # x) . p
then reconsider p9 =
p as
Element of
NAT ;
(ProjMap2 (PP2,0)) . p9 = (Partial_Sums (ProjMap2 (FF2,p9))) . 0
by A98;
then
(ProjMap2 (PP2,0)) . p9 = (ProjMap2 (FF2,p9)) . 0
by Def4;
then
(ProjMap2 (PP2,0)) . p9 = FF2 . (
0,
p9)
by Def9;
then A112:
(ProjMap2 (PP2,0)) . p9 = (ProjMap1 (FF2,0)) . p9
by Def8;
((ProjMap2 (PP2,0)) # x) . p = ((ProjMap2 (PP2,0)) . p9) . x
by MESFUNC5:def 13;
hence
((ProjMap2 (PP2,0)) # x) . p = ((ProjMap1 (FF2,0)) # x) . p
by A112, MESFUNC5:def 13;
verum
end;
then
(ProjMap2 (PP2,0)) # x = (ProjMap1 (FF2,0)) # x
;
then A113:
lim ((ProjMap2 (PP2,0)) # x) = (F . 0) . x
by A1, A39, A23, A96;
defpred S3[
Nat]
means lim ((ProjMap2 (PP2,$1)) # x) = ((Partial_Sums F) # x) . $1;
let n be
Nat;
((Partial_Sums F) # x) . n <= lim (P # x)
reconsider n9 =
n as
Element of
NAT by ORDINAL1:def 12;
A114:
lim ((P # x) ^\ n9) = lim (P # x)
by A97, RINFSUP2:21;
A115:
((ProjMap2 (PP2,n)) # x) ^\ n9 is
convergent
by A99;
A116:
for
k being
Nat st
S3[
k] holds
S3[
k + 1]
proof
let k be
Nat;
( S3[k] implies S3[k + 1] )
reconsider k9 =
k as
Element of
NAT by ORDINAL1:def 12;
assume A117:
S3[
k]
;
S3[k + 1]
A118:
(ProjMap2 (PP2,k9)) # x is
convergent
by A99;
then A119:
(ProjMap1 (FF2,(k + 1))) # x is
V116()
by SUPINF_2:52;
now for m being object st m in dom ((ProjMap2 (PP2,k)) # x) holds
0. <= ((ProjMap2 (PP2,k)) # x) . mlet m be
object ;
( m in dom ((ProjMap2 (PP2,k)) # x) implies 0. <= ((ProjMap2 (PP2,k)) # x) . m )assume
m in dom ((ProjMap2 (PP2,k)) # x)
;
0. <= ((ProjMap2 (PP2,k)) # x) . mthen reconsider m1 =
m as
Element of
NAT ;
A120:
(ProjMap2 (PP2,k)) . m1 = (Partial_Sums (ProjMap2 (FF2,m1))) . k9
by A98;
for
l being
Nat holds
(ProjMap2 (FF2,m1)) . l is
nonnegative
by A38;
then
(ProjMap2 (PP2,k)) . m1 is
nonnegative
by A120, Th36;
then
0. <= ((ProjMap2 (PP2,k)) . m1) . x
by SUPINF_2:51;
hence
0. <= ((ProjMap2 (PP2,k)) # x) . m
by MESFUNC5:def 13;
verum end;
then A121:
(ProjMap2 (PP2,k)) # x is
V116()
by SUPINF_2:52;
x in dom ((Partial_Sums F) . (k + 1))
by A2, A3, A23, A96, Th29;
then A122:
x in dom (((Partial_Sums F) . k) + (F . (k + 1)))
by Def4;
A123:
for
p being
Nat holds
((ProjMap2 (PP2,(k + 1))) # x) . p = (((ProjMap2 (PP2,k)) # x) . p) + (((ProjMap1 (FF2,(k + 1))) # x) . p)
proof
let p be
Nat;
((ProjMap2 (PP2,(k + 1))) # x) . p = (((ProjMap2 (PP2,k)) # x) . p) + (((ProjMap1 (FF2,(k + 1))) # x) . p)
reconsider p9 =
p as
Element of
NAT by ORDINAL1:def 12;
A124:
(ProjMap2 (FF2,p9)) . (k + 1) = FF2 . (
(k + 1),
p9)
by Def9;
A125:
ProjMap2 (
FF2,
p) is
with_the_same_dom
by A10;
A126:
dom ((ProjMap2 (FF2,p)) . 0) = E
by A10;
ProjMap2 (
FF2,
p) is
additive
by A10;
then
E c= dom ((Partial_Sums (ProjMap2 (FF2,p))) . (k + 1))
by A125, A126, Th29;
then A127:
E c= dom ((ProjMap2 (PP2,(k + 1))) . p9)
by A98;
(ProjMap2 (PP2,(k + 1))) . p9 = (Partial_Sums (ProjMap2 (FF2,p9))) . (k + 1)
by A98;
then A128:
(ProjMap2 (PP2,(k + 1))) . p9 = ((Partial_Sums (ProjMap2 (FF2,p9))) . k) + ((ProjMap2 (FF2,p9)) . (k + 1))
by Def4;
(Partial_Sums (ProjMap2 (FF2,p9))) . k9 = (ProjMap2 (PP2,k)) . p9
by A98;
then
(ProjMap2 (PP2,(k + 1))) . p9 = ((ProjMap2 (PP2,k)) . p9) + ((ProjMap1 (FF2,(k + 1))) . p9)
by A128, A124, Def8;
then
((ProjMap2 (PP2,(k + 1))) . p9) . x = (((ProjMap2 (PP2,k)) . p9) . x) + (((ProjMap1 (FF2,(k + 1))) . p9) . x)
by A1, A23, A96, A127, MESFUNC1:def 3;
then A129:
((ProjMap2 (PP2,(k + 1))) . p9) . x = (((ProjMap2 (PP2,k)) # x) . p) + (((ProjMap1 (FF2,(k + 1))) . p9) . x)
by MESFUNC5:def 13;
((ProjMap2 (PP2,(k + 1))) # x) . p = ((ProjMap2 (PP2,(k + 1))) . p9) . x
by MESFUNC5:def 13;
hence
((ProjMap2 (PP2,(k + 1))) # x) . p = (((ProjMap2 (PP2,k)) # x) . p) + (((ProjMap1 (FF2,(k + 1))) # x) . p)
by A129, MESFUNC5:def 13;
verum
end;
A130:
lim ((ProjMap1 (FF2,(k + 1))) # x) = (F . (k + 1)) . x
by A1, A39, A23, A96;
(ProjMap1 (FF2,(k + 1))) # x is
convergent
by A1, A39, A23, A96;
then
lim ((ProjMap2 (PP2,(k + 1))) # x) = (lim ((ProjMap2 (PP2,k)) # x)) + (lim ((ProjMap1 (FF2,(k + 1))) # x))
by A118, A121, A119, A123, Th11;
then
lim ((ProjMap2 (PP2,(k + 1))) # x) = (((Partial_Sums F) . k) . x) + ((F . (k + 1)) . x)
by A117, A130, MESFUNC5:def 13;
then
lim ((ProjMap2 (PP2,(k + 1))) # x) = (((Partial_Sums F) . k) + (F . (k + 1))) . x
by A122, MESFUNC1:def 3;
then
lim ((ProjMap2 (PP2,(k + 1))) # x) = ((Partial_Sums F) . (k + 1)) . x
by Def4;
hence
S3[
k + 1]
by MESFUNC5:def 13;
verum
end;
A131:
for
p being
Nat holds
(((ProjMap2 (PP2,n)) # x) ^\ n9) . p <= ((P # x) ^\ n9) . p
proof
let p be
Nat;
(((ProjMap2 (PP2,n)) # x) ^\ n9) . p <= ((P # x) ^\ n9) . p
A132:
n + p in NAT
by ORDINAL1:def 12;
A133:
n <= n + p
by NAT_1:11;
A134:
ProjMap2 (
FF2,
(n + p)) is
with_the_same_dom
by A10;
A135:
for
i being
Nat holds
(ProjMap2 (FF2,(n + p))) . i is
nonnegative
by A38;
x in dom ((ProjMap2 (FF2,(n + p))) . 0)
by A1, A10, A23, A96;
then
(Partial_Sums (ProjMap2 (FF2,(n + p)))) # x is
non-decreasing
by A134, A135, Th38;
then
((Partial_Sums (ProjMap2 (FF2,(n + p)))) # x) . n9 <= ((Partial_Sums (ProjMap2 (FF2,(n + p)))) # x) . (n9 + p)
by A133, RINFSUP2:7;
then A136:
((Partial_Sums (ProjMap2 (FF2,(n + p)))) # x) . n9 <= ((Partial_Sums (ProjMap2 (FF2,(n + p)))) . (n + p)) . x
by MESFUNC5:def 13;
((P # x) ^\ n9) . p = (P # x) . (n + p)
by NAT_1:def 3;
then
((P # x) ^\ n9) . p = (P . (n + p)) . x
by MESFUNC5:def 13;
then A137:
((P # x) ^\ n9) . p = ((Partial_Sums (ProjMap2 (FF2,(n + p)))) . (n + p)) . x
by A9;
(((ProjMap2 (PP2,n)) # x) ^\ n9) . p = ((ProjMap2 (PP2,n)) # x) . (n + p)
by NAT_1:def 3;
then
(((ProjMap2 (PP2,n)) # x) ^\ n9) . p = ((ProjMap2 (PP2,n)) . (n + p)) . x
by MESFUNC5:def 13;
then
(((ProjMap2 (PP2,n)) # x) ^\ n9) . p = ((Partial_Sums (ProjMap2 (FF2,(n + p)))) . n) . x
by A98, A132;
hence
(((ProjMap2 (PP2,n)) # x) ^\ n9) . p <= ((P # x) ^\ n9) . p
by A137, A136, MESFUNC5:def 13;
verum
end;
((Partial_Sums F) # x) . 0 = ((Partial_Sums F) . 0) . x
by MESFUNC5:def 13;
then A138:
S3[
0 ]
by A113, Def4;
A139:
for
k being
Nat holds
S3[
k]
from NAT_1:sch 2(A138, A116);
(P # x) ^\ n9 is
convergent
by A97, RINFSUP2:21;
then
lim (((ProjMap2 (PP2,n)) # x) ^\ n9) <= lim ((P # x) ^\ n9)
by A115, A131, RINFSUP2:38;
then
lim ((ProjMap2 (PP2,n)) # x) <= lim (P # x)
by A99, A114;
hence
((Partial_Sums F) # x) . n <= lim (P # x)
by A139;
verum
end;
F # x is
summable
by A1, A5, A23, A96;
then A140:
Partial_Sums (F # x) is
convergent
;
(Partial_Sums F) # x is
convergent
then A141:
lim ((Partial_Sums F) # x) <= lim (P # x)
by A111, Th9;
A142:
for
k being
Nat holds
(P # x) . k <= ((Partial_Sums F) # x) . k
(Partial_Sums F) # x is
convergent
by A3, A4, A23, A96, Th38;
then
lim (P # x) <= lim ((Partial_Sums F) # x)
by A97, A142, RINFSUP2:38;
hence
lim (P # x) = lim ((Partial_Sums F) # x)
by A141, XXREAL_0:1;
verum
end;
A143:
for x being Element of X st x in dom (lim (Partial_Sums F)) holds
( P # x is convergent & lim (P # x) = (lim (Partial_Sums F)) . x )
A145:
for n being Nat holds P . n is nonnegative
A146:
for x being object st x in dom (lim (Partial_Sums F)) holds
(lim (Partial_Sums F)) . x >= 0
then A149:
lim (Partial_Sums F) is nonnegative
by SUPINF_2:52;
consider I being ExtREAL_sequence such that
A150:
for n being Nat holds
( I . n = Integral (M,(F . n)) & Integral (M,((Partial_Sums F) . n)) = (Partial_Sums I) . n )
by A1, A2, A3, A4, Th50;
for n being object st n in dom I holds
0 <= I . n
then
I is V116()
by SUPINF_2:52;
then A153:
Partial_Sums I is non-decreasing
by Th16;
then A154:
Partial_Sums I is convergent
by RINFSUP2:37;
deffunc H2( Element of NAT ) -> Element of ExtREAL = integral' (M,(P . $1));
consider J being sequence of ExtREAL such that
A155:
for n being Element of NAT holds J . n = H2(n)
from FUNCT_2:sch 4();
reconsider J = J as ExtREAL_sequence ;
A156:
for n being Nat holds P . n is_simple_func_in S
A157:
for n being Nat holds J . n = integral' (M,(P . n))
for n, m being Nat st m <= n holds
J . m <= J . n
proof
let n,
m be
Nat;
( m <= n implies J . m <= J . n )
A158:
P . n is
nonnegative
by A145;
A159:
P . m is_simple_func_in S
by A156;
A160:
for
n,
m,
l being
Nat holds
dom ((P . n) - (P . m)) = dom (P . l)
then A162:
dom ((P . n) - (P . m)) = dom (P . n)
;
then A163:
(P . n) | (dom ((P . n) - (P . m))) = P . n
;
assume A164:
m <= n
;
J . m <= J . n
A165:
for
x being
object st
x in dom ((P . n) - (P . m)) holds
(P . m) . x <= (P . n) . x
A166:
P . m is
nonnegative
by A145;
dom ((P . n) - (P . m)) = dom (P . m)
by A160;
then A167:
(P . m) | (dom ((P . n) - (P . m))) = P . m
;
P . n is_simple_func_in S
by A156;
then
integral' (
M,
((P . m) | (dom ((P . n) - (P . m)))))
<= integral' (
M,
((P . n) | (dom ((P . n) - (P . m)))))
by A158, A159, A166, A165, MESFUNC5:70;
then
J . m <= integral' (
M,
(P . n))
by A157, A167, A163;
hence
J . m <= J . n
by A157;
verum
end;
then
J is non-decreasing
by RINFSUP2:7;
then A168:
J is convergent
by RINFSUP2:37;
A169:
for n being Nat holds F . n is V124()
by A4, MESFUNC5:12;
then A170:
for n being Nat holds (Partial_Sums F) . n is E -measurable
by A4, Th41;
then
lim (Partial_Sums F) is E -measurable
by A1, A2, A3, A5, Th44;
then
integral+ (M,(lim (Partial_Sums F))) = lim J
by A68, A156, A85, A157, A69, A143, A145, A149, A168, MESFUNC5:def 15;
then A171:
Integral (M,(lim (Partial_Sums F))) = lim J
by A1, A2, A3, A5, A170, A37, A149, Th44, MESFUNC5:88;
A172:
for n being Nat
for x being Element of X st x in dom (F . n) holds
(FF . n) # x is non-decreasing
A177:
for n, p being Nat st p >= n holds
for x being Element of X st x in E holds
( ((Partial_Sums (ProjMap2 (FF2,p))) . n) . x <= (P . p) . x & (P . p) . x = ((Partial_Sums (ProjMap2 (FF2,p))) . p) . x & ((Partial_Sums (ProjMap2 (FF2,p))) . p) . x <= ((Partial_Sums F) . p) . x & ((Partial_Sums F) . p) . x <= (lim (Partial_Sums F)) . x )
proof
let n,
p be
Nat;
( p >= n implies for x being Element of X st x in E holds
( ((Partial_Sums (ProjMap2 (FF2,p))) . n) . x <= (P . p) . x & (P . p) . x = ((Partial_Sums (ProjMap2 (FF2,p))) . p) . x & ((Partial_Sums (ProjMap2 (FF2,p))) . p) . x <= ((Partial_Sums F) . p) . x & ((Partial_Sums F) . p) . x <= (lim (Partial_Sums F)) . x ) )
reconsider p1 =
p,
n1 =
n as
Element of
NAT by ORDINAL1:def 12;
assume A178:
p >= n
;
for x being Element of X st x in E holds
( ((Partial_Sums (ProjMap2 (FF2,p))) . n) . x <= (P . p) . x & (P . p) . x = ((Partial_Sums (ProjMap2 (FF2,p))) . p) . x & ((Partial_Sums (ProjMap2 (FF2,p))) . p) . x <= ((Partial_Sums F) . p) . x & ((Partial_Sums F) . p) . x <= (lim (Partial_Sums F)) . x )
let x be
Element of
X;
( x in E implies ( ((Partial_Sums (ProjMap2 (FF2,p))) . n) . x <= (P . p) . x & (P . p) . x = ((Partial_Sums (ProjMap2 (FF2,p))) . p) . x & ((Partial_Sums (ProjMap2 (FF2,p))) . p) . x <= ((Partial_Sums F) . p) . x & ((Partial_Sums F) . p) . x <= (lim (Partial_Sums F)) . x ) )
A179:
for
i being
Nat holds
(ProjMap2 (FF2,p)) . i is
nonnegative
by A38;
assume A180:
x in E
;
( ((Partial_Sums (ProjMap2 (FF2,p))) . n) . x <= (P . p) . x & (P . p) . x = ((Partial_Sums (ProjMap2 (FF2,p))) . p) . x & ((Partial_Sums (ProjMap2 (FF2,p))) . p) . x <= ((Partial_Sums F) . p) . x & ((Partial_Sums F) . p) . x <= (lim (Partial_Sums F)) . x )
then A181:
x in dom ((ProjMap2 (FF2,p)) . 0)
by A10;
ProjMap2 (
FF2,
p) is
with_the_same_dom
by A10;
then
(Partial_Sums (ProjMap2 (FF2,p))) # x is
non-decreasing
by A181, A179, Th38;
then
((Partial_Sums (ProjMap2 (FF2,p))) # x) . n1 <= ((Partial_Sums (ProjMap2 (FF2,p))) # x) . p1
by A178, RINFSUP2:7;
then
((Partial_Sums (ProjMap2 (FF2,p))) . n) . x <= ((Partial_Sums (ProjMap2 (FF2,p))) # x) . p
by MESFUNC5:def 13;
then
((Partial_Sums (ProjMap2 (FF2,p))) . n) . x <= ((Partial_Sums (ProjMap2 (FF2,p))) . p) . x
by MESFUNC5:def 13;
hence
((Partial_Sums (ProjMap2 (FF2,p))) . n) . x <= (P . p) . x
by A9;
( (P . p) . x = ((Partial_Sums (ProjMap2 (FF2,p))) . p) . x & ((Partial_Sums (ProjMap2 (FF2,p))) . p) . x <= ((Partial_Sums F) . p) . x & ((Partial_Sums F) . p) . x <= (lim (Partial_Sums F)) . x )
thus
(P . p) . x = ((Partial_Sums (ProjMap2 (FF2,p))) . p) . x
by A9;
( ((Partial_Sums (ProjMap2 (FF2,p))) . p) . x <= ((Partial_Sums F) . p) . x & ((Partial_Sums F) . p) . x <= (lim (Partial_Sums F)) . x )
A182:
ProjMap2 (
FF2,
p) is
additive
by A10;
A183:
ProjMap2 (
FF2,
p) is
with_the_same_dom
by A10;
A184:
for
n being
Nat for
x being
Element of
X st
x in (dom ((ProjMap2 (FF2,p)) . 0)) /\ (dom (F . 0)) holds
((ProjMap2 (FF2,p)) . n) . x <= (F . n) . x
proof
let n be
Nat;
for x being Element of X st x in (dom ((ProjMap2 (FF2,p)) . 0)) /\ (dom (F . 0)) holds
((ProjMap2 (FF2,p)) . n) . x <= (F . n) . xlet x be
Element of
X;
( x in (dom ((ProjMap2 (FF2,p)) . 0)) /\ (dom (F . 0)) implies ((ProjMap2 (FF2,p)) . n) . x <= (F . n) . x )
reconsider n1 =
n as
Element of
NAT by ORDINAL1:def 12;
assume
x in (dom ((ProjMap2 (FF2,p)) . 0)) /\ (dom (F . 0))
;
((ProjMap2 (FF2,p)) . n) . x <= (F . n) . x
then
x in dom (F . 0)
by XBOOLE_0:def 4;
then A185:
x in dom (F . n)
by A3;
then
(FF . n) # x is
non-decreasing
by A172;
then
lim ((FF . n) # x) = sup ((FF . n) # x)
by RINFSUP2:37;
then
((FF . n) # x) . p1 <= lim ((FF . n) # x)
by RINFSUP2:23;
then A186:
((FF . n) # x) . p <= (F . n) . x
by A6, A185;
((ProjMap2 (FF2,p)) . n) . x = (FF2 . (n1,p1)) . x
by Def9;
then
((ProjMap2 (FF2,p)) . n) . x = ((FF . n) . p) . x
by A8;
hence
((ProjMap2 (FF2,p)) . n) . x <= (F . n) . x
by A186, MESFUNC5:def 13;
verum
end;
x in (dom ((ProjMap2 (FF2,p)) . 0)) /\ (dom (F . 0))
by A1, A180, A181, XBOOLE_0:def 4;
hence
((Partial_Sums (ProjMap2 (FF2,p))) . p) . x <= ((Partial_Sums F) . p) . x
by A2, A3, A182, A183, A184, Th42;
((Partial_Sums F) . p) . x <= (lim (Partial_Sums F)) . x
(Partial_Sums F) # x is
non-decreasing
by A1, A3, A4, A180, Th38;
then
lim ((Partial_Sums F) # x) = sup ((Partial_Sums F) # x)
by RINFSUP2:37;
then
((Partial_Sums F) # x) . p1 <= lim ((Partial_Sums F) # x)
by RINFSUP2:23;
then
((Partial_Sums F) . p) . x <= lim ((Partial_Sums F) # x)
by MESFUNC5:def 13;
hence
((Partial_Sums F) . p) . x <= (lim (Partial_Sums F)) . x
by A68, A180, MESFUNC8:def 9;
verum
end;
for n being Nat holds (Partial_Sums I) . n <= Integral (M,(lim (Partial_Sums F)))
proof
let n be
Nat;
(Partial_Sums I) . n <= Integral (M,(lim (Partial_Sums F)))
A187:
(Partial_Sums F) . n is
nonnegative
by A4, Th36;
A188:
lim (Partial_Sums F) is
E -measurable
by A1, A2, A3, A5, A170, Th44;
A189:
(Partial_Sums F) . n is
E -measurable
by A4, A169, Th41;
A190:
E = dom ((Partial_Sums F) . n)
by A1, A2, A3, Th29;
then
for
x being
Element of
X st
x in dom ((Partial_Sums F) . n) holds
((Partial_Sums F) . n) . x <= (lim (Partial_Sums F)) . x
by A177;
then
integral+ (
M,
((Partial_Sums F) . n))
<= integral+ (
M,
(lim (Partial_Sums F)))
by A37, A149, A190, A189, A188, A187, MESFUNC5:85;
then
Integral (
M,
((Partial_Sums F) . n))
<= integral+ (
M,
(lim (Partial_Sums F)))
by A170, A190, A187, MESFUNC5:88;
then
Integral (
M,
((Partial_Sums F) . n))
<= Integral (
M,
(lim (Partial_Sums F)))
by A37, A146, A188, MESFUNC5:88, SUPINF_2:52;
hence
(Partial_Sums I) . n <= Integral (
M,
(lim (Partial_Sums F)))
by A150;
verum
end;
then A191:
lim (Partial_Sums I) <= Integral (M,(lim (Partial_Sums F)))
by A153, Th9, RINFSUP2:37;
take
I
; ( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )
thus
for n being Nat holds I . n = Integral (M,((F . n) | E))
( I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )
A192:
for n being Nat holds J . n = Integral (M,(P . n))
for n being Nat holds J . n <= (Partial_Sums I) . n
proof
let n be
Nat;
J . n <= (Partial_Sums I) . n
A195:
P . n is
E -measurable
by A156, MESFUNC2:34;
A196:
(Partial_Sums F) . n is
nonnegative
by A4, Th36;
A197:
n in NAT
by ORDINAL1:def 12;
A198:
for
x being
Element of
X st
x in dom (P . n) holds
(P . n) . x <= ((Partial_Sums F) . n) . x
A199:
P . n is
nonnegative
by A145;
A200:
dom (P . n) = E
by A37, A69;
A201:
E = dom ((Partial_Sums F) . n)
by A1, A2, A3, Th29;
(Partial_Sums F) . n is
E -measurable
by A4, A169, Th41;
then
integral+ (
M,
(P . n))
<= integral+ (
M,
((Partial_Sums F) . n))
by A201, A200, A195, A199, A196, A198, MESFUNC5:85;
then
Integral (
M,
(P . n))
<= integral+ (
M,
((Partial_Sums F) . n))
by A145, A200, A195, MESFUNC5:88;
then
Integral (
M,
(P . n))
<= Integral (
M,
((Partial_Sums F) . n))
by A170, A201, A196, MESFUNC5:88;
then
J . n <= Integral (
M,
((Partial_Sums F) . n))
by A192;
hence
J . n <= (Partial_Sums I) . n
by A150;
verum
end;
then
lim J <= lim (Partial_Sums I)
by A168, A154, RINFSUP2:38;
then
Sum I = Integral (M,(lim (Partial_Sums F)))
by A171, A191, XXREAL_0:1;
hence
( I is summable & Integral (M,((lim (Partial_Sums F)) | E)) = Sum I )
by A37, A154; verum