(* These packages have to be downloaded from 
http://www.risc.jku.at/research/combinat/software/ergosum/ *)
<<RISC`HolonomicFunctions`;
<<RISC`Guess`;
SetDirectory[NotebookDirectory[]];

HolonomicFunctions Package version 1.7.3 (21-Mar-2017)
written by Christoph Koutschan
Copyright Research Institute for Symbolic Computation (RISC),
Johannes Kepler University, Linz, Austria

Guess Package version 0.52
written by Manuel Kauers
Copyright Research Institute for Symbolic Computation (RISC),
Johannes Kepler University, Linz, Austria

Code

(* Display all relevant information about an annihilator ideal. *)
AnnInfo[ann_]:=With[{vars=First/@OreAlgebra[ann][[1]]},Print[
"ByteCount: ",ByteCount[ann],
"\nSupport: ",Support[ann],
"\ndegree "<>ToString[vars]<>": ",Exponent[#,vars]&/@ann,
"\nStandard Monomials: ",UnderTheStaircase[ann],
"\nHolonomic Rank: ",Length[UnderTheStaircase[ann]]
]];

InitializeDeterminantProof[f_,e_,{a_,b_,c_,d_},cf_]:=
InitializeDeterminantProof[f,e,{a,b,c,d},cf,"det"<>ToString[f]<>StringJoin@@Riffle[ToString/@{e,a,b,c,d},"_"]<>"/"];
InitializeDeterminantProof[f_,e_,{a_,b_,c_,d_},cf_,path_]:=(
Clear[mya,mya1,mya2,myb,myc,datac,annc,id2ct1,id2ct2,id3ct1,id3ct2];
(* Define the entries a_{i,j} of the matrix A_n. *)
mya1[i_,j_]:=e^(i+b)*Binomial[i+f j+c,f j+a];mya2[i_,j_]:=Binomial[-i+f j+d,f j+a];mya[i_,j_]:=mya1[i,j]+mya2[i,j];
mya[i_Integer,j_Integer]:=FunctionExpand[mya1[i,j]+mya2[i,j]];
(* Define the conjectured evaluation b_n of det(A_n). *)
myb[0]=1;
SetDelayed@@(Hold[myb[n_],If[IntegerQ[n],FunctionExpand[C/.prod->Product],C]]/.C->cf);
(* Compute c_{n,j} for concrete integers n and j. *)
datac[n_Integer]:=datac[n]=
With[{ns=NullSpace[Table[mya[i,j],{i,0,n-2},{j,0,n-1}]][[1]]},Together[ns/Last[ns]]];
myc[n_Integer,j_Integer]:=Which[n==1&&j==0,1,j≥n,0,True,datac[n][[j+1]]];
(* Load the precomputed proof certificates. *)
{annc,id2ct1,id2ct2,id3ct1,id3ct2}=Get[path<>#<>".m"]&/@{"annc","id2_ct1","id2_ct2","id3_ct1","id3_ct2"};
Print["We are going to prove the following determinant evaluation:"];
start=CurrentDate[];
TraditionalForm[HoldForm@@{Subscript[det,0≤i,j<n][mya[i,j]]==myb[n]}/.prod->Product]
)

(* A straight-forward implementation of reduction modulo a left ideal in the shift algebra. *)
(* Reason: the built-in procedure "OreReduce" in the HolonomicFunctions package sometimes
causes Mathematica to crash. *)
SortLex[m1_,m2_]:=With[{f1=First[m1],f2=First[m2]},If[f1=!=f2||Length[m1]===1,f1>f2,SortLex[Rest[m1],Rest[m2]]]];
SortDLex[m1_,m2_]:=With[{w1=Plus@@m1,w2=Plus@@m2},If[w1===w2,SortLex[m1,m2],w1>w2]];
Add[p1_List,p2_List]:=
Module[{p={},c,i1=1,i2=1,l1=Length[p1],l2=Length[p2],e1,e2},
While[i1≤l1&&i2≤l2,
{e1,e2}={p1[[i1,2]],p2[[i2,2]]};
Which[
e1===e2,If[(c=p1[[i1,1]]+p2[[i2,1]])=!=0,AppendTo[p,{c,e1}]];i1++;i2++;
,
SortDLex[e1,e2],AppendTo[p,p1[[i1]]];i1++;
,
SortDLex[e2,e1],AppendTo[p,p2[[i2]]];i2++;
];
];
If[i1≤l1,p=Join[p,Take[p1,{i1,l1}]]];
If[i2≤l2,p=Join[p,Take[p2,{i2,l2}]]];
Return[p];
];
ScalarMult[s_,p_List]:={Expand[Together[s*#1]],#2}&@@@p;
OreReduce1[p_List,g_List]:=OreReduce1[#,g]&/@p;
OreReduce1[p1_OrePolynomial,g1:{(_OrePolynomial)..}]:=
Module[{p=p1,g=g1,v,e,f,f1,r={},k,gk,gcd},
v=First/@OreAlgebra[p][[1]];
{p,g}={First[p],First/@g};
f=PolynomialLCM@@(Denominator[First[#]]&/@p);
p=ScalarMult[f,p];
While[p=!={},
k=1;
While[Min[e=(p[[1,2]]-g[[k,1,2]])]<0,k++];
If[k>Length[g],
AppendTo[r,p[[1]]];
p=Rest[p];
,
gk={Expand[#1/.Thread[v->(v+e)]],#2+e}&@@@g[[k]];
gcd=PolynomialGCD[p[[1,1]],gk[[1,1]]];
f*=(f1=Together[gk[[1,1]]/gcd]);
gk=ScalarMult[Together[-p[[1,1]]/gcd],Rest[gk]];
p=Add[ScalarMult[f1,Rest[p]],gk];
];
];
Return[OrePolynomial[{Together[#1/f],#2}&@@@r,p1[[2]],p1[[3]]]];
];

prodsimp={prod[a_,{i_,b_}]->prod[a,{i,1,b}],
prod[a_,{i_,b0_,b1_}]/prod[a_,{i_,b0_,b2_}]/;IntegerQ[Expand[b1-b2]]:>If[Expand[b1-b2]≥0,Product[a,{i,b2+1,b1}],1/Product[a,{i,b1+1,b2}]],
prod[a1_,b_]^e1_.*prod[a2_,b_]^e2_.:>prod[FunctionExpand[a1^e1*a2^e2],b]};

det1a: A warmup exercise

(* Define the matrix entries a_{i,j} and display the matrix A_4. *)
mya[i_,j_]:=FunctionExpand[a^i*Binomial[x+i+j-1,j]+Binomial[x-i+j-1,j]];
TableForm[Table[mya[i,j],{i,0,3},{j,0,3}]]

(* Test the conjectured identity. *)
Table[Together[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/(2(a-1)^Binomial[n,2])],{n,8}]

Holonomic description of (Subscript[c, n,j])

(* Define and display the normalized cofactors c_{n,j}. *)
datac[n_Integer]:=datac[n]=
With[{ns=NullSpace[Table[mya[i,j],{i,0,n-2},{j,0,n-1}]][[1]]},Together[ns/Last[ns]]];
myc[n_Integer,j_Integer]:=Which[n==1&&j==0,1,j≥n,0,True,datac[n][[j+1]]];
TableForm[Table[myc[n,j],{n,4},{j,0,n-1}]]

Table[myc[n,j],{n,4},{j,0,3}]

guess=GuessMultRE[Table[myc[n,j],{n,10},{j,0,9}],{c[n,j],c[n,j+1],c[n+1,j],c[n+1,j+1]},{n,j},2,StartPoint->{1,0},Constraints->(j<n)]

annc=OreGroebnerBasis[NormalizeCoefficients/@ToOrePolynomial[guess,c[n,j]]];
Factor[annc]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[Together[test],{n,6},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
Select[AnnihilatorSingularities[annc,{1,0}],FreeQ[#,x|a]&]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,a^i*Binomial[x+i+j-1,j]];
annSmnd2=DFiniteTimesHyper[annci,Binomial[x-i+j-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

Timing[ByteCount/@(id2ct1=FindCreativeTelescoping[annSmnd1,S[j]-1])]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

Timing[ByteCount/@(id2ct2=FindCreativeTelescoping[annSmnd2,S[j]-1])]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

Factor[id2ann]

(* We are required to check initial values at the following indices: *)
Select[AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1],FreeQ[#,x|a]&]

(* Check a few (more than necessary) initial values. *)
Table[Together[Sum[mya[i,j]*myc[n,j],{j,0,n-1}]],{n,6},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,a^(n-1)*Binomial[x+n+j-2,j]];
annSmnd2=DFiniteTimesHyper[annc,Binomial[x-n+j,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

Timing[ByteCount/@(id3ct1=FindCreativeTelescoping[annSmnd1,S[j]-1])]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

Timing[ByteCount/@(id3ct2=FindCreativeTelescoping[annSmnd2,S[j]-1])]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

Factor[id3ann]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
ApplyOreOperator[id3ann,(a-1)^(n-1)]//Simplify

(* Alternatively: *)
OreReduce[id3ann,Annihilator[(a-1)^(n-1),S[n]]]

(* Compare initial values. *)
Table[Together[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]/(a-1)^(n-1)],{n,2,3}]

detdf: Di Francesco’s determinant

InitializeDeterminantProof[2,2,{1,0,1,1},2 prod[(((2^(i-1)) (4i-2)!)/((n+2i-1)!)),{i,1,n}],"detdf/"]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce1[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

det22: Variations I (Theorem 10)

{0,1,-5,-7}

InitializeDeterminantProof[2,2,{0,1,-5,-7},-168 prod[((Gamma[(1/2) (-1+i)] Gamma[-9+4 i])/(Gamma[-(7/2)+((3 i)/2)] Gamma[-6+3 i])),{i,3,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,5,15},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{5,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Check that the leading coefficient does not have any positive integer roots. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Look at the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{5,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Check that the leading coefficient does not have any positive integer roots. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,5,4+LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{0,1,-4,-6}

InitializeDeterminantProof[2,2,{0,1,-4,-6},40 prod[((Gamma[(i/2)] Gamma[-8+4 i])/(Gamma[-2+((3 i)/2)] Gamma[-6+3 i])),{i,3,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,4,12},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{4,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{4,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,4,3+LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{0,1,-3,-5}

InitializeDeterminantProof[2,2,{0,1,-3,-5},-10 prod[(((-3+2 i) Gamma[(1/2) (-1+i)] Gamma[-7+4 i])/(Gamma[(1/2) (-5+3 i)] Gamma[-4+3 i])),{i,3,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,2,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Check that the leading coefficient does not have any positive integer roots. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Look at the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Check that the leading coefficient does not have any positive integer roots. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,3,2+LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{0,1,-2,-4}

InitializeDeterminantProof[2,2,{0,1,-2,-4},3 prod[((Gamma[(i/2)] Gamma[-5+4 i])/(Gamma[3 (-1+i)] Gamma[(1/2) (-4+3 i)])),{i,2,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{0,1,1,-1}

InitializeDeterminantProof[2,2,{0,1,1,-1},3 prod[((Gamma[(1/2) (-1+i)] Gamma[4 i])/(Gamma[(3/2) (-1+i)] Gamma[1+3 i])),{i,2,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{0,2,-5,-9}

InitializeDeterminantProof[2,2,{0,2,-5,-9},-3696 prod[((Gamma[(1/2) (-1+i)] Gamma[-9+4 i])/(Gamma[3 (-2+i)] Gamma[(1/2) (-7+3 i)])),{i,3,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,5,15},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{5,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{5,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,5,4+LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{0,2,3,-1}

InitializeDeterminantProof[2,2,{0,2,3,-1},prod[((3 (-1+2 i) Gamma[((1+i)/2)] Gamma[3+4 i])/(4 (2+i) Gamma[1+3 i] Gamma[(1/2) (5+3 i)])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{1,1,-2,-4}

InitializeDeterminantProof[2,2,{1,1,-2,-4},-32 prod[((Gamma[(i/2)] Gamma[-5+4 i])/(Gamma[3 (-1+i)] Gamma[(1/2) (-4+3 i)])),{i,2,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,4,14},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{4,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{4,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,4,3+LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{1,1,-1,-3}

InitializeDeterminantProof[2,2,{1,1,-1,-3},8 prod[((Gamma[(1/2) (-1+i)] Gamma[-4+4 i])/(3 Gamma[(3/2) (-1+i)] Gamma[-3+3 i])),{i,2,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,3,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{3,0}]

From the previous output it seems that annc cannot be used to compute c_{n,0}. However, this is not true, by the following consideration: although the leading coefficient of the recurrence annc[[3]] vanishes, it can still be used to compute c[n,0].

ApplyOreOperator[Factor[annc[[3]]],c[n,j]]/.j->0

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Check that the leading coefficient does not have any positive integer roots. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Look at the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{3,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Check that the leading coefficient does not have any positive integer roots. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,3,2+LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{1,1,0,-2}

InitializeDeterminantProof[2,2,{1,1,0,-2},-2 prod[(((-1+2 i) Gamma[(i/2)] Gamma[-3+4 i])/(2 Gamma[((3 i)/2)] Gamma[-2+3 i])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{1,1,1,-1}

InitializeDeterminantProof[2,2,{1,1,1,-1},prod[((Gamma[((1+i)/2)] Gamma[-1+4 i])/(Gamma[3 i] Gamma[-(1/2)+((3 i)/2)])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{1,2,-5,-9}

InitializeDeterminantProof[2,2,{1,2,-5,-9},-337920 prod[((Gamma[(1/2) (-1+i)] Gamma[-9+4 i])/(Gamma[-(7/2)+((3 i)/2)] Gamma[-6+3 i])),{i,3,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,7,19},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{7,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{7,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,7,6+LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{1,2,-4,-8}

InitializeDeterminantProof[2,2,{1,2,-4,-8},-24576 prod[((Gamma[(i/2)] Gamma[-8+4 i])/(Gamma[-2+((3 i)/2)] Gamma[-6+3 i])),{i,3,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,6,16},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{6,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{6,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,6,5+LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{1,2,-3,-7}

InitializeDeterminantProof[2,2,{1,2,-3,-7},-2016 prod[(((-3+2 i) Gamma[(1/2) (-1+i)] Gamma[-7+4 i])/(Gamma[(1/2) (-5+3 i)] Gamma[-4+3 i])),{i,3,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,5,15},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{5,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{5,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,5,4+LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{1,2,-2,-6}

InitializeDeterminantProof[2,2,{1,2,-2,-6},-224 prod[((Gamma[(i/2)] Gamma[-5+4 i])/(Gamma[3 (-1+i)] Gamma[(1/2) (-4+3 i)])),{i,2,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,4,15},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{4,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{4,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,4,3+LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{2,1,1,-1}

InitializeDeterminantProof[2,2,{2,1,1,-1},prod[((Gamma[((1+i)/2)] Gamma[-1+4 i])/(Gamma[3 i] Gamma[-(1/2)+((3 i)/2)])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{2,1,2,0}

InitializeDeterminantProof[2,2,{2,1,2,0},prod[((Gamma[1+(i/2)] Gamma[4 i])/(Gamma[3 i] Gamma[1+((3 i)/2)])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{-2,0,-1,-1}

InitializeDeterminantProof[2,2,{-2,0,-1,-1},-2 prod[((8 (-3+2 i) (-1+2 i) Gamma[((1+i)/2)] Gamma[-5+4 i])/(i Gamma[(3/2) (-1+i)] Gamma[-2+3 i])),{i,2,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
(* Recurrences are only valid for j>0, which is ok, because a_{i,0}=0 (for i>1). *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,2,10},{j,1,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{2,1}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{2,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

det33: Variations II (Theorem 12)

{0,1,1,-1}

InitializeDeterminantProof[3,3,{0,1,1,-1},prod[(((2^(1+i)) Gamma[((2+i)/3)] Gamma[-2+4 i])/(i Gamma[-(1/3)+((4 i)/3)] Gamma[-2+3 i])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce1[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce1[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce1[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce1[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{0,3,5,-1}

InitializeDeterminantProof[3,3,{0,3,5,-1},prod[(((2^(1+i)) (-2+3 i) (-1+3 i) Gamma[4 (1+i)] Gamma[((2+i)/3)])/((1+i) (2+i) (3+i) (4+i) Gamma[1+3 i] Gamma[(1/3) (5+4 i)])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce1[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce1[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce1[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce1[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{1,1,2,0}

InitializeDeterminantProof[3,3,{1,1,2,0},prod[(((2^i) Gamma[((4+i)/3)] Gamma[2+4 i])/(9 (i^2) Gamma[(7/3)+((4 i)/3)] Gamma[-1+3 i])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce1[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce1[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce1[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce1[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{4,2,4,0}

InitializeDeterminantProof[3,3,{4,2,4,0},prod[(((2^(1+i)) Gamma[((4+i)/3)] Gamma[3+4 i])/(3 Gamma[(7/3)+((4 i)/3)] Gamma[2+3 i])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce1[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce1[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce1[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce1[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{4,3,3,-3}

InitializeDeterminantProof[3,3,{4,3,3,-3},(5/3) prod[(((2^(1+i)) Gamma[((4+i)/3)] Gamma[3+4 i])/(3 Gamma[(7/3)+((4 i)/3)] Gamma[2+3 i])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce1[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce1[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce1[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce1[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{5,2,5,1}

InitializeDeterminantProof[3,3,{5,2,5,1},prod[(((2^i) Gamma[1+(i/3)] Gamma[4+4 i])/(3 Gamma[2+((4 i)/3)] Gamma[3+3 i])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce1[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce1[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce1[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce1[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{8,4,8,0}

InitializeDeterminantProof[3,3,{8,4,8,0},prod[(((2^(-1+i)) Gamma[((1+i)/3)] Gamma[7+4 i])/(Gamma[((4 (1+i))/3)] Gamma[6+3 i])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce1[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce1[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce1[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce1[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{8,5,7,-3}

InitializeDeterminantProof[3,3,{8,5,7,-3},(5/9) prod[(((2^(-1+i)) Gamma[((1+i)/3)] Gamma[7+4 i])/(Gamma[((4 (1+i))/3)] Gamma[6+3 i])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce1[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce1[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce1[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce1[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{0,0,0,0}

InitializeDeterminantProof[3,3,{0,0,0,0},2 prod[(((2^(-1+i)) Gamma[((1+i)/3)] Gamma[-3+4 i])/(Gamma[(2/3) (-1+2 i)] Gamma[-2+3 i])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce1[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce1[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce1[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce1[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{0,1,-1,-3}

InitializeDeterminantProof[3,3,{0,1,-1,-3},4 prod[(((2^(-1+i)) Gamma[((1+i)/3)] Gamma[-3+4 i])/(Gamma[(2/3) (-1+2 i)] Gamma[-2+3 i])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce1[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce1[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce1[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce1[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{0,2,-2,-6}

InitializeDeterminantProof[3,3,{0,2,-2,-6},10 prod[(((2^(-1+i)) Gamma[((1+i)/3)] Gamma[-3+4 i])/(Gamma[(2/3) (-1+2 i)] Gamma[-2+3 i])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce1[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

AnnihilatorSingularities tells us that id2ann cannot be applied for i=0. Therefore we consider this case separately. We have a_{0,0}=10, a_{0,1}=-10, and a_{0,j}=0 for j>1. Hence it suffices to show that c_{n,0}=c_{n,1} for all n.

(* Compute a recurrence satisfied by c_{n,0}-c_{n,1}. *)
Factor[DFinitePlus[DFiniteSubstitute[annc,{j->0}],DFiniteSubstitute[annc,{j->1}]]]

(* Check the 6 initial values. *)
Table[myc[n,0]==myc[n,1],{n,2,7}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce1[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce1[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce1[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{1,0,1,1}

InitializeDeterminantProof[3,3,{1,0,1,1},2 prod[(((2^(-2+i)) Gamma[(i/3)] Gamma[-1+4 i])/(3 Gamma[((4 i)/3)] Gamma[-1+3 i])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce1[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce1[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce1[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce1[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{1,3,-2,-8}

InitializeDeterminantProof[3,3,{1,3,-2,-8},-168 prod[(((2^(-2+i)) Gamma[(i/3)] Gamma[-1+4 i])/(3 Gamma[((4 i)/3)] Gamma[-1+3 i])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,3,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{3,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce1[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{3,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce1[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce1[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce1[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,3,2+LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{2,0,2,2}

InitializeDeterminantProof[3,3,{2,0,2,2},2 prod[(((2^(-3+i)) Gamma[((2+i)/3)] Gamma[1+4 i])/(Gamma[(2/3)+((4 i)/3)] Gamma[1+3 i])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce1[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce1[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce1[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce1[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{-3,0,-1,-1}

InitializeDeterminantProof[3,3,{-3,0,-1,-1},2 prod[(((2^(1+i)) (-1+2 i) Gamma[((2+i)/3)] Gamma[-5+4 i])/(i (1+i) Gamma[-(1/3)+((4 i)/3)] Gamma[-5+3 i])),{i,2,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
(* Recurrences are only valid for j>0, which is ok, because a_{i,0}=0 (for i>2). *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,1,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,1}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce1[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce1[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce1[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce1[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

det24: Variations III (Theorem 14)

{1,1,-1,-3}

InitializeDeterminantProof[2,4,{1,1,-1,-3},3 prod[(((3^(-1+i)) Gamma[(1/2)+(i/2)] Gamma[-1+3 i])/(Gamma[2 i] Gamma[(1/2) (-1+3 i)])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,3,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{3,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{3,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,3,2+LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{1,1,0,-2}

InitializeDeterminantProof[2,4,{1,1,0,-2},-prod[(((3^(-1+i)) Gamma[(i/2)] Gamma[3 i])/(2 Gamma[((3 i)/2)] Gamma[2 i])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{1,1,1,-1}

InitializeDeterminantProof[2,4,{1,1,1,-1},prod[(((3^i) Gamma[((1+i)/2)] Gamma[-1+3 i])/(Gamma[2 i] Gamma[(1/2) (-1+3 i)])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{1,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{1,2,-3,-7}

InitializeDeterminantProof[2,4,{1,2,-3,-7},42 prod[(((3^(-1+i)) Gamma[((1+i)/2)] Gamma[-1+3 i])/(Gamma[2 i] Gamma[(1/2) (-1+3 i)])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,5,15},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{5,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{5,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

AnnihilatorSingularities tells us that id2ann cannot be applied for i=1. Therefore we consider the cases i=0 and i=1 separately. We have a_{0,0}=-55, a_{0,1}=-51, a_{0,2}=-21, a_{0,3}=-1, and a_{0,j}=0 for j>3. Moreover, we have a_{1,0}=-136, a_{1,1}=-56, a_{1,2}=-56, a_{1,3}=-8, and a_{1,j}=0 for j>3. Hence it suffices to show that -55*c_{n,0}-51*c_{n,1}-21*c_{n,2}-c{n,3}=0 and -136*c_{n,0}-56*c_{n,1}-56*c_{n,2}-8*c{n,3}=0 for all n.

(* Compute a recurrence satisfied by C_0*c_{n,0}+...+C_3*c_{n,3}. *)
Factor[DFinitePlus[DFiniteSubstitute[annc,{j->0}],DFiniteSubstitute[annc,{j->1}],DFiniteSubstitute[annc,{j->2}],DFiniteSubstitute[annc,{j->3}]]]

(* Check the necessary 6 initial values (related to i=0). *)
Table[-55*myc[n,0]-51*myc[n,1]-21*myc[n,2]-myc[n,3],{n,4,9}]

(* Check the necessary 6 initial values (related to i=1). *)
Table[-136*myc[n,0]-56*myc[n,1]-56*myc[n,2]-8*myc[n,3],{n,4,9}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,5,4+LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{1,2,-2,-6}

InitializeDeterminantProof[2,4,{1,2,-2,-6},7 prod[(((3^(-1+i)) Gamma[(i/2)] Gamma[3 i])/(2 Gamma[((3 i)/2)] Gamma[2 i])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,4,14},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{4,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{4,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

AnnihilatorSingularities tells us that id2ann cannot be applied for i=0. Therefore we consider this case separately. We have a_{0,0}=-38, a_{0,1}=-20, a_{0,2}=-6, and a_{0,j}=0 for j>2. Hence it suffices to show that -38*c_{n,0}-20*c_{n,1}-6*c_{n,2}=0 for all n.

(* Compute a recurrence satisfied by -38*c_{n,0}-20*c_{n,1}-6*c_{n,2}. *)
Factor[DFinitePlus[DFiniteSubstitute[annc,{j->0}],DFiniteSubstitute[annc,{j->1}],DFiniteSubstitute[annc,{j->2}]]]

(* Check the necessary 5 initial values. *)
Table[-38*myc[n,0]-20*myc[n,1]-6*myc[n,2],{n,3,7}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,4,3+LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{1,2,-1,-5}

InitializeDeterminantProof[2,4,{1,2,-1,-5},5 prod[(((3^i) Gamma[((1+i)/2)] Gamma[-1+3 i])/(Gamma[2 i] Gamma[(1/2) (-1+3 i)])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,3,12},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{3,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{3,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,3,2+LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

{1,3,-3,-9}

InitializeDeterminantProof[2,4,{1,3,-3,-9},198 prod[(((3^i) Gamma[((1+i)/2)] Gamma[-1+3 i])/(Gamma[2 i] Gamma[(1/2) (-1+3 i)])),{i,1,n}]]

(* Display the matrix A_6. *)
TableForm[Table[mya[i,j],{i,0,5},{j,0,5}]]

(* Test the conjectured identity. *)
Table[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n],{n,10}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,6},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[test,{n,5,15},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
AnnihilatorSingularities[annc,{5,0}]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
AnnihilatorSingularities[id2ann,{5,0},Assumptions->i<n-1]

(* Check a few (more than necessary) initial values. *)
Table[Sum[mya[i,j]*myc[n,j],{j,0,n-1}],{n,12},{i,0,n-2}]

AnnihilatorSingularities tells us that id2ann cannot be applied for i=1. Therefore we consider the cases i=0 and i=1 separately. We have a_{0,0}=-201, a_{0,1}=-148, a_{0,2}=-126, a_{0,3}=-36, a_{0,4}=-1, and a_{0,j}=0 for j>4. Moreover, we have a_{1,0}=-522, a_{1,1}=-120, a_{1,2}=-252, a_{1,3}=-120, a_{1,4}=-10, and a_{1,j}=0 for j>4. Hence it suffices to show that -201*c_{n,0}-148*c_{n,1}-126*c_{n,2}-36*c{n,3}-c_{n,4}=0 and -522*c_{n,0}-120*c_{n,1}-252*c_{n,2}-120*c{n,3}-10*c_{n,4}=0 for all n.

(* Compute a recurrence satisfied by C_0*c_{n,0}+...+C_4*c_{n,4}. *)
Factor[DFinitePlus[DFiniteSubstitute[annc,{j->0}],DFiniteSubstitute[annc,{j->1}],DFiniteSubstitute[annc,{j->2}],DFiniteSubstitute[annc,{j->3}],DFiniteSubstitute[annc,{j->4}]]]

(* Check the necessary 6 initial values (related to i=0). *)
Table[-201*myc[n,0]-148*myc[n,1]-126*myc[n,2]-36*myc[n,3]-myc[n,4],{n,5,12}]

(* Check the necessary 6 initial values (related to i=1). *)
Table[-522*myc[n,0]-120*myc[n,1]-252*myc[n,2]-120*myc[n,3]-10*myc[n,4],{n,5,12}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[mya[n-1,j]*myc[n,j],{j,0,n-1}]==myb[n]/myb[n-1],{n,5,4+LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start

detx41: Variations III (Theorem 15)

InitializeDeterminantProof[2,4,{1,0,x+1,x+1},2 prod[(((2^(2i-1))*(3^(i-1)) *Gamma[i]*Gamma[(3i+x)/2])/(Gamma[2i]*Gamma[(i+x)/2])),{i,1,n}],"detx41/"]

(* Display the matrix A_4. *)
TableForm[Table[mya[i,j],{i,0,3},{j,0,3}]]

(* Test the conjectured identity. *)
Table[Together[Det[Table[mya[i,j],{i,0,n-1},{j,0,n-1}]]/myb[n]],{n,8}]

Holonomic description of (Subscript[c, n,j])

(* The first few values of c_{n,j}. *)
TableForm[Table[myc[n,j],{n,4},{j,0,n-1}]]

(* This is the guessed annihilator for c_{n,j}. *)
AnnInfo[annc]

(* Check whether the first values of c_{n,j} satisfy the guessed recurrences. *)
With[{test=ApplyOreOperator[annc,myc[n,j]]},Union[Flatten[Table[Together[test],{n,9},{j,0,n-1}]]]]

(* The values at these indices have to be given as initial conditions, 
in order to uniquely define c_{n,j} via the recurrences in annc. *)
Select[AnnihilatorSingularities[annc,{1,0}],FreeQ[#,x]&]

Proof of Identity (H1)

(* Compute a recurrence for c_{n,n-1} *)
Support[cnn1=DFiniteSubstitute[annc,{j->n-1}][[1]]]

(* Verify that this recurrence admits a constant sequence as solution. *)
OreReduce1[cnn1,Annihilator[1,S[n]]]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[cnn1]==0,n],IntegerQ]

(* Check the first few initial values. *)
Table[myc[n,n-1],{n,9}]

Proof of Identity (H2)

(* Include the variable i into annc. *)
annci=ToOrePolynomial[Prepend[annc,S[i]-1],OreAlgebra[S[n],S[j],S[i]]];

(* Annihilator for a_{i,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annci,mya1[i,j]];
annSmnd2=DFiniteTimesHyper[annci,mya2[i,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id2ct1 constitutes a set of telescopers for annSmnd1. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct1],annSmnd1]]

(* Verify that id2ct2 constitutes a set of telescopers for annSmnd2. *)
Timing[OreReduce1[MapThread[#1+(S[j]-1)**#2[[1]]&,id2ct2],annSmnd2]]

(* Combine the telescopers to an annihilator of the sum on the LHS of (H2). *)
id2ann=DFinitePlus[id2ct1[[1]],id2ct2[[1]]];
AnnInfo[id2ann]

(* We are required to check initial values at the following indices: *)
Select[AnnihilatorSingularities[id2ann,{1,0},Assumptions->i<n-1],FreeQ[#,x]&]

(* Check a few (more than necessary) initial values. *)
Table[Sum[Expand[mya[i,j]*myc[n,j]],{j,0,n-1}],{n,12},{i,0,n-2}]

Proof of Identity (H3)

(* Annihilator for a_{n-1,j}*c_{n,j}, split into two parts. *)
Timing[
annSmnd1=DFiniteTimesHyper[annc,mya1[n-1,j]];
annSmnd2=DFiniteTimesHyper[annc,mya2[n-1,j]];
ByteCount/@{annSmnd1,annSmnd2}
]

(* Verify that id3ct1 constitutes a telescopic relation for annSmnd1. *)
Timing[OreReduce1[id3ct1[[1,1]]+(S[j]-1)**id3ct1[[2,1,1]],annSmnd1]]

(* Verify that id3ct2 constitutes a telescopic relation for annSmnd2. *)
Timing[OreReduce1[id3ct2[[1,1]]+(S[j]-1)**id3ct2[[2,1,1]],annSmnd2]]

(* Combine the telescopers to a recurrence for the sum on the LHS of (H3). *)
id3ann=DFinitePlus[id3ct1[[1]],id3ct2[[1]]][[1]];
AnnInfo[{id3ann}]

(* Look at the integer roots of the leading coefficient. *)
Select[n/.Solve[LeadingCoefficient[id3ann]==0,n],IntegerQ]

(* Simplify the quotient b_n/b_{n-1}. *)
quot=myb[n]/myb[n-1]/.prod[f_,{i,a_,n}]:>(f/.i->n)*prod[f,{i,a,n-1}];
quot=FunctionExpand[quot/.prodsimp/.prod->Product]

(* Verify that b_n/b_{n-1} satisfies the recurrence derived for the LHS of (H3). *)
OreReduce1[id3ann,Annihilator[quot,S[n]]]

(* Compare initial values. *)
Table[Sum[Expand[mya[n-1,j]*myc[n,j]],{j,0,n-1}]==Expand[myb[n]/myb[n-1]],{n,LeadingExponent[id3ann][[1]]}]

(* How long the calculations in this section took. *)
CurrentDate[]-start