3
$\begingroup$

I wanted to know whether the following statement is correct.

Let $a$, $b$, $c$, $d$ be positive real numbers such that $abcd=1$, then $$\frac{(3 a+1) (d-1)}{a+1}+\frac{(a-1) (3 d+1)}{d+1}+\frac{(3 b+1) (c-1)}{b+1}+\frac{(b-1) (3 c+1)}{c+1}\geq 0$$ always holds.

I tried to use FindInstance[] to find a counterexample,

FindInstance[{((a - 1) (3 d + 1))/(d + 1) + ((b - 1) (3 c + 1))/(
    c + 1) + ((c - 1) (3 b + 1))/(b + 1) + ((d - 1) (3 a + 1))/(
    a + 1) < 0, a b c d == 1}, {a, b, c, d}, PositiveReals]

The output came quickly and it was an empty list {}.

I then tried to use Resolve[] to verify it,

Resolve[ForAll[{a, b, c, 
   d}, {a b c d == 1}, ((a - 1) (3 d + 1))/(
    d + 1) + ((b - 1) (3 c + 1))/(c + 1) + ((c - 1) (3 b + 1))/(
    b + 1) + ((d - 1) (3 a + 1))/(a + 1) >= 0], PositiveReals]

But the evaluation lasted for a long time.

Why is it so?

Improve this question
$\endgroup$
1
  • $\begingroup$ The software failed to evaluate the second code. The kernel quit for some reason (perhaps out of memory) $\endgroup$
    – youthdoo
    Commented Aug 14 at 11:10

3 Answers 3

Reset to default
5
$\begingroup$

Do not use more variables than necessary. If you eliminate one variable using "a b c d ==1", Resolve evaluates quickly to True:

Resolve[ForAll[{a, b, 
   c}, ((a - 1) (3 d + 1))/(d + 1) + ((b - 1) (3 c + 1))/(c + 
        1) + ((c - 1) (3 b + 1))/(b + 1) + ((d - 1) (3 a + 1))/(a + 
        1) >= 0 /. d -> 1/(a b c)], PositiveReals]

True
Improve this answer
$\endgroup$
4
$\begingroup$

One can work with four variables, considering the negation of the implication..

Resolve[Exists[{a, b, c, d},  a  b  c  d == 
1 && ((a - 1)  (3  d + 1))/(d + 1) + ((b - 1)  (3  c + 1))/(c + 
    1) + ((c - 1)  (3  b + 1))/(b + 
    1) + ((d - 1)  (3  a + 1))/(a + 1) < 0], PositiveReals]

False

Addition. In 14.1 on Windows 10

Resolve[ForAll[{a, b, c, d},  Implies[a b c d == 
1, ((a - 1) (3 d + 1))/(d + 1) + ((b - 1) (3 c + 1))/(c + 
    1) + ((c - 1) (3 b + 1))/(b + 1) + ((d - 1) (3 a + 1))/(a + 
    1) >= 0]], PositiveReals]

True

in few minutes.

Improve this answer
$\endgroup$
3
  • $\begingroup$ See Wiki concerning the negation of the implication. $\endgroup$
    – user64494
    Commented Aug 14 at 13:30
  • $\begingroup$ I'll try the code later. So Exists[] is more efficient than ForAll[]? $\endgroup$
    – youthdoo
    Commented Aug 14 at 14:30
  • $\begingroup$ @youthdoo: More exactly, the negation of the quantified implication appears simpler for Resolve than that implication. $\endgroup$
    – user64494
    Commented Aug 14 at 14:54
3
$\begingroup$ 
In[1]:= Implies[a b c d ==                                                      
1, ((a - 1) (3 d + 1))/(d + 1) + ((b - 1) (3 c + 1))/(c +                       
    1) + ((c - 1) (3 b + 1))/(b + 1) + ((d - 1) (3 a + 1))/(a +                 
    1) >= 0]//BooleanConvert//InputForm                                         

Out[1]//InputForm= 
a*b*c*d != 1 || ((1 + 3*b)*(-1 + c))/(1 + b) + ((-1 + b)*(1 + 3*c))/(1 + c) + 
   ((1 + 3*a)*(-1 + d))/(1 + a) + ((-1 + a)*(1 + 3*d))/(1 + d) >= 0

Hence you no longer have an equation that can be used to eliminate a variable. One more variable in an algorithm that is doubly exponential in the number of variables makes a difference.

Improve this answer
$\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.