:: 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 b₁ being sequence of ExtREAL st
for n being Element of NAT holds
( ( n in S implies b₁ . n = H . n ) & ( not n in S implies b₁ . n = 0. ) )

proof end;

uniqueness
for b₁, b₂ being sequence of ExtREAL st ( for n being Element of NAT holds
( ( n in S implies b₁ . n = H . n ) & ( not n in S implies b₁ . n = 0. ) ) ) & ( for n being Element of NAT holds
( ( n in S implies b₂ . n = H . n ) & ( not n in S implies b₂ . n = 0. ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines On MEASURE7:def 1 :
for S being non empty set
for H being Function of S,ExtREAL
for b₃ being sequence of ExtREAL holds
( b₃ = On H iff for n being Element of NAT holds
( ( n in S implies b₃ . n = H . n ) & ( not n in S implies b₃ . 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 b₁ being sequence of (bool REAL) st
( A c= union (rng b₁) & ( for n being Element of NAT holds b₁ . 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 b₂ being sequence of (bool REAL) holds
( b₂ is Interval_Covering of A iff ( A c= union (rng b₂) & ( for n being Element of NAT holds b₂ . 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 b₁ being sequence of (Funcs (NAT,(bool REAL))) st
for n being Element of NAT holds b₁ . 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 b₂ being sequence of (Funcs (NAT,(bool REAL))) holds
( b₂ is Interval_Covering of F iff for n being Element of NAT holds b₂ . n is Interval_Covering of F . n );

definition

let A be Subset of REAL;
let F be Interval_Covering of A;
deffunc H₁( 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 b₁ being sequence of ExtREAL st
for n being Element of NAT holds b₁ . n = diameter (F . n)

proof end;

uniqueness
for b₁, b₂ being sequence of ExtREAL st ( for n being Element of NAT holds b₁ . n = diameter (F . n) ) & ( for n being Element of NAT holds b₂ . n = diameter (F . n) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines vol MEASURE7:def 4 :
for A being Subset of REAL
for F being Interval_Covering of A
for b₃ being sequence of ExtREAL holds
( b₃ = F vol iff for n being Element of NAT holds b₃ . 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 b₁ being sequence of (Funcs (NAT,ExtREAL)) st
for n being Element of NAT holds b₁ . n = (G . n) vol

proof end;

uniqueness
for b₁, b₂ being sequence of (Funcs (NAT,ExtREAL)) st ( for n being Element of NAT holds b₁ . n = (G . n) vol ) & ( for n being Element of NAT holds b₂ . n = (G . n) vol ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defines vol MEASURE7:def 5 :
for F being sequence of (bool REAL)
for G being Interval_Covering of F
for b₃ being sequence of (Funcs (NAT,ExtREAL)) holds
( b₃ = G vol iff for n being Element of NAT holds b₃ . 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 b₁ being sequence of ExtREAL st
for n being Element of NAT holds b₁ . n = vol (G . n)

proof end;

uniqueness
for b₁, b₂ being sequence of ExtREAL st ( for n being Element of NAT holds b₁ . n = vol (G . n) ) & ( for n being Element of NAT holds b₂ . n = vol (G . n) ) holds
b₁ = b₂

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 b₃ being sequence of ExtREAL holds
( b₃ = vol G iff for n being Element of NAT holds b₃ . 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 S₁[ 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 b₁ being Subset of ExtREAL st
for x being R_eal holds
( x in b₁ iff ex F being Interval_Covering of A st x = vol F )

proof end;

uniqueness
for b₁, b₂ being Subset of ExtREAL st ( for x being R_eal holds
( x in b₁ iff ex F being Interval_Covering of A st x = vol F ) ) & ( for x being R_eal holds
( x in b₂ iff ex F being Interval_Covering of A st x = vol F ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines Svc MEASURE7:def 8 :
for A being Subset of REAL
for b₂ being Subset of ExtREAL holds
( b₂ = Svc A iff for x being R_eal holds
( x in b₂ 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 b₁ being Function of (bool REAL),ExtREAL st
for A being Subset of REAL holds b₁ . A = inf (Svc A)

proof end;

uniqueness
for b₁, b₂ being Function of (bool REAL),ExtREAL st ( for A being Subset of REAL holds b₁ . A = inf (Svc A) ) & ( for A being Subset of REAL holds b₂ . A = inf (Svc A) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines OS_Meas MEASURE7:def 10 :
for b₁ being Function of (bool REAL),ExtREAL holds
( b₁ = OS_Meas iff for A being Subset of REAL holds b₁ . 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 b₁ being Interval_Covering of union (rng F) st
for n being Element of NAT holds b₁ . n = (G . ((pr1 H) . n)) . ((pr2 H) . n)

proof end;

uniqueness
for b₁, b₂ being Interval_Covering of union (rng F) st ( for n being Element of NAT holds b₁ . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) ) & ( for n being Element of NAT holds b₂ . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) ) holds
b₁ = b₂

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 b₄ being Interval_Covering of union (rng F) holds
( b₄ = On (G,H) iff for n being Element of NAT holds b₄ . 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;