15
$\begingroup$

Question summary: I would like to learn some tips and tricks on how to prove inequalities with Mathematica.

I'm studying various inequalities in triangle that have the form $R+ar + bs\geq 0$, where $R$ is a circumcircle radius, $r$ is an incircle radius and $s$ is a semiperimeter of a triangle.

ClearAll[R, r, s, isTriangle];
R[x_, y_, z_] := (
 x y z)/Sqrt[(x + y - z) (x - y + z) (-x + y + z) (x + y + z)];
r[x_, y_, z_] := 
  1/2 Sqrt[((x + y - z) (x - y + z) (-x + y + z))/(x + y + z)];
s[x_, y_, z_] := (x + y + z)/2;
isTriangle := 1 >= x > 0 && 1 >= y > 0 && x + y > 1;

I normalize the longest side $z=1$ to simplify the calculation. isTriangle is a condition that there is a triangle with sides $1,x,y$.

I want to prove the following inequalities: $s-3\sqrt{3}r\geq0$ and $-\frac s2+(-2+3\sqrt{3}/2)r+R\geq 0$ for all triangles.

I can easily check that both inequalities are true with the following code:

FindMinimum[{s[1, x, y] - 3 Sqrt[3] r[1, x, y], isTriangle}, {x, y}]

(returns {1.26714*10^-6, {x -> 0.998875, y -> 0.998875}}), i.e. the minimum is $0$);

Resolve[ForAll[{x, y}, isTriangle, 
  s[1, x, y] - 3 Sqrt[3] r[1, x, y] >= 0]]
(* True *)

(checks that inequality holds for all triangles);

FindMinimum[{-s[1, x, y]/2 + (-2 + 3 Sqrt[3]/2) r[1, x, y] + 
   R[1, x, y], isTriangle}, {x, y}]

(returns {9.01882*10^-7, {x -> 0.996601, y -> 0.996601}}, i.e. the minimum is $0$);

Resolve[ForAll[{x, y}, 
  isTriangle, -s[1, x, y]/2 + (-2 + 3 Sqrt[3]/2) r[1, x, y] + 
    R[1, x, y] >= 0]]
(* True *)

(checks that inequality holds for all triangles, but takes some time).

However, I want to find a way to prove them, e.g. so that a human who doesn't trust Mathematica can check that they are always true. I would appreciate some general tips and tricks; e.g. it may be possible to find proves for these particular examples, but I would like to know some (heuristic) methods that could work for some other inequalities, too.

Thanks you very much for your time!

$\endgroup$
8
  • 3
    $\begingroup$ psc.informatik.uni-jena.de/fpp/analytica.pdf $\endgroup$ Jun 12, 2012 at 5:00
  • $\begingroup$ Wow, that was quick! I downloaded Analytica package from here: andrej.com/analytica and noticed that it was written in 1997 for Mathematica 2.0 and never updated since. I'll try to run it but do you by any chance know if it was developed recently? $\endgroup$
    – Victor K.
    Jun 12, 2012 at 5:07
  • 1
    $\begingroup$ I know there was an Analytica 2 for Mathematica v5. Not much, but .. $\endgroup$ Jun 12, 2012 at 5:08
  • 1
    $\begingroup$ If you write a post, you can use a block of code by indenting 4 spaces. This looks far better and magically you get syntax-highlighting for free. I edited your post. $\endgroup$
    – halirutan
    Jun 12, 2012 at 5:41
  • 1
    $\begingroup$ @Victor if you see formatting in a post that you don't know how to do, you can click edit and view the raw text for that very post. $\endgroup$
    – Mr.Wizard
    Jun 12, 2012 at 19:44

1 Answer 1

7
$\begingroup$

Yes, Mathematica can prove these inequalities symbolically. To be more precise, it can Reduce them to True. Generating human-readable proofs is also possible but that's one broad topic.

First, we'll use a “coordinate change”. Notice that your expressions for R, s, r are all symmetric in x, y, z. This hints that we might benefit from using symmetric polynomials of x, y, z instead of x, y, z themselves.

    symPolysTable =
            Thread@Rule[
              SymmetricPolynomial[#, {x, y, z}] & /@ Range@3
            , {α, β, γ}]

(* {x + y + z -> α, x y + x z + y z -> β, x y z -> γ} *)

The only not-so-symmetric expression encountered here is (x + y - z) (x - y + z) (-x + y + z). Let's rewrite it in terms of α, β, γ:

balancedSidesPoly = 
            Part[SymmetricReduction[(x + y - z) (x - y + z) (-x + y + z)
                 , {x, y, z}
                 , {α, β, γ}]
            , 1]

(* -α^3 + 4 α β - 8 γ *)

(Part 2 of the expression is “remainder”. It is zero, because polynomial is symmetric, so we ignore it.)

Check out R, r, s rewritten in terms of greek coordinates:

rules =
            { R -> γ/Sqrt[balancedSidesPoly α]
            , r -> 1/2 Sqrt[balancedSidesPoly/α]
            , s -> α/2 }

(* (…) We shall need these coordinate change rules later, to change statements written in latin coordinates to their “greek” analogues. *)

Now let's gather facts about triangle in greek form:

sidesArePositive = And[α > 0, β > 0, γ > 0];

You may check that this is indeed equivalent to And[x > 0, y > 0, z > 0]:

Reduce[sidesArePositive /. Reverse /@ symPolysTable]

(* z > 0 && y > 0 && x > 0 *)

Reduce[# > 0 & /@ (SymmetricPolynomial[#, {x, y, z}] & /@ Range@3)]

(* z > 0 && y > 0 && x > 0*)

The triangle inequalities for sides are probably represented by the statement *)

sidesAreBalanced = balancedSidesPoly > 0

(* -α^3 + 4 α β - 8 γ > 0 *)

(It is obviously neccessary for triangle existence but I haven't checked if it is sufficient as well.)

The last fact that we shall need is *)

sidesAreReal = 
            Discriminant[
              Collect[(σ - x) (σ - y) (σ - z), σ] /.
              {-x - y - z -> -α, x y + x z + y z -> β, x y z -> γ}
            , σ] >= 0

(* α^2 β^2 - 4 β^3 - 4 α^3 γ + 18 α β γ - 27 γ^2 >= 0

The polynomial in σ is cubic with real roots. Hence, its discriminant must be nonnegative.

Gather all the facts in one statement: *)

allFacts = And[sidesArePositive, sidesAreBalanced, sidesAreReal]

(* α > 0 && β > 0 && γ > 0 && -α^3 + 4 α β - 8 γ > 0 && α^2 β^2 - 4 β^3 - 4 α^3 γ + 18 α β γ - 27 γ^2 >= 0*)

This polynomial reducer will transform arbitrary latin statements to greek ones:

toGreekCoordinates[expr_, knownFacts_] :=
             Refine[expr /. rules // Simplify // Reduce, knownFacts]

Check out the Euler inequality:

    toGreekCoordinates[R >= 2 r, allFacts]

(* True Assuming only that sides are positive wouldn't suffice: *)

toGreekCoordinates[R >= 2 r, sidesArePositive]

(* (α^3 + 8 γ)/(4 α) < β <= (α^3 + 9 γ)/(4 α)

Now, your inequalities can be reduced with allFacts: *)

toGreekCoordinates[3 Sqrt[3] r <= s, allFacts]

(* True *)

toGreekCoordinates[3 Sqrt[3] r + 2 R >= s + 4 r, allFacts]

(* True *)

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.