During high school, like many students, I participated in mathematics competitions. In the process of preparing for these competitions, I solved various competition problems, which naturally included inequality problems. At that time, facing a wide variety of inequality proof problems, I often felt quite lost. Even after seeing the solutions, I always felt that the constructions of the proofs were mysteriously ingenious, yet I could never think of them myself when working independently. Consequently, the idea emerged: “Is there a universal method to prove these inequalities?” To achieve this goal, I came up with the technique presented in this article—sacrificing computational simplicity in exchange for the effectiveness of the proof. Later, although I did not pursue the path of mathematics competitions, this method remained with me. Recently, while discussing inequality problems with friends on a mathematics research forum, I picked up this technique again.
Previously, in the blog post “Physical Proof” of Symmetric Polynomial Inequalities, I touched upon this technique. However, limited by my knowledge at the time, my understanding was not deep. In this article, I will expand upon it. I discovered this technique independently during my own proofs back then, but searching online now reveals that predecessors (such as Yang Lu, Yao Yong, and Yang Xuezhi) had already researched this technique long ago, calling it “Difference Substitution” and exploring its role in machine proofs. This technique can be applied very generally to the proof of homogeneous and non-homogeneous inequalities. Due to space constraints, this article only discusses homogeneous polynomial inequalities, specifically symmetric homogeneous polynomial inequalities, and identifies certain areas where simplification is possible.
Basic Example
We begin with the “old chestnut,” the Arithmetic-Geometric Mean (AM-GM) inequality: a^3+b^3+c^3 \geq 3abc, \quad \forall a,b,c \geq 0 as an introductory example. There are many elegant proof methods for the AM-GM inequality, such as those in Two Clever Proofs of the AM-GM Inequality. Here, we use Difference Substitution for an “inelegant” proof. The trick of Difference Substitution is to assume a \leq b \leq c and then use the following substitution: \begin{aligned} a &= a \\ b &= a + u \\ c &= a + u + v \end{aligned} \quad \forall a,u,v \geq 0 This yields: \begin{aligned} & a^3 + b^3 + c^3 - 3abc \\ =& a^3 + (a+u)^3 + (a+u+v)^3 - 3a(a+u)(a+u+v) \\ =& 3 a u^2 + 3 a u v + 3 a v^2 + 2 u^3 + 3 u^2 v + 3 u v^2 + v^3 \end{aligned} Since the coefficients of the terms in the final expression are all positive, it is clearly non-negative, and thus the inequality holds.
The same technique can be used for non-symmetric inequalities, such as f(a,b,c) \geq 0, provided the inequality attains equality when a=b=c. However, because a,b,c are not symmetric, one must prove it for all permutations of a,b,c (6 cases in total) using the same method (enumeration). The role of symmetry is to reduce the number of enumerations. For example, if there is cyclic symmetry, the number of enumerations can be reduced to 2. If it is fully symmetric, as in this example, only one verification is needed. Because the calculation involves a large number of polynomial expansions, especially when there are many variables or high degrees, it is often difficult to complete manually. Therefore, the Difference Substitution technique is more suitable for machine proofs, where software is used to handle the complex expansion parts.
The Difference Substitution technique has a very wide range of applications. Let’s look at a pre-selected problem from the 31st IMO: (a^2+ab+b^2)(b^2+bc+c^2)(c^2+ca+a^2) \geq (ab+bc+ca)^3
This is a fully symmetric inequality, meaning that swapping any two variables leaves the inequality unchanged. Thus, we can assume a \leq b \leq c. Let b=a+u and c=a+u+v. We have: \begin{aligned} & f(a,b,c) \\ =& (a^2+ab+b^2)(b^2+bc+c^2)(c^2+ca+a^2) - (ab+bc+ca)^3 \\ =& 9 a^4 u^2 + 26 a^3 u^3 + 27 a^2 u^4 + 12 a u^5 + 2 u^6 + 9 a^4 u v + \\ & 39 a^3 u^2 v + 54 a^2 u^3 v + 30 a u^4 v + 6 u^5 v + 9 a^4 v^2 + \\ & 33 a^3 u v^2 + 48 a^2 u^2 v^2 + 30 a u^3 v^2 + 7 u^4 v^2 + \\ & 10 a^3 v^3 + 21 a^2 u v^3 + 15 a u^2 v^3 + 4 u^3 v^3 + 3 a^2 v^4 + \\ & 3 a u v^4 + u^2 v^4 \end{aligned} It is very long and complex; indeed, I expanded this using Mathematica. I do not expect any student to use such a technique in an exam. However, Difference Substitution is indeed an effective means of proof. As can be seen, all coefficients in the final expansion are positive, so the inequality obviously holds.
I have tested many similar fully symmetric inequalities today and found that they can all be successfully proven. What surprised me is that I have not yet found a fully symmetric inequality where the final expansion contains negative coefficients.
Cyclic Symmetric Inequalities
In this section, we prove a cyclic inequality: 4(a+b+c)^3 \geq 27(ab^2+bc^2+ca^2+abc), \quad \forall a,b,c \geq 0
This problem is not fully symmetric; it possesses cyclic symmetry (or rotational symmetry), meaning it remains unchanged under: \begin{aligned} &(a,b,c) \to (b,c,a) \\ &(a,b,c) \to (c,a,b) \end{aligned} This allows us to fix one variable as the minimum, say a, and then separately assume a \leq b \leq c or a \leq c \leq b for verification.
First, let F(a,b,c) = 4(a+b+c)^3 - 27(ab^2+bc^2+ca^2+abc). For a \leq b \leq c, let b=a+u and c=a+u+v. We have: \begin{aligned} & F(a,a+u,a+u+v) \\ =& 9 a u^2 + 5 u^3 + 9 a u v - 6 u^2 v + 9 a v^2 - 3 u v^2 + 4 v^3 \end{aligned} Wait, negative coefficients appeared? However, this is not difficult to handle. We know that a can be arbitrarily large, while u and v can be arbitrarily close to 0. Since the equality holds at u=v=0, the power of a actually represents the “order” of each term. To handle the negative terms, we group terms of the same order: \begin{aligned} & F(a,a+u,a+u+v) \\ =& 9 a u^2 + 5 u^3 + 9 a u v - 6 u^2 v + 9 a v^2 - 3 u v^2 + 4 v^3 \\ =& 9 a (u^2+uv+v^2) + (5 u^3 - 6 u^2 v - 3 u v^2 + 4 v^3) \end{aligned} One only needs to notice that 5 u^3 - 6 u^2 v - 3 u v^2 + 4 v^3 = (u - v)^2 (5 u + 4 v) to complete the proof for this case.
For a \leq c \leq b, let c=a+u and b=a+u+v. We have: \begin{aligned} & F(a,a+u+v,a+u) \\ =& 9 a u^2 + 5 u^3 + 9 a u v + 21 u^2 v + 9 a v^2 + 24 u v^2 + 4 v^3 \end{aligned} This is a simple case with all positive coefficients. The proof is complete.
Next, let’s prove a very difficult inequality: \frac{1}{4}\left(\frac{a^2}{b}+\frac{b^2}{c}+\frac{c^2}{d}+\frac{d^2}{a}\right) \geq \sqrt{\frac{a^4+b^4+c^4+d^4}{4}}, \quad \forall a,b,c,d \geq 0
This problem is also a cyclic symmetric inequality. We can transform the problem into proving the non-negativity of: f(a,b,c,d) = \left[\frac{1}{4}\left(\frac{a^2}{b}+\frac{b^2}{c}+\frac{c^2}{d}+\frac{d^2}{a}\right)\right]^4 - \frac{a^4+b^4+c^4+d^4}{4} which further transforms into the non-negativity of:
There are 4! = 24 possible orderings of a,b,c,d, but cyclic symmetry reduces the number of cases to 6. We assume a is the minimum and prove the six cases for b,c,d in turn. For example, when a \leq b \leq c \leq d, let b=a+u, c=a+u+v, d=a+u+v+w. Expanding this yields a polynomial over 600 lines long!! However, verification shows that every single term has a positive coefficient, thus completing the proof. Checking the remaining cases, we find that only in the cases a \leq c \leq d \leq b and a \leq c \leq b \leq d do negative terms like the following appear: 3248 d^{17} u^3 + 1936 d^{17} u w^2 - 1360 d^{17} u^2 w and - 192 d^{18} u w + 224 d^{18} w^2 + 224 d^{18} u^2 The non-negativity of these terms is obvious.
Conclusion
This article provides a method of “machine proof,” using software to tirelessly complete polynomial expansions and directly prove inequalities by judging the positivity of coefficients or transforming them into simpler inequalities. Surprisingly, if the inequality holds for all real numbers (rather than being restricted to non-negative reals), this technique is somewhat lacking and requires further transformation. For example, to prove Vasc’s inequality (a^2+b^2+c^2)^2 \geq 3(a^3 b + b^3 c + c^3 a), which holds for all real a,b,c, even if we restrict it to non-negative reals, the above technique cannot prove it directly in one step and requires further transformation.
Finally, it is necessary to explain why this article emphasizes “homogeneity.” In fact, homogeneous inequalities are those that possess physical meaning; homogeneity implies that the “dimensions” on both sides are equal, which is the meaning of the “physical proof” I mentioned earlier. If an inequality is non-homogeneous, it generally attains equality at specific points rather than just at a=b=c, which increases the difficulty. Of course, as I have mentioned, the application of Difference Substitution is actually very broad. After expansion, it can be used for many non-homogeneous inequality proofs, but that is beyond the scope of this article. Interested readers can first read relevant papers or books; perhaps we will return to this topic if the opportunity arises.
References
Methods of Proving Elementary Inequalities, edited by Han Jingjun.
Machine Proof and Automated Discovery of Inequalities, by Yang Lu and Xia Bican.
When reposting, please include the original address: https://kexue.fm/archives/2747
For more detailed reposting matters, please refer to: Scientific Space FAQ