:: 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;
:: original: ^

redefine func p ^ q -> XFinSequence of ;

coherence

p ^ q is XFinSequence of ;

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

for n being Nat

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

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

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

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

ex b_{1} being XFinSequence of st

( b_{1} is empty & b_{1} is dominated_by_0 )

ex b_{1} being XFinSequence of st

( not b_{1} is empty & b_{1} is dominated_by_0 )
end;

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 b

( b

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 b

( not b

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

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

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

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

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 )

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

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)

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 )

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 )

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)

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 )

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

( <%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

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;

ex b_{1} being Subset of ({0,1} ^omega) st

for x being set holds

( x in b_{1} iff ex p being XFinSequence of st

( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) )

for b_{1}, b_{2} being Subset of ({0,1} ^omega) st ( for x being set holds

( x in b_{1} 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 b_{2} iff ex p being XFinSequence of st

( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) ) ) holds

b_{1} = b_{2}

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

ex b

for x being set holds

( x in b

( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) )

proof end;

uniqueness for b

( x in b

( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) ) ) & ( for x being set holds

( x in b

( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) ) ) holds

b

proof end;

:: deftheorem Def2 defines Domin_0 CATALAN2:def 2 :

for n, m being Nat

for b_{3} being Subset of ({0,1} ^omega) holds

( b_{3} = Domin_0 (n,m) iff for x being set holds

( x in b_{3} iff ex p being XFinSequence of st

( p = x & p is dominated_by_0 & dom p = n & Sum p = m ) ) );

for n, m being Nat

for b

( b

( x in b

( 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 ) )

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;

registration
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) ) )

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

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)

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)

card (Domin_0 (n,m)) = (((n + 1) - (2 * m)) / ((n + 1) - m)) * (n choose m)

proof end;

definition

let D be set ;

ex b_{1} being non empty functional set st

for x being set st x in b_{1} holds

x is XFinSequence of

end;
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 for x being set st x in it holds

x is XFinSequence of ;

ex b

for x being set st x in b

x is XFinSequence of

proof end;

:: deftheorem Def3 defines OMEGA CATALAN2:def 3 :

for D being set

for b_{2} being non empty functional set holds

( b_{2} is OMEGA of D iff for x being set st x in b_{2} holds

x is XFinSequence of );

for D being set

for b

( b

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

end;
:: original: ^omega

redefine func D ^omega -> OMEGA of D;

coherence

D ^omega is OMEGA of D

proof end;

registration

let D be set ;

let F be OMEGA of D;

coherence

for b_{1} being Element of F holds

( b_{1} is finite & b_{1} is D -valued & b_{1} is T-Sequence-like )
by Def3;

end;
let F be OMEGA of D;

coherence

for b

( b

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

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

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 ) } <> {} ) }

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

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

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

( 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;

ex b_{1} 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 = b_{1} . k )

for b_{1}, b_{2} 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 = b_{1} . 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 = b_{2} . k ) ) holds

b_{1} = b_{2}

for b_{1}, 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 = b_{1} . 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 = b_{1} . k )

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

ex b

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 = b

proof end;

uniqueness for b

( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds

Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = b

( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds

Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = b

b

proof end;

commutativity for b

( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds

Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = b

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 = b

proof end;

:: deftheorem Def4 defines (##) CATALAN2:def 4 :

for seq1, seq2, b_{3} being Real_Sequence holds

( b_{3} = 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 = b_{3} . k ) );

for seq1, seq2, b

( b

( dom Fr = k + 1 & ( for n being Nat st n in k + 1 holds

Fr . n = (seq1 . n) * (seq2 . (k -' n)) ) & Sum Fr = b

theorem :: CATALAN2:43

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)

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)

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

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

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

( 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 ) )

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

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

( 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) ) ) ) )

( ( 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;