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 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 ) ) holds
ex I being ExtREAL_sequence st
for n being Nat holds
( I . n = Integral M,(F . n) & Integral M,((Partial_Sums F) . n) = (Partial_Sums I) . n )
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 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 ) ) holds
ex I being ExtREAL_sequence st
for n being Nat holds
( I . n = Integral M,(F . n) & Integral M,((Partial_Sums F) . n) = (Partial_Sums I) . n )
let M be sigma_Measure of S; :: thesis: 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_measurable_on E & F . n is nonnegative ) ) holds
ex I being ExtREAL_sequence st
for n being Nat holds
( I . n = Integral M,(F . n) & Integral M,((Partial_Sums F) . n) = (Partial_Sums I) . n )
let E be Element of S; :: thesis: 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_measurable_on E & F . n is nonnegative ) ) holds
ex I being ExtREAL_sequence st
for n being Nat holds
( I . n = Integral M,(F . n) & Integral M,((Partial_Sums F) . n) = (Partial_Sums I) . n )
let F be Functional_Sequence of X,ExtREAL ; :: 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 ) ) implies ex I being ExtREAL_sequence st
for n being Nat holds
( I . n = Integral M,(F . n) & Integral M,((Partial_Sums F) . n) = (Partial_Sums I) . n ) )
assume that
A1:
E = dom (F . 0 )
and
A3:
F is additive
and
A4:
F is with_the_same_dom
and
A2:
for n being Nat holds
( F . n is_measurable_on E & F . n is nonnegative )
; :: thesis: ex I being ExtREAL_sequence st
for n being Nat holds
( I . n = Integral M,(F . n) & Integral M,((Partial_Sums F) . n) = (Partial_Sums I) . n )
G3:
for n being Nat holds F . n is without-infty
by A2, MESFUNC5:18;
deffunc H1( Element of NAT ) -> Element of ExtREAL = Integral M,(F . $1);
consider I being Function of NAT ,ExtREAL such that
A6:
for n being Element of NAT holds I . n = H1(n)
from FUNCT_2:sch 4();
reconsider I = I as ExtREAL_sequence ;
take
I
; :: thesis: for n being Nat holds
( I . n = Integral M,(F . n) & Integral M,((Partial_Sums F) . n) = (Partial_Sums I) . n )
set PF = Partial_Sums F;
thus
for n being Nat holds
( I . n = Integral M,(F . n) & Integral M,((Partial_Sums F) . n) = (Partial_Sums I) . n )
:: thesis: verumproof
let n be
Nat;
:: thesis: ( I . n = Integral M,(F . n) & Integral M,((Partial_Sums F) . n) = (Partial_Sums I) . n )
reconsider n' =
n as
Element of
NAT by ORDINAL1:def 13;
I . n = Integral M,
(F . n')
by A6;
hence
I . n = Integral M,
(F . n)
;
:: thesis: Integral M,((Partial_Sums F) . n) = (Partial_Sums I) . n
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 A6;
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]
reconsider k1 =
k + 1 as
Nat ;
A12:
(
dom ((Partial_Sums F) . k) = E &
dom (F . (k + 1)) = E )
by A1, A3, A4, 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 =
(dom ((Partial_Sums F) . k)) /\ (dom (F . (k + 1)))
by A9, A11, MESFUNC5:28
.=
E
by A12
;
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, A3, A4, G3, A2, ADD3C, ADD1, 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 A6, 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) . n) = (Partial_Sums I) . n
;
:: thesis: verum
end;