:: The {C}atalan Numbers. {P}art {II} :: by Karol P\c{a}k :: :: Received October 31, 2006 :: Copyright (c) 2006-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, 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, 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)) );