:: Reconstruction of the One-Dimensional Lebesgue Measure
:: by Noboru Endou
::
:: Received January 13, 2020
:: Copyright (c) 2020-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, SETFAM_1, RCOMP_1,
XXREAL_1, MEASUR10, ARYTM_1, CARD_3, FINSEQ_1, ORDINAL4, VALUED_0,
SERIES_1, MESFUNC5, SEQ_2, CLASSES1, TOPMETR, STRUCT_0, FINSET_1,
UPROOTS, MEASURE8, SRINGS_3, PROB_2, MEASURE9, NEWTON, COMPLEX1, SEQ_1,
RFINSEQ2, RFINSEQ, MEASURE3, REWRITE1, MEASUR12;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, MESFUNC9, CARD_1,
SEQ_1, SETFAM_1, FUNCOP_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
FINSEQ_1, SEQ_2, SERIES_1, RFINSEQ, CARD_3, SEQ_4, CLASSES1, PROB_2,
VALUED_0, FINSET_1, FUNCT_2, XXREAL_2, EXTREAL1, XXREAL_1, XXREAL_0,
XXREAL_3, XCMPLX_0, COMPLEX1, XREAL_0, NUMBERS, MEASURE3, SUPINF_1,
MEASUR10, SUPINF_2, NAT_1, RCOMP_1, RECDEF_1, MEASURE1, MEASURE4,
MEASURE5, MEASURE7, MESFUNC5, PROB_1, MEASURE8, STRUCT_0, PRE_TOPC,
COMPTS_1, TOPMETR, PROB_3, FUNCT_7, FINSEQ_7, FINSEQOP, SRINGS_3,
MEASURE9, NEWTON;
constructors MEASURE5, RECDEF_1, SUPINF_1, MEASURE6, RCOMP_1, MEASURE7,
MESFUNC9, EXTREAL1, TOPS_2, COMPTS_1, TOPMETR, SIMPLEX0, PROB_3, RVSUM_1,
FINSEQ_7, FINSEQOP, MEASUR11, MEASURE3, SEQ_4, NEWTON, COMSEQ_2, RFINSEQ;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0,
MEMBERED, MEASURE1, VALUED_0, XXREAL_2, FUNCT_1, RELSET_1, MEASURE5,
NAT_1, SIMPLEX0, COMPTS_1, FINSEQ_1, RELAT_1, FINSET_1, XXREAL_0, CARD_1,
MEASURE9, XXREAL_1, FUNCT_7, EXCHSORT, ZFMISC_1, ROUGHS_1, RFINSEQ,
FUNCOP_1, XXREAL_3, DBLSEQ_3, MEASURE3;
requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
begin :: Properties of intervals
theorem :: MEASUR12:1
for A,B be non empty Interval st A is open_interval & B is open_interval &
A \/ B is Interval holds
A \/ B is open_interval & A meets B & (inf A < sup B or inf B < sup A);
theorem :: MEASUR12:2
for A,B be open_interval Subset of REAL st
A meets B holds A \/ B is open_interval Subset of REAL;
theorem :: MEASUR12:3
for A be Interval, B,C be open_interval Subset of REAL
st A c= B \/ C & A meets B & A meets C holds B meets C;
theorem :: MEASUR12:4
for A,B be non empty set, p,q,r,s be R_eal st
A = [.p,q.] & B = [.r,s.] & A misses B holds q < r or s < p;
theorem :: MEASUR12:5
for A,B be non empty set, p,q,r,s be R_eal st
A = [.p,q.] & B = [.r,s.[ & A misses B holds q < r or s <= p;
theorem :: MEASUR12:6
for A,B be non empty set, p,q,r,s be R_eal st
A = [.p,q.] & B = ].r,s.] & A misses B holds q <= r or s < p;
theorem :: MEASUR12:7
for A,B be non empty set, p,q,r,s be R_eal st
A = [.p,q.] & B = ].r,s.[ & A misses B holds q <= r or s <= p;
theorem :: MEASUR12:8
for A,B be non empty set, p,q,r,s be R_eal st
A = [.p,q.[ & B = [.r,s.[ & A misses B holds q <= r or s <= p;
theorem :: MEASUR12:9
for A,B be non empty set, p,q,r,s be R_eal st
A = [.p,q.[ & B = ].r,s.] & A misses B holds q <= r or s < p;
theorem :: MEASUR12:10
for A,B be non empty set, p,q,r,s be R_eal st
A = [.p,q.[ & B = ].r,s.[ & A misses B holds q <= r or s <= p;
theorem :: MEASUR12:11
for A,B be non empty set, p,q,r,s be R_eal st
A = ].p,q.] & B = ].r,s.] & A misses B holds q <= r or s <= p;
theorem :: MEASUR12:12
for A,B be non empty set, p,q,r,s be R_eal st
A = ].p,q.] & B = ].r,s.[ & A misses B holds q <= r or s <= p;
theorem :: MEASUR12:13
for A,B be non empty set, p,q,r,s be R_eal st
A = ].p,q.[ & B = ].r,s.[ & A misses B holds q <= r or s <= p;
theorem :: MEASUR12:14
for A,B be non empty Interval, p,q,r,s be R_eal st
A = [.p,q.] & B = [.r,s.] & A misses B holds not A \/ B is Interval;
theorem :: MEASUR12:15
for A,B be non empty Interval, p,q,r,s be R_eal st
A = [.p,q.] & B = [.r,s.[ & A misses B & A \/ B is Interval
holds p = s & A \/ B = [.r,q.];
theorem :: MEASUR12:16
for A,B be non empty Interval, p,q,r,s be R_eal st
A = [.p,q.] & B = ].r,s.] & A misses B & A \/ B is Interval
holds q = r & A \/ B = [.p,s.];
theorem :: MEASUR12:17
for A,B be non empty Interval, p,q,r,s be R_eal st
A = [.p,q.] & B = ].r,s.[ & A misses B & A \/ B is Interval
holds (p = s & A \/ B = ].r,q.]) or (q = r & A \/ B = [.p,s.[);
theorem :: MEASUR12:18
for A,B be non empty Interval, p,q,r,s be R_eal st
A = [.p,q.[ & B = [.r,s.[ & A misses B & A \/ B is Interval
holds (p = s & A \/ B = [.r,q.[) or (q = r & A \/ B = [.p,s.[);
theorem :: MEASUR12:19
for A,B be non empty Interval, p,q,r,s be R_eal st
A = [.p,q.[ & B = ].r,s.] & A misses B holds not A \/ B is Interval;
theorem :: MEASUR12:20
for A,B be non empty Interval, p,q,r,s be R_eal st
A = [.p,q.[ & B = ].r,s.[ & A misses B & A \/ B is Interval
holds p = s & A \/ B = ].r,q.[;
theorem :: MEASUR12:21
for A,B be non empty Interval, p,q,r,s be R_eal st
A = ].p,q.] & B = ].r,s.] & A misses B & A \/ B is Interval
holds (p = s & A \/ B = ].r,q.]) or (q = r & A \/ B = ].p,s.]);
theorem :: MEASUR12:22
for A,B be non empty Interval, p,q,r,s be R_eal st
A = ].p,q.] & B = ].r,s.[ & A misses B & A \/ B is Interval
holds q = r & A \/ B = ].p,s.[;
theorem :: MEASUR12:23
for A,B be non empty Interval, p,q,r,s be R_eal st
A = ].p,q.[ & B = ].r,s.[ & A misses B holds not A \/ B is Interval;
theorem :: MEASUR12:24
for a,b be Real, I be Subset of R^1 st I = [.a,b.] holds I is compact;
begin :: Tools for extended real sequences
definition :: ExtREAL version of RFINSEQ2:def 1
let f be FinSequence of ExtREAL;
func max_p f -> Nat means
:: MEASUR12:def 1
(len f=0 implies it=0) &
(len f>0 implies it in dom f &
(for i being Nat, r1,r2 being ExtReal
st i in dom f & r1=f.i & r2=f.it holds r1<=r2) &
for j being Nat st j in dom f & f.j=f.it holds it<=j );
end;
definition :: ExtREAL version of RFINSEQ2:def 2
let f be FinSequence of ExtREAL;
func min_p f -> Nat means
:: MEASUR12:def 2
(len f=0 implies it=0) & (len f> 0 implies it in dom f &
(for i being Nat,r1,r2 being ExtReal st i in
dom f & r1=f.i & r2=f.it holds r1>=r2) & for j being Nat st j in dom
f & f.j=f.it holds it<=j );
end;
definition :: ExtREAL version of RFINSEQ2:def 3,def 4
let f be FinSequence of ExtREAL;
func max f -> ExtReal equals
:: MEASUR12:def 3
f.(max_p f);
func min f -> ExtReal equals
:: MEASUR12:def 4
f.(min_p f);
end;
theorem :: MEASUR12:25 :: ExtREAL version of RFINSEQ2:1
for f being FinSequence of ExtREAL,i being Nat st 1<=i &
i<=len f holds f.i<=f.(max_p f) & f.i<=max f;
theorem :: MEASUR12:26 :: ExtREAL version of RFINSEQ2:2
for f being FinSequence of ExtREAL,i being Nat st 1<=i &
i<=len f holds f.i>=f.(min_p f) & f.i>=min f;
theorem :: MEASUR12:27 :: Function version for EXCHSORT:42
for F be Function, x,y be object st x in dom F & y in dom F
holds Swap(F,x,y) = F*Swap(id dom F,x,y);
theorem :: MEASUR12:28
for F be Function, x,y be object st x in dom F & y in dom F holds
F,Swap(F,x,y) are_fiberwise_equipotent;
theorem :: MEASUR12:29
for X be set, F be Function, x,y be object
st not x in X & not y in X holds F|X = Swap(F,x,y)|X;
begin
definition
let A be Subset of REAL;
mode Open_Interval_Covering of A -> Interval_Covering of A means
:: MEASUR12:def 5
for n being Element of NAT holds it.n is open_interval;
end;
definition
let A be Subset of REAL;
let F be Open_Interval_Covering of A;
let n be Element of NAT;
redefine func F.n -> open_interval Subset of REAL;
end;
definition
let F be sequence of bool REAL;
mode Open_Interval_Covering of F -> Interval_Covering of F means
:: MEASUR12:def 6
for n being Element of NAT holds it.n is Open_Interval_Covering of F.n;
end;
definition
let F be sequence of bool REAL;
let H be Open_Interval_Covering of F;
let n be Element of NAT;
redefine func H.n -> Open_Interval_Covering of F.n;
end;
definition
let A be Subset of REAL;
func Svc2(A) -> Subset of ExtREAL means
:: MEASUR12:def 7
for x being R_eal holds x in it
iff ex F being Open_Interval_Covering of A st x = vol(F);
end;
registration
let A be Subset of REAL;
cluster Svc2(A) -> non empty;
end;
theorem :: MEASUR12:30
for A be Subset of REAL holds Svc2 A c= Svc A & inf Svc A <= inf Svc2 A;
theorem :: MEASUR12:31
for F be sequence of bool REAL, G be Open_Interval_Covering of F,
H be sequence of [:NAT,NAT:] st rng H = [:NAT,NAT:] holds
On(G,H) is Open_Interval_Covering of union rng F;
theorem :: MEASUR12:32
for A be Subset of REAL, G be sequence of bool REAL st
A c= union rng G & (for n be Element of NAT holds G.n is open_interval)
holds G is Open_Interval_Covering of A;
theorem :: MEASUR12:33
for F be sequence of bool REAL, G be sequence of Funcs(NAT,bool REAL) st
(for n be Element of NAT holds G.n is Open_Interval_Covering of F.n)
holds G is Open_Interval_Covering of F;
theorem :: MEASUR12:34
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 Open_Interval_Covering of F holds
Ser((On(G,H)) vol).k <= Ser(vol(G)).m;
theorem :: MEASUR12:35
for F being sequence of bool REAL holds
for G being Open_Interval_Covering of F
holds inf Svc2(union rng F) <= SUM(vol(G));
definition
let F be non empty Subset-Family of REAL;
redefine mode Element of F -> Subset of REAL;
end;
theorem :: MEASUR12:36
for A being Element of Family_of_Intervals st A is open_interval holds
ex F being Open_Interval_Covering of A st F.0 = A &
(for n being Nat st n <> 0 holds F.n = {}) & union rng F = A
& SUM(F vol) = diameter A;
theorem :: MEASUR12:37
for A,B be Subset of REAL, F be Interval_Covering of A st B c= A holds
F is Interval_Covering of B;
theorem :: MEASUR12:38
for A,B be Subset of REAL, F be Open_Interval_Covering of A st B c= A holds
F is Open_Interval_Covering of B;
theorem :: MEASUR12:39
for A,B be Subset of REAL, F be Interval_Covering of A,
G be Interval_Covering of B st F = G holds F vol = G vol;
theorem :: MEASUR12:40
for F be FinSequence of bool REAL,k be Nat st
(for n be Nat st n in dom F holds F.n is open_interval Subset of REAL)
& (for n be Nat st 1 <= n < len F holds union rng(F|n) meets F.(n+1))
holds union rng(F|k) is open_interval Subset of REAL;
theorem :: MEASUR12:41
for A be non empty closed_interval Subset of REAL,
F be FinSequence of bool REAL
st A c= union rng F
& (for n be Nat st n in dom F holds A meets F.n)
& (for n be Nat st n in dom F holds F.n is open_interval Subset of REAL)
ex G be FinSequence of bool REAL
st F,G are_fiberwise_equipotent
& (for n be Nat st 1 <= n < len G holds union rng(G|n) meets G.(n+1));
begin :: Measure of intervals by OS_Meas
theorem :: MEASUR12:42
for I be Element of Family_of_Intervals st I is open_interval holds
OS_Meas.I <= diameter I;
theorem :: MEASUR12:43
for I be Element of Family_of_Intervals st I <> {} & I is right_open_interval
holds OS_Meas.I <= diameter I;
theorem :: MEASUR12:44
for I be Element of Family_of_Intervals st I is Interval
holds OS_Meas.I <= diameter I;
theorem :: MEASUR12:45
for A be non empty closed_interval Subset of REAL,
F be FinSequence of bool REAL,
G be FinSequence of ExtREAL st A c= union rng F &
len F = len G &
(for n be Nat st n in dom F holds F.n is open_interval Subset of REAL) &
(for n be Nat st n in dom F holds G.n = diameter(F.n)) &
(for n be Nat st n in dom F holds A meets F.n)
holds diameter A <= Sum G;
theorem :: MEASUR12:46
for X be non empty set, f be sequence of X, i,j be Nat
ex g be sequence of X st
(for n be Nat st n <> i & n <> j holds f.n = g.n)
& f.i = g.j & f.j = g.i;
theorem :: MEASUR12:47
for f,g be sequence of ExtREAL st
f is nonnegative &
(ex N be Nat st (Ser f).N <= (Ser g).N
& (for n be Nat st n > N holds f.n <= g.n))
holds SUM f <= SUM g;
theorem :: MEASUR12:48
for f,g be sequence of ExtREAL, j,k be Nat st
k < j & (for n be Nat st n < j holds f.n = g.n)
holds (Ser f).k = (Ser g).k;
theorem :: MEASUR12:49
for f,g be sequence of ExtREAL, i,j be Nat st
f is nonnegative &
i >= j & (for n be Nat st n <> i & n <> j holds f.n = g.n)
& f.i = g.j & f.j = g.i
holds (Ser f).i = (Ser g).i;
theorem :: MEASUR12:50
for f,g be sequence of ExtREAL, i,j be Nat st
f is nonnegative & f.i = g.j & f.j = g.i
& (for n be Nat st n <> i & n <> j holds f.n = g.n)
holds for n be Nat st n >= i & n >= j holds (Ser f).n = (Ser g).n;
theorem :: MEASUR12:51
for f,g be sequence of ExtREAL, i,j be Nat st
f is nonnegative &
i >= j & (for n be Nat st n <> i & n <> j holds f.n = g.n)
& f.i = g.j & f.j = g.i
holds SUM f = SUM g;
theorem :: MEASUR12:52
for A be Subset of REAL, F1,F2 be Interval_Covering of A, n,m be Nat
st (for k be Nat st k <> n & k <> m holds F1.k = F2.k) &
F1.n = F2.m & F1.m = F2.n holds vol F1 = vol F2;
theorem :: MEASUR12:53
for A be Subset of REAL, F1,F2 be Interval_Covering of A, n,m be Nat
st (for k be Nat st k <> n & k <> m holds F1.k = F2.k) &
F1.n = F2.m & F1.m = F2.n holds
for k be Nat st k >= n & k >= m holds (Ser (F1 vol)).k = (Ser (F2 vol)).k;
theorem :: MEASUR12:54
for X be non empty set, seq be sequence of X, f be FinSequence of X
st rng f c= rng seq holds
ex N be Nat st rng f c= rng(seq|(Segm N));
theorem :: MEASUR12:55
for A be non empty Subset of REAL, F be Interval_Covering of A,
G be one-to-one FinSequence of bool REAL st rng G c= rng F
ex F1 be Interval_Covering of A st
(for n be Nat st n in dom G holds G.n = F1.n) &
vol F1 = vol F;
theorem :: MEASUR12:56
for A be non empty Subset of REAL, F be Interval_Covering of A,
G be one-to-one FinSequence of bool REAL,
H be FinSequence of ExtREAL st
rng G c= rng F & dom G = dom H &
(for n be Nat holds H.n = diameter(G.n)) holds Sum H <= vol F;
theorem :: MEASUR12:57
for I be Interval holds diameter I = OS_Meas.I;
begin :: Construction of the one-dimensional Lebesque measure
definition
let F be FinSequence of Family_of_Intervals;
let n be Nat;
redefine func F.n -> interval Subset of REAL;
end;
definition
func pre-Meas -> nonnegative zeroed Function of Family_of_Intervals,ExtREAL
equals
:: MEASUR12:def 8
OS_Meas|Family_of_Intervals;
end;
theorem :: MEASUR12:58
for I be Element of Family_of_Intervals holds pre-Meas.I = diameter I;
theorem :: MEASUR12:59
for I be Interval holds pre-Meas.I = diameter I;
theorem :: MEASUR12:60
for A,B be Element of Family_of_Intervals
st A misses B & A \/ B is Interval
holds pre-Meas.(A \/ B) = pre-Meas.A + pre-Meas.B;
theorem :: MEASUR12:61
for F be non empty disjoint_valued FinSequence of Family_of_Intervals
st Union F is Interval holds
ex n be Nat st n in dom F & Union F \ F.n is Interval;
theorem :: MEASUR12:62
for A be Interval holds pre-Meas*<*A*> = <*pre-Meas.A*>;
theorem :: MEASUR12:63
for F be disjoint_valued FinSequence of Family_of_Intervals
st Union F in Family_of_Intervals
ex G be disjoint_valued FinSequence of Family_of_Intervals
st F,G are_fiberwise_equipotent
& for n be Nat st n in dom G holds Union(G|n) in Family_of_Intervals
& pre-Meas.(Union(G|n)) = Sum(pre-Meas*(G|n));
theorem :: MEASUR12:64
for F,G be FinSequence of ExtREAL holds
(F is without-infty & G is without-infty implies F^G is without-infty)
& (F is without+infty & G is without+infty implies F^G is without+infty);
theorem :: MEASUR12:65
for F be FinSequence of ExtREAL, k be Nat holds
(F is without-infty implies F/^k is without-infty)
& (F is without+infty implies F/^k is without+infty);
theorem :: MEASUR12:66
for F be FinSequence of ExtREAL holds
(F is without-infty implies Sum F <> -infty)
& (F is without+infty implies Sum F <> +infty);
theorem :: MEASUR12:67 :: ExtREAL version of RFINSEQ:9
for R1,R2 be without-infty FinSequence of ExtREAL
st R1,R2 are_fiberwise_equipotent
holds Sum R1 = Sum R2;
theorem :: MEASUR12:68
for F be disjoint_valued FinSequence of Family_of_Intervals
st Union F in Family_of_Intervals holds
pre-Meas.(Union F) = Sum(pre-Meas*F);
theorem :: MEASUR12:69
for K be disjoint_valued Function of NAT,Family_of_Intervals
st Union K in Family_of_Intervals holds
pre-Meas.(Union K) <= SUM(pre-Meas*K);
definition
redefine func pre-Meas -> pre-Measure of Family_of_Intervals;
end;
definition :: Jordan Measure
func J-Meas -> Measure of Field_generated_by Family_of_Intervals
means
:: MEASUR12:def 9
for A be set st A in Field_generated_by Family_of_Intervals holds
for F be disjoint_valued FinSequence of Family_of_Intervals
st A = Union F holds it.A = Sum(pre-Meas*F);
end;
definition
redefine func J-Meas -> induced_Measure of Family_of_Intervals,pre-Meas;
end;
registration
cluster J-Meas -> completely-additive;
end;
definition :: Borel Measure
func B-Meas -> sigma_Measure of Borel_Sets equals
:: MEASUR12:def 10
(sigma_Meas(C_Meas J-Meas))|Borel_Sets;
end;
theorem :: MEASUR12:70
for A be Interval holds J-Meas.A = diameter A;
theorem :: MEASUR12:71
for A be Interval holds B-Meas.A = diameter A;
theorem :: MEASUR12:72
for A be Interval holds A in Borel_Sets;
definition :: Lebesgue Measure
func L-Field -> SigmaField of REAL equals
:: MEASUR12:def 11
COM (Borel_Sets,B-Meas);
end;
definition
func L-Meas -> sigma_Measure of L-Field equals
:: MEASUR12:def 12
COM B-Meas;
end;
registration
cluster L-Meas -> complete;
end;
theorem :: MEASUR12:73
{} is thin of B-Meas;
theorem :: MEASUR12:74
for a be Real holds {a} is thin of B-Meas;
theorem :: MEASUR12:75
Borel_Sets c= L-Field;
theorem :: MEASUR12:76
for A be Interval holds L-Meas.A = diameter A;