Proof of an Inequality

Michael Trott

Let a, b, c be the lengths of the sides of a non-degenerate triangle. Then the following inequality holds (M. Bjelica. FILOMAT 9, 117 (1995)).

We will use Mathematica to prove this inequality in a straightforward way.

Without loss of generality we may assume a = 1. The left hand side then reduces to a function of two variables.

(Subscript[𝒮, 1]) = 
      (a/(Sqrt[2 (b^2) + 2 (c^2) - (a^2)])) + (b/(Sqrt[2 (c^2) + 2 (a^2) - (b^2)])) + 
          (c/(Sqrt[2 (a^2) + 2 (b^2) - (c^2)])) /. a -> 1

Let us look at a contour plot of this function to get a feel for this problem.

Show[
        Graphics[
            ContourPlot[
              Evaluate[
                (Subscript[𝒮, 1]) /. 
                  {b -> (x + y)/2, c -> (x - y)/2}], 
              {x, 1, 6}, {y, -1, 1}, PlotPoints -> {160, 60}, 
              DisplayFunction -> Identity, Contours -> 60, 
              ContourStyle -> {Thickness[0.0001]}, 
              ColorFunction -> (Hue[Random[]] &)]] /. 
          {𝓅_Polygon | 𝓅_Line :> 
              Map[ {Plus@@#1, Subtract@@#1}/2 &, 𝓅, {-2}]}, 
        PlotRange -> {{0, 3}, {0, 3}}, Frame -> False, 
        Axes -> True, AxesLabel -> {"b", "c"}, 
        DisplayFunction -> $DisplayFunction];

We take the gradient of (Subscript[S, 1])to find a local minimum.

grad = 
      {(∂_b) (Subscript[𝒮, 1]), 
        (∂_c) (Subscript[𝒮, 1])}

Since the triangle is non-degenerate, the denominators can never vanish. Therefore we can concentrate on the numerators.

To find all the roots of (Subscript[S, 2]) we will eliminate all the square roots to construct an equivalent polynomial. There are three types of square roots.

\(Union[Cases[𝒮\_2, \@_, ∞]]\)

We introduce auxiliary variables for the square roots.

(Subscript[𝒮, 3]) = 
      (Subscript[𝒮, 2]) /. 
        {(Sqrt[2 + 2 (b^2) - (c^2)]) -> x, 
          (Sqrt[2 - (b^2) + 2 (c^2)]) -> y, 
          (Sqrt[2 (b^2) + 2 (c^2) - 1]) -> z}

Eliminating the auxiliary variables x, y, and z gives two polynomials.

(Subscript[𝒮, 4]) = 
      (GroebnerBasis[
              {#, (x^2) - (2 + 2 (b^2) - (c^2)), 
                (y^2) - (2 - (b^2) + 2 (c^2)), 
                (z^2) - (2 (b^2) + 2 (c^2) - 1)}, {b, c}, {x, y, z}, 
              MonomialOrder -> EliminationOrder] &)/@
        (Subscript[𝒮, 3])

The common zeros of these two polynomials include the zeros of (Subscript[𝒮, 1]). Here are their degrees.

Function[p, Exponent[p, #] &/@{b, c}]/@(Subscript[𝒮, 4])

All the powers are even, so we introduce new variables to halve the degrees.

Eliminating the variable (Subscript[c, 1]) from (Subscript[𝒮, 5]) leaves a univariate polynomial in  (Subscript[b, 1]).

(Subscript[𝒮, 6]) = 
      Factor[Resultant[##, (Subscript[c, 1])]] &@@(Subscript[𝒮, 5])

Eliminating the variable (Subscript[b, 1]) from (Subscript[𝒮, 5]) leaves a univariate polynomial in (Subscript[c, 1]).

(Subscript[𝒮, 7]) = 
      (Factor[Resultant[##, (Subscript[b, 1])]] &)@@(Subscript[𝒮, 5])

These are the roots of (Subscript[𝒮, 6]) for (Subscript[b, 1]).

bRoots = 
      (Subscript[b, 1]) /. Union[{ToRules[Roots[(Subscript[𝒮, 6]) == 0, (Subscript[b, 1])]]}]

We select the positive ones.

bRoots = Select[bRoots, Positive]

These are the roots of (Subscript[𝒮, 7]) for (Subscript[c, 1]).

Again we select the positive ones.

cRoots = Select[cRoots, Positive]

So we arrive at the following 81 potential minimizing pairs for (Subscript[𝒮, 2]).

bcRoots = 
      Flatten[Outer[{b -> #1, c -> #2} &, (Sqrt[bRoots]), (Sqrt[cRoots])], 1]

We delete the pairs that do not make the two functions of (Subscript[𝒮, 2]) vanish.

allPairs = 
      DeleteCases[bcRoots, 
        _?(((Subscript[𝒮, 2]) /. N[#, 22]) ≠ {0, 0} &)]

We substitute these four pairs into the original expression and evaluate numerically.

RootReduce[Simplify[(Subscript[𝒮, 1]) /. allPairs]]

N[%]

This shows that the minimum value is (Sqrt[3]), when the triangle is equilateral.

Finally, we must investigate the behaviour near the boundary of the region.

Series[(Subscript[𝒮, 1]) /. c -> b + ε, 
        {b, ∞, 2}] // Simplify

As b tends to infinity, (Subscript[𝒮, 1]) approaches 2. Since this is greater than (Sqrt[3]), the local minimum we have found is the global minimum.