:: The {C}atalan Numbers. {P}art {II}
:: by Karol P\c{a}k
::
:: Received October 31, 2006
:: Copyright (c) 2006 Association of Mizar Users

theorem Th1: :: CATALAN2:1

for p', q' being XFinSequence holds (p' ^ q') | (dom p') = p'

proof end;

theorem Th2: :: CATALAN2:2

for n being Element of NAT
for p', q' being XFinSequence st n <= dom p' holds
(p' ^ q') | n = p' | n

proof end;

theorem Th3: :: CATALAN2:3

for n, k being Element of NAT
for p', q' being XFinSequence st n = (dom p') + k holds
(p' ^ q') | n = p' ^ (q' | k)

proof end;

theorem Th4: :: CATALAN2:4

for n being Element of NAT
for p' being XFinSequence ex q' being XFinSequence st p' = (p' | n) ^ q'

proof end;

theorem Th5: :: CATALAN2:5

for D being set
for n being Element of 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 :Def1: :: CATALAN2:def 1
( rng p c= {0 ,1} & ( for k being Element of 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 NAT holds
( p is dominated_by_0 iff ( rng p c= {0 ,1} & ( for k being Element of NAT st k <= dom p holds
2 * (Sum (p | k)) <= k ) ) );

theorem Th6: :: CATALAN2:6

for k being Element of NAT
for p being XFinSequence of NAT st p is dominated_by_0 holds
2 * (Sum (p | k)) <= k

proof end;

theorem Th7: :: CATALAN2:7

for p being XFinSequence of NAT st p is dominated_by_0 holds
p . 0 = 0

proof end;

definition

let k, m be Element of NAT ;
:: original: -->
redefine func k --> m -> XFinSequence of NAT ;
coherence
k --> m is XFinSequence of NAT

proof end;

end;

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

proof end;

Lm2: for k, m being Element of NAT holds Sum (k --> m) = k * m

proof end;

Lm3: for k being Element of NAT holds k --> 0 is dominated_by_0

proof end;

registration

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

proof end;

cluster non empty dominated_by_0 M2( NAT );
existence
ex b₁ being XFinSequence of NAT st
( not b₁ is empty & b₁ is dominated_by_0 )

proof end;

end;

theorem :: CATALAN2:8

for n being Element of NAT holds n --> 0 is dominated_by_0 by Lm3;

Lm4: for p, q being XFinSequence of NAT holds Sum (p ^ q) = (Sum p) + (Sum q)

proof end;

theorem Th9: :: CATALAN2:9

for n, m being Element of NAT st n >= m holds
(n --> 0 ) ^ (m --> 1) is dominated_by_0

proof end;

theorem Th10: :: CATALAN2:10

for n being Element of NAT
for p being XFinSequence of NAT st p is dominated_by_0 holds
p | n is dominated_by_0

proof end;

theorem Th11: :: CATALAN2:11

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 Th12: :: CATALAN2:12

for n being Element of 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 Th13: :: CATALAN2:13

for n being Element of 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 Th14: :: CATALAN2:14

for n, k being Element of 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 Th15: :: CATALAN2:15

for k being Element of 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 Th16: :: CATALAN2:16

for k being Element of 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 Th17: :: CATALAN2:17

for k, n being Element of 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 Th18: :: CATALAN2:18

for m being Element of NAT
for p being XFinSequence of NAT 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 NAT st
( p | m = ((1 --> 0 ) ^ q) ^ (1 --> 1) & q is dominated_by_0 )

proof end;

theorem Th19: :: CATALAN2:19

for p being XFinSequence of NAT st rng p c= {0 ,1} & not p is dominated_by_0 holds
ex k being Element of 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 Th20: :: CATALAN2:20

for p, q being XFinSequence of NAT
for k being Element of 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 Th21: :: CATALAN2:21

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

proof end;

theorem Th22: :: CATALAN2:22

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

proof end;

theorem :: CATALAN2:23

for k being Element of NAT
for p being XFinSequence of NAT st rng p c= {0 ,1} & not p is dominated_by_0 & (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;

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 Th24: :: CATALAN2:24

for n, m being Element of 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 Th25: :: CATALAN2:25

for n, m being Element of NAT holds Domin_0 n,m c= Choose n,m,1,0

proof end;

registration

let n, m be Element of NAT ;
cluster Domin_0 n,m -> finite ;
coherence
Domin_0 n,m is finite

proof end;

end;

theorem Th26: :: CATALAN2:26

for n, m being Element of NAT holds
( Domin_0 n,m is empty iff 2 * m > n )

proof end;

theorem Th27: :: CATALAN2:27

for n being Element of NAT holds Domin_0 n,0 = {(n --> 0 )}

proof end;

theorem Th28: :: CATALAN2:28

for n being Element of NAT holds card (Domin_0 n,0 ) = 1

proof end;

theorem Th29: :: CATALAN2:29

for p being XFinSequence of NAT
for n being Element of 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 Element of NAT st k <= len p holds
(Sum (p | k)) + (Sum (q | k)) = n * k ) & ( for k being Element of NAT st k in len p holds
q . k = n - (p . k) ) )

proof end;

theorem Th30: :: CATALAN2:30

for m, n being Element of NAT st m <= n holds
n choose m > 0

proof end;

theorem Th31: :: CATALAN2:31

for m, n being Element of 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 Th32: :: CATALAN2:32

for m, n being Element of NAT st 2 * (m + 1) <= n holds
card (Domin_0 n,(m + 1)) = (n choose (m + 1)) - (n choose m)

proof end;

theorem Th33: :: CATALAN2:33

for m, n being Element of NAT st 2 * m <= n holds
card (Domin_0 n,m) = (((n + 1) - (2 * m)) / ((n + 1) - m)) * (n choose m)

proof end;

theorem Th34: :: CATALAN2:34

for k being Element of NAT holds card (Domin_0 (2 + k),1) = k + 1

proof end;

theorem :: CATALAN2:35

for k being Element of NAT holds card (Domin_0 (4 + k),2) = ((k + 1) * (k + 4)) / 2

proof end;

theorem :: CATALAN2:36

for k being Element of NAT holds card (Domin_0 (6 + k),3) = (((k + 1) * (k + 5)) * (k + 6)) / 6

proof end;

theorem Th37: :: CATALAN2:37

for n being Element of NAT holds card (Domin_0 (2 * n),n) = ((2 * n) choose n) / (n + 1)

proof end;

theorem Th38: :: CATALAN2:38

for n being Element of NAT holds card (Domin_0 (2 * n),n) = Catalan (n + 1)

proof end;

Lm5: for D being set holds D ^omega is functional

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 D;
existence
ex b₁ being non empty functional 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 non empty functional 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;

let F be OMEGA of D;
:: original: Element
redefine mode Element of F -> XFinSequence of D;
coherence
for b₁ being Element of F holds b₁ is XFinSequence of D by Def3;

end;

theorem :: CATALAN2:39

for n being Element of 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 Th40: :: CATALAN2:40

for n, m, k, j, l being Element of 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* { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } ) } = (card (Domin_0 (2 * k),k)) * (card (Domin_0 j,l))

proof end;

theorem Th41: :: CATALAN2:41

for n, m being Element of 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 & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } <> {} ) } = Sum CardF & dom CardF = m & ( for j being Element of 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 Th42: :: CATALAN2:42

for n being Element of 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 & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } <> {} ) }

proof end;

theorem Th43: :: CATALAN2:43

for n being Element of NAT st n > 0 holds
ex Catal being XFinSequence of NAT st
( Sum Catal = Catalan (n + 1) & dom Catal = n & ( for j being Element of NAT st j < n holds
Catal . j = (Catalan (j + 1)) * (Catalan (n -' j)) ) )

proof end;

theorem Th44: :: CATALAN2:44

for n, m being Element of NAT holds card { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n + 1),m & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } = {} ) } = card (Domin_0 n,m)

proof end;

theorem :: CATALAN2:45

for n, m being Element of 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 Element of 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:46

for n, k being Element of 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 Element of NAT st i <= k holds
p . i = card (Domin_0 (((2 * n) + 1) + i),n) ) )

proof end;

definition

let Fr be XFinSequence of REAL ;
func Sum Fr -> Real equals :: CATALAN2:def 4
addreal "**" Fr;
coherence
addreal "**" Fr is Real ;

end;

:: deftheorem defines Sum CATALAN2:def 4 :

for Fr being XFinSequence of REAL holds Sum Fr = addreal "**" Fr;

Lm6: for Fr being XFinSequence of REAL st dom Fr = 0 holds
Sum Fr = 0

proof end;

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

proof end;

Lm8: for Fr being XFinSequence of REAL
for n being Element of NAT st n in dom Fr holds
(Sum (Fr | n)) + (Fr . n) = Sum (Fr | (n + 1))

proof end;

Lm9: for Fr1, Fr2 being XFinSequence of REAL st dom Fr1 = dom Fr2 & ( for n being Element of NAT st n in len Fr1 holds
Fr1 . n = Fr2 . ((len Fr1) -' (1 + n)) ) holds
Sum Fr1 = Sum Fr2

proof end;

definition

let seq1, seq2 be Real_Sequence;
func seq1 (##) seq2 -> Real_Sequence means :Def5: :: CATALAN2:def 5
for k being Nat ex Fr being XFinSequence of REAL st
( dom Fr = k + 1 & ( for n being Element of 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of NAT st n in k + 1 holds
Fr . n = (seq2 . n) * (seq1 . (k -' n)) ) & Sum Fr = b₁ . k )

proof end;

end;

:: deftheorem Def5 defines (##) CATALAN2:def 5 :

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 Element of NAT st n in k + 1 holds
Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = b₃ . k ) );

theorem :: CATALAN2:47

for Fr being XFinSequence of REAL
for n being Element of NAT st n in dom Fr holds
(Sum (Fr | n)) + (Fr . n) = Sum (Fr | (n + 1)) by Lm8;

theorem :: CATALAN2:48

for Fr1, Fr2 being XFinSequence of REAL st dom Fr1 = dom Fr2 & ( for n being Element of NAT st n in len Fr1 holds
Fr1 . n = Fr2 . ((len Fr1) -' (1 + n)) ) holds
Sum Fr1 = Sum Fr2 by Lm9;

theorem Th49: :: CATALAN2:49

for r being real number
for Fr1, Fr2 being XFinSequence of REAL st dom Fr1 = dom Fr2 & ( for n being Element of NAT st n in len Fr1 holds
Fr1 . n = r * (Fr2 . n) ) holds
Sum Fr1 = r * (Sum Fr2)

proof end;

theorem :: CATALAN2:50

for seq1, seq2 being Real_Sequence
for r being real number holds seq1 (##) (r (#) seq2) = r (#) (seq1 (##) seq2)

proof end;

theorem :: CATALAN2:51

for seq1, seq2, seq3 being Real_Sequence holds seq1 (##) (seq2 + seq3) = (seq1 (##) seq2) + (seq1 (##) seq3)

proof end;

theorem Th52: :: CATALAN2:52

for seq1, seq2 being Real_Sequence holds (seq1 (##) seq2) . 0 = (seq1 . 0 ) * (seq2 . 0 )

proof end;

theorem Th53: :: CATALAN2:53

for seq1, seq2 being Real_Sequence
for n being Element of NAT ex Fr being XFinSequence of REAL st
( (Partial_Sums (seq1 (##) seq2)) . n = Sum Fr & dom Fr = n + 1 & ( for i being Element of NAT st i in n + 1 holds
Fr . i = (seq1 . i) * ((Partial_Sums seq2) . (n -' i)) ) )

proof end;

theorem Th54: :: CATALAN2:54

for seq1, seq2 being Real_Sequence
for n being Element of 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 Element of NAT st i in n + 1 holds
Fr . i = (seq1 . i) * (Sum (seq2 ^\ ((n -' i) + 1))) ) )

proof end;

theorem Th55: :: CATALAN2:55

for Fr being XFinSequence of REAL ex absFr being XFinSequence of REAL st
( dom absFr = dom Fr & abs (Sum Fr) <= Sum absFr & ( for i being Element of NAT st i in dom absFr holds
absFr . i = abs (Fr . i) ) )

proof end;

theorem Th56: :: CATALAN2:56

for seq1 being Real_Sequence st seq1 is summable holds
ex r being real number st
( 0 < r & ( for k being Element of NAT holds abs (Sum (seq1 ^\ k)) < r ) )

proof end;

theorem Th57: :: CATALAN2:57

for seq1 being Real_Sequence
for n, m being Element of NAT st n <= m & ( for i being Element of NAT holds seq1 . i >= 0 ) holds
(Partial_Sums seq1) . n <= (Partial_Sums seq1) . m

proof end;

theorem Th58: :: CATALAN2:58

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 Th59: :: CATALAN2:59

for p being XFinSequence of NAT
for Fr being XFinSequence of REAL st p = Fr holds
Sum p = Sum Fr

proof end;

theorem :: CATALAN2:60

for r being real number ex Catal being Real_Sequence st
( ( for n being Element of 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;