Days ago we ran into a need to lower bound .

One possibility is observe the non-negativity and continuity of the function over and apply an integral lower bound:

where in the third line we have retained the first two terms of series expansion for for . The integral approximation gives very messy terms and a somewhat loose lower bound. We can obtain a much neater one:

Before the proof, we may look at a plot to see how tight the lower bound is. Here it goes!

The trick of proof lies with series expansion.

*Proof:* It is true for as . Now suppose the claim holds for , i.e., , we need to show it holds for . It suffices to show . Now we consider the series expansions of and :

So we have

if , and satisfies the condition.

[Updated to the Proof] There is a simpler way to see (Thanks to Dai Liang! See first comment below). Basically it follows from the fact that , where the latter can be observed as follows: and for . (03/07/2012)

Recall that . Thus we have

Acknowledgement: Dr. Tewodros Amdeberhan, at Math Department of Tulane University, has kindly provided the original proof and permitted me to share this on my blog. You may want to read their interesting paper on techniques of evaluating sum of arctangent: Sum of Arctangents and Some Formula of Ramanujan.

我感觉这个证明也是非常自然的。不知道我的理解对不对，或者可能没有真正理解后来那个证明的trick所在。

比如要证明 ，如果不用幂级数展开，因为在起始点0处函数值相等，而在[0,1]之间，前一个函数导数值总是大于第二个，所以 成立。

而 写成那样一个summation 的形式，我感觉也是非常自然的。

Thanks a lot for pointing out this – that helps simplify things considerably.

I will updated the post to include this.