:: 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

definition

let p, q be XFinSequence of NAT ;
:: original: ^
redefine func p ^ q -> XFinSequence of NAT ;
coherence
p ^ q is XFinSequence of NAT ;

end;

theorem Th1: :: CATALAN2:1

for D being set
for n being Nat
for pd being XFinSequence of D ex qd being XFinSequence of D st pd = (pd | n) ^ qd

proof end;

definition

let p be XFinSequence of NAT ;

attr p is dominated_by_0 means :: CATALAN2:def 1
( rng p c= {0,1} & ( for k being Nat st k <= dom p holds
2 * (Sum (p | k)) <= k ) );

end;

:: deftheorem defines dominated_by_0 CATALAN2:def 1 :
for p being XFinSequence of NAT 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 NAT st p is dominated_by_0 holds
2 * (Sum (p | k)) <= k

proof end;

theorem Th3: :: CATALAN2:3

for p being XFinSequence of NAT 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 k, m, n 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 Relation-like omega -defined NAT -valued Function-like empty Sequence-like V42() V43() V44() V45() finite nonnegative-yielding V217() dominated_by_0 for set ;

existence
ex b₁ being XFinSequence of NAT st
( b₁ is empty & b₁ is dominated_by_0 )

proof end;

cluster Relation-like omega -defined NAT -valued Function-like non empty Sequence-like V42() V43() V44() V45() finite nonnegative-yielding V217() dominated_by_0 for set ;

existence
ex b₁ being XFinSequence of NAT st
( not b₁ is empty & b₁ 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 m, n 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 NAT 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 NAT 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 NAT 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 NAT 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 k, n being Nat
for p being XFinSequence of NAT 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 NAT 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 NAT 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 NAT 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 NAT st m = min* { N where N is Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } & m > 0 & p is dominated_by_0 holds
ex q being XFinSequence of NAT st
( p | m = ((1 --> 0) ^ q) ^ (1 --> 1) & q is dominated_by_0 )

proof end;

theorem Th15: :: CATALAN2:15

for p being XFinSequence of NAT 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 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 NAT
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 Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } = (2 * k) + (len q)

proof end;

theorem Th17: :: CATALAN2:17

for p being XFinSequence of NAT st p is dominated_by_0 & { N where N is Nat : ( 2 * (Sum (p | N)) = N & N > 0 ) } = {} & len p > 0 holds
ex q being XFinSequence of NAT st
( p = <%0%> ^ q & q is dominated_by_0 )

proof end;

theorem Th18: :: CATALAN2:18

for p being XFinSequence of NAT st p is dominated_by_0 holds
( <%0%> ^ p is dominated_by_0 & { N where N is Nat : ( 2 * (Sum ((<%0%> ^ p) | N)) = N & N > 0 ) } = {} )

proof end;

theorem :: CATALAN2:19

for k being Nat
for p being XFinSequence of NAT st rng p c= {0,1} & (2 * k) + 1 = min* { N where N is Nat : 2 * (Sum (p | N)) > N } holds
p | (2 * k) is dominated_by_0

proof end;

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 NAT st
( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) );

existence
ex b₁ being Subset of ({0,1} ^omega) st
for x being set holds
( x in b₁ iff ex p being XFinSequence of NAT st
( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) )

proof end;

uniqueness
for b₁, b₂ being Subset of ({0,1} ^omega) st ( for x being set holds
( x in b₁ iff ex p being XFinSequence of NAT st
( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) ) ) & ( for x being set holds
( x in b₂ iff ex p being XFinSequence of NAT st
( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines Domin_0 CATALAN2:def 2 :
for n, m being Nat
for b₃ being Subset of ({0,1} ^omega) holds
( b₃ = Domin_0 (n,m) iff for x being set holds
( x in b₃ iff ex p being XFinSequence of NAT st
( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) ) );

theorem Th20: :: CATALAN2:20

for m, n being Nat
for p being XFinSequence of NAT 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 m, n 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 m, n 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 NAT
for n being Nat st rng p c= {0,n} holds
ex q being XFinSequence of NAT 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 -> functional non empty set means :Def3: :: CATALAN2:def 3
for x being set st x in it holds
x is XFinSequence of D;

existence
ex b₁ being functional non empty set st
for x being set st x in b₁ holds
x is XFinSequence of D

proof end;

end;

:: deftheorem Def3 defines OMEGA CATALAN2:def 3 :
for D being set
for b₂ being functional non empty set holds
( b₂ is OMEGA of D iff for x being set st x in b₂ holds
x is XFinSequence of D );

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 -> D -valued Sequence-like finite for Element of F;

coherence
for b₁ being Element of F holds
( b₁ is finite & b₁ is D -valued & b₁ is 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 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 NAT st
( card { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & { N where N is 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 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 NAT 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 m, n being Nat holds card { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((n + 1),m) & { N where N is 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 NAT 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 NAT 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;

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

proof end;

Lm4: for Fr1, Fr2 being XFinSequence of REAL 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 REAL 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 b₁ being Real_Sequence st
for k being Nat ex Fr being XFinSequence of REAL st
( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds
Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = b₁ . k )

proof end;

uniqueness
for b₁, b₂ being Real_Sequence st ( for k being Nat ex Fr being XFinSequence of REAL st
( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds
Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = b₁ . k ) ) & ( for k being Nat ex Fr being XFinSequence of REAL st
( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds
Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = b₂ . k ) ) holds
b₁ = b₂

proof end;

commutativity
for b₁, seq1, seq2 being Real_Sequence st ( for k being Nat ex Fr being XFinSequence of REAL st
( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds
Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = b₁ . k ) ) holds
for k being Nat ex Fr being XFinSequence of REAL st
( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds
Fr . n = (seq2 . n) * (seq1 . (k -' n)) ) & Sum Fr = b₁ . k )

proof end;

end;

:: deftheorem Def4 defines (##) CATALAN2:def 4 :
for seq1, seq2, b₃ being Real_Sequence holds
( b₃ = seq1 (##) seq2 iff for k being Nat ex Fr being XFinSequence of REAL st
( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds
Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = b₃ . k ) );

theorem :: CATALAN2:43

for Fr1, Fr2 being XFinSequence of REAL 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
for Fr1, Fr2 being XFinSequence of REAL 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 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;

reconsider zz = 0 as Nat ;

theorem Th48: :: CATALAN2:48

for seq1, seq2 being Real_Sequence
for n being Nat ex Fr being XFinSequence of REAL 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 REAL 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 REAL ex absFr being XFinSequence of REAL st
( dom absFr = dom Fr & |.(Sum Fr).| <= Sum absFr & ( for i being Nat st i in dom absFr holds
absFr . i = |.(Fr . i).| ) )

proof end;

theorem Th51: :: CATALAN2:51

for seq1 being Real_Sequence st seq1 is summable holds
ex r being Real st
( 0 < r & ( for k being Nat holds |.(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;

theorem :: CATALAN2:54

for r being Real ex Catal being Real_Sequence st
( ( for n being Nat 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) ) ) ) )

proof end;