:: The {C}atalan Numbers. {P}art {II}
:: by Karol P\c{a}k
::
:: Received October 31, 2006
:: Copyright (c) 2006-2016 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, FUNCT_1, NAT_1, TARSKI, ORDINAL1, FINSET_1,
RELAT_1, AFINSQ_1, ARYTM_1, ARYTM_3, FINSEQ_1, XXREAL_0, CARD_1,
XBOOLE_0, ORDINAL4, CARD_3, FINSOP_1, FUNCOP_1, BINOP_2, FUNCT_2, SEQ_1,
SERIES_1, VALUED_1, SQUARE_1, COMPLEX1, PARTFUN3, ZFMISC_1, CARD_FIN,
REALSET1, CATALAN1, REAL_1, ORDINAL2, SEQ_2, NEWTON, PREPOWER, FUNCT_3,
CATALAN2, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, XCMPLX_0, XREAL_0, ORDINAL1,
NUMBERS, RELAT_1, FUNCT_1, REAL_1, NAT_1, FINSET_1, XXREAL_0, NAT_D,
AFINSQ_1, SEQ_1, VALUED_1, RELSET_1, DOMAIN_1, FUNCT_2, FUNCOP_1,
BINOP_1, BINOP_2, RECDEF_1, SERIES_1, PARTFUN3, AFINSQ_2, ZFMISC_1,
SQUARE_1, NEWTON, STIRL2_1, CARD_FIN, CATALAN1, SEQ_2, PREPOWER,
COMPLEX1, QUIN_1;
constructors QUIN_1, PREPOWER, SERIES_1, PARTFUN3, BINOM, WELLORD2, DOMAIN_1,
SETWISEO, REAL_1, NAT_D, YELLOW20, RECDEF_1, BINOP_2, RELSET_1, SQUARE_1,
CATALAN1, STIRL2_1, CARD_FIN, AFINSQ_2, ABIAN, SEQ_2, COMSEQ_2, NUMBERS,
NEWTON;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2,
FUNCOP_1, FINSET_1, FRAENKEL, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1,
BINOP_2, CARD_1, AFINSQ_1, RELSET_1, VALUED_1, VALUED_0, MEMBERED,
NEWTON, AFINSQ_2, SERIES_1, SQUARE_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin
reserve x, x1, x2, y, X, D for set,
i, j, k, l, m, n for Nat,
N for Nat,
p, q for XFinSequence of NAT,
q9 for XFinSequence,
pd, qd for XFinSequence of D;
definition
let p,q;
redefine func p^q -> XFinSequence of NAT;
end;
theorem :: CATALAN2:1
ex qd st pd = (pd|n)^qd;
definition
let p;
attr p is dominated_by_0 means
:: CATALAN2:def 1
rng p c= {0,1} & for k st k <= dom p holds 2*Sum (p|k) <= k;
end;
theorem :: CATALAN2:2
p is dominated_by_0 implies 2*Sum (p|k) <= k;
theorem :: CATALAN2:3
p is dominated_by_0 implies p.0 = 0;
registration let x;let k be Nat;
cluster x-->k -> NAT-valued;
end;
registration
cluster empty dominated_by_0 for XFinSequence of NAT;
cluster non empty dominated_by_0 for XFinSequence of NAT;
end;
theorem :: CATALAN2:4
n-->0 is dominated_by_0;
theorem :: CATALAN2:5
n >= m implies (n-->0)^(m-->1) is dominated_by_0;
theorem :: CATALAN2:6
p is dominated_by_0 implies p|n is dominated_by_0;
theorem :: CATALAN2:7
p is dominated_by_0 & q is dominated_by_0 implies p^q is dominated_by_0;
theorem :: CATALAN2:8
p is dominated_by_0 implies 2 * Sum (p|(2*n+1)) < 2*n+1;
theorem :: CATALAN2:9
p is dominated_by_0 & n <= len p-2*Sum p implies p^(n-->1) is dominated_by_0;
theorem :: CATALAN2:10
p is dominated_by_0 & n <= k+len p-2*Sum p implies (k-->0)^p^(n
-->1) is dominated_by_0;
theorem :: CATALAN2:11
p is dominated_by_0 & 2*Sum (p|k)=k implies k <= len p & len (p| k) = k;
theorem :: CATALAN2:12
p is dominated_by_0 & 2*Sum (p|k) = k & p = (p|k)^q implies q is
dominated_by_0;
theorem :: CATALAN2:13
p is dominated_by_0 & 2*Sum (p|k) = k & k = n+1 implies p|k = p| n^(1-->1);
theorem :: CATALAN2:14
for m,p st m = min*({N:2*Sum(p|N) = N & N > 0}) & m > 0 & p is
dominated_by_0 ex q st p|m = (1-->0)^q^(1-->1) & q is dominated_by_0;
theorem :: CATALAN2:15
for p st rng p c= {0,1} & p is not dominated_by_0 ex k st 2*k+1
= min*{N : 2*Sum(p|N) > N} & 2*k+1 <= dom p & k = Sum (p|(2*k)) & p.(2*k) = 1
;
theorem :: CATALAN2:16
for p, q, k st p|(2*k+len q) = (k-->0)^q^(k-->1) & q is
dominated_by_0 & 2*Sum q = len q & k > 0 holds min*{N:2*Sum(p|N) = N & N > 0} =
2*k+len q;
theorem :: CATALAN2:17
for p st p is dominated_by_0 & {N: 2*Sum(p|N) = N & N > 0} = {}
& len p > 0 ex q st p = <%0%>^q & q is dominated_by_0;
theorem :: CATALAN2:18
p is dominated_by_0 implies <%0%>^p is dominated_by_0 &
{N: 2*Sum((<%0%>^p)|N) = N & N > 0} = {};
theorem :: CATALAN2:19
rng p c= {0,1} & 2*k+1 = min*{N:2*Sum(p|N) > N} implies p|(2*k) is
dominated_by_0;
begin
definition
let n,m be Nat;
func Domin_0(n,m) -> Subset of {0,1}^omega means
:: CATALAN2:def 2
x in it iff ex p be
XFinSequence of NAT st p = x & p is dominated_by_0 & dom p = n & Sum p = m;
end;
theorem :: CATALAN2:20
p in Domin_0(n,m) iff p is dominated_by_0 & dom p = n & Sum p = m;
theorem :: CATALAN2:21
Domin_0(n,m) c= Choose(n,m,1,0);
registration
let n,m;
cluster Domin_0(n,m) -> finite;
end;
theorem :: CATALAN2:22
Domin_0(n,m) is empty iff 2*m > n;
theorem :: CATALAN2:23
Domin_0(n,0) = {n-->0};
theorem :: CATALAN2:24
card Domin_0(n,0) = 1;
theorem :: CATALAN2:25
for p,n st rng p c= {0,n} ex q st len p = len q & rng q c= {0,n}
& (for k st k <= len p holds Sum (p|k)+Sum (q|k) = n*k) & for k st k in len p
holds q.k = n-p.k;
theorem :: CATALAN2:26
m <= n implies n choose m > 0;
theorem :: CATALAN2:27
2*(m+1) <= n implies card (Choose(n,m+1,1,0) \ Domin_0(n,m+1)) =
card Choose(n,m,1,0);
theorem :: CATALAN2:28
2*(m+1) <= n implies card Domin_0(n,m+1) = (n choose (m+1)) - (n choose m);
theorem :: CATALAN2:29
2*m <= n implies card Domin_0(n,m) = (n+1-2*m) / (n+1-m) * (n choose m);
theorem :: CATALAN2:30
card Domin_0(2+k,1) = k+1;
theorem :: CATALAN2:31
card Domin_0(4+k,2) = (k+1)*(k+4)/2;
theorem :: CATALAN2:32
card Domin_0(6+k,3) = (k+1)*(k+5)*(k+6)/6;
theorem :: CATALAN2:33
card Domin_0(2*n,n) = ((2*n) choose n) / (n+1);
theorem :: CATALAN2:34
card Domin_0(2*n,n) = Catalan(n+1);
definition
let D;
mode OMEGA of D -> functional non empty set means
:: CATALAN2:def 3
for x st x in it holds x is XFinSequence of D;
end;
definition
let D;
redefine func D^omega -> OMEGA of D;
end;
registration
let D;
let F be OMEGA of D;
cluster -> finite D-valued Sequence-like for Element of F;
end;
reserve pN, qN for Element of NAT^omega;
theorem :: CATALAN2:35
card {pN:dom pN = 2*n & pN is dominated_by_0} = (2*n) choose n;
theorem :: CATALAN2:36
for n,m,k,j,l st j = n-2*(k+1) & l = m-(k+1) holds card {pN : pN
in Domin_0(n,m) & 2*(k+1) = min*{N:2*Sum(pN|N) = N & N > 0}} = card Domin_0(2*k
,k) * card Domin_0(j,l);
:: THE RECURRENCE RELATION FOR THE CATALAN NUMBERS
theorem :: CATALAN2:37
for n,m st 2*m <= n ex CardF be XFinSequence of NAT st card {pN:
pN in Domin_0(n,m) & {N:2*Sum(pN|N)=N & N > 0}<>{}} = Sum CardF & dom CardF = m
& for j st j < m holds CardF.j = card Domin_0(2*j,j) * card Domin_0(n-'2*(j+1),
m -'(j+1));
theorem :: CATALAN2:38
for n st n > 0 holds Domin_0(2*n,n)={pN:pN in Domin_0(2*n,n) & {
N: 2*Sum(pN|N) = N & N > 0}<>{}};
theorem :: CATALAN2:39
for n st n > 0 ex Catal be XFinSequence of NAT st Sum Catal =
Catalan(n+1) & dom Catal = n & for j st j < n holds Catal.j = Catalan(j+1)*
Catalan(n-'j);
theorem :: CATALAN2:40
card {pN:pN in Domin_0(n+1,m) & {N: 2*Sum(pN|N) = N & N > 0} =
{}} = card Domin_0(n,m);
theorem :: CATALAN2:41
for n,m st 2*m <= n ex CardF be XFinSequence of NAT st card Domin_0(n,
m) = Sum CardF + card Domin_0(n-'1,m) & dom CardF = m & for j st j < m holds
CardF.j = card Domin_0(2*j,j) * card Domin_0(n-'2*(j+1),m-'(j+1));
theorem :: CATALAN2:42
for n,k ex p st Sum p = card Domin_0(2*n+2+k,n+1) & dom p = k+1 & for
i st i <= k holds p.i = card Domin_0(2*n+1+i,n);
begin
reserve seq1,seq2,seq3,seq4 for Real_Sequence,
r,s,e for Real,
Fr,Fr1, Fr2 for XFinSequence of REAL;
:: CAUCHY PRODUCT
definition
let seq1, seq2 be Real_Sequence;
func seq1 (##) seq2 -> Real_Sequence means
:: CATALAN2:def 4
for k be Nat
ex Fr be XFinSequence of REAL
st dom Fr = k+1 &
(for n st n in k+1 holds Fr.n = seq1.n * seq2.(k-'n)) &
Sum Fr = it.k;
commutativity;
end;
theorem :: CATALAN2:43
for Fr1,Fr2 st dom Fr1=dom Fr2 & for n st n in len Fr1 holds Fr1.n=Fr2
.(len Fr1-'(1+n)) holds Sum Fr1 = Sum Fr2;
theorem :: CATALAN2:44
for Fr1,Fr2 st dom Fr1=dom Fr2 & for n st n in len Fr1 holds Fr1
.n=r*Fr2.n holds Sum Fr1 = r*Sum Fr2;
theorem :: CATALAN2:45
seq1 (##) (r(#)seq2) = r(#)(seq1 (##) seq2);
theorem :: CATALAN2:46
seq1 (##) (seq2 + seq3) = (seq1 (##) seq2) + (seq1 (##) seq3);
theorem :: CATALAN2:47
(seq1 (##) seq2).0=seq1.0*seq2.0;
theorem :: CATALAN2:48
for seq1, seq2, n ex Fr st Partial_Sums(seq1 (##) seq2).n = Sum
Fr & dom Fr=n+1 & for i st i in n+1 holds Fr.i=seq1.i * Partial_Sums(seq2).(n-'
i);
theorem :: CATALAN2:49
for seq1, seq2, n st seq2 is summable ex Fr st Partial_Sums(seq1
(##) seq2).n= Sum seq2 * Partial_Sums(seq1).n- Sum Fr & dom Fr=n+1 & for i st i
in n+1 holds Fr.i=seq1.i * Sum (seq2^\(n-'i+1));
theorem :: CATALAN2:50
for Fr ex absFr be XFinSequence of REAL st dom absFr=dom Fr &
|.Sum Fr.| <= Sum absFr & for i st i in dom absFr holds absFr.i=|.Fr.i.|;
theorem :: CATALAN2:51
for seq1 st seq1 is summable ex r st 0 < r & for k holds |.Sum
(seq1^\k).| < r;
theorem :: CATALAN2:52
for seq1, n, m st n <= m & for i holds seq1.i>=0 holds (
Partial_Sums seq1).n <= (Partial_Sums seq1).m;
:: CAUCHY PRODUCT THEOREM
theorem :: CATALAN2:53
for seq1, seq2 st seq1 is absolutely_summable & seq2 is summable
holds seq1 (##) seq2 is summable & Sum(seq1 (##) seq2) = Sum seq1 * Sum seq2;
begin :: THE GENERATING FUNCTION FOR THE CATALAN NUMBERS
theorem :: CATALAN2:54
for r ex Catal be Real_Sequence st (for n holds Catal.n = Catalan(n+1)
* r|^n) & (|.r.| < 1/4 implies Catal is absolutely_summable & Sum Catal = 1 + r
* (Sum Catal) |^ 2 & Sum Catal = 2 / (1 + sqrt(1-4*r)) & (r<>0 implies Sum
Catal = (1 - sqrt(1-4*r)) / (2*r)) );