Ask Your Question

Lux's profile - activity

2016-06-24 17:08:19 +0100 commented answer Proof inequality given some assumptions on the variables

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?

2016-06-24 17:04:30 +0100 received badge  Supporter (source)
2016-06-11 04:37:47 +0100 received badge  Good Question (source)
2016-06-11 00:17:58 +0100 received badge  Nice Question (source)
2016-06-09 11:21:32 +0100 received badge  Editor (source)
2016-06-08 09:02:08 +0100 received badge  Student (source)
2016-06-08 09:01:36 +0100 asked a question 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?