:: Lebesgue Integral of Simple Valued Function
:: by Yasunari Shidama and Noboru Endou
::
:: Copyright (c) 2004-2021 Association of Mizar Users

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
proof end;

theorem Th2: :: MESFUNC3:2
for F being FinSequence of ExtREAL
for f being FinSequence of REAL st F = f holds
Sum F = Sum f
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 object st x in F . n holds
f . x = a . n ) & ( for x being object 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 )
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
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))
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 )
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)
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)
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)
proof end;

theorem Th11: :: MESFUNC3:11
for F being FinSequence of REAL holds F is FinSequence of ExtREAL
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 ;
pred F,a are_Re-presentation_of f means :: MESFUNC3:def 1
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being object st x in F . n holds
f . x = a . n ) );
end;

:: deftheorem 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 object 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
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 ) ) ) )
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 & f is nonnegative & ( for x being object 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 & f is nonnegative & 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 & f is nonnegative 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 )
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;

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

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 & f is nonnegative ) ;
func integral (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 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 & 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) ) & b1 = Sum x )
proof end;
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 & 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) ) & b1 = 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) ) & b2 = Sum x ) holds
b1 = b2
proof end;
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 & f is nonnegative holds
for b5 being Element of ExtREAL holds
( b5 = integral (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) ) & b5 = Sum x ) );

theorem :: MESFUNC3:18
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 by Lm1;