:: The One-Dimensional Lebesgue Measure As an Example of a Formalization in the Mizar Language of the Classical Definition of a Mathematical Object
:: by J\'ozef Bia{\l}as
::
:: Received February 4, 1995
:: Copyright (c) 1995-2021 Association of Mizar Users


theorem Th1: :: MEASURE7:1
for F being sequence of ExtREAL st ( for n being Element of NAT holds F . n = 0. ) holds
SUM F = 0.
proof end;

theorem Th2: :: MEASURE7:2
for F being sequence of ExtREAL st F is V99() holds
for n being Nat holds F . n <= (Ser F) . n
proof end;

theorem Th3: :: MEASURE7:3
for F, G, H being sequence of ExtREAL st G is V99() & H is V99() & ( for n being Element of 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 sequence of ExtREAL st ( for n being Element of NAT holds F . n = (G . n) + (H . n) ) & G is V99() & H is V99() holds
SUM F <= (SUM G) + (SUM H)
proof end;

theorem Th5: :: MEASURE7:5
for F, G being sequence of ExtREAL st ( for n being Element of NAT holds F . n <= G . n ) holds
for n being Element of NAT holds (Ser F) . n <= SUM G
proof end;

theorem Th6: :: MEASURE7:6
for F being sequence of ExtREAL st F is V99() holds
for n being Element of NAT holds (Ser F) . n <= SUM F
proof end;

definition
let S be non empty set ;
let H be Function of S,ExtREAL;
func On H -> sequence of 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
ex b1 being sequence of ExtREAL st
for n being Element of NAT holds
( ( n in S implies b1 . n = H . n ) & ( not n in S implies b1 . n = 0. ) )
proof end;
uniqueness
for b1, b2 being sequence of ExtREAL st ( for n being Element of NAT holds
( ( n in S implies b1 . n = H . n ) & ( not n in S implies b1 . n = 0. ) ) ) & ( for n being Element of NAT holds
( ( n in S implies b2 . n = H . n ) & ( not n in S implies b2 . n = 0. ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines On MEASURE7:def 1 :
for S being non empty set
for H being Function of S,ExtREAL
for b3 being sequence of ExtREAL holds
( b3 = On H iff for n being Element of NAT holds
( ( n in S implies b3 . n = H . n ) & ( not n in S implies b3 . n = 0. ) ) );

theorem Th7: :: MEASURE7:7
for X being non empty set
for G being Function of X,ExtREAL st G is V99() holds
On G is V99()
proof end;

theorem Th8: :: MEASURE7:8
for F being sequence of ExtREAL st F is V99() holds
for n, k being Nat st n <= k holds
(Ser F) . n <= (Ser F) . k
proof end;

theorem Th9: :: MEASURE7:9
for k being Nat
for F being sequence of ExtREAL st ( for n being Element of NAT st n <> k holds
F . n = 0. ) holds
( ( for n being Element of NAT st n < k holds
(Ser F) . n = 0. ) & ( for n being Element of NAT st k <= n holds
(Ser F) . n = F . k ) )
proof end;

theorem Th10: :: MEASURE7:10
for G being sequence of ExtREAL st G is V99() 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 Th11: :: MEASURE7:11
for F, G being sequence of ExtREAL st G is V99() 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 Element of 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;

REAL in bool REAL
by ZFMISC_1:def 1;

then reconsider G0 = NAT --> REAL as sequence of (bool REAL) by FUNCOP_1:45;

Lm1: rng G0 = {REAL}
by FUNCOP_1:8;

then Lm2: REAL c= union (rng G0)
by ZFMISC_1:25;

Lm3: for n being Element of NAT holds G0 . n is Interval
proof end;

definition
let A be Subset of REAL;
mode Interval_Covering of A -> sequence of (bool REAL) means :Def2: :: MEASURE7:def 2
( A c= union (rng it) & ( for n being Element of NAT holds it . n is Interval ) );
existence
ex b1 being sequence of (bool REAL) st
( A c= union (rng b1) & ( for n being Element of NAT holds b1 . n is Interval ) ) by Lm2, Lm3, XBOOLE_1:1;
end;

:: deftheorem Def2 defines Interval_Covering MEASURE7:def 2 :
for A being Subset of REAL
for b2 being sequence of (bool REAL) holds
( b2 is Interval_Covering of A iff ( A c= union (rng b2) & ( for n being Element of NAT holds b2 . n is Interval ) ) );

definition
let A be Subset of REAL;
let F be Interval_Covering of A;
let n be Element of NAT ;
:: original: .
redefine func F . n -> Interval;
correctness
coherence
F . n is Interval;
by Def2;
end;

definition
let F be sequence of (bool REAL);
mode Interval_Covering of F -> sequence of (Funcs (NAT,(bool REAL))) means :Def3: :: MEASURE7:def 3
 for n being Element of NAT holds it . n is Interval_Covering of F . n;
existence
ex b1 being sequence of (Funcs (NAT,(bool REAL))) st
for n being Element of NAT holds b1 . n is Interval_Covering of F . n
proof end;
end;

:: deftheorem Def3 defines Interval_Covering MEASURE7:def 3 :
for F being sequence of (bool REAL)
for b2 being sequence of (Funcs (NAT,(bool REAL))) holds
( b2 is Interval_Covering of F iff for n being Element of NAT holds b2 . n is Interval_Covering of F . n );

definition
let A be Subset of REAL;
let F be Interval_Covering of A;
deffunc H1( Element of NAT ) -> Element of ExtREAL = diameter (F . $1);
func F vol -> sequence of ExtREAL means :Def4: :: MEASURE7:def 4
 for n being Element of NAT holds it . n = diameter (F . n);
existence
ex b1 being sequence of ExtREAL st
for n being Element of NAT holds b1 . n = diameter (F . n)
proof end;
uniqueness
for b1, b2 being sequence of ExtREAL st ( for n being Element of NAT holds b1 . n = diameter (F . n) ) & ( for n being Element of NAT holds b2 . n = diameter (F . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines vol MEASURE7:def 4 :
for A being Subset of REAL
for F being Interval_Covering of A
for b3 being sequence of ExtREAL holds
( b3 = F vol iff for n being Element of NAT holds b3 . n = diameter (F . n) );

theorem Th12: :: MEASURE7:12
for A being Subset of REAL
for F being Interval_Covering of A holds F vol is V99()
proof end;

definition
let F be sequence of (bool REAL);
let H be Interval_Covering of F;
let n be Element of NAT ;
:: original: .
redefine func H . n -> Interval_Covering of F . n;
correctness
coherence
H . n is Interval_Covering of F . n;
by Def3;
end;

definition
let F be sequence of (bool REAL);
let G be Interval_Covering of F;
func G vol -> sequence of (Funcs (NAT,ExtREAL)) means :: MEASURE7:def 5
 for n being Element of NAT holds it . n = (G . n) vol ;
existence
ex b1 being sequence of (Funcs (NAT,ExtREAL)) st
for n being Element of NAT holds b1 . n = (G . n) vol
proof end;
uniqueness
for b1, b2 being sequence of (Funcs (NAT,ExtREAL)) st ( for n being Element of NAT holds b1 . n = (G . n) vol ) & ( for n being Element of NAT holds b2 . n = (G . n) vol ) holds
b1 = b2
proof end;
end;

:: deftheorem defines vol MEASURE7:def 5 :
for F being sequence of (bool REAL)
for G being Interval_Covering of F
for b3 being sequence of (Funcs (NAT,ExtREAL)) holds
( b3 = G vol iff for n being Element of NAT holds b3 . n = (G . n) vol );

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
coherence
SUM (F vol) is R_eal;
;
end;

:: deftheorem defines vol MEASURE7:def 6 :
for A being Subset of REAL
for F being Interval_Covering of A holds vol F = SUM (F vol);

definition
let F be sequence of (bool REAL);
let G be Interval_Covering of F;
func vol G -> sequence of ExtREAL means :Def7: :: MEASURE7:def 7
 for n being Element of NAT holds it . n = vol (G . n);
existence
ex b1 being sequence of ExtREAL st
for n being Element of NAT holds b1 . n = vol (G . n)
proof end;
uniqueness
for b1, b2 being sequence of ExtREAL st ( for n being Element of NAT holds b1 . n = vol (G . n) ) & ( for n being Element of NAT holds b2 . n = vol (G . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines vol MEASURE7:def 7 :
for F being sequence of (bool REAL)
for G being Interval_Covering of F
for b3 being sequence of ExtREAL holds
( b3 = vol G iff for n being Element of NAT holds b3 . n = vol (G . n) );

theorem Th13: :: MEASURE7:13
for F being sequence of (bool REAL)
for G being Interval_Covering of F
for n being Element of NAT holds 0. <= (vol G) . n
proof end;

definition
let A be Subset of REAL;
defpred S1[ object ] 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
ex b1 being Subset of ExtREAL st
for x being R_eal holds
( x in b1 iff ex F being Interval_Covering of A st x = vol F )
proof end;
uniqueness
for b1, b2 being Subset of ExtREAL st ( for x being R_eal holds
( x in b1 iff ex F being Interval_Covering of A st x = vol F ) ) & ( for x being R_eal holds
( x in b2 iff ex F being Interval_Covering of A st x = vol F ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines Svc MEASURE7:def 8 :
for A being Subset of REAL
for b2 being Subset of ExtREAL holds
( b2 = Svc A iff for x being R_eal holds
( x in b2 iff ex F being Interval_Covering of A st x = vol F ) );

registration
let A be Subset of REAL;
cluster Svc A -> non empty ;
coherence
not Svc A is empty
proof end;
end;

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

:: deftheorem defines COMPLEX MEASURE7:def 9 :
for A being Subset of REAL holds COMPLEX A = inf (Svc A);

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
ex b1 being Function of (bool REAL),ExtREAL st
for A being Subset of REAL holds b1 . A = inf (Svc A)
proof end;
uniqueness
for b1, b2 being Function of (bool REAL),ExtREAL st ( for A being Subset of REAL holds b1 . A = inf (Svc A) ) & ( for A being Subset of REAL holds b2 . A = inf (Svc A) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines OS_Meas MEASURE7:def 10 :
for b1 being Function of (bool REAL),ExtREAL holds
( b1 = OS_Meas iff for A being Subset of REAL holds b1 . A = inf (Svc A) );

definition
let F be sequence of (bool REAL);
let G be Interval_Covering of F;
let H be sequence of [:NAT,NAT:];
assume A1: rng H = [:NAT,NAT:] ;
func On (G,H) -> Interval_Covering of union (rng F) means :Def11: :: MEASURE7:def 11
 for n being Element of NAT holds it . n = (G . ((pr1 H) . n)) . ((pr2 H) . n);
existence
ex b1 being Interval_Covering of union (rng F) st
for n being Element of NAT holds b1 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n)
proof end;
uniqueness
for b1, b2 being Interval_Covering of union (rng F) st ( for n being Element of NAT holds b1 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) ) & ( for n being Element of NAT holds b2 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines On MEASURE7:def 11 :
for F being sequence of (bool REAL)
for G being Interval_Covering of F
for H being sequence of [:NAT,NAT:] st rng H = [:NAT,NAT:] holds
for b4 being Interval_Covering of union (rng F) holds
( b4 = On (G,H) iff for n being Element of NAT holds b4 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) );

reconsider D = NAT --> ({} REAL) as sequence of (bool REAL) ;

theorem Th14: :: MEASURE7:14
for H being sequence of [:NAT,NAT:] st H is one-to-one & rng H = [:NAT,NAT:] holds
for k being Nat ex m being Element of NAT st
for F being sequence of (bool REAL)
for G being Interval_Covering of F holds (Ser ((On (G,H)) vol)) . k <= (Ser (vol G)) . m
proof end;

theorem Th15: :: MEASURE7:15
for F being sequence of (bool REAL)
for G being Interval_Covering of F holds inf (Svc (union (rng F))) <= SUM (vol G)
proof end;

theorem Th16: :: MEASURE7:16
OS_Meas is C_Measure of REAL
proof end;

definition
:: original: OS_Meas
redefine func OS_Meas -> C_Measure of REAL ;
correctness
coherence
OS_Meas is C_Measure of REAL ;
by Th16;
end;

definition
func Lmi_sigmaFIELD -> SigmaField of REAL equals :: MEASURE7:def 12
 sigma_Field OS_Meas;
coherence
sigma_Field OS_Meas is SigmaField of REAL ;
end;

:: deftheorem defines Lmi_sigmaFIELD MEASURE7:def 12 :
Lmi_sigmaFIELD = sigma_Field OS_Meas;

definition
func L_mi -> sigma_Measure of Lmi_sigmaFIELD equals :: MEASURE7:def 13
 sigma_Meas OS_Meas;
correctness
coherence
sigma_Meas OS_Meas is sigma_Measure of Lmi_sigmaFIELD;
;
end;

:: deftheorem defines L_mi MEASURE7:def 13 :
L_mi = sigma_Meas OS_Meas;