:: by Noboru Endou , Keiko Narita and Yasunari Shidama

::

:: Received March 18, 2008

:: Copyright (c) 2008-2016 Association of Mizar Users

theorem :: MESFUNC9:1

for X being non empty set

for f, g being PartFunc of X,ExtREAL st f is V124() & g is V124() holds

dom (f + g) = (dom f) /\ (dom g)

for f, g being PartFunc of X,ExtREAL st f is V124() & g is V124() holds

dom (f + g) = (dom f) /\ (dom g)

proof end;

theorem :: MESFUNC9:2

for X being non empty set

for f, g being PartFunc of X,ExtREAL st f is V124() & g is V123() holds

dom (f - g) = (dom f) /\ (dom g)

for f, g being PartFunc of X,ExtREAL st f is V124() & g is V123() holds

dom (f - g) = (dom f) /\ (dom g)

proof end;

theorem Th3: :: MESFUNC9:3

for X being non empty set

for f, g being PartFunc of X,ExtREAL st f is V123() & g is V123() holds

f + g is V123()

for f, g being PartFunc of X,ExtREAL st f is V123() & g is V123() holds

f + g is V123()

proof end;

theorem Th4: :: MESFUNC9:4

for X being non empty set

for f, g being PartFunc of X,ExtREAL st f is V124() & g is V124() holds

f + g is V124()

for f, g being PartFunc of X,ExtREAL st f is V124() & g is V124() holds

f + g is V124()

proof end;

theorem :: MESFUNC9:5

for X being non empty set

for f, g being PartFunc of X,ExtREAL st f is V123() & g is V124() holds

f - g is V123()

for f, g being PartFunc of X,ExtREAL st f is V123() & g is V124() holds

f - g is V123()

proof end;

theorem :: MESFUNC9:6

for X being non empty set

for f, g being PartFunc of X,ExtREAL st f is V124() & g is V123() holds

f - g is V124()

for f, g being PartFunc of X,ExtREAL st f is V124() & g is V123() holds

f - g is V124()

proof end;

theorem Th7: :: MESFUNC9:7

for seq being ExtREAL_sequence holds

( ( seq is convergent_to_finite_number implies ex g being Real st

( lim seq = g & ( for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - (lim seq)).| < p ) ) ) & ( seq is convergent_to_+infty implies lim seq = +infty ) & ( seq is convergent_to_-infty implies lim seq = -infty ) )

( ( seq is convergent_to_finite_number implies ex g being Real st

( lim seq = g & ( for p being Real st 0 < p holds

ex n being Nat st

for m being Nat st n <= m holds

|.((seq . m) - (lim seq)).| < p ) ) ) & ( seq is convergent_to_+infty implies lim seq = +infty ) & ( seq is convergent_to_-infty implies lim seq = -infty ) )

proof end;

theorem Th9: :: MESFUNC9:9

for seq being ExtREAL_sequence

for p being ExtReal st seq is convergent & ( for k being Nat holds seq . k <= p ) holds

lim seq <= p

for p being ExtReal st seq is convergent & ( for k being Nat holds seq . k <= p ) holds

lim seq <= p

proof end;

theorem Th10: :: MESFUNC9:10

for seq being ExtREAL_sequence

for p being ExtReal st seq is convergent & ( for k being Nat holds p <= seq . k ) holds

p <= lim seq

for p being ExtReal st seq is convergent & ( for k being Nat holds p <= seq . k ) holds

p <= lim seq

proof end;

reconsider zz = 0 as ExtReal ;

theorem Th11: :: MESFUNC9:11

for seq, seq1, seq2 being ExtREAL_sequence st seq1 is convergent & seq2 is convergent & seq1 is V115() & seq2 is V115() & ( for k being Nat holds seq . k = (seq1 . k) + (seq2 . k) ) holds

( seq is V115() & seq is convergent & lim seq = (lim seq1) + (lim seq2) )

( seq is V115() & seq is convergent & lim seq = (lim seq1) + (lim seq2) )

proof end;

theorem Th12: :: MESFUNC9:12

for X being non empty set

for F, G being Functional_Sequence of X,ExtREAL

for x being Element of X

for D being set st ( for n being Nat holds G . n = (F . n) | D ) & x in D holds

( ( F # x is convergent_to_+infty implies G # x is convergent_to_+infty ) & ( F # x is convergent_to_-infty implies G # x is convergent_to_-infty ) & ( F # x is convergent_to_finite_number implies G # x is convergent_to_finite_number ) & ( F # x is convergent implies G # x is convergent ) )

for F, G being Functional_Sequence of X,ExtREAL

for x being Element of X

for D being set st ( for n being Nat holds G . n = (F . n) | D ) & x in D holds

( ( F # x is convergent_to_+infty implies G # x is convergent_to_+infty ) & ( F # x is convergent_to_-infty implies G # x is convergent_to_-infty ) & ( F # x is convergent_to_finite_number implies G # x is convergent_to_finite_number ) & ( F # x is convergent implies G # x is convergent ) )

proof end;

theorem Th13: :: MESFUNC9:13

for X being 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 PartFunc of X,ExtREAL st E = dom f & f is_measurable_on E & f is nonnegative & M . (E /\ (eq_dom (f,+infty))) <> 0 holds

Integral (M,f) = +infty

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f being PartFunc of X,ExtREAL st E = dom f & f is_measurable_on E & f is nonnegative & M . (E /\ (eq_dom (f,+infty))) <> 0 holds

Integral (M,f) = +infty

proof end;

reconsider jj = 1 as Real ;

theorem :: MESFUNC9:14

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S holds

( Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E )

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S holds

( Integral (M,(chi (E,X))) = M . E & Integral (M,((chi (E,X)) | E)) = M . E )

proof end;

theorem Th15: :: MESFUNC9:15

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f, g being PartFunc of X,ExtREAL st E c= dom f & E c= dom g & f is_measurable_on E & g is_measurable_on E & f is nonnegative & ( for x being Element of X st x in E holds

f . x <= g . x ) holds

Integral (M,(f | E)) <= Integral (M,(g | E))

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f, g being PartFunc of X,ExtREAL st E c= dom f & E c= dom g & f is_measurable_on E & g is_measurable_on E & f is nonnegative & ( for x being Element of X st x in E holds

f . x <= g . x ) holds

Integral (M,(f | E)) <= Integral (M,(g | E))

proof end;

definition

let s be ext-real-valued Function;

ex b_{1} being ExtREAL_sequence st

( b_{1} . 0 = s . 0 & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) + (s . (n + 1)) ) )

for b_{1}, b_{2} being ExtREAL_sequence st b_{1} . 0 = s . 0 & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) + (s . (n + 1)) ) & b_{2} . 0 = s . 0 & ( for n being Nat holds b_{2} . (n + 1) = (b_{2} . n) + (s . (n + 1)) ) holds

b_{1} = b_{2}

end;
func Partial_Sums s -> ExtREAL_sequence means :Def1: :: MESFUNC9:def 1

( it . 0 = s . 0 & ( for n being Nat holds it . (n + 1) = (it . n) + (s . (n + 1)) ) );

existence ( it . 0 = s . 0 & ( for n being Nat holds it . (n + 1) = (it . n) + (s . (n + 1)) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines Partial_Sums MESFUNC9:def 1 :

for s being ext-real-valued Function

for b_{2} being ExtREAL_sequence holds

( b_{2} = Partial_Sums s iff ( b_{2} . 0 = s . 0 & ( for n being Nat holds b_{2} . (n + 1) = (b_{2} . n) + (s . (n + 1)) ) ) );

for s being ext-real-valued Function

for b

( b

:: deftheorem defines summable MESFUNC9:def 2 :

for s being ext-real-valued Function holds

( s is summable iff Partial_Sums s is convergent );

for s being ext-real-valued Function holds

( s is summable iff Partial_Sums s is convergent );

definition
end;

:: deftheorem defines Sum MESFUNC9:def 3 :

for s being ext-real-valued Function holds Sum s = lim (Partial_Sums s);

for s being ext-real-valued Function holds Sum s = lim (Partial_Sums s);

theorem Th16: :: MESFUNC9:16

for seq being ExtREAL_sequence st seq is V115() holds

( Partial_Sums seq is V115() & Partial_Sums seq is non-decreasing )

( Partial_Sums seq is V115() & Partial_Sums seq is non-decreasing )

proof end;

theorem :: MESFUNC9:17

for seq being ExtREAL_sequence st ( for n being Nat holds 0 < seq . n ) holds

for m being Nat holds 0 < (Partial_Sums seq) . m

for m being Nat holds 0 < (Partial_Sums seq) . m

proof end;

theorem Th18: :: MESFUNC9:18

for X being non empty set

for F, G being Functional_Sequence of X,ExtREAL

for D being set st F is with_the_same_dom & ( for n being Nat holds G . n = (F . n) | D ) holds

G is with_the_same_dom

for F, G being Functional_Sequence of X,ExtREAL

for D being set st F is with_the_same_dom & ( for n being Nat holds G . n = (F . n) | D ) holds

G is with_the_same_dom

proof end;

theorem Th19: :: MESFUNC9:19

for X being non empty set

for F, G being Functional_Sequence of X,ExtREAL

for D being set st D c= dom (F . 0) & ( for n being Nat holds G . n = (F . n) | D ) & ( for x being Element of X st x in D holds

F # x is convergent ) holds

(lim F) | D = lim G

for F, G being Functional_Sequence of X,ExtREAL

for D being set st D c= dom (F . 0) & ( for n being Nat holds G . n = (F . n) | D ) & ( for x being Element of X st x in D holds

F # x is convergent ) holds

(lim F) | D = lim G

proof end;

theorem Th20: :: MESFUNC9:20

for X being non empty set

for S being SigmaField of X

for E being Element of S

for F, G being Functional_Sequence of X,ExtREAL

for n being Nat st F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds

( F . m is_measurable_on E & G . m = (F . m) | E ) ) holds

G . n is_measurable_on E

for S being SigmaField of X

for E being Element of S

for F, G being Functional_Sequence of X,ExtREAL

for n being Nat st F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds

( F . m is_measurable_on E & G . m = (F . m) | E ) ) holds

G . n is_measurable_on E

proof end;

theorem Th21: :: MESFUNC9:21

for X being non empty set

for S being SigmaField of X

for E being Element of S

for F, G being Functional_Sequence of X,ExtREAL st E c= dom (F . 0) & G is with_the_same_dom & ( for x being Element of X st x in E holds

F # x is summable ) & ( for n being Nat holds G . n = (F . n) | E ) holds

for x being Element of X st x in E holds

G # x is summable

for S being SigmaField of X

for E being Element of S

for F, G being Functional_Sequence of X,ExtREAL st E c= dom (F . 0) & G is with_the_same_dom & ( for x being Element of X st x in E holds

F # x is summable ) & ( for n being Nat holds G . n = (F . n) | E ) holds

for x being Element of X st x in E holds

G # x is summable

proof end;

definition

let X be non empty set ;

let F be Functional_Sequence of X,ExtREAL;

ex b_{1} being Functional_Sequence of X,ExtREAL st

( b_{1} . 0 = F . 0 & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) + (F . (n + 1)) ) )

for b_{1}, b_{2} being Functional_Sequence of X,ExtREAL st b_{1} . 0 = F . 0 & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) + (F . (n + 1)) ) & b_{2} . 0 = F . 0 & ( for n being Nat holds b_{2} . (n + 1) = (b_{2} . n) + (F . (n + 1)) ) holds

b_{1} = b_{2}

end;
let F be Functional_Sequence of X,ExtREAL;

func Partial_Sums F -> Functional_Sequence of X,ExtREAL means :Def4: :: MESFUNC9:def 4

( it . 0 = F . 0 & ( for n being Nat holds it . (n + 1) = (it . n) + (F . (n + 1)) ) );

existence ( it . 0 = F . 0 & ( for n being Nat holds it . (n + 1) = (it . n) + (F . (n + 1)) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines Partial_Sums MESFUNC9:def 4 :

for X being non empty set

for F, b_{3} being Functional_Sequence of X,ExtREAL holds

( b_{3} = Partial_Sums F iff ( b_{3} . 0 = F . 0 & ( for n being Nat holds b_{3} . (n + 1) = (b_{3} . n) + (F . (n + 1)) ) ) );

for X being non empty set

for F, b

( b

:: deftheorem defines additive MESFUNC9:def 5 :

for X being set

for F being Functional_Sequence of X,ExtREAL holds

( F is additive iff for n, m being Nat st n <> m holds

for x being set holds

( not x in (dom (F . n)) /\ (dom (F . m)) or (F . n) . x <> +infty or (F . m) . x <> -infty ) );

for X being set

for F being Functional_Sequence of X,ExtREAL holds

( F is additive iff for n, m being Nat st n <> m holds

for x being set holds

( not x in (dom (F . n)) /\ (dom (F . m)) or (F . n) . x <> +infty or (F . m) . x <> -infty ) );

Lm1: for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for n, m being Nat

for z being set st z in dom ((Partial_Sums F) . n) & m <= n holds

z in dom ((Partial_Sums F) . m)

proof end;

theorem Th22: :: MESFUNC9:22

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for n, m being Nat

for z being set st z in dom ((Partial_Sums F) . n) & m <= n holds

( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )

for F being Functional_Sequence of X,ExtREAL

for n, m being Nat

for z being set st z in dom ((Partial_Sums F) . n) & m <= n holds

( z in dom ((Partial_Sums F) . m) & z in dom (F . m) )

proof end;

theorem Th23: :: MESFUNC9:23

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for n being Nat

for z being set st z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z = +infty holds

ex m being Nat st

( m <= n & (F . m) . z = +infty )

for F being Functional_Sequence of X,ExtREAL

for n being Nat

for z being set st z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z = +infty holds

ex m being Nat st

( m <= n & (F . m) . z = +infty )

proof end;

theorem :: MESFUNC9:24

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for n, m being Nat

for z being set st F is additive & z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z = +infty & m <= n holds

(F . m) . z <> -infty

for F being Functional_Sequence of X,ExtREAL

for n, m being Nat

for z being set st F is additive & z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z = +infty & m <= n holds

(F . m) . z <> -infty

proof end;

theorem Th25: :: MESFUNC9:25

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for n being Nat

for z being set st z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z = -infty holds

ex m being Nat st

( m <= n & (F . m) . z = -infty )

for F being Functional_Sequence of X,ExtREAL

for n being Nat

for z being set st z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z = -infty holds

ex m being Nat st

( m <= n & (F . m) . z = -infty )

proof end;

theorem :: MESFUNC9:26

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for n, m being Nat

for z being set st F is additive & z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z = -infty & m <= n holds

(F . m) . z <> +infty

for F being Functional_Sequence of X,ExtREAL

for n, m being Nat

for z being set st F is additive & z in dom ((Partial_Sums F) . n) & ((Partial_Sums F) . n) . z = -infty & m <= n holds

(F . m) . z <> +infty

proof end;

theorem Th27: :: MESFUNC9:27

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for n being Nat st F is additive holds

( (((Partial_Sums F) . n) " {-infty}) /\ ((F . (n + 1)) " {+infty}) = {} & (((Partial_Sums F) . n) " {+infty}) /\ ((F . (n + 1)) " {-infty}) = {} )

for F being Functional_Sequence of X,ExtREAL

for n being Nat st F is additive holds

( (((Partial_Sums F) . n) " {-infty}) /\ ((F . (n + 1)) " {+infty}) = {} & (((Partial_Sums F) . n) " {+infty}) /\ ((F . (n + 1)) " {-infty}) = {} )

proof end;

theorem Th28: :: MESFUNC9:28

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for n being Nat st F is additive holds

dom ((Partial_Sums F) . n) = meet { (dom (F . k)) where k is Element of NAT : k <= n }

for F being Functional_Sequence of X,ExtREAL

for n being Nat st F is additive holds

dom ((Partial_Sums F) . n) = meet { (dom (F . k)) where k is Element of NAT : k <= n }

proof end;

theorem Th29: :: MESFUNC9:29

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for n being Nat st F is additive & F is with_the_same_dom holds

dom ((Partial_Sums F) . n) = dom (F . 0)

for F being Functional_Sequence of X,ExtREAL

for n being Nat st F is additive & F is with_the_same_dom holds

dom ((Partial_Sums F) . n) = dom (F . 0)

proof end;

theorem Th30: :: MESFUNC9:30

for X being non empty set

for F being Functional_Sequence of X,ExtREAL st ( for n being Nat holds F . n is nonnegative ) holds

F is additive by SUPINF_2:51;

for F being Functional_Sequence of X,ExtREAL st ( for n being Nat holds F . n is nonnegative ) holds

F is additive by SUPINF_2:51;

theorem Th31: :: MESFUNC9:31

for X being non empty set

for F, G being Functional_Sequence of X,ExtREAL

for D being set st F is additive & ( for n being Nat holds G . n = (F . n) | D ) holds

G is additive

for F, G being Functional_Sequence of X,ExtREAL

for D being set st F is additive & ( for n being Nat holds G . n = (F . n) | D ) holds

G is additive

proof end;

theorem Th32: :: MESFUNC9:32

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for n being Nat

for x being Element of X

for D being set st F is additive & F is with_the_same_dom & D c= dom (F . 0) & x in D holds

(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n

for F being Functional_Sequence of X,ExtREAL

for n being Nat

for x being Element of X

for D being set st F is additive & F is with_the_same_dom & D c= dom (F . 0) & x in D holds

(Partial_Sums (F # x)) . n = ((Partial_Sums F) # x) . n

proof end;

theorem Th33: :: MESFUNC9:33

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for x being Element of X

for D being set st F is additive & F is with_the_same_dom & D c= dom (F . 0) & x in D holds

( ( Partial_Sums (F # x) is convergent_to_finite_number implies (Partial_Sums F) # x is convergent_to_finite_number ) & ( (Partial_Sums F) # x is convergent_to_finite_number implies Partial_Sums (F # x) is convergent_to_finite_number ) & ( Partial_Sums (F # x) is convergent_to_+infty implies (Partial_Sums F) # x is convergent_to_+infty ) & ( (Partial_Sums F) # x is convergent_to_+infty implies Partial_Sums (F # x) is convergent_to_+infty ) & ( Partial_Sums (F # x) is convergent_to_-infty implies (Partial_Sums F) # x is convergent_to_-infty ) & ( (Partial_Sums F) # x is convergent_to_-infty implies Partial_Sums (F # x) is convergent_to_-infty ) & ( Partial_Sums (F # x) is convergent implies (Partial_Sums F) # x is convergent ) & ( (Partial_Sums F) # x is convergent implies Partial_Sums (F # x) is convergent ) )

for F being Functional_Sequence of X,ExtREAL

for x being Element of X

for D being set st F is additive & F is with_the_same_dom & D c= dom (F . 0) & x in D holds

( ( Partial_Sums (F # x) is convergent_to_finite_number implies (Partial_Sums F) # x is convergent_to_finite_number ) & ( (Partial_Sums F) # x is convergent_to_finite_number implies Partial_Sums (F # x) is convergent_to_finite_number ) & ( Partial_Sums (F # x) is convergent_to_+infty implies (Partial_Sums F) # x is convergent_to_+infty ) & ( (Partial_Sums F) # x is convergent_to_+infty implies Partial_Sums (F # x) is convergent_to_+infty ) & ( Partial_Sums (F # x) is convergent_to_-infty implies (Partial_Sums F) # x is convergent_to_-infty ) & ( (Partial_Sums F) # x is convergent_to_-infty implies Partial_Sums (F # x) is convergent_to_-infty ) & ( Partial_Sums (F # x) is convergent implies (Partial_Sums F) # x is convergent ) & ( (Partial_Sums F) # x is convergent implies Partial_Sums (F # x) is convergent ) )

proof end;

theorem Th34: :: MESFUNC9:34

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for f being PartFunc of X,ExtREAL

for x being Element of X st F is additive & 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) holds

f . x = lim ((Partial_Sums F) # x)

for F being Functional_Sequence of X,ExtREAL

for f being PartFunc of X,ExtREAL

for x being Element of X st F is additive & 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) holds

f . x = lim ((Partial_Sums F) # x)

proof end;

theorem Th35: :: MESFUNC9:35

for X being non empty set

for S being SigmaField of X

for F being Functional_Sequence of X,ExtREAL

for n being Nat st ( for m being Nat holds F . m is_simple_func_in S ) holds

( F is additive & (Partial_Sums F) . n is_simple_func_in S )

for S being SigmaField of X

for F being Functional_Sequence of X,ExtREAL

for n being Nat st ( for m being Nat holds F . m is_simple_func_in S ) holds

( F is additive & (Partial_Sums F) . n is_simple_func_in S )

proof end;

theorem Th36: :: MESFUNC9:36

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for n being Nat st ( for m being Nat holds F . m is nonnegative ) holds

(Partial_Sums F) . n is nonnegative

for F being Functional_Sequence of X,ExtREAL

for n being Nat st ( for m being Nat holds F . m is nonnegative ) holds

(Partial_Sums F) . n is nonnegative

proof end;

theorem Th37: :: MESFUNC9:37

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for n, m being Nat

for x being Element of X st F is with_the_same_dom & x in dom (F . 0) & ( for k being Nat holds F . k is nonnegative ) & n <= m holds

((Partial_Sums F) . n) . x <= ((Partial_Sums F) . m) . x

for F being Functional_Sequence of X,ExtREAL

for n, m being Nat

for x being Element of X st F is with_the_same_dom & x in dom (F . 0) & ( for k being Nat holds F . k is nonnegative ) & n <= m holds

((Partial_Sums F) . n) . x <= ((Partial_Sums F) . m) . x

proof end;

theorem Th38: :: MESFUNC9:38

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for x being Element of X st F is with_the_same_dom & x in dom (F . 0) & ( for m being Nat holds F . m is nonnegative ) holds

( (Partial_Sums F) # x is non-decreasing & (Partial_Sums F) # x is convergent )

for F being Functional_Sequence of X,ExtREAL

for x being Element of X st F is with_the_same_dom & x in dom (F . 0) & ( for m being Nat holds F . m is nonnegative ) holds

( (Partial_Sums F) # x is non-decreasing & (Partial_Sums F) # x is convergent )

proof end;

theorem Th39: :: MESFUNC9:39

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for n being Nat st ( for m being Nat holds F . m is V123() ) holds

(Partial_Sums F) . n is V123()

for F being Functional_Sequence of X,ExtREAL

for n being Nat st ( for m being Nat holds F . m is V123() ) holds

(Partial_Sums F) . n is V123()

proof end;

theorem :: MESFUNC9:40

for X being non empty set

for F being Functional_Sequence of X,ExtREAL

for n being Nat st ( for m being Nat holds F . m is V124() ) holds

(Partial_Sums F) . n is V124()

for F being Functional_Sequence of X,ExtREAL

for n being Nat st ( for m being Nat holds F . m is V124() ) holds

(Partial_Sums F) . n is V124()

proof end;

theorem Th41: :: MESFUNC9:41

for X being non empty set

for S being SigmaField of X

for E being Element of S

for F being Functional_Sequence of X,ExtREAL

for m being Nat st ( for n being Nat holds

( F . n is_measurable_on E & F . n is V123() ) ) holds

(Partial_Sums F) . m is_measurable_on E

for S being SigmaField of X

for E being Element of S

for F being Functional_Sequence of X,ExtREAL

for m being Nat st ( for n being Nat holds

( F . n is_measurable_on E & F . n is V123() ) ) holds

(Partial_Sums F) . m is_measurable_on E

proof end;

theorem Th42: :: MESFUNC9:42

for X being non empty set

for F, G being Functional_Sequence of X,ExtREAL

for n being Nat

for x being Element of X st F is additive & F is with_the_same_dom & G is additive & G is with_the_same_dom & x in (dom (F . 0)) /\ (dom (G . 0)) & ( for k being Nat

for y being Element of X st y in (dom (F . 0)) /\ (dom (G . 0)) holds

(F . k) . y <= (G . k) . y ) holds

((Partial_Sums F) . n) . x <= ((Partial_Sums G) . n) . x

for F, G being Functional_Sequence of X,ExtREAL

for n being Nat

for x being Element of X st F is additive & F is with_the_same_dom & G is additive & G is with_the_same_dom & x in (dom (F . 0)) /\ (dom (G . 0)) & ( for k being Nat

for y being Element of X st y in (dom (F . 0)) /\ (dom (G . 0)) holds

(F . k) . y <= (G . k) . y ) holds

((Partial_Sums F) . n) . x <= ((Partial_Sums G) . n) . x

proof end;

theorem Th43: :: MESFUNC9:43

for X being non empty set

for F being Functional_Sequence of X,ExtREAL st F is additive & F is with_the_same_dom holds

Partial_Sums F is with_the_same_dom

for F being Functional_Sequence of X,ExtREAL st F is additive & F is with_the_same_dom holds

Partial_Sums F is with_the_same_dom

proof end;

theorem Th44: :: MESFUNC9:44

for X being non empty set

for S being SigmaField of X

for E being Element of S

for F being Functional_Sequence of X,ExtREAL st dom (F . 0) = E & F is additive & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is_measurable_on E ) & ( for x being Element of X st x in E holds

F # x is summable ) holds

lim (Partial_Sums F) is_measurable_on E

for S being SigmaField of X

for E being Element of S

for F being Functional_Sequence of X,ExtREAL st dom (F . 0) = E & F is additive & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is_measurable_on E ) & ( for x being Element of X st x in E holds

F # x is summable ) holds

lim (Partial_Sums F) is_measurable_on E

proof end;

theorem :: MESFUNC9:45

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL st ( for n being Nat holds F . n is_integrable_on M ) holds

for m being Nat holds (Partial_Sums F) . m is_integrable_on M

for S being SigmaField of X

for M being sigma_Measure of S

for F being Functional_Sequence of X,ExtREAL st ( for n being Nat holds F . n is_integrable_on M ) holds

for m being Nat holds (Partial_Sums F) . m is_integrable_on M

proof end;

theorem Th46: :: MESFUNC9:46

for X being 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

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

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

proof end;

Lm2: for X being 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

for f being PartFunc of X,ExtREAL st E c= dom f & f is_measurable_on E & E = {} & ( for n being Nat holds F . n is_simple_func_in S ) holds

ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I )

proof end;

Lm3: for X being 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

for f being PartFunc of X,ExtREAL st E c= dom f & f is nonnegative & f is_measurable_on E & F is additive & E common_on_dom F & ( for n being Nat holds

( F . n is_simple_func_in S & F . n is nonnegative ) ) & ( for x being Element of X st x in E holds

( F # x is summable & f . x = Sum (F # x) ) ) holds

ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I )

proof end;

theorem :: MESFUNC9:47

for X being 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

for f being PartFunc of X,ExtREAL st E c= dom f & f is nonnegative & f is_measurable_on E & F is additive & ( for n being Nat holds

( F . n is_simple_func_in S & F . n is nonnegative & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds

( F # x is summable & f . x = Sum (F # x) ) ) holds

ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I )

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 f being PartFunc of X,ExtREAL st E c= dom f & f is nonnegative & f is_measurable_on E & F is additive & ( for n being Nat holds

( F . n is_simple_func_in S & F . n is nonnegative & E c= dom (F . n) ) ) & ( for x being Element of X st x in E holds

( F # x is summable & f . x = Sum (F # x) ) ) holds

ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,((F . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I )

proof end;

theorem :: MESFUNC9:48

for X being 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 PartFunc of X,ExtREAL st E c= dom f & f is nonnegative & f is_measurable_on E holds

ex g being Functional_Sequence of X,ExtREAL st

( g is additive & ( for n being Nat holds

( g . n is_simple_func_in S & g . n is nonnegative & g . n is_measurable_on E ) ) & ( for x being Element of X st x in E holds

( g # x is summable & f . x = Sum (g # x) ) ) & ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,((g . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I ) )

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f being PartFunc of X,ExtREAL st E c= dom f & f is nonnegative & f is_measurable_on E holds

ex g being Functional_Sequence of X,ExtREAL st

( g is additive & ( for n being Nat holds

( g . n is_simple_func_in S & g . n is nonnegative & g . n is_measurable_on E ) ) & ( for x being Element of X st x in E holds

( g # x is summable & f . x = Sum (g # x) ) ) & ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,((g . n) | E)) ) & I is summable & Integral (M,(f | E)) = Sum I ) )

proof end;

registration

let X be non empty set ;

ex b_{1} being Functional_Sequence of X,ExtREAL st

( b_{1} is additive & b_{1} is with_the_same_dom )

end;
cluster Relation-like NAT -defined PFuncs (X,ExtREAL) -valued non empty Function-like total quasi_total with_the_same_dom additive for Element of bool [:NAT,(PFuncs (X,ExtREAL)):];

existence ex b

( b

proof end;

definition

let C, D, X be non empty set ;

let F be Function of [:C,D:],(PFuncs (X,ExtREAL));

let c be Element of C;

let d be Element of D;

:: original: .

redefine func F . (c,d) -> PartFunc of X,ExtREAL;

correctness

coherence

F . (c,d) is PartFunc of X,ExtREAL;

end;
let F be Function of [:C,D:],(PFuncs (X,ExtREAL));

let c be Element of C;

let d be Element of D;

:: original: .

redefine func F . (c,d) -> PartFunc of X,ExtREAL;

correctness

coherence

F . (c,d) is PartFunc of X,ExtREAL;

proof end;

definition

let C, D, X be non empty set ;

let F be Function of [:C,D:],X;

let c be Element of C;

ex b_{1} being Function of D,X st

for d being Element of D holds b_{1} . d = F . (c,d)

for b_{1}, b_{2} being Function of D,X st ( for d being Element of D holds b_{1} . d = F . (c,d) ) & ( for d being Element of D holds b_{2} . d = F . (c,d) ) holds

b_{1} = b_{2}

end;
let F be Function of [:C,D:],X;

let c be Element of C;

func ProjMap1 (F,c) -> Function of D,X means :: MESFUNC9:def 6

for d being Element of D holds it . d = F . (c,d);

existence for d being Element of D holds it . d = F . (c,d);

ex b

for d being Element of D holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines ProjMap1 MESFUNC9:def 6 :

for C, D, X being non empty set

for F being Function of [:C,D:],X

for c being Element of C

for b_{6} being Function of D,X holds

( b_{6} = ProjMap1 (F,c) iff for d being Element of D holds b_{6} . d = F . (c,d) );

for C, D, X being non empty set

for F being Function of [:C,D:],X

for c being Element of C

for b

( b

definition

let C, D, X be non empty set ;

let F be Function of [:C,D:],X;

let d be Element of D;

ex b_{1} being Function of C,X st

for c being Element of C holds b_{1} . c = F . (c,d)

for b_{1}, b_{2} being Function of C,X st ( for c being Element of C holds b_{1} . c = F . (c,d) ) & ( for c being Element of C holds b_{2} . c = F . (c,d) ) holds

b_{1} = b_{2}

end;
let F be Function of [:C,D:],X;

let d be Element of D;

func ProjMap2 (F,d) -> Function of C,X means :: MESFUNC9:def 7

for c being Element of C holds it . c = F . (c,d);

existence for c being Element of C holds it . c = F . (c,d);

ex b

for c being Element of C holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines ProjMap2 MESFUNC9:def 7 :

for C, D, X being non empty set

for F being Function of [:C,D:],X

for d being Element of D

for b_{6} being Function of C,X holds

( b_{6} = ProjMap2 (F,d) iff for c being Element of C holds b_{6} . c = F . (c,d) );

for C, D, X being non empty set

for F being Function of [:C,D:],X

for d being Element of D

for b

( b

definition

let X, Y be set ;

let F be Function of [:NAT,NAT:],(PFuncs (X,Y));

let n be Nat;

ex b_{1} being Functional_Sequence of X,Y st

for m being Nat holds b_{1} . m = F . (n,m)

for b_{1}, b_{2} being Functional_Sequence of X,Y st ( for m being Nat holds b_{1} . m = F . (n,m) ) & ( for m being Nat holds b_{2} . m = F . (n,m) ) holds

b_{1} = b_{2}

ex b_{1} being Functional_Sequence of X,Y st

for m being Nat holds b_{1} . m = F . (m,n)

for b_{1}, b_{2} being Functional_Sequence of X,Y st ( for m being Nat holds b_{1} . m = F . (m,n) ) & ( for m being Nat holds b_{2} . m = F . (m,n) ) holds

b_{1} = b_{2}

end;
let F be Function of [:NAT,NAT:],(PFuncs (X,Y));

let n be Nat;

func ProjMap1 (F,n) -> Functional_Sequence of X,Y means :Def8: :: MESFUNC9:def 8

for m being Nat holds it . m = F . (n,m);

existence for m being Nat holds it . m = F . (n,m);

ex b

for m being Nat holds b

proof end;

uniqueness for b

b

proof end;

func ProjMap2 (F,n) -> Functional_Sequence of X,Y means :Def9: :: MESFUNC9:def 9

for m being Nat holds it . m = F . (m,n);

existence for m being Nat holds it . m = F . (m,n);

ex b

for m being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines ProjMap1 MESFUNC9:def 8 :

for X, Y being set

for F being Function of [:NAT,NAT:],(PFuncs (X,Y))

for n being Nat

for b_{5} being Functional_Sequence of X,Y holds

( b_{5} = ProjMap1 (F,n) iff for m being Nat holds b_{5} . m = F . (n,m) );

for X, Y being set

for F being Function of [:NAT,NAT:],(PFuncs (X,Y))

for n being Nat

for b

( b

:: deftheorem Def9 defines ProjMap2 MESFUNC9:def 9 :

for X, Y being set

for F being Function of [:NAT,NAT:],(PFuncs (X,Y))

for n being Nat

for b_{5} being Functional_Sequence of X,Y holds

( b_{5} = ProjMap2 (F,n) iff for m being Nat holds b_{5} . m = F . (m,n) );

for X, Y being set

for F being Function of [:NAT,NAT:],(PFuncs (X,Y))

for n being Nat

for b

( b

definition

let X be non empty set ;

let F be sequence of (Funcs (NAT,(PFuncs (X,ExtREAL))));

let n be Nat;

:: original: .

redefine func F . n -> Functional_Sequence of X,ExtREAL;

correctness

coherence

F . n is Functional_Sequence of X,ExtREAL;

end;
let F be sequence of (Funcs (NAT,(PFuncs (X,ExtREAL))));

let n be Nat;

:: original: .

redefine func F . n -> Functional_Sequence of X,ExtREAL;

correctness

coherence

F . n is Functional_Sequence of X,ExtREAL;

proof end;

theorem Th49: :: MESFUNC9:49

for X being non empty set

for S being SigmaField of X

for E being Element of S

for F being Functional_Sequence of X,ExtREAL st E = dom (F . 0) & F is with_the_same_dom & ( for n being Nat holds

( F . n is nonnegative & F . n is_measurable_on E ) ) holds

ex FF being sequence of (Funcs (NAT,(PFuncs (X,ExtREAL)))) st

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 ) ) )

for S being SigmaField of X

for E being Element of S

for F being Functional_Sequence of X,ExtREAL st E = dom (F . 0) & F is with_the_same_dom & ( for n being Nat holds

( F . n is nonnegative & F . n is_measurable_on E ) ) holds

ex FF being sequence of (Funcs (NAT,(PFuncs (X,ExtREAL)))) st

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 ) ) )

proof end;

theorem Th50: :: MESFUNC9:50

for X being 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_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 )

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 )

proof end;

Lm4: for X being 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_measurable_on E ) ) & ( 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 )

proof end;

theorem Th51: :: MESFUNC9:51

for X being 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 c= dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds

( F . n is nonnegative & F . n is_measurable_on E ) ) & ( 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 )

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 c= dom (F . 0) & F is additive & F is with_the_same_dom & ( for n being Nat holds

( F . n is nonnegative & F . n is_measurable_on E ) ) & ( 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 )

proof end;

theorem :: MESFUNC9:52

for X being 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 . 0 is nonnegative & F is with_the_same_dom & ( for n being Nat holds F . n is_measurable_on E ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in E holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in E holds

F # x is convergent ) holds

ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I )

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 . 0 is nonnegative & F is with_the_same_dom & ( for n being Nat holds F . n is_measurable_on E ) & ( for n, m being Nat st n <= m holds

for x being Element of X st x in E holds

(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in E holds

F # x is convergent ) holds

ex I being ExtREAL_sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & I is convergent & Integral (M,(lim F)) = lim I )

proof end;

:: Lebesgue's Monotone Convergence Theorem