ASKSAGE: Sage Q&A Forum - Individual question feedhttps://ask.sagemath.org/questions/Q&A Forum for SageenCopyright Sage, 2010. Some rights reserved under creative commons license.Fri, 24 Jun 2016 10:08:19 -0500Proof inequality given some assumptions on the variableshttps://ask.sagemath.org/question/33690/proof-inequality-given-some-assumptions-on-the-variables/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?Tue, 07 Jun 2016 18:06:41 -0500https://ask.sagemath.org/question/33690/proof-inequality-given-some-assumptions-on-the-variables/Answer by tmonteil for <p>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).</p>
<p>I come from Mathematica, where I can write <code>Reduce[Implies[0<x<1, x>x^2], Reals]</code> and get <code>true</code> as the answer. Is Sage (maybe with some optional package) able to verify these kinds of implications?</p>
<p>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$$</p>
<p>So far I tried qepcad but the following code just ran forever:</p>
<pre><code>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) )
</code></pre>
<p>Are there better ways to formulate my statement using qepcad, are there better packages available or is Sage not able to help me here?</p>
<p>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?</p>
https://ask.sagemath.org/question/33690/proof-inequality-given-some-assumptions-on-the-variables/?answer=33746#post-id-33746As 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
Fri, 10 Jun 2016 17:17:50 -0500https://ask.sagemath.org/question/33690/proof-inequality-given-some-assumptions-on-the-variables/?answer=33746#post-id-33746Comment by Lux for <p>As explained in the documentation, <code>qepcad</code> 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 <code>z>=0</code> because of the square):</p>
<pre><code>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
</code></pre>
<p>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.</p>
<p><strong>EDIT</strong></p>
<p><code>qepcad</code> seem indeed not able to deal with the sqrt, but Sage interace does not handle the error, here is a qepcad session:</p>
<pre><code>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
</code></pre>
https://ask.sagemath.org/question/33690/proof-inequality-given-some-assumptions-on-the-variables/?comment=33907#post-id-33907Thank you very much! Although the above statement can be restated without square roots, my other formulas cannot. Is there another way without using qepcad?Fri, 24 Jun 2016 10:08:19 -0500https://ask.sagemath.org/question/33690/proof-inequality-given-some-assumptions-on-the-variables/?comment=33907#post-id-33907