let X be non empty set ; :: thesis: 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
for I being ExtREAL_sequence
for m being Nat st E = dom (F . 0 ) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is_measurable_on E & F . n is nonnegative & I . n = Integral M,(F . n) ) ) holds
Integral M,((Partial_Sums F) . m) = (Partial_Sums I) . m
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for E being Element of S
for F being Functional_Sequence of X,ExtREAL
for I being ExtREAL_sequence
for m being Nat st E = dom (F . 0 ) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is_measurable_on E & F . n is nonnegative & I . n = Integral M,(F . n) ) ) holds
Integral M,((Partial_Sums F) . m) = (Partial_Sums I) . m
let M be sigma_Measure of S; :: thesis: for E being Element of S
for F being Functional_Sequence of X,ExtREAL
for I being ExtREAL_sequence
for m being Nat st E = dom (F . 0 ) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is_measurable_on E & F . n is nonnegative & I . n = Integral M,(F . n) ) ) holds
Integral M,((Partial_Sums F) . m) = (Partial_Sums I) . m
let E be Element of S; :: thesis: for F being Functional_Sequence of X,ExtREAL
for I being ExtREAL_sequence
for m being Nat st E = dom (F . 0 ) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is_measurable_on E & F . n is nonnegative & I . n = Integral M,(F . n) ) ) holds
Integral M,((Partial_Sums F) . m) = (Partial_Sums I) . m
let F be Functional_Sequence of X,ExtREAL ; :: thesis: for I being ExtREAL_sequence
for m being Nat st E = dom (F . 0 ) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is_measurable_on E & F . n is nonnegative & I . n = Integral M,(F . n) ) ) holds
Integral M,((Partial_Sums F) . m) = (Partial_Sums I) . m
let I be ExtREAL_sequence; :: thesis: for m being Nat st E = dom (F . 0 ) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is_measurable_on E & F . n is nonnegative & I . n = Integral M,(F . n) ) ) holds
Integral M,((Partial_Sums F) . m) = (Partial_Sums I) . m
let m be Nat; :: thesis: ( E = dom (F . 0 ) & F is additive & F is with_the_same_dom & ( for n being Nat holds
( F . n is_measurable_on E & F . n is nonnegative & I . n = Integral M,(F . n) ) ) implies Integral M,((Partial_Sums F) . m) = (Partial_Sums I) . m )
assume that
A1:
E = dom (F . 0 )
and
A4:
F is additive
and
A5:
F is with_the_same_dom
and
A2:
for n being Nat holds
( F . n is_measurable_on E & F . n is nonnegative & I . n = Integral M,(F . n) )
; :: thesis: Integral M,((Partial_Sums F) . m) = (Partial_Sums I) . m
G3:
for n being Nat holds F . n is without-infty
by A2, MESFUNC5:18;
set PF = Partial_Sums F;
thus
Integral M,((Partial_Sums F) . m) = (Partial_Sums I) . m
:: thesis: verumproof
defpred S1[
Nat]
means Integral M,
((Partial_Sums F) . $1) = (Partial_Sums I) . $1;
set PI =
Partial_Sums I;
Integral M,
((Partial_Sums F) . 0 ) = Integral M,
(F . 0 )
by Def0;
then
Integral M,
((Partial_Sums F) . 0 ) = I . 0
by A2;
then A8:
S1[
0 ]
by Def1;
B1:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
:: thesis: ( S1[k] implies S1[k + 1] )
assume B2:
S1[
k]
;
:: thesis: S1[k + 1]
A12:
(
dom ((Partial_Sums F) . k) = E &
dom (F . (k + 1)) = E )
by A1, A4, A5, ADD0, MESFUNC8:def 2;
A9:
(
(Partial_Sums F) . k is_measurable_on E &
F . (k + 1) is_measurable_on E &
(Partial_Sums F) . k is
nonnegative &
F . (k + 1) is
nonnegative )
by A2, G3, ADD1, ADD3C;
then consider D being
Element of
S such that A11:
(
D = dom (((Partial_Sums F) . k) + (F . (k + 1))) &
integral+ M,
(((Partial_Sums F) . k) + (F . (k + 1))) = (integral+ M,(((Partial_Sums F) . k) | D)) + (integral+ M,((F . (k + 1)) | D)) )
by A12, MESFUNC5:84;
D = E /\ E
by A12, A9, A11, MESFUNC5:28;
then A14:
(
((Partial_Sums F) . k) | D = (Partial_Sums F) . k &
(F . (k + 1)) | D = F . (k + 1) )
by A12, RELAT_1:97;
(
dom ((Partial_Sums F) . (k + 1)) = E &
(Partial_Sums F) . (k + 1) is_measurable_on E &
(Partial_Sums F) . (k + 1) is
nonnegative )
by A1, G3, A2, A4, A5, ADD1, ADD3C, ADD0;
then Integral M,
((Partial_Sums F) . (k + 1)) =
integral+ M,
((Partial_Sums F) . (k + 1))
by MESFUNC5:94
.=
(integral+ M,(((Partial_Sums F) . k) | D)) + (integral+ M,((F . (k + 1)) | D))
by A11, Def0
.=
(Integral M,((Partial_Sums F) . k)) + (integral+ M,((F . (k + 1)) | D))
by A9, A12, A14, MESFUNC5:94
.=
(Integral M,((Partial_Sums F) . k)) + (Integral M,(F . (k + 1)))
by A9, A12, A14, MESFUNC5:94
.=
((Partial_Sums I) . k) + (I . (k + 1))
by A2, B2
;
hence
S1[
k + 1]
by Def1;
:: thesis: verum
end;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A8, B1);
hence
Integral M,
((Partial_Sums F) . m) = (Partial_Sums I) . m
;
:: thesis: verum
end;