:: MESFUNC3 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: MESFUNC3:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for S being sigma_Field_Subset 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for A being set
for S being sigma_Field_Subset 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for S being sigma_Field_Subset 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for S being sigma_Field_Subset 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being FinSequence of ExtREAL
for a being R_eal st ( ( a <> +infty & a <> -infty ) 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being FinSequence of REAL holds F is FinSequence of ExtREAL
proof end;

definition
let X be non empty set ;
let S be sigma_Field_Subset 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 :Def1: :: 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 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 sigma_Field_Subset 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for S being sigma_Field_Subset 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for S being sigma_Field_Subset 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 sigma_Field_Subset 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 sigma_Field_Subset 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for S being sigma_Field_Subset 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for S being sigma_Field_Subset 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence of ExtREAL
for q being FinSequence of REAL st p = q holds
Sum p = Sum q
proof end;

theorem Th17: :: MESFUNC3:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence of ExtREAL st ( for n being Nat st n in dom p holds
0. <=' p . n ) & ex n being Nat st
( n in dom p & p . n = +infty ) holds
Sum p = +infty
proof end;

definition
let X be non empty set ;
let S be sigma_Field_Subset of X;
let M be sigma_Measure of S;
let f be PartFunc of X, ExtREAL ;
assume A1: ( f is_simple_func_in S & dom f <> {} & ( 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 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 sigma_Field_Subset of X
for M being sigma_Measure of S
for f being PartFunc of X, ExtREAL st f is_simple_func_in S & dom f <> {} & ( 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 & 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;