Trying to prove that $x\sin(\frac{\pi}{x})\ge\pi \cos(\frac{\pi}{x})$ for $x\ge 1$

Question

As an intermediate step, consider the function:

f[x_] := x Sin[Pi/x]

I want to prove that this function is increasing for $x\ge 1$. This can be done with the first derivative. We have to prove that $f'[x]\ge 0$ for $x\ge 1$. First I tried:

FullSimplify[f'[x] >= 0, x >= 1]
(*Out: x Sin[π/x] >= π Cos[π/x] *)

Then I realized that Mathematica probably doesn't know about the inequality $\tan(x)>x$ for $0<x<\pi/2$. So I tried:

FullSimplify[f'[x] >= 0, x >= 1 && ForAll[y, 0 < y < Pi/2, Tan[y] > y]]
(*Out: x Sin[π/x] >= π Cos[π/x] *)

This inequality seems to be easy, I tried replacing x >= 1 with x >= Pi and I get the same result. How can I properly use Mathematica to prove some theorems like this one?

EDIT: The main point of the problem is not trying to prove that the function is increasing (that is the motivation of the problem) , the main point is trying to prove that $x\sin(\frac{\pi}{x})\ge\pi \cos(\frac{\pi}{x})$ for $x\ge 1$ using that $\tan(x)>x$ for $0<x<\pi/2$, i.e. i want to use the proving features of Mathematica.

Answer 1

The proof of the original statement that $f(x)\equiv x\sin\frac{\pi}{x}$ is a monotonically increasing function of $x$ for $x>1$ can be done as follows:

First, we show that the second derivative $f''(x)$ of the function is negative:

Simplify[D[x Sin[π/x], x, x] < 0, Assumptions -> x > 1]

True

This means that the first derivative $f'(x)$ is a monotonically decreasing function of $x$ for $x>1$.

Now we show that the derivative of the function approaches zero as $x\to\infty$:

Limit[D[x Sin[π/x], x], x -> ∞]

0

Since the derivative has been shown to be decreasing and to have a limit of zero for $x\to\infty$, it follows that $f'(x) > 0$ for $x>1$. This proves the desired statement about $f(x)$.

Edit

To take the other route proposed in the edited version of the question, you could do the following:

Resolve[ForAll[{x}, x > 1 && Tan[π/x] >= π/x, f'[x] >= 0], Reals]

True

Edit 2

In the Resolve statement above, ForAll has three arguments: the variable {x}, a condition, and the statement to be proved. In words, this says the following: for all $x$ that satisfy the condition $x>1$ and $\tan(\pi/x)\ge \pi/x$, it holds that $f'(x)\ge0$. Of course, the condition can actually be simplified because the tangent inequality as stated here only holds for $x>2$.

To make the condition fully consistent with the desired interval $x>1$, we simply have to replace $x$ by $2 x$ in the tangent inequality. This leaves the inequality unaffected but extends its range of validity to $x>1$. Therefore, we get the following statement that can be fed to Mathematica:

Resolve[ForAll[x, x > 1 && Tan[π/(2 x)] >= π/x/2, f'[x] >= 0], Reals]

True

Answer 2

Mathematica often responds well when provided a little expert assistance. Let's focus on techniques that have a wide application rather than just to this problem.

1. Can the function be decomposed into simpler pieces? Yes, obviously: $f(x)$ is the product of $x$ and $\sin{\pi / x}$. Both are obviously increasing for $x \in [1,2]$. After that, $\sin{\pi / x}$ turns around: it decreases while $x$ continues to increase. The challenge is to show that the increase in $x$ overpowers the decrease in the rest of the function. However, perhaps we have accomplished something: we can focus on the cases $x \ge 2$.

2. It can be more difficult, both theoretically and computationally, to determine characteristics of a function on an infinite (or noncompact) set like the interval $[2,\infty)$ than it is to work on a compact (finite) set. From the appearance of $\pi/x$ in $f$ and the infinite limit of its domain, it is both natural and immediate to attempt the change of variable $y = 1/x$. Because this change reverses the direction of $x$, we now wish to show that $g(y) = \sin{\pi y}/y$ is decreasing on the interval $[0, 1/2]$.

Let's begin a Mathematica implementation by creating $g$ and its derivative:

ClearAll[g, dg];
g[y_] := Sin[\[Pi] y] / y;
dg[y_] := Evaluate @ D[g[y], y]

Why not try the obvious: can we demonstrate that the derivative of $g$ is everywhere negative on this interval simply by requesting its supremum?

Maximize[{dg[y], 0 < y <= 1/2}, y]

The only solution is y -> 0 (reached in 0.11 seconds). This technique exploits two properties of Maximize announced in its documentation:

Maximize will return exact results if given exact input.

If the maximum is achieved only infinitesimally outside the region defined by the constraints, or only asymptotically, Maximize will return the supremum and the closest specifiable point.

Mathematica issues a warning message, because this is a boundary value and in fact dg is not defined at $0$, so to be sure, let's check:

 In[3]:= Limit[dg[y], y -> 0]
Out[3] = 0

Whence--because the supremum is $0$ and occurs uniquely at $y=0$--the derivative of $g$ is non-positive throughout $[0,1/2]$ and negative on $(0,1/2]$, QED.

This problem can also be solved via Taylor's Theorem (with remainder, not just naive inspection of the coefficients) by computing the power series of $g$ around $0$ out to first order and analyzing the remainder term. It becomes so trivial with this approach that Mathematica's power is unneeded, so I won't pursue the details here. It is noteworthy, though, that this solution is available only for g, not for f (where the expansion would be around $\infty$, which doesn't accomplish anything in this case).

---

More generally, when tackling more complex or recalcitrant problems, try to decompose them into simpler pieces; use mathematical identities to reformulate the subproblems; attack the subproblems in multiple ways (rather than focusing on just one method, such as that based on a tangent identity in this problem); and let mathematical principles guide you.

Answer 3

I have no rigorous training in mathematics - I'm not quite sure what constitutes a proof and what doesn't.

How can I properly use Mathematica to prove some theorems like this one? Well, what you can do is use Mathematica to help visualise the function as well as computing derivatives, integrals or limits. My approach is a bit hacky :)

The function

Okay, so we're dealing with x Sin[Pi/x] which is, obviously, a periodic function. It is also even (its plot is symmetric and x Sin[Pi/x] == -x Sin[Pi/-x] evaluates to True). The fact that the function is even is interesting if you want to generalize your "proof".

From the plot of Sin[x],

you can get a good idea of what the plot of x Sin[Pi/x] will look like, even before asking Mathematica to generate it. The fact that Sin[x] has a value between 0 and 1 while $ 0\lt x \leq \pi$ is obvious from the graph. What is also obvious is that the function's value has negative sign from $\pi \leq x \leq 2\pi$.

What are we expecting?

We're expecting a sinusoidal with ascending amplitude and frequency (the x multiplying Sin[Pi/x]). We can guess that because at values of x below 1, we will be evaluating the sine of a number larger than $\pi$, this trend being reversed at x=1. What happens after x=1? Let's ask Mathematica.

Plotting the functions

It turns out we were right about the amplitude and frequency. Right up to a point, at x=1 - past this point, there are no more zeros. There's no need to go further, because it is obvious that our function has an asymptote. But what if we had our PlotRange wrong, and the (presumably more complicated) function really does have zeros after x=1? Let's again ask Mathematica.

It turns out that the limit of our function

Limit[x Sin[Pi/x], x -> \[Infinity]]

is $\pi$. Confirmation of asymptotic behaviour.

What about $\pi \cos (\frac{\pi}{x})$?

You could take a guess like we did before, or simply not bother and ask Mathematica right away.

It is clear from this image that the inequality $x \sin (\frac{\pi}{x})\geq \pi \cos (\frac{\pi}{x})$ can be valid for $x \geq 1$. To confirm, we need to check the limit of the cosine function with

Limit[Pi Cos[Pi/x], x -> \[Infinity]]

which also evaluates to $\pi$. Good news.

But how can I prove it's increasing?

As halirutan said, you can use derivatives. As a non-mathematician, I would be convinced by the plots of the functions, and their limits. If you want to know how fast each function converges to $\pi$, then go ahead and take a look at each function's first/second derivative plot.

This approach might not qualify as rigorous, but I think it shows how you can use Mathematica to walk through math problems.

Answer 4

It's 5am here and no, I'm not already up; so be warned. It seems Reduce cannot really help here but maybe someone else finds a direct way to do it. In the meantime you could take your derivative f'[x]

$$\frac{df}{dx} = \sin \left( \frac{\pi }{x} \right) -\frac{\pi \cos \left(\frac{\pi }{x}\right)}{x}$$

$x$ can have values from 1 to infinity and we need to show, that the above expression is always positive. Keeping in mind the interval for $x$ we could make a substitution to simplify the expression

f'[x] /. x :> Pi/y

which leads us to an easier problem to prove

$$\sin (y)-y \cos (y)>0$$

Now you could subtract $\sin(y)$ and then divide by $\cos(y)$. In the division step you have to take care, because remember $y$ runs from $\pi$ (when $x=1$) to 0 (when $x$ goes to infinity) and plotting this range for $\cos(y)$ shows

Plot[Cos[y], {y, 0, Pi}]

that you have to make a case-by-case analysis. For $\pi/2 \leq y \leq \pi$ the cosine is negative and you have to turn the sign of the inequality. Therefore, you have to show

$$\tan(y)>y,\quad\quad 0 < y < \pi/2$$

and

$$\tan(y)<y,\quad\quad \pi/2 < y \leq \pi$$

You maybe have to think about what happens at $\pi/2$ and I'm sure there are easier ways to solve this, but the tangens inequality caught my eye since you already mentioned it.

Answer 5

Starting in M10, you can use FunctionRange. For example:

FunctionRange[{x Sin[π/x] - π Cos[π/x], x>1.}, x, y]

0 < y <= 3.33984

Hence it is true that:

x Sin[π/x] - π Cos[π/x] > 0

or equivalently:

x Sin[π/x] > π Cos[π/x]

for x>1. Similarly:

FunctionRange[{D[x Sin[π/x], x], x>1.}, x, y]

0 < y < 3.14159

implies that x Sin[π/x] is monotonically increasing for x>1.

Also, starting in M11, Reduce has been enhanced to be able to resolve these kinds of propositions:

proposition = Exists[x, x>1, x Sin[π/x] <= π Cos[π/x]];
Reduce[proposition]

False

So, there are no values of x greater than 1 where x Sin[π/x] - π Cos[π/x] < 0. Alternatively, the following must be true:

FullSimplify[!proposition] //TeXForm

$\forall _{x,x>1}x \sin \left(\frac{\pi }{x}\right)>\pi \cos \left(\frac{\pi }{x}\right)$

Similarly:

Reduce[Exists[x, x>1, D[x Sin[π/x], x] <= 0]]

False

shows that x Sin[π/x] is monotonically increasing for x>1.

Answer 6

Maybe trivial, but just for the sake of completeness: the inequality holds not only for x>=1 but already for x>=x0, where

x0 = x /. FindRoot[x Sin[\[Pi]/x] == \[Pi] Cos[\[Pi]/x], {x, 0.7}, WorkingPrecision -> 100]

(* Out[122]= 0.6991556596428411966369319152386816172807303061005296218612315287681429432614\
994992474339172310490725 *)

Remark: x0/pi is correctly recognized by Wolfram Alpha as "1/CTa, where CTa is the smallest root of the Tanc function" (=Tan[z]/z)

Answer 7

What about using Taylor series?

fp = Normal[Series[f'[1/y], {y, 1, 20}]] /. y -> 1/x

FullSimplify[fp >= 0, x >= 1]

True