:: Construction of Measure from Semialgebra of Sets
:: by Noboru Endou
::
:: Received August 14, 2015
:: Copyright (c) 2015-2018 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;