:: MEASURE7 semantic presentation

theorem Th1: :: MEASURE7:1

for F being Function of NAT , ExtREAL st ( for n being Nat holds F . n = 0. ) holds
SUM F = 0.

proof end;

theorem Th2: :: MEASURE7:2

for F being Function of NAT , ExtREAL st F is nonnegative holds
for n being Nat holds F . n <=' (Ser F) . n

proof end;

theorem Th3: :: MEASURE7:3

for F, G, H being Function of NAT , ExtREAL st G is nonnegative & H is nonnegative & ( for n being Nat holds F . n = (G . n) + (H . n) ) holds
for n being Nat holds (Ser F) . n = ((Ser G) . n) + ((Ser H) . n)

proof end;

theorem Th4: :: MEASURE7:4

for F, G, H being Function of NAT , ExtREAL st ( for n being Nat holds F . n = (G . n) + (H . n) ) & G is nonnegative & H is nonnegative holds
SUM F <=' (SUM G) + (SUM H)

proof end;

theorem :: MEASURE7:5

canceled;

theorem Th6: :: MEASURE7:6

for F, G being Function of NAT , ExtREAL st F is nonnegative & ( for n being Nat holds F . n <=' G . n ) holds
for n being Nat holds (Ser F) . n <=' SUM G

proof end;

theorem Th7: :: MEASURE7:7

for F being Function of NAT , ExtREAL st F is nonnegative holds
for n being Nat holds (Ser F) . n <=' SUM F

proof end;

definition

let S be non empty Subset of NAT ;
let H be Function of S, NAT ;
let n be Element of S;
:: original: .
redefine func H . n -> Nat;
correctness

proof end;

end;

definition

let S be non empty set ;
let H be Function of S, ExtREAL ;
func On H -> Function of NAT , ExtREAL means :Def1: :: MEASURE7:def 1
for n being Element of NAT holds
( ( n in S implies it . n = H . n ) & ( not n in S implies it . n = 0. ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines On MEASURE7:def 1 :

theorem Th8: :: MEASURE7:8

for X being non empty set
for G being Function of X, ExtREAL st G is nonnegative holds
On G is nonnegative

proof end;

theorem Th9: :: MEASURE7:9

for F being Function of NAT , ExtREAL st F is nonnegative holds
for n, k being Nat st n <= k holds
(Ser F) . n <=' (Ser F) . k

proof end;

theorem Th10: :: MEASURE7:10

for k being Nat
for F being Function of NAT , ExtREAL st ( for n being Nat st n <> k holds
F . n = 0. ) holds
( ( for n being Nat st n < k holds
(Ser F) . n = 0. ) & ( for n being Nat st k <= n holds
(Ser F) . n = F . k ) )

proof end;

theorem Th11: :: MEASURE7:11

for G being Function of NAT , ExtREAL st G is nonnegative holds
for S being non empty Subset of NAT
for H being Function of S, NAT st H is one-to-one holds
SUM (On (G * H)) <=' SUM G

proof end;

theorem Th12: :: MEASURE7:12

for F, G being Function of NAT , ExtREAL st F is nonnegative & G is nonnegative holds
for S being non empty Subset of NAT
for H being Function of S, NAT st H is one-to-one & ( for k being Nat holds
( ( k in S implies F . k = (G * H) . k ) & ( not k in S implies F . k = 0. ) ) ) holds
SUM F <=' SUM G

proof end;

Lm1: REAL c= REAL
;

then consider G0 being Function of NAT , bool REAL such that
Lm2: rng G0 = {REAL } by MEASURE1:34;

REAL in {REAL }
by TARSKI:def 1;

then Lm3: REAL c= union (rng G0)
by Lm2, ZFMISC_1:92;

Lm4: for n being Nat holds G0 . n is Interval

proof end;

definition

let A be Subset of REAL ;
mode Interval_Covering of A -> Function of NAT , bool REAL means :Def2: :: MEASURE7:def 2
( A c= union (rng it) & ( for n being Nat holds it . n is Interval ) );
existence

proof end;

end;

:: deftheorem Def2 defines Interval_Covering MEASURE7:def 2 :

definition

let A be Subset of REAL ;
let F be Interval_Covering of A;
let n be Nat;
:: original: .
redefine func F . n -> Interval;
correctness by Def2;

end;

definition

let F be Function of NAT , bool REAL ;
mode Interval_Covering of F -> Function of NAT , Funcs NAT ,(bool REAL ) means :Def3: :: MEASURE7:def 3
for n being Nat holds it . n is Interval_Covering of F . n;
existence

proof end;

end;

:: deftheorem Def3 defines Interval_Covering MEASURE7:def 3 :

definition

let A be Subset of REAL ;
let F be Interval_Covering of A;
deffunc H₁( Nat) -> Element of ExtREAL = vol (F . $1);
func F vol -> Function of NAT , ExtREAL means :Def4: :: MEASURE7:def 4
for n being Nat holds it . n = vol (F . n);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines vol MEASURE7:def 4 :

theorem Th13: :: MEASURE7:13

for A being Subset of REAL
for F being Interval_Covering of A holds F vol is nonnegative

proof end;

definition

let F be Function of NAT , bool REAL ;
let H be Interval_Covering of F;
let n be Nat;
:: original: .
redefine func H . n -> Interval_Covering of F . n;
correctness by Def3;

end;

definition

let F be Function of NAT , bool REAL ;
let G be Interval_Covering of F;
func G vol -> Function of NAT , Funcs NAT ,ExtREAL means :: MEASURE7:def 5
for n being Nat holds it . n = (G . n) vol ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines vol MEASURE7:def 5 :

definition

let A be Subset of REAL ;
let F be Interval_Covering of A;
func vol F -> R_eal equals :: MEASURE7:def 6
SUM (F vol );
correctness ;

end;

:: deftheorem defines vol MEASURE7:def 6 :

definition

let F be Function of NAT , bool REAL ;
let G be Interval_Covering of F;
func vol G -> Function of NAT , ExtREAL means :Def7: :: MEASURE7:def 7
for n being Nat holds it . n = vol (G . n);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines vol MEASURE7:def 7 :

theorem Th14: :: MEASURE7:14

for F being Function of NAT , bool REAL
for G being Interval_Covering of F
for n being Nat holds 0. <=' (vol G) . n

proof end;

definition

let A be Subset of REAL ;
defpred S₁[ set ] means ex F being Interval_Covering of A st $1 = vol F;
func Svc A -> Subset of ExtREAL means :Def8: :: MEASURE7:def 8
for x being R_eal holds
( x in it iff ex F being Interval_Covering of A st x = vol F );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines Svc MEASURE7:def 8 :

registration

let A be Subset of REAL ;
cluster Svc A -> non empty ;
coherence

proof end;

end;

definition

let A be Subset of REAL ;
func COMPLEX A -> Element of ExtREAL equals :: MEASURE7:def 9
inf (Svc A);
correctness ;

end;

:: deftheorem defines COMPLEX MEASURE7:def 9 :

definition

func OS_Meas -> Function of bool REAL , ExtREAL means :Def10: :: MEASURE7:def 10
for A being Subset of REAL holds it . A = inf (Svc A);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines OS_Meas MEASURE7:def 10 :

definition

let H be Function of NAT ,[:NAT ,NAT :];
:: original: pr1
redefine func pr1 H -> Function of NAT , NAT means :: MEASURE7:def 11
for n being Element of NAT ex s being Element of NAT st H . n = [(it . n),s];
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem defines pr1 MEASURE7:def 11 :

definition

let H be Function of NAT ,[:NAT ,NAT :];
:: original: pr2
redefine func pr2 H -> Function of NAT , NAT means :Def12: :: MEASURE7:def 12
for n being Element of NAT holds H . n = [((pr1 H) . n),(it . n)];
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem Def12 defines pr2 MEASURE7:def 12 :

definition

let F be Function of NAT , bool REAL ;
let G be Interval_Covering of F;
let H be Function of NAT ,[:NAT ,NAT :];
assume A1: rng H = [:NAT ,NAT :] ;
func On G,H -> Interval_Covering of union (rng F) means :Def13: :: MEASURE7:def 13
for n being Element of NAT holds it . n = (G . ((pr1 H) . n)) . ((pr2 H) . n);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines On MEASURE7:def 13 :

reconsider D = NAT --> {} as Function of NAT , bool REAL by FUNCOP_1:57;

Lm5: for n being Element of NAT holds D . n = {}
by FUNCOP_1:13;

theorem Th15: :: MEASURE7:15

for H being Function of NAT ,[:NAT ,NAT :] st H is one-to-one & rng H = [:NAT ,NAT :] holds
for k being Nat ex m being Nat st
for F being Function of NAT , bool REAL
for G being Interval_Covering of F holds (Ser ((On G,H) vol )) . k <=' (Ser (vol G)) . m

proof end;

theorem Th16: :: MEASURE7:16