:: The {C}atalan Numbers. {P}art {II} :: by Karol P\c{a}k :: :: Received October 31, 2006 :: Copyright (c) 2006-2012 Association of Mizar Users begin definition let p, q be XFinSequence of ; :: original:^ redefine funcp ^ q -> XFinSequence of ; coherence p ^ q is XFinSequence of ; end; theorem Th1: :: CATALAN2:1 for D being set for n being Nat for pd being XFinSequence of ex qd being XFinSequence of st pd = (pd | n) ^ qd proofend; definition let p be XFinSequence of ; attrp is dominated_by_0 means :Def1: :: CATALAN2:def 1 ( rng p c= {0,1} & ( for k being Nat st k <= dom p holds 2 * (Sum (p | k)) <= k ) ); end; :: deftheorem Def1 defines dominated_by_0 CATALAN2:def_1_:_ for p being XFinSequence of holds ( p is dominated_by_0 iff ( rng p c= {0,1} & ( for k being Nat st k <= dom p holds 2 * (Sum (p | k)) <= k ) ) ); theorem Th2: :: CATALAN2:2 for k being Nat for p being XFinSequence of st p is dominated_by_0 holds 2 * (Sum (p | k)) <= k proofend; theorem Th3: :: CATALAN2:3 for p being XFinSequence of st p is dominated_by_0 holds p . 0 = 0 proofend; registration let x be set ; let k be Nat; clusterx --> k -> NAT -valued ; coherence x --> k is NAT -valued proofend; end; Lm1: for n, m, k being Nat st n <= m holds (m --> k) | n = n --> k proofend; Lm2: for k being Nat holds k --> 0 is dominated_by_0 proofend; registration cluster empty T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() dominated_by_0 for set ; existence ex b1 being XFinSequence of st ( b1 is empty & b1 is dominated_by_0 ) proofend; cluster non empty T-Sequence-like Relation-like NAT -defined NAT -valued Function-like V35() V36() V37() V38() finite nonnegative-yielding V213() dominated_by_0 for set ; existence ex b1 being XFinSequence of st ( not b1 is empty & b1 is dominated_by_0 ) proofend; end; theorem :: CATALAN2:4 for n being Nat holds n --> 0 is dominated_by_0 by Lm2; theorem Th5: :: CATALAN2:5 for n, m being Nat st n >= m holds (n --> 0) ^ (m --> 1) is dominated_by_0 proofend; theorem Th6: :: CATALAN2:6 for n being Nat for p being XFinSequence of st p is dominated_by_0 holds p | n is dominated_by_0 proofend; theorem Th7: :: CATALAN2:7 for p, q being XFinSequence of st p is dominated_by_0 & q is dominated_by_0 holds p ^ q is dominated_by_0 proofend; theorem Th8: :: CATALAN2:8 for n being Nat for p being XFinSequence of st p is dominated_by_0 holds 2 * (Sum (p | ((2 * n) + 1))) < (2 * n) + 1 proofend; theorem Th9: :: CATALAN2:9 for n being Nat for p being XFinSequence of st p is dominated_by_0 & n <= (len p) - (2 * (Sum p)) holds p ^ (n --> 1) is dominated_by_0 proofend; theorem Th10: :: CATALAN2:10 for n, k being Nat for p being XFinSequence of st p is dominated_by_0 & n <= (k + (len p)) - (2 * (Sum p)) holds ((k --> 0) ^ p) ^ (n --> 1) is dominated_by_0 proofend; theorem Th11: :: CATALAN2:11 for k being Nat for p being XFinSequence of st p is dominated_by_0 & 2 * (Sum (p | k)) = k holds ( k <= len p & len (p | k) = k ) proofend; theorem Th12: :: CATALAN2:12 for k being Nat for p, q being XFinSequence of st p is dominated_by_0 & 2 * (Sum (p | k)) = k & p = (p | k) ^ q holds q is dominated_by_0 proofend; theorem Th13: :: CATALAN2:13 for k, n being Nat for p being XFinSequence of st p is dominated_by_0 & 2 * (Sum (p | k)) = k & k = n + 1 holds p | k = (p | n) ^ (1 --> 1) proofend; theorem Th14: :: CATALAN2:14 for m being Nat for p being XFinSequence of st m = min* { N where N is Element of NAT : ( 2 * (Sum (p | N)) = N & N > 0 ) } & m > 0 & p is dominated_by_0 holds ex q being XFinSequence of st ( p | m = ((1 --> 0) ^ q) ^ (1 --> 1) & q is dominated_by_0 ) proofend; theorem Th15: :: CATALAN2:15 for p being XFinSequence of st rng p c= {0,1} & not p is dominated_by_0 holds ex k being Nat st ( (2 * k) + 1 = min* { N where N is Element of NAT : 2 * (Sum (p | N)) > N } & (2 * k) + 1 <= dom p & k = Sum (p | (2 * k)) & p . (2 * k) = 1 ) proofend; theorem Th16: :: CATALAN2:16 for p, q being XFinSequence of for k being Nat 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 where N is Element of NAT : ( 2 * (Sum (p | N)) = N & N > 0 ) } = (2 * k) + (len q) proofend; theorem Th17: :: CATALAN2:17 for p being XFinSequence of st p is dominated_by_0 & { N where N is Element of NAT : ( 2 * (Sum (p | N)) = N & N > 0 ) } = {} & len p > 0 holds ex q being XFinSequence of st ( p = <%0%> ^ q & q is dominated_by_0 ) proofend; theorem Th18: :: CATALAN2:18 for p being XFinSequence of st p is dominated_by_0 holds ( <%0%> ^ p is dominated_by_0 & { N where N is Element of NAT : ( 2 * (Sum ((<%0%> ^ p) | N)) = N & N > 0 ) } = {} ) proofend; theorem :: CATALAN2:19 for k being Nat for p being XFinSequence of st rng p c= {0,1} & (2 * k) + 1 = min* { N where N is Element of NAT : 2 * (Sum (p | N)) > N } holds p | (2 * k) is dominated_by_0 proofend; begin definition let n, m be Nat; func Domin_0 (n,m) -> Subset of ({0,1} ^omega) means :Def2: :: CATALAN2:def 2 for x being set holds ( x in it iff ex p being XFinSequence of st ( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) ); existence ex b1 being Subset of ({0,1} ^omega) st for x being set holds ( x in b1 iff ex p being XFinSequence of st ( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) ) proofend; uniqueness for b1, b2 being Subset of ({0,1} ^omega) st ( for x being set holds ( x in b1 iff ex p being XFinSequence of st ( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) ) ) & ( for x being set holds ( x in b2 iff ex p being XFinSequence of st ( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines Domin_0 CATALAN2:def_2_:_ for n, m being Nat for b3 being Subset of ({0,1} ^omega) holds ( b3 = Domin_0 (n,m) iff for x being set holds ( x in b3 iff ex p being XFinSequence of st ( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) ) ); theorem Th20: :: CATALAN2:20 for n, m being Nat for p being XFinSequence of holds ( p in Domin_0 (n,m) iff ( p is dominated_by_0 & dom p = n & Sum p = m ) ) proofend; theorem Th21: :: CATALAN2:21 for n, m being Nat holds Domin_0 (n,m) c= Choose (n,m,1,0) proofend; registration let n, m be Nat; cluster Domin_0 (n,m) -> finite ; coherence Domin_0 (n,m) is finite proofend; end; theorem Th22: :: CATALAN2:22 for n, m being Nat holds ( Domin_0 (n,m) is empty iff 2 * m > n ) proofend; theorem Th23: :: CATALAN2:23 for n being Nat holds Domin_0 (n,0) = {(n --> 0)} proofend; theorem Th24: :: CATALAN2:24 for n being Nat holds card (Domin_0 (n,0)) = 1 proofend; theorem Th25: :: CATALAN2:25 for p being XFinSequence of for n being Nat st rng p c= {0,n} holds ex q being XFinSequence of st ( len p = len q & rng q c= {0,n} & ( for k being Nat st k <= len p holds (Sum (p | k)) + (Sum (q | k)) = n * k ) & ( for k being Nat st k in len p holds q . k = n - (p . k) ) ) proofend; theorem Th26: :: CATALAN2:26 for m, n being Nat st m <= n holds n choose m > 0 proofend; theorem Th27: :: CATALAN2:27 for m, n being Nat st 2 * (m + 1) <= n holds card ((Choose (n,(m + 1),1,0)) \ (Domin_0 (n,(m + 1)))) = card (Choose (n,m,1,0)) proofend; theorem Th28: :: CATALAN2:28 for m, n being Nat st 2 * (m + 1) <= n holds card (Domin_0 (n,(m + 1))) = (n choose (m + 1)) - (n choose m) proofend; theorem Th29: :: CATALAN2:29 for m, n being Nat st 2 * m <= n holds card (Domin_0 (n,m)) = (((n + 1) - (2 * m)) / ((n + 1) - m)) * (n choose m) proofend; theorem Th30: :: CATALAN2:30 for k being Nat holds card (Domin_0 ((2 + k),1)) = k + 1 proofend; theorem :: CATALAN2:31 for k being Nat holds card (Domin_0 ((4 + k),2)) = ((k + 1) * (k + 4)) / 2 proofend; theorem :: CATALAN2:32 for k being Nat holds card (Domin_0 ((6 + k),3)) = (((k + 1) * (k + 5)) * (k + 6)) / 6 proofend; theorem Th33: :: CATALAN2:33 for n being Nat holds card (Domin_0 ((2 * n),n)) = ((2 * n) choose n) / (n + 1) proofend; theorem Th34: :: CATALAN2:34 for n being Nat holds card (Domin_0 ((2 * n),n)) = Catalan (n + 1) proofend; definition let D be set ; mode OMEGA of D -> non empty functional set means :Def3: :: CATALAN2:def 3 for x being set st x in it holds x is XFinSequence of ; existence ex b1 being non empty functional set st for x being set st x in b1 holds x is XFinSequence of proofend; end; :: deftheorem Def3 defines OMEGA CATALAN2:def_3_:_ for D being set for b2 being non empty functional set holds ( b2 is OMEGA of D iff for x being set st x in b2 holds x is XFinSequence of ); definition let D be set ; :: original:^omega redefine funcD ^omega -> OMEGA of D; coherence D ^omega is OMEGA of D proofend; end; registration let D be set ; let F be OMEGA of D; cluster -> T-Sequence-like D -valued finite for Element of F; coherence for b1 being Element of F holds ( b1 is finite & b1 is D -valued & b1 is T-Sequence-like ) by Def3; end; theorem :: CATALAN2:35 for n being Nat holds card { pN where pN is Element of NAT ^omega : ( dom pN = 2 * n & pN is dominated_by_0 ) } = (2 * n) choose n proofend; theorem Th36: :: CATALAN2:36 for n, m, k, j, l being Nat st j = n - (2 * (k + 1)) & l = m - (k + 1) holds card { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Element of NAT : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } = (card (Domin_0 ((2 * k),k))) * (card (Domin_0 (j,l))) proofend; :: THE RECURRENCE RELATION FOR THE CATALAN NUMBERS theorem Th37: :: CATALAN2:37 for n, m being Nat st 2 * m <= n holds ex CardF being XFinSequence of st ( card { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & { N where N is Element of NAT : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } = Sum CardF & dom CardF = m & ( for j being Nat st j < m holds CardF . j = (card (Domin_0 ((2 * j),j))) * (card (Domin_0 ((n -' (2 * (j + 1))),(m -' (j + 1))))) ) ) proofend; theorem Th38: :: CATALAN2:38 for n being Nat st n > 0 holds Domin_0 ((2 * n),n) = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((2 * n),n) & { N where N is Element of NAT : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } proofend; theorem Th39: :: CATALAN2:39 for n being Nat st n > 0 holds ex Catal being XFinSequence of st ( Sum Catal = Catalan (n + 1) & dom Catal = n & ( for j being Nat st j < n holds Catal . j = (Catalan (j + 1)) * (Catalan (n -' j)) ) ) proofend; theorem Th40: :: CATALAN2:40 for n, m being Nat holds card { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((n + 1),m) & { N where N is Element of NAT : ( 2 * (Sum (pN | N)) = N & N > 0 ) } = {} ) } = card (Domin_0 (n,m)) proofend; theorem :: CATALAN2:41 for n, m being Nat st 2 * m <= n holds ex CardF being XFinSequence of st ( card (Domin_0 (n,m)) = (Sum CardF) + (card (Domin_0 ((n -' 1),m))) & dom CardF = m & ( for j being Nat st j < m holds CardF . j = (card (Domin_0 ((2 * j),j))) * (card (Domin_0 ((n -' (2 * (j + 1))),(m -' (j + 1))))) ) ) proofend; theorem :: CATALAN2:42 for n, k being Nat ex p being XFinSequence of st ( Sum p = card (Domin_0 ((((2 * n) + 2) + k),(n + 1))) & dom p = k + 1 & ( for i being Nat st i <= k holds p . i = card (Domin_0 ((((2 * n) + 1) + i),n)) ) ) proofend; begin Lm3: for Fr being XFinSequence of st ( dom Fr = 1 or len Fr = 1 ) holds Sum Fr = Fr . 0 proofend; Lm4: for Fr1, Fr2 being XFinSequence of st dom Fr1 = dom Fr2 & ( for n being Nat st n in len Fr1 holds Fr1 . n = Fr2 . ((len Fr1) -' (1 + n)) ) holds Sum Fr1 = Sum Fr2 proofend; :: CAUCHY PRODUCT definition let seq1, seq2 be Real_Sequence; funcseq1 (##) seq2 -> Real_Sequence means :Def4: :: CATALAN2:def 4 for k being Nat ex Fr being XFinSequence of st ( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = it . k ); existence ex b1 being Real_Sequence st for k being Nat ex Fr being XFinSequence of st ( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = b1 . k ) proofend; uniqueness for b1, b2 being Real_Sequence st ( for k being Nat ex Fr being XFinSequence of st ( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = b1 . k ) ) & ( for k being Nat ex Fr being XFinSequence of st ( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = b2 . k ) ) holds b1 = b2 proofend; commutativity for b1, seq1, seq2 being Real_Sequence st ( for k being Nat ex Fr being XFinSequence of st ( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = b1 . k ) ) holds for k being Nat ex Fr being XFinSequence of st ( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds Fr . n = (seq2 . n) * (seq1 . (k -' n)) ) & Sum Fr = b1 . k ) proofend; end; :: deftheorem Def4 defines (##) CATALAN2:def_4_:_ for seq1, seq2, b3 being Real_Sequence holds ( b3 = seq1 (##) seq2 iff for k being Nat ex Fr being XFinSequence of st ( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = b3 . k ) ); theorem :: CATALAN2:43 for Fr1, Fr2 being XFinSequence of st dom Fr1 = dom Fr2 & ( for n being Nat st n in len Fr1 holds Fr1 . n = Fr2 . ((len Fr1) -' (1 + n)) ) holds Sum Fr1 = Sum Fr2 by Lm4; theorem Th44: :: CATALAN2:44 for r being real number for Fr1, Fr2 being XFinSequence of st dom Fr1 = dom Fr2 & ( for n being Nat st n in len Fr1 holds Fr1 . n = r * (Fr2 . n) ) holds Sum Fr1 = r * (Sum Fr2) proofend; theorem :: CATALAN2:45 for seq1, seq2 being Real_Sequence for r being real number holds seq1 (##) (r (#) seq2) = r (#) (seq1 (##) seq2) proofend; theorem :: CATALAN2:46 for seq1, seq2, seq3 being Real_Sequence holds seq1 (##) (seq2 + seq3) = (seq1 (##) seq2) + (seq1 (##) seq3) proofend; theorem Th47: :: CATALAN2:47 for seq1, seq2 being Real_Sequence holds (seq1 (##) seq2) . 0 = (seq1 . 0) * (seq2 . 0) proofend; theorem Th48: :: CATALAN2:48 for seq1, seq2 being Real_Sequence for n being Nat ex Fr being XFinSequence of st ( (Partial_Sums (seq1 (##) seq2)) . n = Sum Fr & dom Fr = n + 1 & ( for i being Nat st i in n + 1 holds Fr . i = (seq1 . i) * ((Partial_Sums seq2) . (n -' i)) ) ) proofend; theorem Th49: :: CATALAN2:49 for seq1, seq2 being Real_Sequence for n being Nat st seq2 is summable holds ex Fr being XFinSequence of st ( (Partial_Sums (seq1 (##) seq2)) . n = ((Sum seq2) * ((Partial_Sums seq1) . n)) - (Sum Fr) & dom Fr = n + 1 & ( for i being Nat st i in n + 1 holds Fr . i = (seq1 . i) * (Sum (seq2 ^\ ((n -' i) + 1))) ) ) proofend; theorem Th50: :: CATALAN2:50 for Fr being XFinSequence of ex absFr being XFinSequence of st ( dom absFr = dom Fr & abs (Sum Fr) <= Sum absFr & ( for i being Nat st i in dom absFr holds absFr . i = abs (Fr . i) ) ) proofend; theorem Th51: :: CATALAN2:51 for seq1 being Real_Sequence st seq1 is summable holds ex r being real number st ( 0 < r & ( for k being Nat holds abs (Sum (seq1 ^\ k)) < r ) ) proofend; theorem Th52: :: CATALAN2:52 for seq1 being Real_Sequence for n, m being Nat st n <= m & ( for i being Nat holds seq1 . i >= 0 ) holds (Partial_Sums seq1) . n <= (Partial_Sums seq1) . m proofend; :: CAUCHY PRODUCT THEOREM theorem Th53: :: CATALAN2:53 for seq1, seq2 being Real_Sequence st seq1 is absolutely_summable & seq2 is summable holds ( seq1 (##) seq2 is summable & Sum (seq1 (##) seq2) = (Sum seq1) * (Sum seq2) ) proofend; begin theorem :: CATALAN2:54 for r being real number ex Catal being Real_Sequence st ( ( for n being Nat holds Catal . n = (Catalan (n + 1)) * (r |^ n) ) & ( abs 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) ) ) ) ) proofend;