:: MEASURE7 semantic presentation

theorem Th1: :: MEASURE7:1

for b₁ being Function of NAT , ExtREAL st ( for b₂ being Nat holds b₁ . b₂ = 0. ) holds
SUM b₁ = 0.

proof end;

theorem Th2: :: MEASURE7:2

for b₁ being Function of NAT , ExtREAL st b₁ is nonnegative holds
for b₂ being Nat holds b₁ . b₂ <=' (Ser b₁) . b₂

proof end;

theorem Th3: :: MEASURE7:3

for b₁, b₂, b₃ being Function of NAT , ExtREAL st b₂ is nonnegative & b₃ is nonnegative & ( for b₄ being Nat holds b₁ . b₄ = (b₂ . b₄) + (b₃ . b₄) ) holds
for b₄ being Nat holds (Ser b₁) . b₄ = ((Ser b₂) . b₄) + ((Ser b₃) . b₄)

proof end;

theorem Th4: :: MEASURE7:4

for b₁, b₂, b₃ being Function of NAT , ExtREAL st ( for b₄ being Nat holds b₁ . b₄ = (b₂ . b₄) + (b₃ . b₄) ) & b₂ is nonnegative & b₃ is nonnegative holds
SUM b₁ <=' (SUM b₂) + (SUM b₃)

proof end;

theorem Th5: :: MEASURE7:5

canceled;

theorem Th6: :: MEASURE7:6

for b₁, b₂ being Function of NAT , ExtREAL st b₁ is nonnegative & ( for b₃ being Nat holds b₁ . b₃ <=' b₂ . b₃ ) holds
for b₃ being Nat holds (Ser b₁) . b₃ <=' SUM b₂

proof end;

theorem Th7: :: MEASURE7:7

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

proof end;

definition

let c₁ be non empty Subset of NAT ;
let c₂ be Function of c₁, NAT ;
let c₃ be Element of c₁;
redefine func . as c₂ . c₃ -> Nat;
correctness

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be Function of c₁, ExtREAL ;
func On c₂ -> Function of NAT , ExtREAL means :Def1: :: MEASURE7:def 1
for b₁ being Element of NAT holds
( ( b₁ in a₁ implies a₃ . b₁ = a₂ . b₁ ) & ( not b₁ in a₁ implies a₃ . b₁ = 0. ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines On MEASURE7:def 1 :

theorem Th8: :: MEASURE7:8

for b₁ being non empty set
for b₂ being Function of b₁, ExtREAL st b₂ is nonnegative holds
On b₂ is nonnegative

proof end;

theorem Th9: :: MEASURE7:9

for b₁ being Function of NAT , ExtREAL st b₁ is nonnegative holds
for b₂, b₃ being Nat st b₂ <= b₃ holds
(Ser b₁) . b₂ <=' (Ser b₁) . b₃

proof end;

theorem Th10: :: MEASURE7:10

for b₁ being Nat
for b₂ being Function of NAT , ExtREAL st ( for b₃ being Nat st b₃ <> b₁ holds
b₂ . b₃ = 0. ) holds
( ( for b₃ being Nat st b₃ < b₁ holds
(Ser b₂) . b₃ = 0. ) & ( for b₃ being Nat st b₁ <= b₃ holds
(Ser b₂) . b₃ = b₂ . b₁ ) )

proof end;

theorem Th11: :: MEASURE7:11

for b₁ being Function of NAT , ExtREAL st b₁ is nonnegative holds
for b₂ being non empty Subset of NAT
for b₃ being Function of b₂, NAT st b₃ is one-to-one holds
SUM (On (b₁ * b₃)) <=' SUM b₁

proof end;

theorem Th12: :: MEASURE7:12

for b₁, b₂ being Function of NAT , ExtREAL st b₁ is nonnegative & b₂ is nonnegative holds
for b₃ being non empty Subset of NAT
for b₄ being Function of b₃, NAT st b₄ is one-to-one & ( for b₅ being Nat holds
( ( b₅ in b₃ implies b₁ . b₅ = (b₂ * b₄) . b₅ ) & ( not b₅ in b₃ implies b₁ . b₅ = 0. ) ) ) holds
SUM b₁ <=' SUM b₂

proof end;

Lemma13: REAL c= REAL
;

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

REAL in {REAL }
by TARSKI:def 1;

then Lemma15: REAL c= union (rng c₁)
by Lemma14, ZFMISC_1:92;

Lemma16: for b₁ being Nat holds c₁ . b₁ is Interval

proof end;

definition

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

proof end;

end;

:: deftheorem Def2 defines Interval_Covering MEASURE7:def 2 :

definition

let c₂ be Subset of REAL ;
let c₃ be Interval_Covering of c₂;
let c₄ be Nat;
redefine func . as c₂ . c₃ -> Interval;
correctness by Def2;

end;

definition

let c₂ be Function of NAT , bool REAL ;
mode Interval_Covering of c₁ -> Function of NAT , Funcs NAT ,(bool REAL ) means :Def3: :: MEASURE7:def 3
for b₁ being Nat holds a₂ . b₁ is Interval_Covering of a₁ . b₁;
existence

proof end;

end;

:: deftheorem Def3 defines Interval_Covering MEASURE7:def 3 :

definition

let c₂ be Subset of REAL ;
let c₃ be Interval_Covering of c₂;
deffunc H₁( Nat) -> Element of ExtREAL = vol (c₃ . a₁);
func c₂ vol -> Function of NAT , ExtREAL means :Def4: :: MEASURE7:def 4
for b₁ being Nat holds a₃ . b₁ = vol (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines vol MEASURE7:def 4 :

theorem Th13: :: MEASURE7:13

for b₁ being Subset of REAL
for b₂ being Interval_Covering of b₁ holds b₂ vol is nonnegative

proof end;

definition

let c₂ be Function of NAT , bool REAL ;
let c₃ be Interval_Covering of c₂;
let c₄ be Nat;
redefine func . as c₂ . c₃ -> Interval_Covering of a₁ . a₃;
correctness by Def3;

end;

definition

let c₂ be Function of NAT , bool REAL ;
let c₃ be Interval_Covering of c₂;
func c₂ vol -> Function of NAT , Funcs NAT ,ExtREAL means :: MEASURE7:def 5
for b₁ being Nat holds a₃ . b₁ = (a₂ . b₁) vol ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines vol MEASURE7:def 5 :

definition

let c₂ be Subset of REAL ;
let c₃ be Interval_Covering of c₂;
func vol c₂ -> R_eal equals :: MEASURE7:def 6
SUM (a₂ vol );
correctness ;

end;

:: deftheorem Def6 defines vol MEASURE7:def 6 :

definition

let c₂ be Function of NAT , bool REAL ;
let c₃ be Interval_Covering of c₂;
func vol c₂ -> Function of NAT , ExtREAL means :Def7: :: MEASURE7:def 7
for b₁ being Nat holds a₃ . b₁ = vol (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines vol MEASURE7:def 7 :

theorem Th14: :: MEASURE7:14

for b₁ being Function of NAT , bool REAL
for b₂ being Interval_Covering of b₁
for b₃ being Nat holds 0. <=' (vol b₂) . b₃

proof end;

definition

let c₂ be Subset of REAL ;
defpred S₁[ set ] means ex b₁ being Interval_Covering of c₂ st a₁ = vol b₁;
func Svc c₁ -> Subset of ExtREAL means :Def8: :: MEASURE7:def 8
for b₁ being R_eal holds
( b₁ in a₂ iff ex b₂ being Interval_Covering of a₁ st b₁ = vol b₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines Svc MEASURE7:def 8 :

registration

let c₂ be Subset of REAL ;
cluster Svc a₁ -> non empty ;
coherence

proof end;

end;

definition

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

end;

:: deftheorem Def9 defines COMPLEX MEASURE7:def 9 :

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines OS_Meas MEASURE7:def 10 :

definition

let c₂ be Function of NAT ,[:NAT ,NAT :];
redefine func pr1 as pr1 c₁ -> Function of NAT , NAT means :: MEASURE7:def 11
for b₁ being Element of NAT ex b₂ being Element of NAT st a₁ . b₁ = [(a₂ . b₁),b₂];
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem Def11 defines pr1 MEASURE7:def 11 :

definition

let c₂ be Function of NAT ,[:NAT ,NAT :];
redefine func pr2 as pr2 c₁ -> Function of NAT , NAT means :Def12: :: MEASURE7:def 12
for b₁ being Element of NAT holds a₁ . b₁ = [((pr1 a₁) . b₁),(a₂ . b₁)];
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem Def12 defines pr2 MEASURE7:def 12 :

definition

let c₂ be Function of NAT , bool REAL ;
let c₃ be Interval_Covering of c₂;
let c₄ be Function of NAT ,[:NAT ,NAT :];
assume E26: rng c₄ = [:NAT ,NAT :] ;
func On c₂,c₃ -> Interval_Covering of union (rng a₁) means :Def13: :: MEASURE7:def 13
for b₁ being Element of NAT holds a₄ . b₁ = (a₂ . ((pr1 a₃) . b₁)) . ((pr2 a₃) . b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines On MEASURE7:def 13 :

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

Lemma27: for b₁ being Element of NAT holds c₂ . b₁ = {}
by FUNCOP_1:13;

theorem Th15: :: MEASURE7:15

for b₁ being Function of NAT ,[:NAT ,NAT :] st b₁ is one-to-one & rng b₁ = [:NAT ,NAT :] holds
for b₂ being Nat ex b₃ being Nat st
for b₄ being Function of NAT , bool REAL
for b₅ being Interval_Covering of b₄ holds (Ser ((On b₅,b₁) vol )) . b₂ <=' (Ser (vol b₅)) . b₃

proof end;

theorem Th16: :: MEASURE7:16

for b₁ being Function of NAT , bool REAL
for b₂ being Interval_Covering of b₁ holds inf (Svc (union (rng b₁))) <=' SUM (vol b₂)

proof end;

theorem Th17: :: MEASURE7:17

OS_Meas is C_Measure of REAL

proof end;

definition

redefine func OS_Meas as OS_Meas -> C_Measure of REAL ;
correctness by Th17;

end;

definition

func Lmi_sigmaFIELD -> sigma_Field_Subset of REAL equals :: MEASURE7:def 14
sigma_Field OS_Meas ;
correctness ;

end;

:: deftheorem Def14 defines Lmi_sigmaFIELD MEASURE7:def 14 :

definition

func L_mi -> sigma_Measure of Lmi_sigmaFIELD equals :: MEASURE7:def 15
sigma_Meas OS_Meas ;
correctness ;

end;

:: deftheorem Def15 defines L_mi MEASURE7:def 15 :

theorem Th18: :: MEASURE7:18

L_mi is_complete Lmi_sigmaFIELD by MEASURE4:25;

theorem Th19: :: MEASURE7:19

canceled;

theorem Th20: :: MEASURE7:20

canceled;

theorem Th21: :: MEASURE7:21

for b₁ being set st b₁ in Lmi_sigmaFIELD holds
REAL \ b₁ in Lmi_sigmaFIELD by MEASURE4:16;