:: MESFUNC9 semantic presentation

theorem M5th22: :: MESFUNC9:1

for X being non empty set
for f, g being PartFunc of X, ExtREAL st f is without+infty & g is without+infty holds
dom (f + g) = (dom f) /\ (dom g)

proof end;

theorem M5th23: :: MESFUNC9:2

for X being non empty set
for f, g being PartFunc of X, ExtREAL st f is without+infty & g is without-infty holds
dom (f - g) = (dom f) /\ (dom g)

proof end;

theorem ADD1a: :: MESFUNC9:3

for X being non empty set
for f, g being PartFunc of X, ExtREAL st f is without-infty & g is without-infty holds
f + g is without-infty

proof end;

theorem ADD1b: :: MESFUNC9:4

for X being non empty set
for f, g being PartFunc of X, ExtREAL st f is without+infty & g is without+infty holds
f + g is without+infty

proof end;

theorem :: MESFUNC9:5

for X being non empty set
for f, g being PartFunc of X, ExtREAL st f is without-infty & g is without+infty holds
f - g is without-infty

proof end;

theorem :: MESFUNC9:6

for X being non empty set
for f, g being PartFunc of X, ExtREAL st f is without+infty & g is without-infty holds
f - g is without+infty

proof end;

theorem LIM: :: MESFUNC9:7

for seq being ExtREAL_sequence holds
( ( seq is convergent_to_finite_number implies ex g being real number st
( lim seq = g & ( for p being real number 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 LIM2a: :: MESFUNC9:8

for seq being ExtREAL_sequence st seq is nonnegative holds
not seq is convergent_to_-infty

proof end;

theorem LIM3: :: MESFUNC9:9

for seq being ExtREAL_sequence
for p being ext-real number st seq is convergent & ( for k being Nat holds seq . k <= p ) holds
lim seq <= p

proof end;

theorem LIM3a: :: MESFUNC9:10

for seq being ExtREAL_sequence
for p being ext-real number st seq is convergent & ( for k being Nat holds p <= seq . k ) holds
p <= lim seq

proof end;

theorem LIM2: :: MESFUNC9:11

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

proof end;

theorem Lm16: :: MESFUNC9:12

for X being non empty set
for G, F 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 Lem13: :: 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

proof end;

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 )

proof end;

theorem Prop3: :: 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)

proof end;

definition

let f be ext-real-valued Function;
let x be set ;
:: original: .
redefine func f . x -> Element of ExtREAL ;
coherence by XXREAL_0:def 1;

end;

definition

let s be ext-real-valued Function;
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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Partial_Sums MESFUNC9:def 1 :

definition

let s be ext-real-valued Function;
attr s is summable means :Def2: :: MESFUNC9:def 2
Partial_Sums s is convergent;

end;

:: deftheorem Def2 defines summable MESFUNC9:def 2 :

definition

let s be ext-real-valued Function;
func Sum s -> R_eal equals :: MESFUNC9:def 3
lim (Partial_Sums s);
correctness ;

end;

:: deftheorem defines Sum MESFUNC9:def 3 :

theorem ADD3a: :: MESFUNC9:16

for seq being ExtREAL_sequence st seq is nonnegative holds
( Partial_Sums seq is nonnegative & 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

proof end;

theorem Lm17: :: 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

proof end;

theorem Lm15: :: 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

proof end;

theorem Prop1: :: 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

proof end;

theorem Prop2: :: 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

proof end;

definition

let X be non empty set ;
let F be Functional_Sequence of X, ExtREAL ;
func Partial_Sums F -> Functional_Sequence of X, ExtREAL means :Def0: :: MESFUNC9:def 4
( it . 0 = F . 0 & ( for n being Nat holds it . (n + 1) = (it . n) + (F . (n + 1)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def0 defines Partial_Sums MESFUNC9:def 4 :

definition

let X be set ;
let F be Functional_Sequence of X, ExtREAL ;
attr F is additive means :Def1a: :: MESFUNC9:def 5
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 );

end;

:: deftheorem Def1a defines additive MESFUNC9:def 5 :

Lem01: 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 Lem02: :: 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) )

proof end;

theorem Lem03: :: 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 )

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

proof end;

theorem Lem05: :: 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 )

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

proof end;

theorem Lem07b: :: 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 }) = {} )

proof end;

theorem Lem07: :: 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 }

proof end;

theorem ADD0: :: 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 )

proof end;

theorem LIM4: :: 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

proof end;

theorem Lem09: :: 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

proof end;

theorem Cor00: :: 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

proof end;

theorem Cor01: :: MESFUNC9:33

proof end;

theorem Cor02: :: 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)

proof end;

theorem Lem10: :: 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 )

proof end;

theorem ADD3C: :: 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

proof end;

theorem ADD3D: :: 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

proof end;

theorem ADD3: :: 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 )

proof end;

theorem ADD1e: :: 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 without-infty ) holds
(Partial_Sums F) . n is without-infty

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 without+infty ) holds
(Partial_Sums F) . n is without+infty

proof end;

theorem ADD1: :: 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 without-infty ) ) holds
(Partial_Sums F) . m is_measurable_on E

proof end;

theorem ADD4: :: 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