Proof inequality given some assumptions on the variables

asked 2016-06-08 01:08:24 +0100

Lux
31 ●1 ●4

updated 2016-06-09 11:21:32 +0100

I have an inequality in multiple variables and want to show that it is true given that the variables satisfy some conditions (also formulated as inequalities).

I come from Mathematica, where I can write Reduce[Implies[0<x<1, x>x^2], Reals] and get true as the answer. Is Sage (maybe with some optional package) able to verify these kinds of implications?

This is a simplified implication I want to show: $0 < f \leq 1$ and $z \geq \frac{1}{\sqrt{1+0.8f}}$, implies $$\left((z+f)^2-f^2-1\right)^2+\left((z-1+2f)^2-4f^2\right) > 0$$

So far I tried qepcad but the following code just ran forever:

var('z, f'); qf = qepcad_formula;
qepcad( qf.implies(qf.and_(f>0, f<=1, z>=1/(sqrt(1+4*f/5))), ((z + f)^2 - f^2 - 1)^2 + (z - 1 + 2*f)^2 - 4*f^2>0) )

Are there better ways to formulate my statement using qepcad, are there better packages available or is Sage not able to help me here?

Note that I don't need help for the given example, as I proved this already. However I have similar more complicated implications of the same form which I need to check using some other CAS than Mathematica. Can Coq do this?

answered 2016-06-11 00:17:50 +0100

tmonteil
27413 ●31 ●204 ●517 http://wiki.sagemath.o...

updated 2016-06-11 14:47:47 +0100

As explained in the documentation, qepcad is supposed to deal with polynomials, so it is likely it is not able to handle the square root (nor the fraction). So, a correct way to formulate your statement using qepcad would be the following (note the additional z>=0 because of the square):

sage: qepcad(qf.implies(qf.and_(f>0, f<=1, z>=0, z^2*(1+4*f/5)>=1), ((z + f)^2 - f^2 - 1)^2 + (z - 1 + 2*f)^2 - 4*f^2>0))
TRUE

The main concern is that it does not raises an error when there is a square root in the formula (probably a lack of sanity checking and/or error handling). I will have a deeper look to the source code and tell if it could be improved. Thanks for reporting anyway.

EDIT

qepcad seem indeed not able to deal with the sqrt, but Sage interace does not handle the error, here is a qepcad session:

Enter a variable list:
(f,z)
Enter the number of free variables:
0
Enter a prenex formula:
(A f) (A z) [[f > 0 /\ f <= 1 /\ z >= 1/sqrt(4/5 f + 1)] ==> ((f + z)^2 - f^2 - 1)^2 + (2 f + z - 1)^2 - 4 f^2 > 0]
Error RPFACTREAD: Digit was expected.
(A f) (A z) [[f > 0 /\ f <= 1 /\ z >= 1/s

edit flag offensive delete link

Comments

Thank you very much! Although the above statement can be restated without square roots, my other formulas cannot. Is there another way without using qepcad?

Lux ( 2016-06-24 17:08:19 +0100 )edit

add a comment

Your Answer

Please start posting anonymously - your entry will be published after you log in or create a new account.

Proof inequality given some assumptions on the variables

1 Answer

Comments

Your Answer

Question Tools

Stats

Related questions

Proof inequality given some assumptions on the variables edit

1 Answer

Comments

Your Answer

Question Tools

Stats

Related questions

Proof inequality given some assumptions on the variables