:: Set Sequences and Monotone Class
:: by Bo Zhang , Hiroshi Yamazaki and Yatsuka Nakamura
::
:: Received August 12, 2005
:: Copyright (c) 2005-2019 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, NAT_1, XREAL_0, PROB_1, FINSEQ_1, ZFMISC_1, XBOOLE_0,
CARD_1, ARYTM_3, XXREAL_0, ARYTM_1, RELAT_1, SEQ_1, FUNCT_1, SEQ_2,
ORDINAL2, SUBSET_1, COMPLEX1, RPR_1, TARSKI, VALUED_0, EQREL_1, CARD_3,
PROB_2, SERIES_1, XXREAL_2, FINSEQ_2, SETFAM_1, BINOP_2, SETWISEO,
FINSOP_1, SEQM_3, SETLIM_2, PROB_3, SEQ_4, REAL_1;
notations FINSEQ_1, ORDINAL1, CARD_3, REAL_1, RELAT_1, TARSKI, XBOOLE_0,
RVSUM_1, FINSOP_1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, SETFAM_1,
BINOP_1, SETWOP_2, BINOP_2, SETWISEO, NAT_1, FINSEQ_2, COMPLEX1, SEQ_1,
COMSEQ_2, SEQ_2, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, PROB_1, PROB_2,
KURATO_0, SETLIM_2, SEQM_3, SETLIM_1, RINFSUP1, SERIES_1, XXREAL_0;
constructors SETFAM_1, PARTFUN1, SETWISEO, XXREAL_0, REAL_1, NAT_1, BINOP_2,
COMPLEX1, SEQ_2, SEQM_3, PROB_2, FINSOP_1, RVSUM_1, SERIES_1, BINOP_1,
KURATO_0, SETLIM_1, RINFSUP1, SETLIM_2, PROB_1, RELSET_1, SETWOP_2,
COMSEQ_2;
registrations SUBSET_1, ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, PROB_1,
VALUED_0, SEQ_2, FUNCT_2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin
reserve n,m,k,i for Nat,
g,s,t,p for Real,
x,y,z for object, X,Y,Z for set,
A1 for SetSequence of X,
F1 for FinSequence of bool X,
RFin for FinSequence of REAL,
Si for SigmaField of X,
XSeq,YSeq for SetSequence of Si,
Omega for non empty set,
Sigma for SigmaField of Omega,
ASeq,BSeq for SetSequence of Sigma,
P for Probability of Sigma;
theorem :: PROB_3:1
for f being FinSequence holds not 0 in dom f;
theorem :: PROB_3:2
for f being FinSequence holds n in dom f iff n<>0 & n <= len f;
theorem :: PROB_3:3
for f being Real_Sequence st (ex k st for n st k<=n holds f.n=g)
holds f is convergent & lim f = g;
theorem :: PROB_3:4
(P * ASeq).n >= 0;
theorem :: PROB_3:5
ASeq.n c= BSeq.n implies (P * ASeq).n <= (P * BSeq).n;
theorem :: PROB_3:6
ASeq is non-descending implies P * ASeq is non-decreasing;
theorem :: PROB_3:7
ASeq is non-ascending implies P * ASeq is non-increasing;
definition
let X be set, A1 be SetSequence of X;
func Partial_Intersection A1 -> SetSequence of X means
:: PROB_3:def 1
it.0 = A1.0 & for n being Nat holds it.(n+1) = it.n /\ A1.(n+1);
end;
definition
let X be set, A1 be SetSequence of X;
func Partial_Union A1 -> SetSequence of X means
:: PROB_3:def 2
it.0 = A1.0 & for n being Nat holds it.(n+1) = it.n \/ A1.(n+1);
end;
theorem :: PROB_3:8
(Partial_Intersection A1).n c= A1.n;
theorem :: PROB_3:9
A1.n c= (Partial_Union A1).n;
theorem :: PROB_3:10
Partial_Intersection A1 is non-ascending;
theorem :: PROB_3:11
Partial_Union A1 is non-descending;
theorem :: PROB_3:12
for x being object holds
x in (Partial_Intersection A1).n iff for k st k <= n holds x in A1.k;
theorem :: PROB_3:13
x in (Partial_Union A1).n iff ex k st k <= n & x in A1.k;
theorem :: PROB_3:14
Intersection Partial_Intersection A1 = Intersection A1;
theorem :: PROB_3:15
Union Partial_Union A1 = Union A1;
definition
let X be set, A1 be SetSequence of X;
func Partial_Diff_Union A1 -> SetSequence of X means
:: PROB_3:def 3
it.0 = A1.0 &
for n being Nat holds it.(n+1) = A1.(n+1) \ (Partial_Union A1).n;
end;
theorem :: PROB_3:16
x in (Partial_Diff_Union A1).n iff x in A1.n & for k st k < n
holds not x in A1.k;
theorem :: PROB_3:17
(Partial_Diff_Union A1).n c= A1.n;
theorem :: PROB_3:18
(Partial_Diff_Union A1).n c= (Partial_Union A1).n;
theorem :: PROB_3:19
Partial_Union (Partial_Diff_Union A1) = Partial_Union A1;
theorem :: PROB_3:20
Union Partial_Diff_Union A1 = Union A1;
definition
let X,A1;
redefine attr A1 is disjoint_valued means
:: PROB_3:def 4
for m,n st m <> n holds A1. m misses A1.n;
end;
registration let X,A1;
cluster Partial_Diff_Union A1 -> disjoint_valued;
end;
registration
let X be set, Si be SigmaField of X, XSeq be SetSequence of Si;
cluster Partial_Intersection XSeq -> Si-valued;
end;
registration
let X be set, Si be SigmaField of X, XSeq be SetSequence of Si;
cluster Partial_Union XSeq -> Si-valued;
end;
registration
let X be set, Si be SigmaField of X, XSeq be SetSequence of Si;
cluster Partial_Diff_Union XSeq -> Si-valued;
end;
theorem :: PROB_3:21
YSeq = Partial_Intersection XSeq implies YSeq.0 = XSeq.0 & for n
holds YSeq.(n+1) = YSeq.n /\ XSeq.(n+1);
theorem :: PROB_3:22
YSeq = Partial_Union XSeq implies YSeq.0 = XSeq.0 & for n holds YSeq.
(n+1) = YSeq.n \/ XSeq.(n+1);
theorem :: PROB_3:23
(Partial_Intersection XSeq).n c= XSeq.n;
theorem :: PROB_3:24
XSeq.n c= (Partial_Union XSeq).n;
theorem :: PROB_3:25
for x being object holds
x in (Partial_Intersection XSeq).n iff
for k st k <= n holds x in XSeq.k;
theorem :: PROB_3:26
x in (Partial_Union XSeq).n iff ex k st k <= n & x in XSeq.k;
theorem :: PROB_3:27
Partial_Intersection XSeq is non-ascending;
theorem :: PROB_3:28
Partial_Union XSeq is non-descending;
theorem :: PROB_3:29
Intersection Partial_Intersection XSeq = Intersection XSeq;
theorem :: PROB_3:30
Union Partial_Union XSeq = Union XSeq;
theorem :: PROB_3:31
YSeq = Partial_Diff_Union XSeq implies YSeq.0 = XSeq.0 & for n holds
YSeq.(n+1) = XSeq.(n+1) \ (Partial_Union XSeq).n;
theorem :: PROB_3:32
x in (Partial_Diff_Union XSeq).n iff x in XSeq.n & for k st k < n
holds not x in XSeq.k;
theorem :: PROB_3:33
(Partial_Diff_Union XSeq).n c= XSeq.n;
theorem :: PROB_3:34
(Partial_Diff_Union XSeq).n c= (Partial_Union XSeq).n;
theorem :: PROB_3:35
Partial_Union (Partial_Diff_Union XSeq) = Partial_Union XSeq;
theorem :: PROB_3:36
Union Partial_Diff_Union XSeq = Union XSeq;
theorem :: PROB_3:37
(P * Partial_Union ASeq) is non-decreasing;
theorem :: PROB_3:38
(P * Partial_Intersection ASeq) is non-increasing;
theorem :: PROB_3:39
Partial_Sums(P * ASeq) is non-decreasing;
theorem :: PROB_3:40
(P * Partial_Union ASeq).0 = Partial_Sums(P * ASeq).0;
theorem :: PROB_3:41
P * Partial_Union ASeq is convergent & lim (P * Partial_Union
ASeq) = upper_bound (P * Partial_Union ASeq) & lim (P * Partial_Union ASeq)
= P.Union
ASeq;
theorem :: PROB_3:42
ASeq is disjoint_valued implies for n,m st n < m holds (
Partial_Union ASeq).n misses ASeq.m;
theorem :: PROB_3:43
ASeq is disjoint_valued implies (P * Partial_Union ASeq).n =
Partial_Sums(P * ASeq).n;
theorem :: PROB_3:44
ASeq is disjoint_valued implies (P * Partial_Union ASeq) =
Partial_Sums(P * ASeq);
theorem :: PROB_3:45
ASeq is disjoint_valued implies Partial_Sums(P * ASeq) is
convergent & lim Partial_Sums(P * ASeq) = upper_bound Partial_Sums(P * ASeq)
& lim
Partial_Sums(P * ASeq) = P.Union ASeq;
theorem :: PROB_3:46
ASeq is disjoint_valued implies P.(Union ASeq) = Sum(P * ASeq);
definition
let X,F1,n;
redefine func F1.n -> Subset of X;
end;
theorem :: PROB_3:47
ex F1 being FinSequence of bool X st for k st k in dom F1 holds F1.k = X;
theorem :: PROB_3:48
for F1 being FinSequence of bool X holds union rng F1 is Subset of X;
definition
let X be set, F1 be FinSequence of bool X;
redefine func Union F1 -> Subset of X;
end;
theorem :: PROB_3:49
x in Union F1 iff ex k st k in dom F1 & x in F1.k;
definition
let X, F1;
func Complement F1 -> FinSequence of bool X means
:: PROB_3:def 5
len it = len F1 & for n st n in dom it holds it.n = (F1.n)`;
end;
definition
let X, F1;
func Intersection F1 -> Subset of X equals
:: PROB_3:def 6
(Union Complement F1)` if
F1 <> {} otherwise {};
end;
theorem :: PROB_3:50
dom Complement F1 = dom F1;
theorem :: PROB_3:51
for x being object holds
F1 <> {} implies (x in Intersection F1 iff for k st k in dom F1
holds x in F1.k );
theorem :: PROB_3:52
F1 <> {} implies (x in meet rng F1 iff for n st n in dom F1 holds x in F1.n);
theorem :: PROB_3:53
Intersection F1 = meet rng F1;
theorem :: PROB_3:54
for F1 being FinSequence of bool X holds ex A1 being SetSequence
of X st (for k st k in dom F1 holds A1.k = F1.k) & for k st not k in dom F1
holds A1.k = {};
theorem :: PROB_3:55
for F1 being FinSequence of bool X for A1 being SetSequence of X
st (for k st k in dom F1 holds A1.k = F1.k) &
(for k st not k in dom F1 holds A1.k = {})
holds A1.0={} & Union A1 = Union F1;
definition :: czy wystarczy rejestracja?
let X be set, Si be SigmaField of X;
redefine mode FinSequence of Si -> FinSequence of bool X;
end;
definition
let X be set, Si be SigmaField of X, FSi be FinSequence of Si,n;
redefine func FSi.n -> Event of Si;
end;
theorem :: PROB_3:56
for FSi being FinSequence of Si holds ex ASeq being SetSequence
of Si st (for k st k in dom FSi holds ASeq.k = FSi.k) & for k st not k in dom
FSi holds ASeq.k = {};
theorem :: PROB_3:57
for FSi being FinSequence of Si holds Union FSi in Si;
registration
let X be set, S be SigmaField of X, F being FinSequence of S;
cluster Complement F -> S-valued;
end;
theorem :: PROB_3:58
for FSi being FinSequence of Si holds Intersection FSi in Si;
reserve FSeq for FinSequence of Sigma;
theorem :: PROB_3:59
dom(P * FSeq) = dom FSeq;
theorem :: PROB_3:60
P * FSeq is FinSequence of REAL;
definition
let Omega,Sigma,FSeq,P;
redefine func P * FSeq -> FinSequence of REAL;
end;
theorem :: PROB_3:61
len (P * FSeq) = len FSeq;
theorem :: PROB_3:62
len RFin = 0 implies Sum RFin = 0;
theorem :: PROB_3:63
len RFin >= 1 implies ex f being Real_Sequence st f.1 = RFin.1 &
(for n st 0 <> n & n < len RFin holds f.(n+1) = f.n+RFin.(n+1)) & Sum(RFin) = f
.(len RFin);
theorem :: PROB_3:64
for FSeq being FinSequence of Sigma, ASeq being SetSequence of
Sigma st (for k st k in dom FSeq holds ASeq.k = FSeq.k) & (for k st not k in
dom FSeq holds ASeq.k = {}) holds Partial_Sums(P * ASeq) is convergent & Sum(P
* ASeq) = Partial_Sums(P * ASeq).(len FSeq) & P.(Union ASeq) <= Sum(P * ASeq) &
Sum(P * FSeq) = Sum(P * ASeq);
theorem :: PROB_3:65
P.(Union FSeq) <= Sum(P * FSeq) & (FSeq is disjoint_valued implies P.(
Union FSeq) = Sum(P * FSeq));
definition
::$CD 2
let X;
let IT be Subset-Family of X;
attr IT is non-decreasing-closed means
:: PROB_3:def 9
for A1 being SetSequence of X
st A1 is non-descending & rng A1 c= IT holds Union A1 in IT;
attr IT is non-increasing-closed means
:: PROB_3:def 10
for A1 being SetSequence of X
st A1 is non-ascending & rng A1 c= IT holds Intersection A1 in IT;
end;
theorem :: PROB_3:66
for IT be Subset-Family of X holds IT is non-decreasing-closed
iff for A1 being SetSequence of X st A1 is non-descending & rng A1 c= IT holds
lim A1 in IT;
theorem :: PROB_3:67
for IT be Subset-Family of X holds IT is non-increasing-closed
iff for A1 being SetSequence of X st A1 is non-ascending & rng A1 c= IT holds
lim A1 in IT;
theorem :: PROB_3:68
bool X is non-decreasing-closed & bool X is non-increasing-closed;
registration
let X;
cluster non-decreasing-closed non-increasing-closed for Subset-Family of X;
end;
definition
let X;
mode MonotoneClass of X is non-decreasing-closed non-increasing-closed
Subset-Family of X;
end;
theorem :: PROB_3:69
Z is MonotoneClass of X iff Z c= bool X & for A1 being
SetSequence of X st A1 is monotone & rng A1 c= Z holds lim A1 in Z;
theorem :: PROB_3:70
for F being Field_Subset of X holds F is SigmaField of X iff F
is MonotoneClass of X;
theorem :: PROB_3:71
bool Omega is MonotoneClass of Omega;
definition
let Omega;
let X be Subset-Family of Omega;
func monotoneclass(X) -> MonotoneClass of Omega means
:: PROB_3:def 11
X c= it & for Z st X c= Z & Z is MonotoneClass of Omega holds it c= Z;
end;
theorem :: PROB_3:72
for Z being Field_Subset of Omega holds monotoneclass(Z) is
Field_Subset of Omega;
theorem :: PROB_3:73
for Z being Field_Subset of Omega holds sigma Z = monotoneclass Z;