:: 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 func p ^ 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
proof end;

definition
let p be XFinSequence of ;
attr p 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
proof end;

theorem Th3: :: CATALAN2:3
for p being XFinSequence of st p is dominated_by_0 holds
p . 0 = 0
proof end;

registration
let x be set ;
let k be Nat;
cluster x --> k -> NAT -valued ;
coherence
x --> k is NAT -valued
proof end;
end;

Lm1: for n, m, k being Nat st n <= m holds
(m --> k) | n = n --> k

proof end;

Lm2: for k being Nat holds k --> 0 is dominated_by_0
proof end;

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 )
proof end;
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 )
proof end;
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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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 )
proof end;

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
proof end;

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)
proof end;

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 )
proof end;

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 )
proof end;

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)
proof end;

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 )
proof end;

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 ) } = {} )
proof end;

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
proof end;

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 ) )
proof end;
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
proof end;
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 ) )
proof end;

theorem Th21: :: CATALAN2:21
for n, m being Nat holds Domin_0 (n,m) c= Choose (n,m,1,0)
proof end;

registration
let n, m be Nat;
cluster Domin_0 (n,m) -> finite ;
coherence
Domin_0 (n,m) is finite
proof end;
end;

theorem Th22: :: CATALAN2:22
for n, m being Nat holds
( Domin_0 (n,m) is empty iff 2 * m > n )
proof end;

theorem Th23: :: CATALAN2:23
for n being Nat holds Domin_0 (n,0) = {(n --> 0)}
proof end;

theorem Th24: :: CATALAN2:24
for n being Nat holds card (Domin_0 (n,0)) = 1
proof end;

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) ) )
proof end;

theorem Th26: :: CATALAN2:26
for m, n being Nat st m <= n holds
n choose m > 0
proof end;

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))
proof end;

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)
proof end;

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)
proof end;

theorem Th30: :: CATALAN2:30
for k being Nat holds card (Domin_0 ((2 + k),1)) = k + 1
proof end;

theorem :: CATALAN2:31
for k being Nat holds card (Domin_0 ((4 + k),2)) = ((k + 1) * (k + 4)) / 2
proof end;

theorem :: CATALAN2:32
for k being Nat holds card (Domin_0 ((6 + k),3)) = (((k + 1) * (k + 5)) * (k + 6)) / 6
proof end;

theorem Th33: :: CATALAN2:33
for n being Nat holds card (Domin_0 ((2 * n),n)) = ((2 * n) choose n) / (n + 1)
proof end;

theorem Th34: :: CATALAN2:34
for n being Nat holds card (Domin_0 ((2 * n),n)) = Catalan (n + 1)
proof end;

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
proof end;
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 func D ^omega -> OMEGA of D;
coherence
D ^omega is OMEGA of D
proof end;
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
proof end;

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)))
proof end;

:: 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))))) ) )
proof end;

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 ) } <> {} ) }
proof end;

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)) ) )
proof end;

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))
proof end;

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))))) ) )
proof end;

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)) ) )
proof end;

begin

Lm3: for Fr being XFinSequence of st ( dom Fr = 1 or len Fr = 1 ) holds
Sum Fr = Fr . 0

proof end;

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

proof end;

:: CAUCHY PRODUCT
definition
let seq1, seq2 be Real_Sequence;
func seq1 (##) 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 )
proof end;
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
proof end;
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 )
proof end;
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)
proof end;

theorem :: CATALAN2:45
for seq1, seq2 being Real_Sequence
for r being real number holds seq1 (##) (r (#) seq2) = r (#) (seq1 (##) seq2)
proof end;

theorem :: CATALAN2:46
for seq1, seq2, seq3 being Real_Sequence holds seq1 (##) (seq2 + seq3) = (seq1 (##) seq2) + (seq1 (##) seq3)
proof end;

theorem Th47: :: CATALAN2:47
for seq1, seq2 being Real_Sequence holds (seq1 (##) seq2) . 0 = (seq1 . 0) * (seq2 . 0)
proof end;

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)) ) )
proof end;

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))) ) )
proof end;

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) ) )
proof end;

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 ) )
proof end;

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
proof end;

:: 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) )
proof end;

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) ) ) ) )
proof end;