# Prove an inequality over the reals, given a constraint

Given $$a,b,c \geq 0$$ and $$a + b + c = 3$$

prove

$$\frac{a}{b^2 + 1} + \frac{b}{c^2 + 1} + \frac{c}{a^2 + 1} \geq \frac{3}{2}$$

One can prove the above using a great deal of "human" insight and equation manipulation, as shown here.

I would like to prove this with as much automatic symbol manipulation as possible. I've tried obvious techniques using Solve, RootIntervals, and such, including the naive directly testing logically:

Assuming[a + b + c == 3,
a/(b^2 + 1) + b/(c^2 + 1) + c/(a^2 + 1) >= 3/2]


all without success.

I have a sense there must be some way of automatically finding a solution domain for the second equation (given the constraint of the first equation), but have not been able to find it.

• Could use Minimize: In[296]:= Minimize[{a/(b^2 + 1) + b/(c^2 + 1) + c/(a^2 + 1) - 3/2, a + b + c == 3, a >= 0, b >= 0, c >= 0}, {a, b, c}] Out[296]= {0, {a -> 1, b -> 1, c -> 1}} Sep 17 at 14:25
• Whoops. I missed a response that was substantially the same. Sep 17 at 19:52
• Accepting the intent of this question is use of Mathematica in-built functions to automate and with respect, this is a direct application of the (weighted) harmonic mean-arithmetic mean inequality. This was alluded to by Artes. Sep 18 at 7:16

This can be done as follows.

Resolve[ForAll[{a, b, c}, {a, b, c} >= 0,
Implies[a + b + c == 3, a/(b^2 + 1) + b/(c^2 + 1) + c/(a^2 + 1) >= 3/2]], Reals]


True

or/and

FindInstance[ a + b + c == 3 && {a, b, c} >= 0 &&
a/(b^2 + 1) + b/(c^2 + 1) + c/(a^2 + 1) < 3/2, {a, b, c}, Reals]


{}

• Thanks so much. ($\checkmark$). I'm learning these functions and this is very helpful. Sep 16 at 4:34
Minimize[{a/(b^2 + 1) + b/(c^2 + 1) + c/(a^2 + 1), {a, b, c} > 0,
a + b + c == 3}, {a, b, c}]


{3/2, {a -> 1, b -> 1, c -> 1}}

• NMinimize[{a/(b^2 + 1) + b/(c^2 + 1) + c/(d^2 + 1) + d/(a^2 + 1), a + b + c + d == 4}, {a, b, c, d}] Sep 17 at 2:11
• This results in {2., {a -> 1., b -> 1., c -> 1., d -> 1.}}, not proving the inequality. Sep 17 at 6:15

The most straightforward method involves Simplify with assumptions being its second argument:

Simplify[ a/(b^2 + 1) + b/(c^2 + 1) + c/(a^2 + 1) >= 3/2,
a + b + c == 3 && a >= 0 && b >= 0 && c >= 0]

 True


The assumption that a, b, c are nonnegative is important (this should be mentioned in the original question), e.g.

With[ {a = 2, b = 2, c = -1},
a/(1 + b^2) + c/(1 + a^2) + b/(1 + c^2) >= 3/2]

 False


For another examples how Simplify (or FullSimplify) can be powerful see e.g.

Solving a system of diophantine equations from a mathematical competition

or

EDIT

Taking a look at the inequality with three variables $$a, b, c \geq 0$$ we can generalize it to the case with four variables $$a, b, c, d \geq 0$$ such that $$a+b+c+d=4$$: $$\frac{a}{b^2+1}+\frac{b}{c^2+1}+\frac{c}{d^2+1}+\frac{d}{a^2+1}\geq2$$

We take $$2$$ for the r.h.s. of the inequality since it is natural to expect that the minimum is achived when all numbers are equal i.e. $$a=b=c=d=1$$, and now this works well

Simplify[ a/(b^2 + 1) + b/(c^2 + 1) + c/(d^2 + 1) + d/(a^2 + 1) >= 2,
a + b + c + d == 4 && a >= 0 && b >= 0 && c >= 0 && d >= 0]

 True


it takes a few minutes, while Minimize (analogously like in another post) haven't provided the result for much longer time. On the other hand the construction involving Resolve, ForAll, Implies works similarily like Simplify.

• Thanks ($+1$). The original problem didn't specify that $\{ a,b,c \} >0$ but your example shows that it is indeed necessary, so I've updated the question. Sep 16 at 19:20
• @DavidG.Stork You are welcome. I updated my answer with a generalization of the inequality to the four variables case, which is computationally much more expensive than three variables case. Sep 17 at 1:14
• FindInstance[ a/(b^2 + 1) + b/(c^2 + 1) + c/(d^2 + 1) + d/(a^2 + 1) < 2 && a + b + c + d == 4 && a >= 0 && b >= 0 && c >= 0 && d >= 0, {a, b, c, d}, Reals] // AbsoluteTiming results in {248.005, {}} on my comp. Sep 17 at 6:13
• The comment regarding FindInstance doesn't make sense (as usual from this user). FindInstance doesn't serve anything and the inequality should be a/(b^2 + 1) + b/(c^2 + 1) + c/(d^2 + 1) + d/(a^2 + 1) >= 2. Sep 17 at 9:27
• @artes: The question is how to show that x+y+z==3&&{x,y,z}>=0 implies the inequality a/(1 + b^2) + c/(1 + a^2) + b/(1 + c^2) >= 3/2. The negation of this implication is a/(b^2 + 1) + b/(c^2 + 1) + c/(a^2 + 1) < 3/2 && a + b + c == 3 && a >= 0 && b >= 0 && c >= 0 (see Negation of implication). The FindInstance command shows that this negation is false, so the implication is true. The same for the generalization for four variables. Don't hesitate to ask for further explanation in need. Sep 17 at 12:19