:: Lebesgue Integral of Simple Valued Function
:: 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
proofend;

theorem Th2: :: MESFUNC3:2
for F being FinSequence of ExtREAL
for f being FinSequence of REAL st F = f holds
Sum F = Sum f
proofend;

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

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 &amp; j in dom F &amp; i <> j holds
F . i misses F . j )
proofend;

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 &amp; ( for i being Nat st i in dom G holds
G . i = A /\ (F . i) ) holds
G is Finite_Sep_Sequence of S
proofend;

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 &amp; ( for i being Nat st i in dom G holds
G . i = A /\ (F . i) ) holds
union (rng G) = A /\ (union (rng F))
proofend;

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) &amp; (F . i) /\ (union (rng F)) = F . i )
proofend;

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

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

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 ) &amp; dom F = dom G &amp; ( for i being Nat st i in dom G holds
G . i = a * (F . i) ) holds
Sum G = a * (Sum F)
proofend;

theorem Th11: :: MESFUNC3:11
for F being FinSequence of REAL holds F is FinSequence of ExtREAL
proofend;

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 ;
predF,a are_Re-presentation_of f means :Def1: :: MESFUNC3:def 1
( dom f = union (rng F) &amp; dom F = dom a &amp; ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) );
end;

:: 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) &amp; dom F = dom a &amp; ( 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
proofend;

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) &amp; ( for n being Nat st n in dom G holds
( G . n <> {} &amp; ex m being Nat st
( m in dom F &amp; F . m = G . n ) ) ) )
proofend;

Lm1:  for a being FinSequence of ExtREAL
for p, N being Element of ExtREAL st N = len a &amp; ( for n being Nat st n in dom a holds
a . n = p ) holds
Sum a = N * p
proofend;

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 &amp; ( for x being set st x in dom f holds
0. <= f . x ) &amp; ( 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 &amp; a . 1 = 0. &amp; ( for n being Nat st 2 <= n &amp; n in dom a holds
( 0. < a . n &amp; a . n < +infty ) ) )
proofend;

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 &amp; ( for x being set st x in dom f holds
0. <= f . x ) &amp; ex x being set st
( x in dom f &amp; 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 &amp; a . 1 = 0. &amp; ( for n being Nat st 2 <= n &amp; n in dom a holds
( 0. < a . n &amp; a . n < +infty ) ) )
proofend;

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 &amp; ( 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 &amp; a . 1 = 0. &amp; ( for n being Nat st 2 <= n &amp; n in dom a holds
( 0. < a . n &amp; a . n < +infty ) ) )
proofend;

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 &amp; x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a &amp; ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) &amp; f . x = Sum ax )
proofend;

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;

theorem Th17: :: MESFUNC3:17
for p being FinSequence of ExtREAL st not -infty in rng p &amp; +infty in rng p holds
Sum p = +infty
proofend;

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 &amp; ( 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 &amp; a . 1 = 0. &amp; ( for n being Nat st 2 <= n &amp; n in dom a holds
( 0. < a . n &amp; a . n < +infty ) ) &amp; dom x = dom F &amp; ( for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) ) &amp; it = Sum x );
existence
 ex b1 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 &amp; a . 1 = 0. &amp; ( for n being Nat st 2 <= n &amp; n in dom a holds
( 0. < a . n &amp; a . n < +infty ) ) &amp; dom x = dom F &amp; ( for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) ) &amp; b1 = Sum x )
proofend;
uniqueness
 for b1, b2 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 &amp; a . 1 = 0. &amp; ( for n being Nat st 2 <= n &amp; n in dom a holds
( 0. < a . n &amp; a . n < +infty ) ) &amp; dom x = dom F &amp; ( for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) ) &amp; b1 = Sum x ) &amp; ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st
( F,a are_Re-presentation_of f &amp; a . 1 = 0. &amp; ( for n being Nat st 2 <= n &amp; n in dom a holds
( 0. < a . n &amp; a . n < +infty ) ) &amp; dom x = dom F &amp; ( for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) ) &amp; b2 = Sum x ) holds
b1 = b2
proofend;
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 &amp; ( for x being set st x in dom f holds
0. <= f . x ) holds
for b5 being Element of ExtREAL holds
( b5 = 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 &amp; a . 1 = 0. &amp; ( for n being Nat st 2 <= n &amp; n in dom a holds
( 0. < a . n &amp; a . n < +infty ) ) &amp; dom x = dom F &amp; ( for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) ) &amp; b5 = Sum x ) );

begin

theorem :: MESFUNC3:18
for a being FinSequence of ExtREAL
for p, N being Element of ExtREAL st N = len a &amp; ( for n being Nat st n in dom a holds
a . n = p ) holds
Sum a = N * p by Lm1;