:: 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
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FUNCT_1, NUMBERS, SUBSET_1, SUPINF_2, ARYTM_3, CARD_1, RELAT_1,
TARSKI, ORDINAL2, XXREAL_0, NAT_1, XXREAL_2, ORDINAL1, XBOOLE_0,
ZFMISC_1, FUNCOP_1, MEASURE5, FUNCT_2, SUPINF_1, MCART_1, MEASURE4,
REAL_1, PROB_1, MEASURE1, MEASURE7, FUNCT_7, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, DOMAIN_1, ORDINAL1,
NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, XXREAL_3, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, NAT_1, PROB_1, XXREAL_2, SUPINF_1,
SUPINF_2, MEASURE1, MEASURE4, MEASURE5, RECDEF_1;
constructors PARTFUN1, DOMAIN_1, FUNCOP_1, NAT_1, MEASURE4, MEASURE5,
RECDEF_1, SUPINF_1, XREAL_0, RELSET_1, XXREAL_2, MEASURE1, PROB_2;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0,
MEMBERED, MEASURE1, MEASURE4, VALUED_0, XXREAL_2, XXREAL_3, FUNCT_1,
RELSET_1, XXREAL_0;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Some theorems about series of R_eal numbers
theorem :: MEASURE7:1
for F being sequence of ExtREAL st for n being Element of NAT
holds F.n = 0. holds SUM(F) = 0.;
theorem :: MEASURE7:2
for F being sequence of ExtREAL st F is nonnegative holds for
n being Nat holds F.n <= Ser(F).n;
theorem :: MEASURE7:3
for F,G,H being sequence of ExtREAL st G is nonnegative & H
is nonnegative holds (for n being Element of NAT holds F.n = G.n + H.n )
implies for n being Nat holds (Ser F).n = (Ser G).n + (Ser H).n;
theorem :: MEASURE7:4
for F,G,H being sequence of ExtREAL st for n being Element of
NAT holds F.n = G.n + H.n holds G is nonnegative & H is nonnegative implies SUM
(F) <= SUM(G) + SUM(H);
theorem :: MEASURE7:5
for F,G being sequence of ExtREAL holds ( for n being Element
of NAT holds F.n <= G.n) implies for n being Element of NAT holds (Ser(F)).n <=
SUM(G);
theorem :: MEASURE7:6
for F being sequence of ExtREAL holds F is nonnegative
implies for n being Element of NAT holds (Ser(F)).n <= SUM(F);
definition
let S be non empty set;
let H be Function of S,ExtREAL;
func On H -> sequence of ExtREAL means
:: 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.);
end;
theorem :: MEASURE7:7
for X being non empty set for G being Function of X,ExtREAL st G
is nonnegative holds On G is nonnegative;
theorem :: MEASURE7:8
for F being sequence of ExtREAL st F is nonnegative holds for
n,k being Nat st n <= k holds Ser(F).n <= Ser(F).k;
theorem :: MEASURE7:9
for k being Nat holds for F being sequence of
ExtREAL holds ((for n being Element of NAT st n <> k holds F.n = 0.) implies (
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 );
theorem :: MEASURE7:10
for G being sequence of ExtREAL st G is nonnegative holds
for S being non empty Subset of NAT holds for H being Function of S,NAT st H is
one-to-one holds SUM(On(G*H)) <= SUM(G);
theorem :: MEASURE7:11
for F,G being sequence of ExtREAL st G is nonnegative holds
for S being non empty Subset of NAT holds for H being Function of S,NAT st H is
one-to-one holds (for k being Element of NAT holds ((k in S implies F.k = (G*H)
.k) & ((not k in S) implies F.k = 0.))) implies SUM(F) <= SUM(G);
definition
let A be Subset of REAL;
mode Interval_Covering of A -> sequence of bool REAL means
:: MEASURE7:def 2
A c= union(rng it) & for n being Element of NAT holds it.n is Interval;
end;
definition
let A be Subset of REAL;
let F be Interval_Covering of A;
let n be Element of NAT;
redefine func F.n ->Interval;
end;
definition
let F be sequence of bool REAL;
mode Interval_Covering of F -> sequence of Funcs(NAT,bool REAL) means
:: MEASURE7:def 3
for n being Element of NAT holds it.n is Interval_Covering of F.n;
end;
definition
let A be Subset of REAL;
let F be Interval_Covering of A;
func F vol -> sequence of ExtREAL means
:: MEASURE7:def 4
for n being Element of NAT holds it.n = diameter(F.n);
end;
theorem :: MEASURE7:12
for A being Subset of REAL holds for F being Interval_Covering
of A holds (F vol) is nonnegative;
definition
let F be sequence of bool REAL;
let H be Interval_Covering of F;
let n be Element of NAT;
redefine func H.n -> Interval_Covering of F.n;
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;
end;
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);
end;
definition
let F be sequence of (bool REAL);
let G be Interval_Covering of F;
func vol(G) -> sequence of ExtREAL means
:: MEASURE7:def 7
for n being Element of NAT holds it.n = vol(G.n);
end;
theorem :: MEASURE7:13
for F being sequence of (bool REAL) holds for G being
Interval_Covering of F holds for n being Element of NAT holds 0. <= (vol(G)).n;
definition
let A be Subset of REAL;
func Svc(A) -> Subset of ExtREAL means
:: MEASURE7:def 8
for x being R_eal holds x in
it iff ex F being Interval_Covering of A st x = vol(F);
end;
registration
let A be Subset of REAL;
cluster Svc(A) -> non empty;
end;
definition
let A be Subset of REAL;
func COMPLEX(A) -> Element of ExtREAL equals
:: MEASURE7:def 9
inf(Svc(A));
end;
definition
func OS_Meas -> Function of bool REAL,ExtREAL means
:: MEASURE7:def 10
for A being Subset of REAL holds it.A = inf(Svc(A));
end;
definition
let F be sequence of bool REAL;
let G be Interval_Covering of F;
let H be sequence of [:NAT,NAT:] such that
rng H = [:NAT,NAT:];
func On(G,H) -> Interval_Covering of union rng F means
:: MEASURE7:def 11
for n being Element of NAT holds it.n = (G.(pr1(H).n)).(pr2(H).n);
end;
theorem :: MEASURE7:14
for H being sequence of [:NAT,NAT:] st H is one-to-one & rng
H = [:NAT,NAT:] holds for k being Nat holds ex m being Element of
NAT st for F being sequence of bool REAL holds for G being
Interval_Covering of F holds Ser((On(G,H)) vol).k <= Ser(vol(G)).m;
theorem :: MEASURE7:15
for F being sequence of bool REAL holds for G being
Interval_Covering of F holds inf Svc(union rng F) <= SUM(vol(G));
theorem :: MEASURE7:16
OS_Meas is C_Measure of REAL;
definition
redefine func OS_Meas -> C_Measure of REAL;
end;
definition
func Lmi_sigmaFIELD -> SigmaField of REAL equals
:: MEASURE7:def 12
sigma_Field(OS_Meas);
end;
definition
func L_mi -> sigma_Measure of Lmi_sigmaFIELD equals
:: MEASURE7:def 13
sigma_Meas(OS_Meas);
end;