:: 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;