:: by Yasunari Shidama and Noboru Endou

::

:: Received September 25, 2004

:: Copyright (c) 2004-2012 Association of Mizar Users

begin

theorem Th1: :: MESFUNC3:1

for n, m being Nat

for a being Function of [:(Seg n),(Seg m):],REAL

for p, q being FinSequence of REAL st dom p = Seg n & ( for i being Nat st i in dom p holds

ex r being FinSequence of REAL st

( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds

r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds

ex s being FinSequence of REAL st

( dom s = Seg n & q . j = Sum s & ( for i being Nat st i in dom s holds

s . i = a . [i,j] ) ) ) holds

Sum p = Sum q

for a being Function of [:(Seg n),(Seg m):],REAL

for p, q being FinSequence of REAL st dom p = Seg n & ( for i being Nat st i in dom p holds

ex r being FinSequence of REAL st

( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds

r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds

ex s being FinSequence of REAL st

( dom s = Seg n & q . j = Sum s & ( for i being Nat st i in dom s holds

s . i = a . [i,j] ) ) ) holds

Sum p = Sum q

proof end;

theorem Th3: :: MESFUNC3:3

for X being non empty set

for S being SigmaField of X

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

ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st

( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

f . x = a . n ) & ( for x being set st x in dom f holds

ex ax being FinSequence of ExtREAL st

( dom ax = dom a & ( for n being Nat st n in dom ax holds

ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) )

for S being SigmaField of X

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

ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st

( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

f . x = a . n ) & ( for x being set st x in dom f holds

ex ax being FinSequence of ExtREAL st

( dom ax = dom a & ( for n being Nat st n in dom ax holds

ax . n = (a . n) * ((chi ((F . n),X)) . x) ) ) ) )

proof end;

theorem Th4: :: MESFUNC3:4

for X being set

for F being FinSequence of X holds

( F is disjoint_valued iff for i, j being Nat st i in dom F & j in dom F & i <> j holds

F . i misses F . j )

for F being FinSequence of X holds

( F is disjoint_valued iff for i, j being Nat st i in dom F & j in dom F & i <> j holds

F . i misses F . j )

proof end;

theorem Th5: :: MESFUNC3:5

for X being non empty set

for A being set

for S being SigmaField of X

for F being Finite_Sep_Sequence of S

for G being FinSequence of S st dom G = dom F & ( for i being Nat st i in dom G holds

G . i = A /\ (F . i) ) holds

G is Finite_Sep_Sequence of S

for A being set

for S being SigmaField of X

for F being Finite_Sep_Sequence of S

for G being FinSequence of S st dom G = dom F & ( for i being Nat st i in dom G holds

G . i = A /\ (F . i) ) holds

G is Finite_Sep_Sequence of S

proof end;

theorem Th6: :: MESFUNC3:6

for X being non empty set

for A being set

for F, G being FinSequence of X st dom G = dom F & ( for i being Nat st i in dom G holds

G . i = A /\ (F . i) ) holds

union (rng G) = A /\ (union (rng F))

for A being set

for F, G being FinSequence of X st dom G = dom F & ( for i being Nat st i in dom G holds

G . i = A /\ (F . i) ) holds

union (rng G) = A /\ (union (rng F))

proof end;

theorem Th7: :: MESFUNC3:7

for X being set

for F being FinSequence of X

for i being Nat st i in dom F holds

( F . i c= union (rng F) & (F . i) /\ (union (rng F)) = F . i )

for F being FinSequence of X

for i being Nat st i in dom F holds

( F . i c= union (rng F) & (F . i) /\ (union (rng F)) = F . i )

proof end;

theorem Th8: :: MESFUNC3:8

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for F being Finite_Sep_Sequence of S holds dom F = dom (M * F)

for S being SigmaField of X

for M being sigma_Measure of S

for F being Finite_Sep_Sequence of S holds dom F = dom (M * F)

proof end;

theorem Th9: :: MESFUNC3:9

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for F being Finite_Sep_Sequence of S holds M . (union (rng F)) = Sum (M * F)

for S being SigmaField of X

for M being sigma_Measure of S

for F being Finite_Sep_Sequence of S holds M . (union (rng F)) = Sum (M * F)

proof end;

theorem Th10: :: MESFUNC3:10

for F, G being FinSequence of ExtREAL

for a being R_eal st ( a is real or for i being Nat st i in dom F holds

F . i < 0. or for i being Nat st i in dom F holds

0. < F . i ) & dom F = dom G & ( for i being Nat st i in dom G holds

G . i = a * (F . i) ) holds

Sum G = a * (Sum F)

for a being R_eal st ( a is real or for i being Nat st i in dom F holds

F . i < 0. or for i being Nat st i in dom F holds

0. < F . i ) & dom F = dom G & ( for i being Nat st i in dom G holds

G . i = a * (F . i) ) holds

Sum G = a * (Sum F)

proof end;

definition

let X be non empty set ;

let S be SigmaField of X;

let f be PartFunc of X,ExtREAL;

let F be Finite_Sep_Sequence of S;

let a be FinSequence of ExtREAL ;

end;
let S be SigmaField of X;

let f be PartFunc of X,ExtREAL;

let F be Finite_Sep_Sequence of S;

let a be FinSequence of ExtREAL ;

:: deftheorem Def1 defines are_Re-presentation_of MESFUNC3:def 1 :

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,ExtREAL

for F being Finite_Sep_Sequence of S

for a being FinSequence of ExtREAL holds

( F,a are_Re-presentation_of f iff ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

f . x = a . n ) ) );

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,ExtREAL

for F being Finite_Sep_Sequence of S

for a being FinSequence of ExtREAL holds

( F,a are_Re-presentation_of f iff ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds

for x being set st x in F . n holds

f . x = a . n ) ) );

theorem :: MESFUNC3:12

for X being non empty set

for S being SigmaField of X

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

ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st F,a are_Re-presentation_of f

for S being SigmaField of X

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

ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st F,a are_Re-presentation_of f

proof end;

theorem Th13: :: MESFUNC3:13

for X being non empty set

for S being SigmaField of X

for F being Finite_Sep_Sequence of S ex G being Finite_Sep_Sequence of S st

( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds

( G . n <> {} & ex m being Nat st

( m in dom F & F . m = G . n ) ) ) )

for S being SigmaField of X

for F being Finite_Sep_Sequence of S ex G being Finite_Sep_Sequence of S st

( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds

( G . n <> {} & ex m being Nat st

( m in dom F & F . m = G . n ) ) ) )

proof end;

Lm1: for a being FinSequence of ExtREAL

for p, N being Element of ExtREAL st N = len a & ( for n being Nat st n in dom a holds

a . n = p ) holds

Sum a = N * p

proof end;

Lm2: for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds

0. <= f . x ) & ( for x being set st x in dom f holds

0. <> f . x ) holds

ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds

( 0. < a . n & a . n < +infty ) ) )

proof end;

Lm3: for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds

0. <= f . x ) & ex x being set st

( x in dom f & 0. = f . x ) holds

ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds

( 0. < a . n & a . n < +infty ) ) )

proof end;

theorem Th14: :: MESFUNC3:14

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds

0. <= f . x ) holds

ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds

( 0. < a . n & a . n < +infty ) ) )

for S being SigmaField of X

for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds

0. <= f . x ) holds

ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds

( 0. < a . n & a . n < +infty ) ) )

proof end;

theorem :: MESFUNC3:15

for X being non empty set

for S being SigmaField of X

for f being PartFunc of X,ExtREAL

for F being Finite_Sep_Sequence of S

for a being FinSequence of ExtREAL

for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds

ex ax being FinSequence of ExtREAL st

( dom ax = dom a & ( for n being Nat st n in dom ax holds

ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )

for S being SigmaField of X

for f being PartFunc of X,ExtREAL

for F being Finite_Sep_Sequence of S

for a being FinSequence of ExtREAL

for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds

ex ax being FinSequence of ExtREAL st

( dom ax = dom a & ( for n being Nat st n in dom ax holds

ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )

proof end;

theorem :: MESFUNC3:16

for p being FinSequence of ExtREAL

for q being FinSequence of REAL st p = q holds

Sum p = Sum q by Th2;

for q being FinSequence of REAL st p = q holds

Sum p = Sum q by Th2;

definition

let X be non empty set ;

let S be SigmaField of X;

let M be sigma_Measure of S;

let f be PartFunc of X,ExtREAL;

assume A1: ( f is_simple_func_in S & ( for x being set st x in dom f holds

0. <= f . x ) ) ;

ex b_{1} being Element of ExtREAL ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds

( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & b_{1} = Sum x )

for b_{1}, b_{2} being Element of ExtREAL st ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds

( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & b_{1} = Sum x ) & ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds

( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & b_{2} = Sum x ) holds

b_{1} = b_{2}

end;
let S be SigmaField of X;

let M be sigma_Measure of S;

let f be PartFunc of X,ExtREAL;

assume A1: ( f is_simple_func_in S & ( for x being set st x in dom f holds

0. <= f . x ) ) ;

func integral (X,S,M,f) -> Element of ExtREAL means :: MESFUNC3:def 2

ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds

( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & it = Sum x );

existence ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds

( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & it = Sum x );

ex b

( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds

( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & b

proof end;

uniqueness for b

( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds

( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & b

( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds

( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & b

b

proof end;

:: deftheorem defines integral MESFUNC3:def 2 :

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds

0. <= f . x ) holds

for b_{5} being Element of ExtREAL holds

( b_{5} = integral (X,S,M,f) iff ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds

( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & b_{5} = Sum x ) );

for X being non empty set

for S being SigmaField of X

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_simple_func_in S & ( for x being set st x in dom f holds

0. <= f . x ) holds

for b

( b

( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds

( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & b

begin

theorem :: MESFUNC3:18