:: by Keiko Narita , Noboru Endou and Yasunari Shidama

::

:: Received March 17, 2009

:: Copyright (c) 2009-2021 Association of Mizar Users

definition

let X, Y be set ;

let F be Functional_Sequence of X,Y;

let D be set ;

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

for n being Nat holds b_{1} . n = (F . n) | D

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

b_{1} = b_{2}

end;
let F be Functional_Sequence of X,Y;

let D be set ;

func F || D -> Functional_Sequence of X,Y means :Def1: :: MESFUN9C:def 1

for n being Nat holds it . n = (F . n) | D;

existence for n being Nat holds it . n = (F . n) | D;

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines || MESFUN9C:def 1 :

for X, Y being set

for F being Functional_Sequence of X,Y

for D being set

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

( b_{5} = F || D iff for n being Nat holds b_{5} . n = (F . n) | D );

for X, Y being set

for F being Functional_Sequence of X,Y

for D being set

for b

( b

theorem Th1: :: MESFUN9C:1

for X being non empty set

for F being Functional_Sequence of X,REAL

for x being Element of X

for D being set st x in D & F # x is convergent holds

(F || D) # x is convergent

for F being Functional_Sequence of X,REAL

for x being Element of X

for D being set st x in D & F # x is convergent holds

(F || D) # x is convergent

proof end;

theorem Th2: :: MESFUN9C:2

for X, Y, D being set

for F being Functional_Sequence of X,Y st F is with_the_same_dom holds

F || D is with_the_same_dom

for F being Functional_Sequence of X,Y st F is with_the_same_dom holds

F || D is with_the_same_dom

proof end;

theorem Th3: :: MESFUN9C:3

for X being non empty set

for F being Functional_Sequence of X,REAL

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

F # x is convergent ) holds

(lim F) | D = lim (F || D)

for F being Functional_Sequence of X,REAL

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

F # x is convergent ) holds

(lim F) | D = lim (F || D)

proof end;

theorem Th4: :: MESFUN9C:4

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,REAL

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

(F || E) . n is E -measurable

for S being SigmaField of X

for E being Element of S

for F being Functional_Sequence of X,REAL

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

(F || E) . n is E -measurable

proof end;

theorem Th6: :: MESFUN9C:6

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,REAL st ( for x being Element of X st x in E holds

F # x is summable ) holds

for x being Element of X st x in E holds

(F || E) # x is summable

for S being SigmaField of X

for E being Element of S

for F being Functional_Sequence of X,REAL st ( for x being Element of X st x in E holds

F # x is summable ) holds

for x being Element of X st x in E holds

(F || E) # x is summable

proof end;

definition

let X be non empty set ;

let F be Functional_Sequence of X,REAL;

ex b_{1} being Functional_Sequence of X,REAL 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,REAL 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,REAL;

func Partial_Sums F -> Functional_Sequence of X,REAL means :Def2: :: MESFUN9C:def 2

( 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 Def2 defines Partial_Sums MESFUN9C:def 2 :

for X being non empty set

for F, b_{3} being Functional_Sequence of X,REAL 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

theorem Th7: :: MESFUN9C:7

for X being non empty set

for F being Functional_Sequence of X,REAL holds Partial_Sums (R_EAL F) = R_EAL (Partial_Sums F)

for F being Functional_Sequence of X,REAL holds Partial_Sums (R_EAL F) = R_EAL (Partial_Sums F)

proof end;

theorem Th8: :: MESFUN9C:8

for X being non empty set

for F being Functional_Sequence of X,REAL

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,REAL

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 Th10: :: MESFUN9C:10

for X being non empty set

for F being Functional_Sequence of X,REAL

for n being Nat 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,REAL

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

proof end;

theorem Th11: :: MESFUN9C:11

for X being non empty set

for F being Functional_Sequence of X,REAL

for n being Nat st F is with_the_same_dom holds

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

for F being Functional_Sequence of X,REAL

for n being Nat st F is with_the_same_dom holds

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

proof end;

theorem Th12: :: MESFUN9C:12

for X being non empty set

for F being Functional_Sequence of X,REAL

for n being Nat

for x being Element of X

for D being set st 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,REAL

for n being Nat

for x being Element of X

for D being set st 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 Th13: :: MESFUN9C:13

for X being non empty set

for F being Functional_Sequence of X,REAL

for x being Element of X

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

( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )

for F being Functional_Sequence of X,REAL

for x being Element of X

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

( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )

proof end;

theorem Th14: :: MESFUN9C:14

for X being non empty set

for F being Functional_Sequence of X,REAL

for f being PartFunc of X,REAL

for x being Element of X st F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & f . x = Sum (F # x) holds

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

for F being Functional_Sequence of X,REAL

for f being PartFunc of X,REAL

for x being Element of X st F is with_the_same_dom & dom f c= dom (F . 0) & x in dom f & f . x = Sum (F # x) holds

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

proof end;

theorem Th15: :: MESFUN9C:15

for X being non empty set

for S being SigmaField of X

for F being Functional_Sequence of X,REAL

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

(Partial_Sums F) . n is_simple_func_in S

for S being SigmaField of X

for F being Functional_Sequence of X,REAL

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

(Partial_Sums F) . n is_simple_func_in S

proof end;

theorem Th16: :: MESFUN9C:16

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,REAL

for m being Nat st ( for n being Nat holds F . n is E -measurable ) holds

(Partial_Sums F) . m is E -measurable

for S being SigmaField of X

for E being Element of S

for F being Functional_Sequence of X,REAL

for m being Nat st ( for n being Nat holds F . n is E -measurable ) holds

(Partial_Sums F) . m is E -measurable

proof end;

theorem Th17: :: MESFUN9C:17

for X being non empty set

for F being Functional_Sequence of X,REAL st F is with_the_same_dom holds

Partial_Sums F is with_the_same_dom

for F being Functional_Sequence of X,REAL st F is with_the_same_dom holds

Partial_Sums F is with_the_same_dom

proof end;

theorem Th18: :: MESFUN9C:18

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,REAL st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is E -measurable ) & ( for x being Element of X st x in E holds

F # x is summable ) holds

lim (Partial_Sums F) is E -measurable

for S being SigmaField of X

for E being Element of S

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

F # x is summable ) holds

lim (Partial_Sums F) is E -measurable

proof end;

theorem Th19: :: MESFUN9C:19

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,REAL 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,REAL 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 Th20: :: MESFUN9C:20

for X being non empty set

for f being PartFunc of X,COMPLEX

for A being set holds

( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) )

for f being PartFunc of X,COMPLEX

for A being set holds

( (Re f) | A = Re (f | A) & (Im f) | A = Im (f | A) )

proof end;

Lm1: for X being non empty set

for D being set

for F being Functional_Sequence of X,COMPLEX

for n being Nat holds

( (Re (F || D)) . n = ((Re F) . n) | D & (Im (F || D)) . n = ((Im F) . n) | D )

proof end;

theorem Th21: :: MESFUN9C:21

for X being non empty set

for D being set

for F being Functional_Sequence of X,COMPLEX holds Re (F || D) = (Re F) || D

for D being set

for F being Functional_Sequence of X,COMPLEX holds Re (F || D) = (Re F) || D

proof end;

theorem Th22: :: MESFUN9C:22

for X being non empty set

for D being set

for F being Functional_Sequence of X,COMPLEX holds Im (F || D) = (Im F) || D

for D being set

for F being Functional_Sequence of X,COMPLEX holds Im (F || D) = (Im F) || D

proof end;

theorem Th23: :: MESFUN9C:23

for X being non empty set

for x being Element of X

for D being set

for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D c= dom (F . 0) & x in D & F # x is convergent holds

(F || D) # x is convergent

for x being Element of X

for D being set

for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D c= dom (F . 0) & x in D & F # x is convergent holds

(F || D) # x is convergent

proof end;

theorem Th24: :: MESFUN9C:24

for X being non empty set

for F being Functional_Sequence of X,COMPLEX holds

( F is with_the_same_dom iff Re F is with_the_same_dom )

for F being Functional_Sequence of X,COMPLEX holds

( F is with_the_same_dom iff Re F is with_the_same_dom )

proof end;

theorem Th25: :: MESFUN9C:25

for X being non empty set

for F being Functional_Sequence of X,COMPLEX holds

( Re F is with_the_same_dom iff Im F is with_the_same_dom )

for F being Functional_Sequence of X,COMPLEX holds

( Re F is with_the_same_dom iff Im F is with_the_same_dom )

proof end;

theorem :: MESFUN9C:26

for X being non empty set

for D being set

for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D = dom (F . 0) & ( for x being Element of X st x in D holds

F # x is convergent ) holds

(lim F) | D = lim (F || D)

for D being set

for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D = dom (F . 0) & ( for x being Element of X st x in D holds

F # x is convergent ) holds

(lim F) | D = lim (F || D)

proof end;

theorem :: MESFUN9C:27

for X being non empty set

for S being SigmaField of X

for E being Element of S

for n being Nat

for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds F . m is E -measurable ) holds

(F || E) . n is E -measurable

for S being SigmaField of X

for E being Element of S

for n being Nat

for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & E c= dom (F . 0) & ( for m being Nat holds F . m is E -measurable ) holds

(F || E) . n is E -measurable

proof end;

theorem :: MESFUN9C:28

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,COMPLEX st E c= dom (F . 0) & F is with_the_same_dom & ( for x being Element of X st x in E holds

F # x is summable ) holds

for x being Element of X st x in E holds

(F || E) # x is summable

for S being SigmaField of X

for E being Element of S

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

F # x is summable ) holds

for x being Element of X st x in E holds

(F || E) # x is summable

proof end;

definition

let X be non empty set ;

let F be Functional_Sequence of X,COMPLEX;

ex b_{1} being Functional_Sequence of X,COMPLEX 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,COMPLEX 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,COMPLEX;

func Partial_Sums F -> Functional_Sequence of X,COMPLEX means :Def3: :: MESFUN9C:def 3

( 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 Def3 defines Partial_Sums MESFUN9C:def 3 :

for X being non empty set

for F, b_{3} being Functional_Sequence of X,COMPLEX 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

theorem Th29: :: MESFUN9C:29

for X being non empty set

for F being Functional_Sequence of X,COMPLEX holds

( Partial_Sums (Re F) = Re (Partial_Sums F) & Partial_Sums (Im F) = Im (Partial_Sums F) )

for F being Functional_Sequence of X,COMPLEX holds

( Partial_Sums (Re F) = Re (Partial_Sums F) & Partial_Sums (Im F) = Im (Partial_Sums F) )

proof end;

theorem :: MESFUN9C:30

for X being non empty set

for n, m being Nat

for z being set

for F being Functional_Sequence of X,COMPLEX st z in dom ((Partial_Sums F) . n) & m <= n holds

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

for n, m being Nat

for z being set

for F being Functional_Sequence of X,COMPLEX 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 :: MESFUN9C:31

for X being non empty set

for n being Nat

for F being Functional_Sequence of X,COMPLEX holds dom ((Partial_Sums F) . n) = meet { (dom (F . k)) where k is Element of NAT : k <= n }

for n being Nat

for F being Functional_Sequence of X,COMPLEX holds dom ((Partial_Sums F) . n) = meet { (dom (F . k)) where k is Element of NAT : k <= n }

proof end;

theorem Th32: :: MESFUN9C:32

for X being non empty set

for n being Nat

for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom holds

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

for n being Nat

for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom holds

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

proof end;

theorem :: MESFUN9C:33

for X being non empty set

for n being Nat

for x being Element of X

for D being set

for F being Functional_Sequence of X,COMPLEX st 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 n being Nat

for x being Element of X

for D being set

for F being Functional_Sequence of X,COMPLEX st 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 Th34: :: MESFUN9C:34

for X being non empty set

for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom holds

Partial_Sums F is with_the_same_dom

for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom holds

Partial_Sums F is with_the_same_dom

proof end;

theorem Th35: :: MESFUN9C:35

for X being non empty set

for x being Element of X

for D being set

for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D c= dom (F . 0) & x in D holds

( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )

for x being Element of X

for D being set

for F being Functional_Sequence of X,COMPLEX st F is with_the_same_dom & D c= dom (F . 0) & x in D holds

( Partial_Sums (F # x) is convergent iff (Partial_Sums F) # x is convergent )

proof end;

theorem :: MESFUN9C:36

for X being non empty set

for x being Element of X

for F being Functional_Sequence of X,COMPLEX

for f being PartFunc of X,COMPLEX st 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 x being Element of X

for F being Functional_Sequence of X,COMPLEX

for f being PartFunc of X,COMPLEX st 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 :: MESFUN9C:37

for X being non empty set

for S being SigmaField of X

for n being Nat

for F being Functional_Sequence of X,COMPLEX st ( for m being Nat holds F . m is_simple_func_in S ) holds

(Partial_Sums F) . n is_simple_func_in S

for S being SigmaField of X

for n being Nat

for F being Functional_Sequence of X,COMPLEX st ( for m being Nat holds F . m is_simple_func_in S ) holds

(Partial_Sums F) . n is_simple_func_in S

proof end;

Lm2: for X being non empty set

for S being SigmaField of X

for E being Element of S

for m being Nat

for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is E -measurable ) holds

( (Re F) . m is E -measurable & (Im F) . m is E -measurable )

proof end;

theorem :: MESFUN9C:38

for X being non empty set

for S being SigmaField of X

for E being Element of S

for m being Nat

for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is E -measurable ) holds

(Partial_Sums F) . m is E -measurable

for S being SigmaField of X

for E being Element of S

for m being Nat

for F being Functional_Sequence of X,COMPLEX st ( for n being Nat holds F . n is E -measurable ) holds

(Partial_Sums F) . m is E -measurable

proof end;

theorem :: MESFUN9C:39

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,COMPLEX st dom (F . 0) = E & F is with_the_same_dom & ( for n being Nat holds (Partial_Sums F) . n is E -measurable ) & ( for x being Element of X st x in E holds

F # x is summable ) holds

lim (Partial_Sums F) is E -measurable

for S being SigmaField of X

for E being Element of S

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

F # x is summable ) holds

lim (Partial_Sums F) is E -measurable

proof end;

theorem :: MESFUN9C:40

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,COMPLEX 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,COMPLEX 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 :: MESFUN9C:41

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for A being Element of S st f is_simple_func_in S holds

f is A -measurable

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for A being Element of S st f is_simple_func_in S holds

f is A -measurable

proof end;

theorem :: MESFUN9C:42

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for A being Element of S st f is_simple_func_in S holds

f | A is_simple_func_in S

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for A being Element of S st f is_simple_func_in S holds

f | A is_simple_func_in S

proof end;

theorem :: MESFUN9C:43

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,COMPLEX st f is_simple_func_in S holds

dom f is Element of S by MESFUNC2:31;

for S being SigmaField of X

for f being PartFunc of X,COMPLEX st f is_simple_func_in S holds

dom f is Element of S by MESFUNC2:31;

theorem :: MESFUN9C:44

for X being non empty set

for S being SigmaField of X

for f, g being PartFunc of X,COMPLEX st f is_simple_func_in S & g is_simple_func_in S holds

f + g is_simple_func_in S

for S being SigmaField of X

for f, g being PartFunc of X,COMPLEX st f is_simple_func_in S & g is_simple_func_in S holds

f + g is_simple_func_in S

proof end;

theorem :: MESFUN9C:45

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for c being Complex st f is_simple_func_in S holds

c (#) f is_simple_func_in S

for S being SigmaField of X

for f being PartFunc of X,COMPLEX

for c being Complex st f is_simple_func_in S holds

c (#) f is_simple_func_in S

proof end;

theorem Th46: :: MESFUN9C: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 with_the_same_dom Functional_Sequence of X,ExtREAL

for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

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

F # x is convergent ) holds

lim F is_integrable_on M

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for F being with_the_same_dom Functional_Sequence of X,ExtREAL

for P being PartFunc of X,ExtREAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

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

F # x is convergent ) holds

lim F is_integrable_on M

proof end;

theorem Th47: :: MESFUN9C: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 with_the_same_dom Functional_Sequence of X,REAL

for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

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

F # x is convergent ) holds

lim F is_integrable_on M

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for F being with_the_same_dom Functional_Sequence of X,REAL

for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

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

F # x is convergent ) holds

lim F is_integrable_on M

proof end;

:: Lebesgue's Convergence theorem

theorem Th48: :: MESFUN9C: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 with_the_same_dom Functional_Sequence of X,REAL

for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Real_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds

F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for F being with_the_same_dom Functional_Sequence of X,REAL

for P being PartFunc of X,REAL st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Real_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds

F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )

proof end;

:: deftheorem defines uniformly_bounded MESFUN9C:def 4 :

for X being set

for F being Functional_Sequence of X,REAL holds

( F is uniformly_bounded iff ex K being Real st

for n being Nat

for x being Element of X st x in dom (F . 0) holds

|.((F . n) . x).| <= K );

for X being set

for F being Functional_Sequence of X,REAL holds

( F is uniformly_bounded iff ex K being Real st

for n being Nat

for x being Element of X st x in dom (F . 0) holds

|.((F . n) . x).| <= K );

:: Lebesgue's Bounded Convergence Theorem

theorem Th49: :: MESFUN9C:49

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 with_the_same_dom Functional_Sequence of X,REAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) holds

( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being ExtREAL_sequence st

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

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for F being with_the_same_dom Functional_Sequence of X,REAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) holds

( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being ExtREAL_sequence st

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

proof end;

:: deftheorem defines is_uniformly_convergent_to MESFUN9C:def 5 :

for X being set

for F being Functional_Sequence of X,REAL

for f being PartFunc of X,REAL holds

( F is_uniformly_convergent_to f iff ( F is with_the_same_dom & dom (F . 0) = dom f & ( for e being Real st e > 0 holds

ex N being Nat st

for n being Nat

for x being Element of X st n >= N & x in dom (F . 0) holds

|.(((F . n) . x) - (f . x)).| < e ) ) );

for X being set

for F being Functional_Sequence of X,REAL

for f being PartFunc of X,REAL holds

( F is_uniformly_convergent_to f iff ( F is with_the_same_dom & dom (F . 0) = dom f & ( for e being Real st e > 0 holds

ex N being Nat st

for n being Nat

for x being Element of X st n >= N & x in dom (F . 0) holds

|.(((F . n) . x) - (f . x)).| < e ) ) );

theorem Th50: :: MESFUN9C: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 with_the_same_dom Functional_Sequence of X,REAL

for f being PartFunc of X,REAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds

( f is_integrable_on M & ex I being ExtREAL_sequence st

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

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for F being with_the_same_dom Functional_Sequence of X,REAL

for f being PartFunc of X,REAL st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds

( f is_integrable_on M & ex I being ExtREAL_sequence st

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

proof end;

theorem Th51: :: MESFUN9C: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 P being PartFunc of X,REAL

for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

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

F # x is convergent ) holds

lim F is_integrable_on M

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for P being PartFunc of X,REAL

for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

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

F # x is convergent ) holds

lim F is_integrable_on M

proof end;

:: Lebesgue's Convergence theorem

theorem :: MESFUN9C: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 P being PartFunc of X,REAL

for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds

F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for P being PartFunc of X,REAL

for F being with_the_same_dom Functional_Sequence of X,COMPLEX st E = dom (F . 0) & E = dom P & ( for n being Nat holds F . n is E -measurable ) & P is_integrable_on M & ( for x being Element of X

for n being Nat st x in E holds

|.(F . n).| . x <= P . x ) holds

ex I being Complex_Sequence st

( ( for n being Nat holds I . n = Integral (M,(F . n)) ) & ( ( for x being Element of X st x in E holds

F # x is convergent ) implies ( I is convergent & lim I = Integral (M,(lim F)) ) ) )

proof end;

:: deftheorem defines uniformly_bounded MESFUN9C:def 6 :

for X being set

for F being Functional_Sequence of X,COMPLEX holds

( F is uniformly_bounded iff ex K being Real st

for n being Nat

for x being Element of X st x in dom (F . 0) holds

|.((F . n) . x).| <= K );

for X being set

for F being Functional_Sequence of X,COMPLEX holds

( F is uniformly_bounded iff ex K being Real st

for n being Nat

for x being Element of X st x in dom (F . 0) holds

|.((F . n) . x).| <= K );

:: Lebesgue's Bounded Convergence Theorem

theorem :: MESFUN9C:53

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 with_the_same_dom Functional_Sequence of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) holds

( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being Complex_Sequence st

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

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for F being with_the_same_dom Functional_Sequence of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is E -measurable ) & F is uniformly_bounded & ( for x being Element of X st x in E holds

F # x is convergent ) holds

( ( for n being Nat holds F . n is_integrable_on M ) & lim F is_integrable_on M & ex I being Complex_Sequence st

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

proof end;

definition
end;

:: deftheorem defines is_uniformly_convergent_to MESFUN9C:def 7 :

for X being set

for F being Functional_Sequence of X,COMPLEX

for f being PartFunc of X,COMPLEX holds

( F is_uniformly_convergent_to f iff ( F is with_the_same_dom & dom (F . 0) = dom f & ( for e being Real st e > 0 holds

ex N being Nat st

for n being Nat

for x being Element of X st n >= N & x in dom (F . 0) holds

|.(((F . n) . x) - (f . x)).| < e ) ) );

for X being set

for F being Functional_Sequence of X,COMPLEX

for f being PartFunc of X,COMPLEX holds

( F is_uniformly_convergent_to f iff ( F is with_the_same_dom & dom (F . 0) = dom f & ( for e being Real st e > 0 holds

ex N being Nat st

for n being Nat

for x being Element of X st n >= N & x in dom (F . 0) holds

|.(((F . n) . x) - (f . x)).| < e ) ) );

theorem :: MESFUN9C:54

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 with_the_same_dom Functional_Sequence of X,COMPLEX

for f being PartFunc of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds

( f is_integrable_on M & ex I being Complex_Sequence st

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

for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for F being with_the_same_dom Functional_Sequence of X,COMPLEX

for f being PartFunc of X,COMPLEX st M . E < +infty & E = dom (F . 0) & ( for n being Nat holds F . n is_integrable_on M ) & F is_uniformly_convergent_to f holds

( f is_integrable_on M & ex I being Complex_Sequence st

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

proof end;