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!
edit
and view the raw text for that very post. $\endgroup$