Mathematica FindInstance[] 给出了错误的答案

Mathematica FindInstance[] gives wrong answer

我正在尝试使用 Mathematica 来验证以下函数

V[x1_, x2_, u1_, u2_] = 1.494*u1^2 - 2.094 10^-24*u1 + 1.494*u2^2 - 3.988*u2 + 1.994*x2^2 - 7.333 10^-24*x2 + 2.494

是正定约束 u1^2+u2^2==1

Reduce[ForAll[{x1, x2, u1, u2}, u1^2 + u2^2 == 1, V[x1, x2, u1, u2] >= 0], {x1, x2, u1, u2}, Reals]

returns 错误。但是搜索反例

cex = FindInstance[u1^2 + u2^2 == 1 && V[x1, x2, u1, u2] < 0, {x1, x2, u1, u2}, Reals] V[x1, x2, u1, u2] /. cex

给予

{{x1 -> 0.2, x2 -> 0, u1 -> 5.16988*10^-25, u2 -> 1.}} {2.22045*10^-16}

因此,Mathematica 似乎自相矛盾。我犯了什么错误?

此处的一种方法:使表达式准确。 (你应该检查我做对了)

exp=1494/1000*u1^2 - 2094 10^-27*u1 + 1494/1000*u2^2 - 3988/1000*u2 + 
 1994/1000*x2^2 - 7333 10^-27*x2 + 2494/1000

现在我们可以找到一个精确的最小值:

min = Minimize[{exp, u1^2 + u2^2 == 1}, {u1, u2, x2}] // Simplify //First

这是否定的:

min<0

True

然而它是一个非常小的负值:

N[min, 20]

-7.2915903961885656971*10^-48

我的猜测是原始表达式被构造为具有零最小值,并且没有为常量提供足够的精度。 使最后一个常量为零的示例需要

2.4940000000000000000000000000000000000000000000072915903961..

虽然考虑到您的系数在 10^-24 的数量级,但也许这很重要。