:: Construction of Measure from Semialgebra of Sets :: by Noboru Endou :: :: Received August 14, 2015 :: Copyright (c) 2015-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 NUMBERS, SUBSET_1, CARD_3, FUNCT_1, RELAT_1, FINSEQ_1, XBOOLE_0, ARYTM_3, ARYTM_1, XXREAL_0, CARD_1, TARSKI, NAT_1, ZFMISC_1, ORDINAL4, PROB_1, FINSUB_1, SETFAM_1, PROB_2, MEASURE9, MSSUBFAM, FUNCOP_1, SUPINF_2, VALUED_0, PARTFUN1, MEASURE1, ORDINAL2, SERIES_1, MESFUNC5, SUPINF_1, MEASURE4, SEQ_2, MATRIX_1, QC_LANG1, MATRIXC1, ORDINAL1, PRE_POLY, TREES_1, FINSEQ_3, INCSP_1, FINSEQ_2, XREAL_0, MEASURE8, REAL_1, XCMPLX_0, COMPLEX1, DBLSEQ_1, DBLSEQ_2, MESFUNC9, RFINSEQ, SIMPLEX0, ASYMPT_1, SRINGS_3, DBLSEQ_3, LATTICE5; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSUB_1, CARD_3, NUMBERS, XXREAL_3, BINOP_1, XTUPLE_0, PROB_1, XCMPLX_0, XREAL_0, XXREAL_0, SIMPLEX0, NAT_1, VALUED_0, SUPINF_1, SEQ_1, MEASURE8, FINSEQ_1, FINSEQ_2, FINSEQOP, SUPINF_2, PROB_2, MEASURE1, MEASURE4, MESFUNC1, MESFUNC5, MESFUNC9, MATRIX_0, SEQ_2, SERIES_1, RVSUM_1, RFINSEQ, WSIERP_1, MATRLIN, EXTREAL1, SRINGS_3, DBLSEQ_3; constructors PROB_2, EXTREAL1, SUPINF_1, MESFUNC9, RINFSUP2, FINSEQOP, MATRPROB, MATRLIN, MEASURE6, SEQ_1, MEASURE8, SERIES_1, WSIERP_1, COMSEQ_2, RFINSEQ, SRINGS_3, DBLSEQ_3; registrations XREAL_0, MEMBERED, FUNCT_1, XBOOLE_0, FINSEQ_1, RELAT_1, SUBSET_1, XXREAL_0, ROUGHS_1, NUMBERS, VALUED_0, FUNCT_2, ORDINAL1, RELSET_1, FINSUB_1, MEASURE1, MESFUNC5, MATRLIN, NAT_1, XXREAL_3, CARD_1, PBOOLE, SIMPLEX0, SEQ_2, SEQ_1, SETFAM_1, NUMPOLY1, SRINGS_3, DBLSEQ_3; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; begin :: Join of many finite sequence theorem :: MEASURE9:1 for K be Relation st rng K is empty-membered holds union rng K = {}; theorem :: MEASURE9:2 for K be Function holds rng K is empty-membered iff (for x be object holds K.x = {}); definition let D be set, F be FinSequenceSet of D, f be FinSequence of F, n be Nat; redefine func f.n -> FinSequence of D; end; definition let D be set, Y be FinSequenceSet of D, F be FinSequence of Y; func Length F -> FinSequence of NAT means :: MEASURE9:def 1 dom it = dom F & for n be Nat st n in dom it holds it.n = len(F.n); end; theorem :: MEASURE9:3 for D be set, Y be FinSequenceSet of D, F be FinSequence of Y st (for n be Nat st n in dom F holds F.n = <*>D) holds Sum Length F = 0; theorem :: MEASURE9:4 for D be set, Y be FinSequenceSet of D, F be FinSequence of Y, k be Nat st k < len F holds Length(F|(k+1)) = Length(F|k) ^ <*len(F.(k+1))*>; theorem :: MEASURE9:5 for D be set, Y be FinSequenceSet of D, F be FinSequence of Y, n be Nat st 1 <= n & n <= Sum Length F holds ex k,m be Nat st 1 <= m & m <= len(F.(k+1)) & k < len F & m + Sum Length(F|k) = n & n <= Sum Length(F|(k+1)); theorem :: MEASURE9:6 for D be set, Y be FinSequenceSet of D, F1,F2 be FinSequence of Y holds Length(F1^F2) = (Length F1) ^ (Length F2); theorem :: MEASURE9:7 for D be set, Y be FinSequenceSet of D, F be FinSequence of Y, k1,k2 be Nat st k1 <= k2 holds Sum Length(F|k1) <= Sum Length(F|k2); theorem :: MEASURE9:8 for D be set, Y be FinSequenceSet of D, F be FinSequence of Y, m1,m2,k1,k2 be Nat st 1 <= m1 & 1 <= m2 & m1 + Sum Length(F|k1) = m2 + Sum Length(F|k2) & m1 + Sum Length(F|k1) <= Sum Length(F|(k1+1)) & m2 + Sum Length(F|k2) <= Sum Length(F|(k2+1)) holds m1=m2 & k1=k2; definition let D be non empty set, Y be FinSequenceSet of D, F be FinSequence of Y; func joined_FinSeq F -> FinSequence of D means :: MEASURE9:def 2 len it = Sum Length F & for n be Nat st n in dom it ex k,m be Nat st 1 <= m & m <= len(F.(k+1)) & k < len F & m + Sum Length(F|k) = n & n <= Sum Length(F|(k+1)) & it.n = (F.(k+1)).m; end; definition let D be set, Y be FinSequenceSet of D, s be sequence of Y; func Length s -> sequence of NAT means :: MEASURE9:def 3 for n be Nat holds it.n = len(s.n); end; definition let s be sequence of NAT; redefine func Partial_Sums s -> sequence of NAT; end; registration let D be non empty set; cluster non empty with_non-empty_element for FinSequenceSet of D; end; theorem :: MEASURE9:9 for D be non empty set, Y be non empty with_non-empty_element FinSequenceSet of D, s be non-empty sequence of Y, n be Nat holds len(s.n) >= 1 & n < (Partial_Sums(Length s)).n & (Partial_Sums(Length s)).n < (Partial_Sums(Length s)).(n+1); theorem :: MEASURE9:10 for D be non empty set, Y be non empty with_non-empty_element FinSequenceSet of D, s be non-empty sequence of Y, n be Nat holds ex k,m be Nat st m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m - 1 = n; theorem :: MEASURE9:11 for D be non empty set, Y be non empty with_non-empty_element FinSequenceSet of D, s be non-empty sequence of Y holds Partial_Sums(Length s) is increasing; theorem :: MEASURE9:12 for D be non empty set, Y be non empty with_non-empty_element FinSequenceSet of D, s be non-empty sequence of Y, m1,m2,k1,k2 be Nat st m1 in dom(s.k1) & m2 in dom(s.k2) & (Partial_Sums(Length s)).k1 - len(s.k1) + m1 = (Partial_Sums(Length s)).k2 - len(s.k2) + m2 holds m1=m2 & k1=k2; theorem :: MEASURE9:13 for D be non empty set, Y be with_non-empty_element FinSequenceSet of D, s be non-empty sequence of Y ex N be increasing sequence of NAT st for k be Nat holds N.k = (Partial_Sums(Length s)).k - 1; definition let D be non empty set, Y be with_non-empty_element FinSequenceSet of D, s be non-empty sequence of Y; func joined_seq s -> sequence of D means :: MEASURE9:def 4 for n be Nat ex k,m be Nat st m in dom(s.k) & (Partial_Sums(Length s)).k - len(s.k) + m - 1 = n & it.n = (s.k).m; end; theorem :: MEASURE9:14 for D be non empty set, Y be with_non-empty_element FinSequenceSet of D, s be non-empty sequence of Y, s1 be sequence of D st ( for n be Nat holds s1.n = (joined_seq s).(Partial_Sums(Length s).n - 1) ) holds s1 is subsequence of joined_seq s; theorem :: MEASURE9:15 for D be non empty set, Y be with_non-empty_element FinSequenceSet of D, s be non-empty sequence of Y, k,m be Nat st m in dom(s.k) ex n be Nat st n = (Partial_Sums(Length s)).k - len(s.k) + m - 1 & (joined_seq s).n = (s.k).m; theorem :: MEASURE9:16 for D be non empty set, Y be FinSequenceSet of D, F be FinSequence of Y st ( for n,m be Nat st n <> m holds union rng(F.n) misses union rng(F.m) ) & ( for n be Nat holds F.n is disjoint_valued) holds (joined_FinSeq F) is disjoint_valued; theorem :: MEASURE9:17 for D be non empty set, Y be FinSequenceSet of D, F be FinSequence of Y holds rng(joined_FinSeq F) = union {rng(F.n) where n is Nat : n in dom F}; begin :: Extended real valued matrix definition let x be ext-real number; redefine func <*x*> -> FinSequence of ExtREAL; end; definition let e be FinSequence of ExtREAL*; func Sum e -> FinSequence of ExtREAL means :: MEASURE9:def 5 len it = len e & for k be Nat st k in dom it holds it.k = Sum(e.k); end; definition let M be Matrix of ExtREAL; func SumAll M -> Element of ExtREAL equals :: MEASURE9:def 6 Sum Sum M; end; theorem :: MEASURE9:18 for M be Matrix of ExtREAL holds len Sum M = len M & for i be Nat st i in Seg len M holds (Sum M).i=Sum Line(M,i); theorem :: MEASURE9:19 for F be FinSequence of ExtREAL st for i be Nat st i in dom F holds F.i <> -infty holds Sum F <> -infty; theorem :: MEASURE9:20 for F,G,H be FinSequence of ExtREAL st not -infty in rng F & not -infty in rng G & dom F = dom G & H = F + G holds Sum H = Sum F + Sum G; theorem :: MEASURE9:21 for r be R_eal, F be FinSequence of ExtREAL holds Sum(F^<*r*>) = Sum F + r; theorem :: MEASURE9:22 for r be R_eal, i be Nat st r is real holds Sum(i |-> r) = i*r; theorem :: MEASURE9:23 for M be Matrix of ExtREAL st len M = 0 holds SumAll M = 0; theorem :: MEASURE9:24 for m be Nat, M be Matrix of m,0,ExtREAL holds SumAll M = 0; theorem :: MEASURE9:25 for n,m,k be Nat, M1 be Matrix of n,k,ExtREAL, M2 be Matrix of m,k,ExtREAL holds Sum (M1^M2) = (Sum M1)^(Sum M2); theorem :: MEASURE9:26 for M1,M2 be Matrix of ExtREAL st (for i be Nat st i in dom M1 holds not -infty in rng (M1.i) ) & (for i be Nat st i in dom M2 holds not -infty in rng (M2.i) ) holds Sum M1 + Sum M2 = Sum (M1 ^^ M2); theorem :: MEASURE9:27 for M1,M2 be Matrix of ExtREAL st len M1 = len M2 & (for i be Nat st i in dom M1 holds not -infty in rng (M1.i) ) & (for i be Nat st i in dom M2 holds not -infty in rng (M2.i) ) holds SumAll M1 + SumAll M2 = SumAll(M1 ^^ M2); theorem :: MEASURE9:28 for p be FinSequence of ExtREAL st not -infty in rng p holds SumAll <*p*> = SumAll(<*p*>@); theorem :: MEASURE9:29 for p be ext-real number, M be Matrix of ExtREAL st (for i be Nat st i in dom M holds not p in rng (M.i)) holds (for j be Nat st j in dom (M@) holds not p in rng((M@).j)); theorem :: MEASURE9:30 for M be Matrix of ExtREAL st (for i be Nat st i in dom M holds not -infty in rng (M.i)) holds SumAll M = SumAll(M@); begin :: Definition of pre-measure registration let x be object; cluster <*x*> -> disjoint_valued; end; theorem :: MEASURE9:31 for X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, F be FinSequence of S, G be Element of S ex H be disjoint_valued FinSequence of S st G \ Union F = Union H; registration let X be set, P be with_empty_element semi-diff-closed cap-closed Subset-Family of X; cluster disjoint_valued for sequence of P; end; registration let X be set, P be non empty Subset-Family of X; cluster nonnegative additive zeroed for Function of P,ExtREAL; end; registration let X be set, P be with_empty_element Subset-Family of X; cluster disjoint_valued for Function of NAT,P; end; definition let X be set, P be with_empty_element Subset-Family of X; mode pre-Measure of P -> nonnegative zeroed Function of P,ExtREAL means :: MEASURE9:def 7 ( for F be disjoint_valued FinSequence of P st Union F in P holds it.(Union F) = Sum(it*F) ) & ( for K be disjoint_valued Function of NAT,P st Union K in P holds it.(Union K) <= SUM(it*K) ); end; theorem :: MEASURE9:32 for X be with_empty_element set, F be FinSequence of X holds ex G be Function of NAT,X st (for i be Nat holds F.i = G.i) & Union F = Union G; theorem :: MEASURE9:33 for X be non empty set, F be FinSequence of X, G be Function of NAT,X st (for i be Nat holds F.i = G.i) holds F is disjoint_valued iff G is disjoint_valued; theorem :: MEASURE9:34 for F be FinSequence of ExtREAL, G be ExtREAL_sequence st (for i be Nat holds F.i = G.i) holds F is nonnegative iff G is nonnegative; registration cluster nonnegative for FinSequence of ExtREAL; cluster without-infty for FinSequence of ExtREAL; cluster nonpositive for FinSequence of ExtREAL; cluster without+infty for FinSequence of ExtREAL; cluster nonnegative -> without-infty for FinSequence of ExtREAL; cluster nonpositive -> without+infty for FinSequence of ExtREAL; end; registration let X,Y be non empty set, F be without-infty Function of Y,ExtREAL, G be Function of X,Y; cluster F*G -> without-infty for Function of X,ExtREAL; end; registration let X,Y be non empty set, F be nonnegative Function of Y,ExtREAL, G be Function of X,Y; cluster F*G -> nonnegative for Function of X,ExtREAL; end; theorem :: MEASURE9:35 for a be R_eal holds Sum <*a*> = a; theorem :: MEASURE9:36 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 :: MEASURE9:37 for F be without-infty FinSequence of ExtREAL, G be ExtREAL_sequence st (for i be Nat holds F.i = G.i) holds for i be Nat holds Sum(F|i) = (Partial_Sums G).i; theorem :: MEASURE9:38 for F be without-infty FinSequence of ExtREAL, G be ExtREAL_sequence st (for i be Nat holds F.i = G.i) holds G is summable & Sum F = Sum G; theorem :: MEASURE9:39 for X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, F be disjoint_valued FinSequence of S, R be non empty preBoolean Subset-Family of X st S c= R & Union F in R holds for i be Nat holds Union (F|i) in R; theorem :: MEASURE9:40 for X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, P be pre-Measure of S, F1,F2 be disjoint_valued FinSequence of S st Union F1 in S & Union F1 = Union F2 holds P.(Union F1) = P.(Union F2); theorem :: MEASURE9:41 for S be non empty cap-closed set, F1,F2 be FinSequence of S holds ex Mx be Matrix of len F1,len F2,S st for i,j be Nat st [i,j] in Indices Mx holds Mx*(i,j) = F1.i /\ F2.j; theorem :: MEASURE9:42 for X be set, S be with_empty_element cap-closed Subset-Family of X, F1,F2 be non empty disjoint_valued FinSequence of S, P be nonnegative zeroed Function of S,ExtREAL, Mx be Matrix of len F1,len F2,ExtREAL st Union F1 = Union F2 & ( for i,j be Nat st [i,j] in Indices Mx holds Mx*(i,j) = P.(F1.i /\ F2.j) ) & ( for F be disjoint_valued FinSequence of S st Union F in S holds P.(Union F) = Sum(P*F) ) holds ( for i be Nat st i <= len(P*F1) holds (P*F1).i = (Sum Mx).i ) & Sum(P*F1) = SumAll(Mx); theorem :: MEASURE9:43 for X be set, S be with_empty_element cap-closed Subset-Family of X, F1,F2 be non empty disjoint_valued FinSequence of S, P be nonnegative zeroed Function of S,ExtREAL, Mx be Matrix of len F1,len F2,ExtREAL st Union F1 = Union F2 & ( for i,j be Nat st [i,j] in Indices Mx holds Mx*(i,j) = P.(F1.i /\ F2.j) ) & ( for F be disjoint_valued FinSequence of S st Union F in S holds P.(Union F) = Sum(P*F) ) holds ( for i be Nat st i <= len (P*F2) holds (P*F2).i = (Sum(Mx@)).i ) & Sum(P*F2) = SumAll(Mx@); theorem :: MEASURE9:44 for X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, P be pre-Measure of S, A be set st A in Ring_generated_by S holds for F1,F2 be disjoint_valued FinSequence of S st A = Union F1 & A = Union F2 holds Sum(P*F1) = Sum(P*F2); theorem :: MEASURE9:45 for f1,f2 be FinSequence st f1 is disjoint_valued & f2 is disjoint_valued & union rng f1 misses union rng f2 holds f1^f2 is disjoint_valued; theorem :: MEASURE9:46 for X be set, P be with_empty_element semi-diff-closed Subset-Family of X, M be pre-Measure of P, A,B be set st A in P & B in P & A \ B in P & B c= A holds M.A >= M.B; theorem :: MEASURE9:47 for Y,S be non empty set, F be PartFunc of Y,S, M be Function of S,ExtREAL st M is nonnegative holds M*F is nonnegative; theorem :: MEASURE9:48 for X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, P be pre-Measure of S ex M be nonnegative additive zeroed Function of (Ring_generated_by S),ExtREAL st for A be set st A in Ring_generated_by S holds for F be disjoint_valued FinSequence of S st A = Union F holds M.A = Sum(P*F); theorem :: MEASURE9:49 for X,Y be set, F,G be Function of NAT,bool X st (for i be Nat holds G.i = F.i /\ Y) & Union F = Y holds Union G = Union F; theorem :: MEASURE9:50 for X be set, S be with_empty_element semi-diff-closed cap-closed Subset-Family of X, P be pre-Measure of S ex M be Function of Ring_generated_by S,ExtREAL st M.{} = 0 & for K be disjoint_valued FinSequence of S st Union K in Ring_generated_by S holds M.(Union K) = Sum(P*K); theorem :: MEASURE9:51 for X,Z be set, P be with_empty_element semi-diff-closed cap-closed Subset-Family of X, K be disjoint_valued Function of NAT,Ring_generated_by P st Z = {[n,F] where n is Nat, F is disjoint_valued FinSequence of P : Union F = K.n & (K.n = {} implies F = <*{}*>) } holds proj2 Z is FinSequenceSet of P & (for x be object holds x in rng K iff ex F be FinSequence of P st F in proj2 Z & Union F = x) & proj2 Z is with_non-empty_elements; theorem :: MEASURE9:52 for X be set, P be with_empty_element semi-diff-closed cap-closed Subset-Family of X, K be disjoint_valued Function of NAT,Ring_generated_by P st rng K is with_non-empty_element holds ex Y be non empty FinSequenceSet of P st Y = {F where F is disjoint_valued FinSequence of P : Union F in rng K & F <> {} } & Y is with_non-empty_elements; begin :: Pre-measure on semialgera and construction of measure theorem :: MEASURE9:53 for X,Z be set, P be semialgebra_of_sets of X, K be disjoint_valued Function of NAT,Field_generated_by P st Z = {[n,F] where n is Nat, F is disjoint_valued FinSequence of P : Union F = K.n & (K.n = {} implies F = <*{}*>) } holds proj2 Z is FinSequenceSet of P & (for x be object holds x in rng K iff ex F be FinSequence of P st F in proj2 Z & Union F = x) & proj2 Z is with_non-empty_elements; theorem :: MEASURE9:54 for X be set, S be semialgebra_of_sets of X, P be pre-Measure of S, A be set holds for F1,F2 be disjoint_valued FinSequence of S st A = Union F1 & A = Union F2 holds Sum(P*F1) = Sum(P*F2); theorem :: MEASURE9:55 for X be set, S be semialgebra_of_sets of X, P be pre-Measure of S ex M be Measure of Field_generated_by S st for A be set st A in Field_generated_by S holds for F be disjoint_valued FinSequence of S st A = Union F holds M.A = Sum(P*F); theorem :: MEASURE9:56 for F be ExtREAL_sequence, n be Nat, a be R_eal st (for k be Nat holds F.k = a) holds (Partial_Sums F).n = a*(n+1); theorem :: MEASURE9:57 for X be non empty set, F be sequence of X, n be Nat holds rng(F|Segm(n+1)) = rng(F|Segm n) \/ {F.n}; theorem :: MEASURE9:58 for X be set, S be Field_Subset of X, M be Measure of S, F be Sep_Sequence of S, n be Nat holds union rng(F|Segm(n+1)) in S & Partial_Sums(M*F).n = M.(union rng(F|Segm(n+1))); theorem :: MEASURE9:59 for X be set, S be semialgebra_of_sets of X, P be pre-Measure of S, M be Measure of Field_generated_by S st ( for A be set st A in Field_generated_by S holds for F be disjoint_valued FinSequence of S st A = Union F holds M.A = Sum(P*F) ) holds M is completely-additive; definition let X be set, S be semialgebra_of_sets of X, P be pre-Measure of S; mode induced_Measure of S,P -> Measure of Field_generated_by S means :: MEASURE9:def 8 for A be set st A in Field_generated_by S holds for F be disjoint_valued FinSequence of S st A = Union F holds it.A = Sum(P*F); end; theorem :: MEASURE9:60 for X be set, S be semialgebra_of_sets of X, P be pre-Measure of S, M be induced_Measure of S,P holds M is completely-additive; theorem :: MEASURE9:61 for X be non empty set, S be semialgebra_of_sets of X, P be pre-Measure of S, M be induced_Measure of S,P holds (sigma_Meas(C_Meas M))|(sigma (Field_generated_by S)) is sigma_Measure of sigma Field_generated_by S; definition let X be non empty set, S be semialgebra_of_sets of X, P be pre-Measure of S, M be induced_Measure of S,P; mode induced_sigma_Measure of S,M -> sigma_Measure of sigma Field_generated_by S means :: MEASURE9:def 9 it = (sigma_Meas(C_Meas M))|(sigma (Field_generated_by S)); end; theorem :: MEASURE9:62 for X be non empty set, S be semialgebra_of_sets of X, P be pre-Measure of S, m be induced_Measure of S,P, M be induced_sigma_Measure of S,m holds M is_extension_of m;