<<RISC`SumCracker`

SumCracker Package version 0.11
written by Manuel Kauers
Copyright 2008-2011, Research Institute for Symbolic Computation (RISC),
Johannes Kepler University, Linz, Austria

The examples in this notebook are stated in Table 5.10, p. 56-57 of “Algorithms for Nonlinear Higher Order Difference Equations” (http://www.algebra.uni-linz.ac.at/people/mkauers/publications/kauers05c.pdf). The inequalities taken from the book of Mitrinović (1964). The inequalities appear in the book 
under the labels given below (and in the source column of Table 5.10). This notebook was compiled by Miriam Schussler.

3.27

ProveInequality[1/(2*f[n])<4^(-n) Binomial[2 n,n],Free->{f,g},Variable->n,Using->{f[n]^2==n,f[n]>0,g[n]^2==3*n+1,g[n]>0},From->2]

3.28

ProveInequality[PRODUCT[(4*k-1)/(4*k+1),{k,1,n}]<p[n],Using->{p[n]^2==3/(4*n+3),p[n]>0},Free->{p},Variable->n,From->1]

3.29

ProveInequality[1/(2*s[n])<PRODUCT[(2 k-1)/(2 k),{k,1,n}],Using->{s[n]^2==n,s[n]>0},Free->{s},Variable->n,From->2]

ProveInequality[PRODUCT[(2 k-1)/(2*k),{k,1,n}]<1/t[n],Using->{t[n]^2==2*n+1,t[n]>0},Free->{t},Variable->n,From->2]

3.31

ProveInequality[PRODUCT[(3*k+4)/(3*k+2),{k,0,n}]>1+2/3HarmonicNumber[n+1],Using->{HarmonicNumber[n]≥0},Variable->n,From->1]

3.57

ProveInequality[(n+a)!+n!>(n+a-1)!+(n+1)!,Using->{n!>0,(n+a)!>0,a≥1},Variable->n,From->1,CheckInitialValues->False]

4.1

ProveInequality[SUM[1/s[k],{k,1,n}]≥2 (t[n]-1),Using->{s[n]^2==n,t[n]^2==n+1,s[n]>0,t[n]>0},Free->{s,t},Variable->n,From->1]

4.3

ProveInequality[p[n]>q[n],Where->{p[n+1]==p[n]+1/(2n+1)+1/(2n+2),p[0]==0,q[n+1]==q[n]+1/(n+1),q[0]==1/2},From->2]

4.4

ProveInequality[p[n]>q[n], Where->{p[n+1]==p[n]+1/(3n+2)+1/(3n+3)+1/(3n+4),q[n+1]==q[n]+1/(n+1),p[0]==1,q[0]==1},From->1]

4.8

ProveInequality[SUM[a^(2k),{k,1,n}]≤n(a^(2*n+1)+1),Using->{n≥1,a≥1,a^(2*n)≥0,SUM[a^(2*k),{k,1,n}]≥0},Variable->n,From->1,Free->a]

4.14

ProveInequality[SUM[1/f[k],{k,1,n}]>f[n],Free->{f},Using->{f[n]^2==n,f[n]>0,SUM[1/f[k],{k,1,n}]≥0},Variable->n,From->2,CheckInitialValues->False]

4.15

ProveInequality[f[n]≥g[n], Using->{f[n]^2==SUM[k^2,{k,1,n}],g[n]^3==SUM[k^3,{k,1,n}],f[n]>0,g[n]>0},Free->{f,g},Variable->n,From->0]

4.16

ProveInequality[PRODUCT[a[k]+1,{k,1,n}]≥1+SUM[a[k],{k,1,n}],Using->{a[n]>0,SUM[a[k],{k,1,n}]≥0},Free->{a},Variable->n,From->1]

4.17

ProveInequality[PRODUCT[1-a[k],{k,1,n}]>1-SUM[a[k],{k,1,n}],Using->{0<a[n]<1,0<SUM[a[k],{k,1,n}]<1,0<PRODUCT[1-a[k],{k,1,n}]<1},Free->{a},Variable->n,From->1,CheckInitialValues->False]

4.18

ProveInequality[PRODUCT[a[k]+1,{k,1,n}]<1/(1-SUM[a[k],{k,1,n}]),Using->{0<a[n]<1,0<SUM[a[k],{k,1,n}]<1},Free->{a},Variable->n,From->1,CheckInitialValues->False]

4.19

ProveInequality[PRODUCT[1-a[k],{k,1,n}]<1/(1+SUM[a[k],{k,1,n}]),Using->{0<a[n]<1,0<SUM[a[k],{k,1,n}]<1},Free->{a},Variable->n,From->1,CheckInitialValues->False]

4.22

ProveInequality[PRODUCT[a^k+1,{k,1,n-1}]<(1-a)/(a^n-2a+1),Using->{0<a<1/2,a≥a^n>0},Free->{a},Variable->n,From->1,CheckInitialValues->False]

4.23 (changed condition to a[n]≥1 - as in the book of Mitrinović)

ProveInequality[(n+1) 2^(-n)PRODUCT[a[k]+1,{k,1,n}]≥(SUM[a[k],{k,1,n}]+1),Using->{a[n]≥1,n≥1,2^(-n) PRODUCT[a[k]+1,{k,1,n}]>1,SUM[a[k],{k,1,n}]>1},Free->{a},Variable->n,From->1]

4.29

ProveInequality[1/2-1/(n+1)<SUM[1/k^2,{k,2,n}]<1-1/n,From->2, Variable->n]

4.30

ProveInequality[1/(a+1)-1/(a+n+1)<SUM[1/(a+k)^2,{k,1,n}]<1/a-1/(a+n),Using->{a>0},From->1,Variable->n]

4.41

ProveInequality[p[n]r[n]≥q[n]q[n],Where->{p[n+1]==(2n+1)(2n+2)p[n],r[n+1]==r[n]-(2n+1)/p[n+1],q[n+1]==(2n+1)q[n],p[2]==24,q[2]==3,r[2]==3/8},Using->{p[n]>1,q[n]>1},From->2,Variable->n]

7.35

ProveInequality[(2*n+1) x^n≤(x^(2*n+1)-1)/(x-1),Using->{x≥0,x^n≥0},Variable->n]

7.36

ProveInequality[1-x^(2*n)≥2*n*x^n(1-x),Using->{0≤x≤1},Variable->n]

7.44

ProveInequality[(n-1)(SUM[a[k],{k,1,n}])^2≥2*n*SUM[a[k]*(SUM[a[i],{i,1,k-1}]),{k,1,n}],Free->{a},From->1,Variable->n]

8.3

ProveInequality[(SUM[1/a[k],{k,1,n}]) SUM[a[k],{k,1,n}]≥n^2,Free->{a},Using->{a[n]>0,SUM[a[k],{k,1,n}]≥0},Variable->n,From->1,CheckInitialValues->False]

8.4

ProveInequality[SUM[a[k]*b[k],{k,1,n}]^2≤SUM[k*a[k]^2,{k,1,n}]SUM[(1/k)b[k]^2,{k,1,n}],Using->{SUM[k*a[k]^2,{k,1,n}]≥0,SUM[(1/k)b[k]^2,{k,1,n}]≥0},From->1,Free->{a,b} ,Variable->n]

8.8

ProveInequality[SUM[(1/k)a[k],{k,1,n}]^2≤SUM[k^3a[k]^2,{k,1,n}]SUM[1/k^5,{k,1,n}],Using->{SUM[k^3a[k]^2,{k,1,n}]≥0,SUM[1/k^5,{k,1,n}]≥0},From->1,Free->{a}, Variable->n]

8.25

ProveInequality[SUM[a[k],{k,1,n}]^2≤n*SUM[a[k]^2,{k,1,n}],From->1,Free->{a}, Variable->n]

11.1

ProveInequality[f[n]<(g[n]+1),Using->{f[n+1]^2==n+1+f[n],g[n]^2==n,0<g[n],f[n]>0},Free->{f,g},Variable->n,From->1,CheckInitialValues->False]