为了更好的数学公式和代码块体验，建议在 plweb 阅读本文． 本文是知乎文章 https://zhuanlan.zhihu.com/p/490165068 的导读．原文的问题难度和计算量较大，本文尝试用更简洁直观的例子讲解 **约束法** 证不等式． 换元是代数不等式中的常用手段，但是代换前后的变量往往存在不同的相互关系．如果不能充分分析和利用，就好比做题抛弃已知条件，自然不能成功． 以印度 IMOTC 第 1 天第 1 题为例， > 设实数 $a,b,c$ 满足 > $$\max\left\{a\left(b^2+c^2\right),b\left(c^2+a^2\right),c\left(a^2+b^2\right)\right\}\le2abc+1,$$ > 证明 > $$a\left(b^2+c^2\right)+b\left(c^2+a^2\right)+c\left(a^2+b^2\right)\le6abc+2.$$ 因为 $a\left(b^2+c^2\right)-2abc=a(b-c)^2$，所以可根据对称性设 $x=a(b-c)^2$，$y=b(c-a)^2$，$z=c(a-b)^2$．现在条件变为 $\max\{x,y,z\}\le1$，也就是 $x\le1$，$y\le1$，$z\le1$；目标变为 $x+y+z\le2$． 事实上，三个不超过 $1$ 的数之和的最大值是 $1+1+1=3$，因此做到这一步还证不出目标中的上界 $2$．究其原因，在换元之后，$(x,y,z)$ 的取值范围不再如 $(a,b,c)$ 般是 $\mathbb R^3$，而是变得更窄．例如假设 $x=y=z=1$，检验得 ``` from sympy import solve, symbols a, b, c = symbols('a b c', real=True) eqns = [a*(b-c)**2 - 1,b*(c-a)**2 - 1,c*(a-b)**2 - 1] solve(eqns, a, b, c, dict=True) # 无解 ``` 为了找出 $x$，$y$，$z$ 的额外约束，我们采用和上述验证代码相同的思路，考虑方程组 $$a(b-c)^2-x=b(c-a)^2-y=c(a-b)^2-z=0$$ 何时有解 $(a,b,c)\in\mathbb R^3$．用结式消去 $b$ 和 $c$ 得 $$Q_{x,y,z}\left(a^3\right)=0.（具体结果见文末~[1]）$$ 这是关于 $a^3$ 的二次方程，有解的条件是判别式非负，计算得 $$\begin{aligned}\Delta=(y-z)^2 &(x y-y^2+x z+2 y z-z^2)^2\\ \cdot&(x^2-2 x y+y^2-2 x z-2 y z+z^2)^3.\end{aligned}$$ 所以 $\Delta\ge0$ 关键在最后一个奇数次方的因式，需要 $$x^2+y^2+z^2-2xy-2yz-2zx\ge0.$$ 另一方面，容易验证该式的确成立： $$\sum x^2-2\sum xy\equiv(a-b)^2(b-c)^2(c-a)^2\ge0.$$ 有了这个不等式，我们再进行一次验证（z3）[2] ``` (set-logic NRA) (declare-const x Real) (declare-const y Real) (declare-const z Real) (assert (>=(-(+(* x x)(* y y)(* z z))(* 2 x y)(* 2 y z)(* 2 z x))0)) (assert (<= x 1)) (assert (<= y 1)) (assert (<= z 1)) (assert (> (+ x y z) 2)) (check-sat) ; 输出 unsat，即无反例 ``` 也就是说，下述结论成立 $$\begin{cases}x,y,z\in\mathbb R,\ x,y,z\le1,\\\sum x^2-2\sum xy\ge0\end{cases}\Rightarrow x+y+z\le2.$$ 至此，换元结构引入的限制被新的不等式充分表达，问题真正脱离了最初的变量．后续不难用初等对称多项式的方式解决，详见笔者在 AoPS 上的贴文 https://artofproblemsolving.com/community/c6h3585178p35207339 或下述恒等式 $$2-\sum x=\frac{\sum\left(x^2-2xy\right)+4\sum(1-x)(1-y)+3\left(2-\sum x\right)^2}{4\sum(1-x)}\ge0.$$ 本题获取限制条件的方法是消元后计算 *二次方程* 的判别式．一般地，消元的结果可能是高次多项式 $$f(x) = a_n x^n + a_{n-1} x^{n-1} + \cdots + a_1 x + a_0,$$ 这里各项系数是关于参数的函数．直观上（严格论证需代数基本定理、Rouché 定理等）参数值连续变化使 $a_i$ 连续变化，进而使 $f$ 根的集合连续变化．因此在有实根到无实根的临界点应该是有 **重根**．重根是 $f$ 和 $f'$ 的公共根，因此考虑 $$\Delta=\operatorname{Res}(f,f').（标准判别式有系数\ \frac{(-1)^{\frac{n(n-1)}2}}{a_n}）$$ 再分析一个更复杂的例题， > 已知 $a,b,c>0$，求证：$\sum\frac ab+\frac{11abc}{4\sum a^3}\ge\frac{47}{12}$． 题目的结构已经十分清晰，我们设 $x=\sum\frac ab$，$y=\frac{abc}{\sum a^3}$，则要证明 $x+\frac{11}4y\ge\frac{47}{12}$．为此寻找 $x$ 和 $y$ 之间的约束．不妨设 $a=1$，消去 $b$，再计算关于 $c$ 的判别式，找到唯一的奇数次因式 $$F(x,y)=:27 x^6 y^4-2 x^3 y (3 y+2) \left(63 y^2+3 y+1\right)+27 \left(9 y^2+3 y+1\right)^2.$$ 代入得 $$F(x,y)=-\frac{\big[\sum\big(a^{5}c-2a^{4}b^{2}+a^{3}bc^{2}\big)\big]^{2}\sum\big(4a^{5}c+a^{4}b^{2}+22a^{3}bc^{2}\big)}{a^{2}b^{2}c^{2}\left(a^{3}+b^{3}+c^{3}\right)^{4}}\le0.$$ 这是一个典型的目标简洁，条件复杂的情况，因此适合 **反证法**：假设 $x+\frac{11}4y<\frac{47}{12}$，证明 $F(x,y)>0$． 若 $y\ge\frac13$，则 $$F(x, y)=27 y^{4}\left(x^{3}-\frac{378 y^{4}+270 y^{3}+18 y^{2}+4 y}{54 y^{4}}\right)^{2}+\frac{4(3 y-1)^{3}(6 y+1)^{3}}{27 y^{2}} \geq 0 .$$ 若 $y<\frac13$，有 $$\frac{378 y^{4}+270 y^{3}+18 y^{2}+4 y}{54 y^{4}} \geq\left(\frac{47-33 y}{12}\right)^{3},$$ 所以 $$F(x,y)\ge F\left(\frac{47-33y}{12},y\right)=\cdots\ge0.$$ 部分计算过程略． ### 总结 约束法是解决进行复杂换元后条件不足以推出所需结论的问题的有效办法，寻找约束的基本流程是 消元 + 求判别式． 应当注意的问题是： - 实践中随着换元变得复杂，得到的约束可能也更难使用， - 所得约束只是“必要条件”，不一定完整刻画实际可行范围（例如第二个例题并没有完美处理反解出原变量为正数的要求）． --- [1] $$x^3 y^2 z^2+a^6 \left(\begin{aligned}x^5-4 x^4 y+6 x^3 y^2-4 x^2 y^3+x y^4-4 x^4 z+4 x^3 y z+4 x^2 y^2 z\\-4 x y^3 z+6 x^3 z^2+4 x^2 y z^2+6 x y^2 z^2-4 x^2 z^3-4 x y z^3+x z^4\end{aligned}\right)\\+a^3 \left(\begin{aligned}-x^4 y^2+4 x^3 y^3-6 x^2 y^4+4 x y^5-y^6+6 x^2 y^3 z-12 x y^4 z+\\6 y^5 z-x^4 z^2+8 x y^3 z^2-15 y^4 z^2+4 x^3 z^3+6 x^2 y z^3+8 x y^2 z^3\\+20 y^3 z^3-6 x^2 z^4-12 x y z^4-15 y^2 z^4+4 x z^5+6 y z^5-z^6\end{aligned}\right)=0.$$ [2] 可在如下网页运行 z3 代码： https://microsoft.github.io/z3guide/playground/Freeform%20Editing