使用 Sympy 检查不等式展开式

Question

我正在使用 Sympy 来检查我为解决完全参数不等式所做的计算是否正确。在这种情况下，我从

exp1 >= exp2

开始，并且用手获得了

exp3 >= exp4

形状的东西。四个表达式中的三个在符号上有些复杂（因为

exp3

只是一个孤立的变量），我想验证我是否犯了错误。

我想在 Sympy 中找到一种方法来执行此操作，或者是否有任何其他软件/库更适合执行此操作。

自从

exp1-exp2>=0

和

exp3-exp4>=0

开始，我尝试使用

simplify((exp1-exp2)-(exp3-exp4))

并检查新表达式是否等于0，但这会导致非零值作为

(exp1-exp2)=a(exp3-exp4)

，其中

a

是非零恒定值（尽管也是象征性的）。由于我要隔离一个参数，因此我还尝试了

reduce_inequalities(exp1>=exp2, [I])

，其中

I

是

exp3

中的变量隔离，但是 Sympy 没有正确隔离变量，我陷入了中间表达式。

Answer 1

您已经快要检查答案了。您已发现

e1 - e2

与

e3 - e4

存在乘法常数的差异。与积分的加法常数一样，等式的乘法常数可以忽略不计。因此，如果可以证明，对于

d1 >= 0

和

d2 >= 0

（其中

di = eq.gts - eq.lts

），ratio

d1/d2

是常数，那么您就已经验证了这两个表达式是相似的。但是，如果您执行诸如扎根一种表达式而不是另一种表达式之类的操作，则这将不起作用。例如

A = x**2 >= 4*y and 

B = x > 2*sqrt(y)`。

检查两个表达式共有的任何表达式的解是否满足另一个表达式，例如

from sympy.abc import x, y
from sympy.core.relational import Relational
A = x**2 >= 4*y
B = x > 2*sqrt(y)
a = Relational(A.lhs - A.rhs, 0, A.rel_op)
b = B.lhs - B.rhs
>>> a.subs(x, solve(b,    x,dict=True)[0][x]).expand(),
True
>>> a.subs(y, solve(b    ,y,dict=True)[0][y]).expand(),
True
>>> a.subs(y, solve(b + 1,y,dict=True)[0][y]).expand()
-2*x - 1 >= 0