DOE MACSYMA Version 10. (c1) Batching the file triang Batching done. (d1) triang (c2) (c3) /* */ showproof: true $ (c4) /* 4.2 */ trineq(s^2>=3*K*sqrt(3)); 2 To prove: s >= 3 sqrt(3) K Since 3 sqrt(3) is positive, and since 2 s is positive, we can square both sides to get: 4 4 3 2 s >= 27 s + (- 27 c - 27 b - 27 a) s + ((27 b + 27 a) c + 27 a b) s - 27 a b c s Expanding and collecting terms of the same sign gives: 3 3 3 27 c s + 27 b s + 27 a s + 27 a b c s >= 4 2 2 2 26 s + 27 b c s + 27 a c s + 27 a b s Dividing both sides by s gives: 2 2 2 27 c s + 27 b s + 27 a s + 27 a b c >= 3 26 s + 27 b c s + 27 a c s + 27 a b s Let s = (c+b+a)/2 . We get: 3 2 2 2 3 2 (27 c + (81 b + 81 a) c + (81 b + 270 a b + 81 a ) c + 27 b + 81 a b 2 3 3 2 + 81 a b + 27 a )/4 >= (13 c + (93 b + 93 a) c 2 2 3 2 2 3 + (93 b + 240 a b + 93 a ) c + 13 b + 93 a b + 93 a b + 13 a )/4 Multiplying both sides by 4 gives: 3 2 2 2 2 3 2 27 c + 81 b c + 81 a c + 81 b c + 270 a b c + 81 a c + 27 b + 81 a b 2 3 3 2 2 2 2 + 81 a b + 27 a >= 13 c + 93 b c + 93 a c + 93 b c + 240 a b c + 93 a c 3 2 2 3 + 13 b + 93 a b + 93 a b + 13 a Expanding and collecting terms of the same sign gives: 3 3 3 2 2 2 2 14 c + 30 a b c + 14 b + 14 a >= 12 b c + 12 a c + 12 b c + 12 a c 2 2 + 12 a b + 12 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 3 2 2 2 3 2 (7 z + (18 y + 18 x) z + (18 y + 15 x y + 18 x ) z + 7 y + 18 x y 2 3 3 2 2 2 + 18 x y + 7 x )/2 >= (6 z + (15 y + 15 x) z + (15 y + 36 x y + 15 x ) z 3 2 2 3 + 6 y + 15 x y + 15 x y + 6 x )/2 Multiplying both sides by 2 gives: 3 2 2 2 2 3 2 7 z + 18 y z + 18 x z + 18 y z + 15 x y z + 18 x z + 7 y + 18 x y 2 3 3 2 2 2 2 + 18 x y + 7 x >= 6 z + 15 y z + 15 x z + 15 y z + 36 x y z + 15 x z 3 2 2 3 + 6 y + 15 x y + 15 x y + 6 x Expanding and collecting terms of the same sign gives: 3 2 2 2 2 3 2 2 3 z + 3 y z + 3 x z + 3 y z + 3 x z + y + 3 x y + 3 x y + x >= 21 x y z Expressing in terms of symmetric polynomials gives: {3, 0, 0} + 6 {2, 1, 0} >= 7 {1, 1, 1} This follows from the following majorizations: 6 {2, 1, 0} >= 6 {1, 1, 1} {3, 0, 0} >= {1, 1, 1} (d4) true (c5) /* 4.3 */ trineq(s^2>=3*K*sqrt(3)+(1/2)*csum((a-b)^2)); 2 2 2 2 (c - a) + (b - c) + (a - b) To prove: s >= ------------------------------ + 3 sqrt(3) K 2 Expanding and collecting terms of the same sign gives: 2 2 2 2 s + b c + a c + a b >= c + b + a + 3 sqrt(3) K Bringing all terms involving K to the right side yields: 2 2 2 2 s - c + (b + a) c - b + a b - a >= 3 sqrt(3) K Since 3 sqrt(3) is positive, and since 2 2 2 2 s - c + (b + a) c - b + a b - a is positive, we can square both sides to get: 4 2 2 2 2 4 3 s + (- 2 c + (2 b + 2 a) c - 2 b + 2 a b - 2 a ) s + c + (- 2 b - 2 a) c 2 2 2 3 3 4 3 2 2 3 + (3 b + 3 a ) c + (- 2 b - 2 a ) c + b - 2 a b + 3 a b - 2 a b 4 4 3 2 + a >= 27 s + (- 27 c - 27 b - 27 a) s + ((27 b + 27 a) c + 27 a b) s - 27 a b c s Expanding and collecting terms of the same sign gives: 3 3 3 4 2 2 2 2 4 27 c s + 27 b s + 27 a s + 27 a b c s + c + 3 b c + 3 a c + b 2 2 4 4 2 2 2 2 2 2 + 3 a b + a >= 26 s + 2 c s + 25 b c s + 25 a c s + 2 b s 2 2 2 3 3 3 3 3 3 + 25 a b s + 2 a s + 2 b c + 2 a c + 2 b c + 2 a c + 2 a b + 2 a b Let s = (c+b+a)/2 . We get: 4 3 2 2 2 (35 c + (108 b + 108 a) c + (186 b + 432 a b + 186 a ) c 3 2 2 3 4 3 2 2 + (108 b + 432 a b + 432 a b + 108 a ) c + 35 b + 108 a b + 186 a b 3 4 4 3 + 108 a b + 35 a )/8 >= (17 c + (126 b + 126 a) c 2 2 2 3 2 2 3 + (186 b + 414 a b + 186 a ) c + (126 b + 414 a b + 414 a b + 126 a ) c 4 3 2 2 3 4 + 17 b + 126 a b + 186 a b + 126 a b + 17 a )/8 Multiplying both sides by 8 gives: 4 3 3 2 2 2 2 2 3 35 c + 108 b c + 108 a c + 186 b c + 432 a b c + 186 a c + 108 b c 2 2 3 4 3 2 2 3 + 432 a b c + 432 a b c + 108 a c + 35 b + 108 a b + 186 a b + 108 a b 4 4 3 3 2 2 2 2 2 + 35 a >= 17 c + 126 b c + 126 a c + 186 b c + 414 a b c + 186 a c 3 2 2 3 4 3 2 2 + 126 b c + 414 a b c + 414 a b c + 126 a c + 17 b + 126 a b + 186 a b 3 4 + 126 a b + 17 a Expanding and collecting terms of the same sign gives: 4 2 2 2 4 4 18 c + 18 a b c + 18 a b c + 18 a b c + 18 b + 18 a >= 3 3 3 3 3 3 18 b c + 18 a c + 18 b c + 18 a c + 18 a b + 18 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 4 3 2 2 2 (9 z + (27 y + 27 x) z + (45 y + 36 x y + 45 x ) z 3 2 2 3 4 3 2 2 3 + (27 y + 36 x y + 36 x y + 27 x ) z + 9 y + 27 x y + 45 x y + 27 x y 4 4 3 2 2 2 + 9 x )/4 >= (9 z + (27 y + 27 x) z + (27 y + 54 x y + 27 x ) z 3 2 2 3 4 3 2 2 3 + (27 y + 54 x y + 54 x y + 27 x ) z + 9 y + 27 x y + 27 x y + 27 x y 4 + 9 x )/4 Multiplying both sides by 4 gives: 4 3 3 2 2 2 2 2 3 9 z + 27 y z + 27 x z + 45 y z + 36 x y z + 45 x z + 27 y z 2 2 3 4 3 2 2 3 + 36 x y z + 36 x y z + 27 x z + 9 y + 27 x y + 45 x y + 27 x y 4 4 3 3 2 2 2 2 2 3 + 9 x >= 9 z + 27 y z + 27 x z + 27 y z + 54 x y z + 27 x z + 27 y z 2 2 3 4 3 2 2 3 4 + 54 x y z + 54 x y z + 27 x z + 9 y + 27 x y + 27 x y + 27 x y + 9 x Expanding and collecting terms of the same sign gives: 2 2 2 2 2 2 2 2 2 18 y z + 18 x z + 18 x y >= 18 x y z + 18 x y z + 18 x y z Dividing both sides by 18 gives: 2 2 2 2 2 2 2 2 2 y z + x z + x y >= x y z + x y z + x y z Expressing in terms of symmetric polynomials gives: {2, 2, 0} >= {2, 1, 1} This result follows from the majorization theorem. (d5) true (c6) /* 4.4 */ trineq(csum(a^2)>=4*K*sqrt(3)); 2 2 2 To prove: c + b + a >= 4 sqrt(3) K Since 4 sqrt(3) is positive, and since 2 2 2 c + b + a is positive, we can square both sides to get: 4 2 2 2 4 2 2 4 c + (2 b + 2 a ) c + b + 2 a b + a >= 4 3 2 48 s + (- 48 c - 48 b - 48 a) s + ((48 b + 48 a) c + 48 a b) s - 48 a b c s Expanding and collecting terms of the same sign gives: 3 3 3 4 2 2 2 2 4 48 c s + 48 b s + 48 a s + 48 a b c s + c + 2 b c + 2 a c + b 2 2 4 4 2 2 2 + 2 a b + a >= 48 s + 48 b c s + 48 a c s + 48 a b s Let s = (c+b+a)/2 . We get: 4 3 2 2 2 7 c + (24 b + 24 a) c + (38 b + 96 a b + 38 a ) c 3 2 2 3 4 3 2 2 3 + (24 b + 96 a b + 96 a b + 24 a ) c + 7 b + 24 a b + 38 a b + 24 a b 4 4 3 2 2 2 + 7 a >= 3 c + (24 b + 24 a) c + (42 b + 96 a b + 42 a ) c 3 2 2 3 4 3 2 2 3 + (24 b + 96 a b + 96 a b + 24 a ) c + 3 b + 24 a b + 42 a b + 24 a b 4 + 3 a Expanding and collecting terms of the same sign gives: 4 4 4 2 2 2 2 2 2 4 c + 4 b + 4 a >= 4 b c + 4 a c + 4 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 4 3 2 2 2 3 3 4 3 (z + (2 y + 2 x) z + (3 y + 3 x ) z + (2 y + 2 x ) z + y + 2 x y 2 2 3 4 4 3 2 2 2 + 3 x y + 2 x y + x )/2 >= (z + (2 y + 2 x) z + (3 y + 8 x y + 3 x ) z 3 2 2 3 4 3 2 2 3 4 + (2 y + 8 x y + 8 x y + 2 x ) z + y + 2 x y + 3 x y + 2 x y + x )/4 Multiplying both sides by 4 gives: 4 3 3 2 2 2 2 3 3 4 3 2 z + 4 y z + 4 x z + 6 y z + 6 x z + 4 y z + 4 x z + 2 y + 4 x y 2 2 3 4 4 3 3 2 2 2 + 6 x y + 4 x y + 2 x >= z + 2 y z + 2 x z + 3 y z + 8 x y z 2 2 3 2 2 3 4 3 2 2 + 3 x z + 2 y z + 8 x y z + 8 x y z + 2 x z + y + 2 x y + 3 x y 3 4 + 2 x y + x Expanding and collecting terms of the same sign gives: 4 3 3 2 2 2 2 3 3 4 3 z + 2 y z + 2 x z + 3 y z + 3 x z + 2 y z + 2 x z + y + 2 x y 2 2 3 4 2 2 2 + 3 x y + 2 x y + x >= 8 x y z + 8 x y z + 8 x y z Expressing in terms of symmetric polynomials gives: {4, 0, 0} + 4 {3, 1, 0} + 3 {2, 2, 0} >= 8 {2, 1, 1} This follows from the following majorizations: 3 {2, 2, 0} >= 3 {2, 1, 1} 4 {3, 1, 0} >= 4 {2, 1, 1} {4, 0, 0} >= {2, 1, 1} (d6) true (c7) /* 4.5 */ trineq(csum(a*b)>=4*K*sqrt(3)); To prove: b c + a c + a b >= 4 sqrt(3) K Since 4 sqrt(3) is positive, and since (b + a) c + a b is positive, we can square both sides to get: 2 2 2 2 2 2 2 (b + 2 a b + a ) c + (2 a b + 2 a b) c + a b >= 4 3 2 48 s + (- 48 c - 48 b - 48 a) s + ((48 b + 48 a) c + 48 a b) s - 48 a b c s Expanding and collecting terms of the same sign gives: 3 3 3 2 2 2 2 2 2 48 c s + 48 b s + 48 a s + 48 a b c s + b c + 2 a b c + a c + 2 a b c 2 2 2 4 2 2 2 + 2 a b c + a b >= 48 s + 48 b c s + 48 a c s + 48 a b s Let s = (c+b+a)/2 . We get: 4 3 2 2 2 6 c + (24 b + 24 a) c + (37 b + 98 a b + 37 a ) c 3 2 2 3 4 3 2 2 3 + (24 b + 98 a b + 98 a b + 24 a ) c + 6 b + 24 a b + 37 a b + 24 a b 4 4 3 2 2 2 + 6 a >= 3 c + (24 b + 24 a) c + (42 b + 96 a b + 42 a ) c 3 2 2 3 4 3 2 2 3 + (24 b + 96 a b + 96 a b + 24 a ) c + 3 b + 24 a b + 42 a b + 24 a b 4 + 3 a Expanding and collecting terms of the same sign gives: 4 2 2 2 4 4 3 c + 2 a b c + 2 a b c + 2 a b c + 3 b + 3 a >= 2 2 2 2 2 2 5 b c + 5 a c + 5 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 4 3 2 2 2 (3 z + (8 y + 8 x) z + (13 y + 8 x y + 13 x ) z 3 2 2 3 4 3 2 2 3 + (8 y + 8 x y + 8 x y + 8 x ) z + 3 y + 8 x y + 13 x y + 8 x y 4 4 3 2 2 2 + 3 x )/8 >= (5 z + (10 y + 10 x) z + (15 y + 40 x y + 15 x ) z 3 2 2 3 4 3 2 2 3 + (10 y + 40 x y + 40 x y + 10 x ) z + 5 y + 10 x y + 15 x y + 10 x y 4 + 5 x )/16 Multiplying both sides by 16 gives: 4 3 3 2 2 2 2 2 3 6 z + 16 y z + 16 x z + 26 y z + 16 x y z + 26 x z + 16 y z 2 2 3 4 3 2 2 3 + 16 x y z + 16 x y z + 16 x z + 6 y + 16 x y + 26 x y + 16 x y 4 4 3 3 2 2 2 2 2 3 + 6 x >= 5 z + 10 y z + 10 x z + 15 y z + 40 x y z + 15 x z + 10 y z 2 2 3 4 3 2 2 3 4 + 40 x y z + 40 x y z + 10 x z + 5 y + 10 x y + 15 x y + 10 x y + 5 x Expanding and collecting terms of the same sign gives: 4 3 3 2 2 2 2 3 3 4 3 z + 6 y z + 6 x z + 11 y z + 11 x z + 6 y z + 6 x z + y + 6 x y 2 2 3 4 2 2 2 + 11 x y + 6 x y + x >= 24 x y z + 24 x y z + 24 x y z Expressing in terms of symmetric polynomials gives: {4, 0, 0} + 12 {3, 1, 0} + 11 {2, 2, 0} >= 24 {2, 1, 1} This follows from the following majorizations: 11 {2, 2, 0} >= 11 {2, 1, 1} 12 {3, 1, 0} >= 12 {2, 1, 1} {4, 0, 0} >= {2, 1, 1} (d7) true (c8) /* 4.6 */ trineq(csum(a*b)>=4*K*sqrt(3)+(1/2)*csum((a-b)^2)); 2 2 2 (c - a) + (b - c) + (a - b) To prove: b c + a c + a b >= ------------------------------ + 4 sqrt(3) K 2 Expanding and collecting terms of the same sign gives: 2 2 2 2 b c + 2 a c + 2 a b >= c + b + a + 4 sqrt(3) K Bringing all terms involving K to the right side yields: 2 2 2 - c + (2 b + 2 a) c - b + 2 a b - a >= 4 sqrt(3) K Since 4 sqrt(3) is positive, and since 2 2 2 - c + (2 b + 2 a) c - b + 2 a b - a is positive, we can square both sides to get: 4 3 2 2 2 c + (- 4 b - 4 a) c + (6 b + 4 a b + 6 a ) c 3 2 2 3 4 3 2 2 3 + (- 4 b + 4 a b + 4 a b - 4 a ) c + b - 4 a b + 6 a b - 4 a b 4 4 3 2 + a >= 48 s + (- 48 c - 48 b - 48 a) s + ((48 b + 48 a) c + 48 a b) s - 48 a b c s Expanding and collecting terms of the same sign gives: 3 3 3 4 2 2 2 2 2 48 c s + 48 b s + 48 a s + 48 a b c s + c + 6 b c + 4 a b c + 6 a c 2 2 4 2 2 4 + 4 a b c + 4 a b c + b + 6 a b + a >= 4 2 2 2 3 3 3 3 48 s + 48 b c s + 48 a c s + 48 a b s + 4 b c + 4 a c + 4 b c + 4 a c 3 3 + 4 a b + 4 a b Let s = (c+b+a)/2 . We get: 4 3 2 2 2 7 c + (24 b + 24 a) c + (42 b + 100 a b + 42 a ) c 3 2 2 3 4 3 2 2 + (24 b + 100 a b + 100 a b + 24 a ) c + 7 b + 24 a b + 42 a b 3 4 4 3 2 2 2 + 24 a b + 7 a >= 3 c + (28 b + 28 a) c + (42 b + 96 a b + 42 a ) c 3 2 2 3 4 3 2 2 3 + (28 b + 96 a b + 96 a b + 28 a ) c + 3 b + 28 a b + 42 a b + 28 a b 4 + 3 a Expanding and collecting terms of the same sign gives: 4 2 2 2 4 4 4 c + 4 a b c + 4 a b c + 4 a b c + 4 b + 4 a >= 3 3 3 3 3 3 4 b c + 4 a c + 4 b c + 4 a c + 4 a b + 4 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 4 3 2 2 2 (z + (3 y + 3 x) z + (5 y + 4 x y + 5 x ) z 3 2 2 3 4 3 2 2 3 4 + (3 y + 4 x y + 4 x y + 3 x ) z + y + 3 x y + 5 x y + 3 x y + x ) 4 3 2 2 2 /2 >= (z + (3 y + 3 x) z + (3 y + 6 x y + 3 x ) z 3 2 2 3 4 3 2 2 3 4 + (3 y + 6 x y + 6 x y + 3 x ) z + y + 3 x y + 3 x y + 3 x y + x )/2 Multiplying both sides by 2 gives: 4 3 3 2 2 2 2 2 3 2 z + 3 y z + 3 x z + 5 y z + 4 x y z + 5 x z + 3 y z + 4 x y z 2 3 4 3 2 2 3 4 + 4 x y z + 3 x z + y + 3 x y + 5 x y + 3 x y + x >= 4 3 3 2 2 2 2 2 3 2 z + 3 y z + 3 x z + 3 y z + 6 x y z + 3 x z + 3 y z + 6 x y z 2 3 4 3 2 2 3 4 + 6 x y z + 3 x z + y + 3 x y + 3 x y + 3 x y + x Expanding and collecting terms of the same sign gives: 2 2 2 2 2 2 2 2 2 2 y z + 2 x z + 2 x y >= 2 x y z + 2 x y z + 2 x y z Dividing both sides by 2 gives: 2 2 2 2 2 2 2 2 2 y z + x z + x y >= x y z + x y z + x y z Expressing in terms of symmetric polynomials gives: {2, 2, 0} >= {2, 1, 1} This result follows from the majorization theorem. (d8) true (c9) /* 4.7 */ trineq(4*K*sqrt(3)+csum((a-b)^2)<=csum(a^2)); 2 2 2 2 2 2 To prove: c + b + a >= (c - a) + (b - c) + (a - b) + 4 sqrt(3) K Expanding and collecting terms of the same sign gives: 2 2 2 2 b c + 2 a c + 2 a b >= c + b + a + 4 sqrt(3) K Bringing all terms involving K to the right side yields: 2 2 2 - c + (2 b + 2 a) c - b + 2 a b - a >= 4 sqrt(3) K Since 4 sqrt(3) is positive, and since 2 2 2 - c + (2 b + 2 a) c - b + 2 a b - a is positive, we can square both sides to get: 4 3 2 2 2 c + (- 4 b - 4 a) c + (6 b + 4 a b + 6 a ) c 3 2 2 3 4 3 2 2 3 + (- 4 b + 4 a b + 4 a b - 4 a ) c + b - 4 a b + 6 a b - 4 a b 4 4 3 2 + a >= 48 s + (- 48 c - 48 b - 48 a) s + ((48 b + 48 a) c + 48 a b) s - 48 a b c s Expanding and collecting terms of the same sign gives: 3 3 3 4 2 2 2 2 2 48 c s + 48 b s + 48 a s + 48 a b c s + c + 6 b c + 4 a b c + 6 a c 2 2 4 2 2 4 + 4 a b c + 4 a b c + b + 6 a b + a >= 4 2 2 2 3 3 3 3 48 s + 48 b c s + 48 a c s + 48 a b s + 4 b c + 4 a c + 4 b c + 4 a c 3 3 + 4 a b + 4 a b Let s = (c+b+a)/2 . We get: 4 3 2 2 2 7 c + (24 b + 24 a) c + (42 b + 100 a b + 42 a ) c 3 2 2 3 4 3 2 2 + (24 b + 100 a b + 100 a b + 24 a ) c + 7 b + 24 a b + 42 a b 3 4 4 3 2 2 2 + 24 a b + 7 a >= 3 c + (28 b + 28 a) c + (42 b + 96 a b + 42 a ) c 3 2 2 3 4 3 2 2 3 + (28 b + 96 a b + 96 a b + 28 a ) c + 3 b + 28 a b + 42 a b + 28 a b 4 + 3 a Expanding and collecting terms of the same sign gives: 4 2 2 2 4 4 4 c + 4 a b c + 4 a b c + 4 a b c + 4 b + 4 a >= 3 3 3 3 3 3 4 b c + 4 a c + 4 b c + 4 a c + 4 a b + 4 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 4 3 2 2 2 (z + (3 y + 3 x) z + (5 y + 4 x y + 5 x ) z 3 2 2 3 4 3 2 2 3 4 + (3 y + 4 x y + 4 x y + 3 x ) z + y + 3 x y + 5 x y + 3 x y + x ) 4 3 2 2 2 /2 >= (z + (3 y + 3 x) z + (3 y + 6 x y + 3 x ) z 3 2 2 3 4 3 2 2 3 4 + (3 y + 6 x y + 6 x y + 3 x ) z + y + 3 x y + 3 x y + 3 x y + x )/2 Multiplying both sides by 2 gives: 4 3 3 2 2 2 2 2 3 2 z + 3 y z + 3 x z + 5 y z + 4 x y z + 5 x z + 3 y z + 4 x y z 2 3 4 3 2 2 3 4 + 4 x y z + 3 x z + y + 3 x y + 5 x y + 3 x y + x >= 4 3 3 2 2 2 2 2 3 2 z + 3 y z + 3 x z + 3 y z + 6 x y z + 3 x z + 3 y z + 6 x y z 2 3 4 3 2 2 3 4 + 6 x y z + 3 x z + y + 3 x y + 3 x y + 3 x y + x Expanding and collecting terms of the same sign gives: 2 2 2 2 2 2 2 2 2 2 y z + 2 x z + 2 x y >= 2 x y z + 2 x y z + 2 x y z Dividing both sides by 2 gives: 2 2 2 2 2 2 2 2 2 y z + x z + x y >= x y z + x y z + x y z Expressing in terms of symmetric polynomials gives: {2, 2, 0} >= {2, 1, 1} This result follows from the majorization theorem. (d9) true (c10) trineq(csum(a^2)<=4*K*sqrt(3)+3*csum((a-b)^2)); 2 2 2 2 2 2 To prove: 3 ((c - a) + (b - c) + (a - b) ) + 4 sqrt(3) K >= c + b + a Expanding and collecting terms of the same sign gives: 2 2 2 5 c + 5 b + 5 a + 4 sqrt(3) K >= 6 b c + 6 a c + 6 a b left side: [2 {1, 1, 0}] right side: [{2, 0, 0}] Warning: cannot determine if the other side, 2 2 2 - 5 c + (6 b + 6 a) c - 5 b + 6 a b - 5 a is positive. (Assuming it is.) Bringing all terms involving K to the left side yields: 2 2 2 4 sqrt(3) K >= - 5 c + (6 b + 6 a) c - 5 b + 6 a b - 5 a Since 4 sqrt(3) is positive, and since 2 2 2 - 5 c + (6 b + 6 a) c - 5 b + 6 a b - 5 a is positive, we can square both sides to get: 4 3 2 48 s + (- 48 c - 48 b - 48 a) s + ((48 b + 48 a) c + 48 a b) s 4 3 2 2 2 - 48 a b c s >= 25 c + (- 60 b - 60 a) c + (86 b + 12 a b + 86 a ) c 3 2 2 3 4 3 2 2 + (- 60 b + 12 a b + 12 a b - 60 a ) c + 25 b - 60 a b + 86 a b 3 4 - 60 a b + 25 a Expanding and collecting terms of the same sign gives: 4 2 2 2 3 3 3 48 s + 48 b c s + 48 a c s + 48 a b s + 60 b c + 60 a c + 60 b c 3 3 3 3 3 3 + 60 a c + 60 a b + 60 a b >= 48 c s + 48 b s + 48 a s + 48 a b c s 4 2 2 2 2 2 2 2 4 + 25 c + 86 b c + 12 a b c + 86 a c + 12 a b c + 12 a b c + 25 b 2 2 4 + 86 a b + 25 a Let s = (c+b+a)/2 . We get: 4 3 2 2 2 3 c + (84 b + 84 a) c + (42 b + 96 a b + 42 a ) c 3 2 2 3 4 3 2 2 3 + (84 b + 96 a b + 96 a b + 84 a ) c + 3 b + 84 a b + 42 a b + 84 a b 4 4 3 2 2 2 + 3 a >= 31 c + (24 b + 24 a) c + (122 b + 108 a b + 122 a ) c 3 2 2 3 4 3 2 2 + (24 b + 108 a b + 108 a b + 24 a ) c + 31 b + 24 a b + 122 a b 3 4 + 24 a b + 31 a Expanding and collecting terms of the same sign gives: 3 3 3 3 3 3 60 b c + 60 a c + 60 b c + 60 a c + 60 a b + 60 a b >= 4 2 2 2 2 2 2 2 4 28 c + 80 b c + 12 a b c + 80 a c + 12 a b c + 12 a b c + 28 b 2 2 4 + 80 a b + 28 a Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 4 3 2 2 2 (15 z + (45 y + 45 x) z + (45 y + 90 x y + 45 x ) z 3 2 2 3 4 3 2 2 3 + (45 y + 90 x y + 90 x y + 45 x ) z + 15 y + 45 x y + 45 x y + 45 x y 4 4 3 2 2 2 + 15 x )/2 >= (17 z + (37 y + 37 x) z + (57 y + 92 x y + 57 x ) z 3 2 2 3 4 3 2 2 3 + (37 y + 92 x y + 92 x y + 37 x ) z + 17 y + 37 x y + 57 x y + 37 x y 4 + 17 x )/2 Multiplying both sides by 2 gives: 4 3 3 2 2 2 2 2 3 15 z + 45 y z + 45 x z + 45 y z + 90 x y z + 45 x z + 45 y z 2 2 3 4 3 2 2 3 + 90 x y z + 90 x y z + 45 x z + 15 y + 45 x y + 45 x y + 45 x y 4 4 3 3 2 2 2 2 2 + 15 x >= 17 z + 37 y z + 37 x z + 57 y z + 92 x y z + 57 x z 3 2 2 3 4 3 2 2 + 37 y z + 92 x y z + 92 x y z + 37 x z + 17 y + 37 x y + 57 x y 3 4 + 37 x y + 17 x Expanding and collecting terms of the same sign gives: 3 3 3 3 3 3 8 y z + 8 x z + 8 y z + 8 x z + 8 x y + 8 x y >= 4 2 2 2 2 2 2 2 4 2 2 2 z + 12 y z + 2 x y z + 12 x z + 2 x y z + 2 x y z + 2 y + 12 x y 4 + 2 x Dividing both sides by 2 gives: 3 3 3 3 3 3 4 y z + 4 x z + 4 y z + 4 x z + 4 x y + 4 x y >= 4 2 2 2 2 2 2 2 4 2 2 4 z + 6 y z + x y z + 6 x z + x y z + x y z + y + 6 x y + x Expressing in terms of symmetric polynomials gives: 8 {3, 1, 0} >= {4, 0, 0} + 6 {2, 2, 0} + {2, 1, 1} This follows from the following majorizations: 6 {3, 1, 0} >= 6 {2, 2, 0} {3, 1, 0} >= {2, 1, 1} left side: [8 {3, 1, 0}] right side: [{2, 1, 1}, 6 {2, 2, 0}, {4, 0, 0}] (d10) notyetimplemented (c11) /* 4.9 */ trineq(12*K*sqrt(3)+2*csum((a-b)^2)<=csum(a)^2); 2 2 2 2 To prove: (c + b + a) >= 2 ((c - a) + (b - c) + (a - b) ) + 12 sqrt(3) K Expanding and collecting terms of the same sign gives: 2 2 2 6 b c + 6 a c + 6 a b >= 3 c + 3 b + 3 a + 12 sqrt(3) K Bringing all terms involving K to the right side yields: 2 2 2 - 3 c + (6 b + 6 a) c - 3 b + 6 a b - 3 a >= 12 sqrt(3) K Since 12 sqrt(3) is positive, and since 2 2 2 - 3 c + (6 b + 6 a) c - 3 b + 6 a b - 3 a is positive, we can square both sides to get: 4 3 2 2 2 9 c + (- 36 b - 36 a) c + (54 b + 36 a b + 54 a ) c 3 2 2 3 4 3 2 2 + (- 36 b + 36 a b + 36 a b - 36 a ) c + 9 b - 36 a b + 54 a b 3 4 4 3 - 36 a b + 9 a >= 432 s + (- 432 c - 432 b - 432 a) s 2 + ((432 b + 432 a) c + 432 a b) s - 432 a b c s Expanding and collecting terms of the same sign gives: 3 3 3 4 2 2 2 432 c s + 432 b s + 432 a s + 432 a b c s + 9 c + 54 b c + 36 a b c 2 2 2 2 4 2 2 4 + 54 a c + 36 a b c + 36 a b c + 9 b + 54 a b + 9 a >= 4 2 2 2 3 3 3 432 s + 432 b c s + 432 a c s + 432 a b s + 36 b c + 36 a c + 36 b c 3 3 3 + 36 a c + 36 a b + 36 a b Dividing both sides by 9 gives: 3 3 3 4 2 2 2 2 2 48 c s + 48 b s + 48 a s + 48 a b c s + c + 6 b c + 4 a b c + 6 a c 2 2 4 2 2 4 + 4 a b c + 4 a b c + b + 6 a b + a >= 4 2 2 2 3 3 3 3 48 s + 48 b c s + 48 a c s + 48 a b s + 4 b c + 4 a c + 4 b c + 4 a c 3 3 + 4 a b + 4 a b Let s = (c+b+a)/2 . We get: 4 3 2 2 2 7 c + (24 b + 24 a) c + (42 b + 100 a b + 42 a ) c 3 2 2 3 4 3 2 2 + (24 b + 100 a b + 100 a b + 24 a ) c + 7 b + 24 a b + 42 a b 3 4 4 3 2 2 2 + 24 a b + 7 a >= 3 c + (28 b + 28 a) c + (42 b + 96 a b + 42 a ) c 3 2 2 3 4 3 2 2 3 + (28 b + 96 a b + 96 a b + 28 a ) c + 3 b + 28 a b + 42 a b + 28 a b 4 + 3 a Expanding and collecting terms of the same sign gives: 4 2 2 2 4 4 4 c + 4 a b c + 4 a b c + 4 a b c + 4 b + 4 a >= 3 3 3 3 3 3 4 b c + 4 a c + 4 b c + 4 a c + 4 a b + 4 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 4 3 2 2 2 (z + (3 y + 3 x) z + (5 y + 4 x y + 5 x ) z 3 2 2 3 4 3 2 2 3 4 + (3 y + 4 x y + 4 x y + 3 x ) z + y + 3 x y + 5 x y + 3 x y + x ) 4 3 2 2 2 /2 >= (z + (3 y + 3 x) z + (3 y + 6 x y + 3 x ) z 3 2 2 3 4 3 2 2 3 4 + (3 y + 6 x y + 6 x y + 3 x ) z + y + 3 x y + 3 x y + 3 x y + x )/2 Multiplying both sides by 2 gives: 4 3 3 2 2 2 2 2 3 2 z + 3 y z + 3 x z + 5 y z + 4 x y z + 5 x z + 3 y z + 4 x y z 2 3 4 3 2 2 3 4 + 4 x y z + 3 x z + y + 3 x y + 5 x y + 3 x y + x >= 4 3 3 2 2 2 2 2 3 2 z + 3 y z + 3 x z + 3 y z + 6 x y z + 3 x z + 3 y z + 6 x y z 2 3 4 3 2 2 3 4 + 6 x y z + 3 x z + y + 3 x y + 3 x y + 3 x y + x Expanding and collecting terms of the same sign gives: 2 2 2 2 2 2 2 2 2 2 y z + 2 x z + 2 x y >= 2 x y z + 2 x y z + 2 x y z Dividing both sides by 2 gives: 2 2 2 2 2 2 2 2 2 y z + x z + x y >= x y z + x y z + x y z Expressing in terms of symmetric polynomials gives: {2, 2, 0} >= {2, 1, 1} This result follows from the majorization theorem. (d11) true (c12) trineq(csum(a)^2<=12*K*sqrt(3)+8*csum((a-b)^2)); 2 2 2 2 To prove: 8 ((c - a) + (b - c) + (a - b) ) + 12 sqrt(3) K >= (c + b + a) Expanding and collecting terms of the same sign gives: 2 2 2 15 c + 15 b + 15 a + 12 sqrt(3) K >= 18 b c + 18 a c + 18 a b left side: [2 {1, 1, 0}] right side: [{2, 0, 0}] Warning: cannot determine if the other side, 2 2 2 - 15 c + (18 b + 18 a) c - 15 b + 18 a b - 15 a is positive. (Assuming it is.) Bringing all terms involving K to the left side yields: 2 2 2 12 sqrt(3) K >= - 15 c + (18 b + 18 a) c - 15 b + 18 a b - 15 a Since 12 sqrt(3) is positive, and since 2 2 2 - 15 c + (18 b + 18 a) c - 15 b + 18 a b - 15 a is positive, we can square both sides to get: 4 3 2 432 s + (- 432 c - 432 b - 432 a) s + ((432 b + 432 a) c + 432 a b) s 4 3 - 432 a b c s >= 225 c + (- 540 b - 540 a) c 2 2 2 3 2 2 3 + (774 b + 108 a b + 774 a ) c + (- 540 b + 108 a b + 108 a b - 540 a ) c 4 3 2 2 3 4 + 225 b - 540 a b + 774 a b - 540 a b + 225 a Expanding and collecting terms of the same sign gives: 4 2 2 2 3 3 3 432 s + 432 b c s + 432 a c s + 432 a b s + 540 b c + 540 a c + 540 b c 3 3 3 3 3 3 + 540 a c + 540 a b + 540 a b >= 432 c s + 432 b s + 432 a s 4 2 2 2 2 2 2 + 432 a b c s + 225 c + 774 b c + 108 a b c + 774 a c + 108 a b c 2 4 2 2 4 + 108 a b c + 225 b + 774 a b + 225 a Dividing both sides by 9 gives: 4 2 2 2 3 3 3 48 s + 48 b c s + 48 a c s + 48 a b s + 60 b c + 60 a c + 60 b c 3 3 3 3 3 3 + 60 a c + 60 a b + 60 a b >= 48 c s + 48 b s + 48 a s + 48 a b c s 4 2 2 2 2 2 2 2 4 + 25 c + 86 b c + 12 a b c + 86 a c + 12 a b c + 12 a b c + 25 b 2 2 4 + 86 a b + 25 a Let s = (c+b+a)/2 . We get: 4 3 2 2 2 3 c + (84 b + 84 a) c + (42 b + 96 a b + 42 a ) c 3 2 2 3 4 3 2 2 3 + (84 b + 96 a b + 96 a b + 84 a ) c + 3 b + 84 a b + 42 a b + 84 a b 4 4 3 2 2 2 + 3 a >= 31 c + (24 b + 24 a) c + (122 b + 108 a b + 122 a ) c 3 2 2 3 4 3 2 2 + (24 b + 108 a b + 108 a b + 24 a ) c + 31 b + 24 a b + 122 a b 3 4 + 24 a b + 31 a Expanding and collecting terms of the same sign gives: 3 3 3 3 3 3 60 b c + 60 a c + 60 b c + 60 a c + 60 a b + 60 a b >= 4 2 2 2 2 2 2 2 4 28 c + 80 b c + 12 a b c + 80 a c + 12 a b c + 12 a b c + 28 b 2 2 4 + 80 a b + 28 a Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 4 3 2 2 2 (15 z + (45 y + 45 x) z + (45 y + 90 x y + 45 x ) z 3 2 2 3 4 3 2 2 3 + (45 y + 90 x y + 90 x y + 45 x ) z + 15 y + 45 x y + 45 x y + 45 x y 4 4 3 2 2 2 + 15 x )/2 >= (17 z + (37 y + 37 x) z + (57 y + 92 x y + 57 x ) z 3 2 2 3 4 3 2 2 3 + (37 y + 92 x y + 92 x y + 37 x ) z + 17 y + 37 x y + 57 x y + 37 x y 4 + 17 x )/2 Multiplying both sides by 2 gives: 4 3 3 2 2 2 2 2 3 15 z + 45 y z + 45 x z + 45 y z + 90 x y z + 45 x z + 45 y z 2 2 3 4 3 2 2 3 + 90 x y z + 90 x y z + 45 x z + 15 y + 45 x y + 45 x y + 45 x y 4 4 3 3 2 2 2 2 2 + 15 x >= 17 z + 37 y z + 37 x z + 57 y z + 92 x y z + 57 x z 3 2 2 3 4 3 2 2 + 37 y z + 92 x y z + 92 x y z + 37 x z + 17 y + 37 x y + 57 x y 3 4 + 37 x y + 17 x Expanding and collecting terms of the same sign gives: 3 3 3 3 3 3 8 y z + 8 x z + 8 y z + 8 x z + 8 x y + 8 x y >= 4 2 2 2 2 2 2 2 4 2 2 2 z + 12 y z + 2 x y z + 12 x z + 2 x y z + 2 x y z + 2 y + 12 x y 4 + 2 x Dividing both sides by 2 gives: 3 3 3 3 3 3 4 y z + 4 x z + 4 y z + 4 x z + 4 x y + 4 x y >= 4 2 2 2 2 2 2 2 4 2 2 4 z + 6 y z + x y z + 6 x z + x y z + x y z + y + 6 x y + x Expressing in terms of symmetric polynomials gives: 8 {3, 1, 0} >= {4, 0, 0} + 6 {2, 2, 0} + {2, 1, 1} This follows from the following majorizations: 6 {3, 1, 0} >= 6 {2, 2, 0} {3, 1, 0} >= {2, 1, 1} left side: [8 {3, 1, 0}] right side: [{2, 1, 1}, 6 {2, 2, 0}, {4, 0, 0}] (d12) notyetimplemented (c13) /* 4.10 */ trineq(csum(a^4)>=16*K^2); 4 4 4 2 To prove: c + b + a >= 16 K Replacing K^2 by F^2 gives: 4 4 4 2 c + b + a >= 16 F Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 4 4 4 4 2 2 2 4 2 2 4 c + b + a >= - c + (2 b + 2 a ) c - b + 2 a b - a Expanding and collecting terms of the same sign gives: 4 4 4 2 2 2 2 2 2 2 c + 2 b + 2 a >= 2 b c + 2 a c + 2 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 4 3 2 2 2 3 3 4 3 (z + (2 y + 2 x) z + (3 y + 3 x ) z + (2 y + 2 x ) z + y + 2 x y 2 2 3 4 4 3 2 2 2 + 3 x y + 2 x y + x )/4 >= (z + (2 y + 2 x) z + (3 y + 8 x y + 3 x ) z 3 2 2 3 4 3 2 2 3 4 + (2 y + 8 x y + 8 x y + 2 x ) z + y + 2 x y + 3 x y + 2 x y + x )/8 Multiplying both sides by 8 gives: 4 3 3 2 2 2 2 3 3 4 3 2 z + 4 y z + 4 x z + 6 y z + 6 x z + 4 y z + 4 x z + 2 y + 4 x y 2 2 3 4 4 3 3 2 2 2 + 6 x y + 4 x y + 2 x >= z + 2 y z + 2 x z + 3 y z + 8 x y z 2 2 3 2 2 3 4 3 2 2 + 3 x z + 2 y z + 8 x y z + 8 x y z + 2 x z + y + 2 x y + 3 x y 3 4 + 2 x y + x Expanding and collecting terms of the same sign gives: 4 3 3 2 2 2 2 3 3 4 3 z + 2 y z + 2 x z + 3 y z + 3 x z + 2 y z + 2 x z + y + 2 x y 2 2 3 4 2 2 2 + 3 x y + 2 x y + x >= 8 x y z + 8 x y z + 8 x y z Expressing in terms of symmetric polynomials gives: {4, 0, 0} + 4 {3, 1, 0} + 3 {2, 2, 0} >= 8 {2, 1, 1} This follows from the following majorizations: 3 {2, 2, 0} >= 3 {2, 1, 1} 4 {3, 1, 0} >= 4 {2, 1, 1} {4, 0, 0} >= {2, 1, 1} (d13) true (c14) /* 4.11 */ trineq(csum(a^4)>=16*K^2+4*K*csum((a-b)^2)*sqrt(3)+(1/2)*csum((a-b)^2)^2); 2 2 2 2 4 4 4 ((c - a) + (b - c) + (a - b) ) To prove: c + b + a >= --------------------------------- 2 2 2 2 2 + 4 sqrt(3) K ((c - a) + (b - c) + (a - b) ) + 16 K Expanding and collecting terms of the same sign gives: 3 3 3 3 3 4 b c + 4 a c + 4 b c + 8 sqrt(3) K b c + 4 a c + 8 sqrt(3) K a c + 4 a b 3 4 2 2 2 2 2 4 + 4 a b + 8 sqrt(3) K a b >= c + 6 b c + 6 a c + 8 sqrt(3) K c + b 2 2 2 4 2 2 + 6 a b + 8 sqrt(3) K b + a + 8 sqrt(3) K a + 16 K Replacing K^2 by F^2 gives: 3 3 3 3 (4 b + 4 a) c + (4 b + 8 sqrt(3) K b + 4 a + 8 sqrt(3) K a) c + 4 a b 3 4 2 2 2 4 + (4 a + 8 sqrt(3) K a) b >= c + (6 b + 6 a + 8 sqrt(3) K) c + b 2 2 4 2 2 + (6 a + 8 sqrt(3) K) b + a + 8 sqrt(3) K a + 16 F Bringing all terms involving K to the right side yields: 4 3 2 2 2 3 3 4 3 - c + (4 b + 4 a) c - (6 b + 6 a ) c + (4 b + 4 a ) c - b + 4 a b 2 2 3 4 2 2 2 - 6 a b + 4 a b - a - 16 F >= K (8 sqrt(3) c + 8 sqrt(3) b 2 + 8 sqrt(3) a ) - K ((8 sqrt(3) b + 8 sqrt(3) a) c + 8 sqrt(3) a b) 2 2 Since 8 sqrt(3) c - (8 sqrt(3) b + 8 sqrt(3) a) c + 8 sqrt(3) b 2 - 8 sqrt(3) a b + 8 sqrt(3) a is positive, and since 4 3 2 2 2 3 3 4 3 - c + (4 b + 4 a) c - (6 b + 6 a ) c + (4 b + 4 a ) c - b + 4 a b 2 2 3 4 2 - 6 a b + 4 a b - a - 16 F is positive, we can square both sides to get: 8 7 2 2 6 c + (- 8 b - 8 a) c + (28 b + 32 a b + 28 a ) c 3 2 2 3 5 + (- 56 b - 48 a b - 48 a b - 56 a ) c 4 3 2 2 3 4 2 4 + (70 b + 24 a b + 84 a b + 24 a b + 70 a + 32 F ) c 5 4 2 3 3 2 4 2 5 + (- 56 b + 24 a b - 64 a b - 64 a b + (24 a - 128 F ) b - 56 a 2 3 6 5 2 4 3 3 4 2 2 - 128 F a) c + (28 b - 48 a b + 84 a b - 64 a b + (84 a + 192 F ) b 5 6 2 2 2 7 6 2 5 3 4 - 48 a b + 28 a + 192 F a ) c + (- 8 b + 32 a b - 48 a b + 24 a b 4 2 3 5 2 6 7 2 3 8 7 + (24 a - 128 F ) b - 48 a b + 32 a b - 8 a - 128 F a ) c + b - 8 a b 2 6 3 5 4 2 4 5 2 3 + 28 a b - 56 a b + (70 a + 32 F ) b + (- 56 a - 128 F a) b 6 2 2 2 7 2 3 8 2 4 4 + (28 a + 192 F a ) b + (- 8 a - 128 F a ) b + a + 32 F a + 256 F >= 4 3 2 2 2 3 3 (192 c + (- 384 b - 384 a) c + (576 b + 576 a ) c + (- 384 b - 384 a ) c 4 3 2 2 3 4 4 + 192 b - 384 a b + 576 a b - 384 a b + 192 a ) s 5 4 2 2 3 + (- 192 c + (192 b + 192 a) c + (- 192 b + 768 a b - 192 a ) c 3 2 2 3 2 + (- 192 b - 576 a b - 576 a b - 192 a ) c 4 3 2 2 3 4 5 4 + (192 b + 768 a b - 576 a b + 768 a b + 192 a ) c - 192 b + 192 a b 2 3 3 2 4 5 3 - 192 a b - 192 a b + 192 a b - 192 a ) s 5 2 2 4 + ((192 b + 192 a) c + (- 384 b - 576 a b - 384 a ) c 3 2 2 3 3 + (576 b + 192 a b + 192 a b + 576 a ) c 4 3 3 4 2 + (- 384 b + 192 a b + 192 a b - 384 a ) c 5 4 2 3 3 2 4 5 5 + (192 b - 576 a b + 192 a b + 192 a b - 576 a b + 192 a ) c + 192 a b 2 4 3 3 4 2 5 2 - 384 a b + 576 a b - 384 a b + 192 a b) s 5 2 2 4 3 3 3 + (- 192 a b c + (384 a b + 384 a b) c + (- 576 a b - 576 a b) c 4 4 2 5 2 4 3 3 4 2 + (384 a b + 384 a b) c + (- 192 a b + 384 a b - 576 a b + 384 a b 5 - 192 a b) c) s Expanding and collecting terms of the same sign gives: 3 4 3 4 3 4 3 4 3 4 384 b c s + 384 a c s + 384 b c s + 384 a c s + 384 a b s 3 4 5 3 2 3 3 2 3 3 3 2 3 + 384 a b s + 192 c s + 192 b c s + 192 a c s + 192 b c s 2 2 3 2 2 3 3 2 3 2 2 3 5 3 + 576 a b c s + 576 a b c s + 192 a c s + 576 a b c s + 192 b s 2 3 3 3 2 3 5 3 2 4 2 4 2 + 192 a b s + 192 a b s + 192 a s + 384 b c s + 576 a b c s 2 4 2 4 2 2 4 2 2 4 2 4 2 + 384 a c s + 384 b c s + 384 a c s + 576 a b c s + 576 a b c s 2 4 2 4 2 2 5 3 3 3 3 + 384 a b s + 384 a b s + 192 a b c s + 576 a b c s + 576 a b c s 5 3 3 5 8 2 6 6 + 192 a b c s + 576 a b c s + 192 a b c s + c + 28 b c + 32 a b c 2 6 4 4 3 4 2 2 4 3 4 4 4 + 28 a c + 70 b c + 24 a b c + 84 a b c + 24 a b c + 70 a c 2 4 4 3 4 3 6 2 2 4 2 4 2 2 + 32 F c + 24 a b c + 24 a b c + 28 b c + 84 a b c + 84 a b c 2 2 2 6 2 2 2 2 6 3 4 4 3 + 192 F b c + 28 a c + 192 F a c + 32 a b c + 24 a b c + 24 a b c 6 8 2 6 4 4 2 4 6 2 2 2 2 + 32 a b c + b + 28 a b + 70 a b + 32 F b + 28 a b + 192 F a b 8 2 4 4 4 4 2 2 4 2 2 4 + a + 32 F a + 256 F >= 192 c s + 576 b c s + 576 a c s 4 4 2 2 4 4 4 4 3 4 3 + 192 b s + 576 a b s + 192 a s + 192 b c s + 192 a c s 3 3 4 3 3 3 3 3 4 3 + 768 a b c s + 192 b c s + 768 a b c s + 768 a b c s + 192 a c s 4 3 4 3 5 2 5 2 3 3 2 + 192 a b s + 192 a b s + 192 b c s + 192 a c s + 576 b c s 2 3 2 2 3 2 3 3 2 3 2 2 + 192 a b c s + 192 a b c s + 576 a c s + 192 a b c s 3 2 2 5 2 2 3 2 3 2 2 5 2 + 192 a b c s + 192 b c s + 192 a b c s + 192 a b c s + 192 a c s 5 2 3 3 2 5 2 2 4 2 4 + 192 a b s + 576 a b s + 192 a b s + 384 a b c s + 384 a b c s 4 2 4 2 2 4 4 2 7 + 384 a b c s + 384 a b c s + 384 a b c s + 384 a b c s + 8 b c 7 3 5 2 5 2 5 3 5 5 3 + 8 a c + 56 b c + 48 a b c + 48 a b c + 56 a c + 56 b c 2 3 3 3 2 3 2 3 5 3 2 3 + 64 a b c + 64 a b c + 128 F b c + 56 a c + 128 F a c 5 2 3 3 2 5 2 7 2 5 2 3 + 48 a b c + 64 a b c + 48 a b c + 8 b c + 48 a b c + 128 F b c 5 2 7 2 3 7 3 5 5 3 + 48 a b c + 8 a c + 128 F a c + 8 a b + 56 a b + 56 a b 2 3 7 2 3 + 128 F a b + 8 a b + 128 F a b Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 8 7 2 2 6 24 c + (96 b + 96 a) c + (304 b + 608 a b + 304 a ) c 3 2 2 3 5 + (480 b + 1224 a b + 1224 a b + 480 a ) c 4 3 2 2 3 4 4 + (624 b + 1584 a b + 1832 a b + 1584 a b + 624 a ) c 5 4 2 3 3 2 4 5 3 + (480 b + 1584 a b + 1824 a b + 1824 a b + 1584 a b + 480 a ) c 6 5 2 4 3 3 4 2 5 + (304 b + 1224 a b + 1832 a b + 1824 a b + 1832 a b + 1224 a b 6 2 7 6 2 5 3 4 4 3 + 304 a ) c + (96 b + 608 a b + 1224 a b + 1584 a b + 1584 a b 5 2 6 7 8 7 2 6 3 5 + 1224 a b + 608 a b + 96 a ) c + 24 b + 96 a b + 304 a b + 480 a b 4 4 5 3 6 2 7 8 + 624 a b + 480 a b + 304 a b + 96 a b + 24 a >= 8 7 2 2 6 12 c + (120 b + 120 a) c + (276 b + 576 a b + 276 a ) c 3 2 2 3 5 + (520 b + 1240 a b + 1240 a b + 520 a ) c 4 3 2 2 3 4 4 + (576 b + 1576 a b + 1836 a b + 1576 a b + 576 a ) c 5 4 2 3 3 2 4 5 3 + (520 b + 1576 a b + 1824 a b + 1824 a b + 1576 a b + 520 a ) c 6 5 2 4 3 3 4 2 5 + (276 b + 1240 a b + 1836 a b + 1824 a b + 1836 a b + 1240 a b 6 2 7 6 2 5 3 4 4 3 + 276 a ) c + (120 b + 576 a b + 1240 a b + 1576 a b + 1576 a b 5 2 6 7 8 7 2 6 3 5 + 1240 a b + 576 a b + 120 a ) c + 12 b + 120 a b + 276 a b + 520 a b 4 4 5 3 6 2 7 8 + 576 a b + 520 a b + 276 a b + 120 a b + 12 a Expanding and collecting terms of the same sign gives: 8 2 6 6 2 6 4 4 3 4 3 4 12 c + 28 b c + 32 a b c + 28 a c + 48 b c + 8 a b c + 8 a b c 4 4 4 3 4 3 6 2 6 2 6 + 48 a c + 8 a b c + 8 a b c + 28 b c + 28 a c + 32 a b c 3 4 4 3 6 8 2 6 4 4 6 2 + 8 a b c + 8 a b c + 32 a b c + 12 b + 28 a b + 48 a b + 28 a b 8 7 7 3 5 2 5 2 5 3 5 + 12 a >= 24 b c + 24 a c + 40 b c + 16 a b c + 16 a b c + 40 a c 2 2 4 5 3 5 3 5 2 2 4 2 4 2 2 + 4 a b c + 40 b c + 40 a c + 16 a b c + 4 a b c + 4 a b c 5 2 7 2 5 5 2 7 7 + 16 a b c + 24 b c + 16 a b c + 16 a b c + 24 a c + 24 a b 3 5 5 3 7 + 40 a b + 40 a b + 24 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 8 7 2 2 6 (8 z + (37 y + 37 x) z + (88 y + 132 x y + 88 x ) z 3 2 2 3 5 + (135 y + 240 x y + 240 x y + 135 x ) z 4 3 2 2 3 4 4 + (160 y + 296 x y + 360 x y + 296 x y + 160 x ) z 5 4 2 3 3 2 4 5 3 + (135 y + 296 x y + 372 x y + 372 x y + 296 x y + 135 x ) z 6 5 2 4 3 3 4 2 5 6 2 + (88 y + 240 x y + 360 x y + 372 x y + 360 x y + 240 x y + 88 x ) z 7 6 2 5 3 4 4 3 5 2 6 + (37 y + 132 x y + 240 x y + 296 x y + 296 x y + 240 x y + 132 x y 7 8 7 2 6 3 5 4 4 5 3 + 37 x ) z + 8 y + 37 x y + 88 x y + 135 x y + 160 x y + 135 x y 6 2 7 8 8 7 + 88 x y + 37 x y + 8 x )/16 >= (8 z + (37 y + 37 x) z 2 2 6 3 2 2 3 5 + (84 y + 136 x y + 84 x ) z + (135 y + 244 x y + 244 x y + 135 x ) z 4 3 2 2 3 4 4 + (152 y + 316 x y + 328 x y + 316 x y + 152 x ) z 5 4 2 3 3 2 4 5 3 + (135 y + 316 x y + 368 x y + 368 x y + 316 x y + 135 x ) z 6 5 2 4 3 3 4 2 5 6 2 + (84 y + 244 x y + 328 x y + 368 x y + 328 x y + 244 x y + 84 x ) z 7 6 2 5 3 4 4 3 5 2 6 + (37 y + 136 x y + 244 x y + 316 x y + 316 x y + 244 x y + 136 x y 7 8 7 2 6 3 5 4 4 5 3 + 37 x ) z + 8 y + 37 x y + 84 x y + 135 x y + 152 x y + 135 x y 6 2 7 8 + 84 x y + 37 x y + 8 x )/16 Multiplying both sides by 16 gives: 8 7 7 2 6 6 2 6 3 5 8 z + 37 y z + 37 x z + 88 y z + 132 x y z + 88 x z + 135 y z 2 5 2 5 3 5 4 4 3 4 + 240 x y z + 240 x y z + 135 x z + 160 y z + 296 x y z 2 2 4 3 4 4 4 5 3 4 3 + 360 x y z + 296 x y z + 160 x z + 135 y z + 296 x y z 2 3 3 3 2 3 4 3 5 3 6 2 + 372 x y z + 372 x y z + 296 x y z + 135 x z + 88 y z 5 2 2 4 2 3 3 2 4 2 2 5 2 + 240 x y z + 360 x y z + 372 x y z + 360 x y z + 240 x y z 6 2 7 6 2 5 3 4 4 3 + 88 x z + 37 y z + 132 x y z + 240 x y z + 296 x y z + 296 x y z 5 2 6 7 8 7 2 6 3 5 + 240 x y z + 132 x y z + 37 x z + 8 y + 37 x y + 88 x y + 135 x y 4 4 5 3 6 2 7 8 + 160 x y + 135 x y + 88 x y + 37 x y + 8 x >= 8 7 7 2 6 6 2 6 3 5 8 z + 37 y z + 37 x z + 84 y z + 136 x y z + 84 x z + 135 y z 2 5 2 5 3 5 4 4 3 4 + 244 x y z + 244 x y z + 135 x z + 152 y z + 316 x y z 2 2 4 3 4 4 4 5 3 4 3 + 328 x y z + 316 x y z + 152 x z + 135 y z + 316 x y z 2 3 3 3 2 3 4 3 5 3 6 2 + 368 x y z + 368 x y z + 316 x y z + 135 x z + 84 y z 5 2 2 4 2 3 3 2 4 2 2 5 2 + 244 x y z + 328 x y z + 368 x y z + 328 x y z + 244 x y z 6 2 7 6 2 5 3 4 4 3 + 84 x z + 37 y z + 136 x y z + 244 x y z + 316 x y z + 316 x y z 5 2 6 7 8 7 2 6 3 5 + 244 x y z + 136 x y z + 37 x z + 8 y + 37 x y + 84 x y + 135 x y 4 4 5 3 6 2 7 8 + 152 x y + 135 x y + 84 x y + 37 x y + 8 x Expanding and collecting terms of the same sign gives: 2 6 2 6 4 4 2 2 4 4 4 2 3 3 3 2 3 4 y z + 4 x z + 8 y z + 32 x y z + 8 x z + 4 x y z + 4 x y z 6 2 2 4 2 3 3 2 4 2 2 6 2 2 6 + 4 y z + 32 x y z + 4 x y z + 32 x y z + 4 x z + 4 x y 4 4 6 2 6 2 5 2 5 3 4 + 8 x y + 4 x y >= 4 x y z + 4 x y z + 4 x y z + 20 x y z 3 4 4 3 4 3 5 2 5 2 6 + 20 x y z + 20 x y z + 20 x y z + 4 x y z + 4 x y z + 4 x y z 2 5 3 4 4 3 5 2 6 + 4 x y z + 20 x y z + 20 x y z + 4 x y z + 4 x y z Dividing both sides by 4 gives: 2 6 2 6 4 4 2 2 4 4 4 2 3 3 3 2 3 6 2 y z + x z + 2 y z + 8 x y z + 2 x z + x y z + x y z + y z 2 4 2 3 3 2 4 2 2 6 2 2 6 4 4 6 2 + 8 x y z + x y z + 8 x y z + x z + x y + 2 x y + x y >= 6 2 5 2 5 3 4 3 4 4 3 4 3 x y z + x y z + x y z + 5 x y z + 5 x y z + 5 x y z + 5 x y z 5 2 5 2 6 2 5 3 4 4 3 5 2 + x y z + x y z + x y z + x y z + 5 x y z + 5 x y z + x y z 6 + x y z Expressing in terms of symmetric polynomials gives: 2 {6, 2, 0} + 2 {4, 4, 0} + 8 {4, 2, 2} + {3, 3, 2} >= {6, 1, 1} + 2 {5, 2, 1} + 10 {4, 3, 1} This follows from the following majorizations: {6, 2, 0} >= {6, 1, 1} {6, 2, 0} >= {5, 2, 1} 2 {4, 4, 0} >= 2 {4, 3, 1} left side: [{3, 3, 2}, 8 {4, 2, 2}, 2 {4, 4, 0}, 2 {6, 2, 0}] right side: [10 {4, 3, 1}, 2 {5, 2, 1}, {6, 1, 1}] (d14) notsure (c15) /* 4.12 */ trineq(csum(a^2*b^2)>=16*K^2); 2 2 2 2 2 2 2 To prove: b c + a c + a b >= 16 K Replacing K^2 by F^2 gives: 2 2 2 2 2 2 (b + a ) c + a b >= 16 F Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 2 2 2 2 2 4 2 2 2 4 2 2 4 (b + a ) c + a b >= - c + (2 b + 2 a ) c - b + 2 a b - a Expanding and collecting terms of the same sign gives: 4 4 4 2 2 2 2 2 2 c + b + a >= b c + a c + a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 4 3 2 2 2 3 3 4 3 (z + (2 y + 2 x) z + (3 y + 3 x ) z + (2 y + 2 x ) z + y + 2 x y 2 2 3 4 4 3 2 2 2 + 3 x y + 2 x y + x )/8 >= (z + (2 y + 2 x) z + (3 y + 8 x y + 3 x ) z 3 2 2 3 4 3 2 2 3 4 + (2 y + 8 x y + 8 x y + 2 x ) z + y + 2 x y + 3 x y + 2 x y + x )/16 Multiplying both sides by 16 gives: 4 3 3 2 2 2 2 3 3 4 3 2 z + 4 y z + 4 x z + 6 y z + 6 x z + 4 y z + 4 x z + 2 y + 4 x y 2 2 3 4 4 3 3 2 2 2 + 6 x y + 4 x y + 2 x >= z + 2 y z + 2 x z + 3 y z + 8 x y z 2 2 3 2 2 3 4 3 2 2 + 3 x z + 2 y z + 8 x y z + 8 x y z + 2 x z + y + 2 x y + 3 x y 3 4 + 2 x y + x Expanding and collecting terms of the same sign gives: 4 3 3 2 2 2 2 3 3 4 3 z + 2 y z + 2 x z + 3 y z + 3 x z + 2 y z + 2 x z + y + 2 x y 2 2 3 4 2 2 2 + 3 x y + 2 x y + x >= 8 x y z + 8 x y z + 8 x y z Expressing in terms of symmetric polynomials gives: {4, 0, 0} + 4 {3, 1, 0} + 3 {2, 2, 0} >= 8 {2, 1, 1} This follows from the following majorizations: 3 {2, 2, 0} >= 3 {2, 1, 1} 4 {3, 1, 0} >= 4 {2, 1, 1} {4, 0, 0} >= {2, 1, 1} (d15) true (c16) /* 4.13 */ trineq(4*K*sqrt(3)<=9*a*b*c/csum(a)); 9 a b c To prove: --------- >= 4 sqrt(3) K c + b + a Multiplying both sides by c + b + a gives: 9 a b c >= 4 sqrt(3) K c + 4 sqrt(3) K b + 4 sqrt(3) K a Since 4 sqrt(3) c + 4 sqrt(3) b + 4 sqrt(3) a is positive, and since 9 a b c is positive, we can square both sides to get: 2 2 2 2 2 2 4 81 a b c >= (48 c + (96 b + 96 a) c + 48 b + 96 a b + 48 a ) s 3 2 2 2 3 + (- 48 c + (- 144 b - 144 a) c + (- 144 b - 288 a b - 144 a ) c - 48 b 2 2 3 3 3 - 144 a b - 144 a b - 48 a ) s + ((48 b + 48 a) c 2 2 2 3 2 2 3 + (96 b + 240 a b + 96 a ) c + (48 b + 240 a b + 240 a b + 48 a ) c 3 2 2 3 2 3 2 2 2 + 48 a b + 96 a b + 48 a b) s + (- 48 a b c + (- 96 a b - 96 a b) c 3 2 2 3 + (- 48 a b - 96 a b - 48 a b) c) s Expanding and collecting terms of the same sign gives: 3 3 2 3 2 3 2 3 3 2 3 48 c s + 144 b c s + 144 a c s + 144 b c s + 288 a b c s + 144 a c s 3 3 2 3 2 3 3 3 3 2 2 + 48 b s + 144 a b s + 144 a b s + 48 a s + 48 a b c s + 96 a b c s 2 2 3 2 2 3 2 2 2 + 96 a b c s + 48 a b c s + 96 a b c s + 48 a b c s + 81 a b c >= 2 4 4 4 2 4 4 2 4 3 2 48 c s + 96 b c s + 96 a c s + 48 b s + 96 a b s + 48 a s + 48 b c s 3 2 2 2 2 2 2 2 2 2 3 2 + 48 a c s + 96 b c s + 240 a b c s + 96 a c s + 48 b c s 2 2 2 2 3 2 3 2 2 2 2 + 240 a b c s + 240 a b c s + 48 a c s + 48 a b s + 96 a b s 3 2 + 48 a b s Dividing both sides by 3 gives: 3 3 2 3 2 3 2 3 3 2 3 16 c s + 48 b c s + 48 a c s + 48 b c s + 96 a b c s + 48 a c s 3 3 2 3 2 3 3 3 3 2 2 + 16 b s + 48 a b s + 48 a b s + 16 a s + 16 a b c s + 32 a b c s 2 2 3 2 2 3 2 2 2 + 32 a b c s + 16 a b c s + 32 a b c s + 16 a b c s + 27 a b c >= 2 4 4 4 2 4 4 2 4 3 2 16 c s + 32 b c s + 32 a c s + 16 b s + 32 a b s + 16 a s + 16 b c s 3 2 2 2 2 2 2 2 2 2 3 2 + 16 a c s + 32 b c s + 80 a b c s + 32 a c s + 16 b c s 2 2 2 2 3 2 3 2 2 2 2 + 80 a b c s + 80 a b c s + 16 a c s + 16 a b s + 32 a b s 3 2 + 16 a b s Let s = (c+b+a)/2 . We get: 6 5 2 2 4 2 c + (12 b + 12 a) c + (30 b + 68 a b + 30 a ) c 3 2 2 3 3 + (40 b + 144 a b + 144 a b + 40 a ) c 4 3 2 2 3 4 2 + (30 b + 144 a b + 255 a b + 144 a b + 30 a ) c 5 4 2 3 3 2 4 5 6 + (12 b + 68 a b + 144 a b + 144 a b + 68 a b + 12 a ) c + 2 b 5 2 4 3 3 4 2 5 6 + 12 a b + 30 a b + 40 a b + 30 a b + 12 a b + 2 a >= 6 5 2 2 4 c + (10 b + 10 a) c + (31 b + 66 a b + 31 a ) c 3 2 2 3 3 + (44 b + 148 a b + 148 a b + 44 a ) c 4 3 2 2 3 4 2 + (31 b + 148 a b + 234 a b + 148 a b + 31 a ) c 5 4 2 3 3 2 4 5 6 5 + (10 b + 66 a b + 148 a b + 148 a b + 66 a b + 10 a ) c + b + 10 a b 2 4 3 3 4 2 5 6 + 31 a b + 44 a b + 31 a b + 10 a b + a Expanding and collecting terms of the same sign gives: 6 5 5 4 2 2 2 5 4 4 c + 2 b c + 2 a c + 2 a b c + 21 a b c + 2 b c + 2 a b c + 2 a b c 5 6 5 5 6 + 2 a c + b + 2 a b + 2 a b + a >= 2 4 2 4 3 3 2 3 2 3 3 3 4 2 3 2 b c + a c + 4 b c + 4 a b c + 4 a b c + 4 a c + b c + 4 a b c 3 2 4 2 2 3 3 2 2 4 3 3 4 2 + 4 a b c + a c + 4 a b c + 4 a b c + a b + 4 a b + a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 6 5 2 2 4 (3 z + (13 y + 13 x) z + (38 y + 51 x y + 38 x ) z 3 2 2 3 3 + (57 y + 97 x y + 97 x y + 57 x ) z 4 3 2 2 3 4 2 + (38 y + 97 x y + 123 x y + 97 x y + 38 x ) z 5 4 2 3 3 2 4 5 6 5 + (13 y + 51 x y + 97 x y + 97 x y + 51 x y + 13 x ) z + 3 y + 13 x y 2 4 3 3 4 2 5 6 + 38 x y + 57 x y + 38 x y + 13 x y + 3 x )/32 >= 6 5 2 2 4 (6 z + (26 y + 26 x) z + (49 y + 112 x y + 49 x ) z 3 2 2 3 3 + (60 y + 224 x y + 224 x y + 60 x ) z 4 3 2 2 3 4 2 + (49 y + 224 x y + 360 x y + 224 x y + 49 x ) z 5 4 2 3 3 2 4 5 6 + (26 y + 112 x y + 224 x y + 224 x y + 112 x y + 26 x ) z + 6 y 5 2 4 3 3 4 2 5 6 + 26 x y + 49 x y + 60 x y + 49 x y + 26 x y + 6 x )/64 Multiplying both sides by 64 gives: 6 5 5 2 4 4 2 4 3 3 6 z + 26 y z + 26 x z + 76 y z + 102 x y z + 76 x z + 114 y z 2 3 2 3 3 3 4 2 3 2 + 194 x y z + 194 x y z + 114 x z + 76 y z + 194 x y z 2 2 2 3 2 4 2 5 4 2 3 + 246 x y z + 194 x y z + 76 x z + 26 y z + 102 x y z + 194 x y z 3 2 4 5 6 5 2 4 3 3 + 194 x y z + 102 x y z + 26 x z + 6 y + 26 x y + 76 x y + 114 x y 4 2 5 6 6 5 5 2 4 + 76 x y + 26 x y + 6 x >= 6 z + 26 y z + 26 x z + 49 y z 4 2 4 3 3 2 3 2 3 3 3 + 112 x y z + 49 x z + 60 y z + 224 x y z + 224 x y z + 60 x z 4 2 3 2 2 2 2 3 2 4 2 5 + 49 y z + 224 x y z + 360 x y z + 224 x y z + 49 x z + 26 y z 4 2 3 3 2 4 5 6 + 112 x y z + 224 x y z + 224 x y z + 112 x y z + 26 x z + 6 y 5 2 4 3 3 4 2 5 6 + 26 x y + 49 x y + 60 x y + 49 x y + 26 x y + 6 x Expanding and collecting terms of the same sign gives: 2 4 2 4 3 3 3 3 4 2 4 2 2 4 27 y z + 27 x z + 54 y z + 54 x z + 27 y z + 27 x z + 27 x y 3 3 4 2 4 2 3 2 3 3 2 + 54 x y + 27 x y >= 10 x y z + 30 x y z + 30 x y z + 30 x y z 2 2 2 3 2 4 2 3 3 2 4 + 114 x y z + 30 x y z + 10 x y z + 30 x y z + 30 x y z + 10 x y z Expressing in terms of symmetric polynomials gives: 27 {4, 2, 0} + 27 {3, 3, 0} >= 5 {4, 1, 1} + 30 {3, 2, 1} + 19 {2, 2, 2} This follows from the following majorizations: 5 {4, 2, 0} >= 5 {4, 1, 1} 22 {4, 2, 0} >= 22 {3, 2, 1} 8 {3, 3, 0} >= 8 {3, 2, 1} 19 {3, 3, 0} >= 19 {2, 2, 2} (d16) true (c17) /* 4.14 */ trineq((a*b*c)^2>=(4*K/sqrt(3))^2); 2 2 2 2 16 K To prove: a b c >= ----- 3 Multiplying both sides by 3 gives: 2 2 2 2 3 a b c >= 16 K Replacing K^2 by F^2 gives: 2 2 2 2 3 a b c >= 16 F Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 2 2 2 4 2 2 2 4 2 2 4 3 a b c >= - c + (2 b + 2 a ) c - b + 2 a b - a Expanding and collecting terms of the same sign gives: 4 2 2 2 4 4 2 2 2 2 2 2 c + 3 a b c + b + a >= 2 b c + 2 a c + 2 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 2 2 4 3 2 2 3 ((3 y + 6 x y + 3 x + 8) z + (6 y + 18 x y + (18 x + 16) y + 6 x + 16 x) 3 4 3 2 2 3 4 2 2 z + (3 y + 18 x y + (30 x + 24) y + 18 x y + 3 x + 24 x ) z 4 2 3 3 2 4 3 2 4 + (6 x y + (18 x + 16) y + 18 x y + 6 x y + 16 x ) z + (3 x + 8) y 3 3 4 2 2 3 4 + (6 x + 16 x) y + (3 x + 24 x ) y + 16 x y + 8 x )/64 >= 4 3 2 2 2 (z + (2 y + 2 x) z + (3 y + 8 x y + 3 x ) z 3 2 2 3 4 3 2 2 3 4 + (2 y + 8 x y + 8 x y + 2 x ) z + y + 2 x y + 3 x y + 2 x y + x )/8 Multiplying both sides by 64 gives: 2 4 4 2 4 4 3 3 2 3 2 3 3 y z + 6 x y z + 3 x z + 8 z + 6 y z + 18 x y z + 18 x y z 3 3 3 3 4 2 3 2 2 2 2 2 2 + 16 y z + 6 x z + 16 x z + 3 y z + 18 x y z + 30 x y z + 24 y z 3 2 4 2 2 2 4 2 3 3 + 18 x y z + 3 x z + 24 x z + 6 x y z + 18 x y z + 16 y z 3 2 4 3 2 4 4 3 3 3 + 18 x y z + 6 x y z + 16 x z + 3 x y + 8 y + 6 x y + 16 x y 4 2 2 2 3 4 + 3 x y + 24 x y + 16 x y + 8 x >= 4 3 3 2 2 2 2 2 3 8 z + 16 y z + 16 x z + 24 y z + 64 x y z + 24 x z + 16 y z 2 2 3 4 3 2 2 3 4 + 64 x y z + 64 x y z + 16 x z + 8 y + 16 x y + 24 x y + 16 x y + 8 x Expanding and collecting terms of the same sign gives: 2 4 4 2 4 3 3 2 3 2 3 3 3 3 y z + 6 x y z + 3 x z + 6 y z + 18 x y z + 18 x y z + 6 x z 4 2 3 2 2 2 2 3 2 4 2 4 + 3 y z + 18 x y z + 30 x y z + 18 x y z + 3 x z + 6 x y z 2 3 3 2 4 2 4 3 3 4 2 + 18 x y z + 18 x y z + 6 x y z + 3 x y + 6 x y + 3 x y >= 2 2 2 64 x y z + 64 x y z + 64 x y z Expressing in terms of symmetric polynomials gives: 3 {4, 2, 0} + 3 {4, 1, 1} + 3 {3, 3, 0} + 18 {3, 2, 1} + 5 {2, 2, 2} >= 32 {2, 1, 1} This follows from the following majorizations: 5 {2, 2, 2} >= 5 {2, 1, 1} 18 {3, 2, 1} >= 18 {2, 1, 1} 3 {3, 3, 0} >= 3 {2, 1, 1} 3 {4, 1, 1} >= 3 {2, 1, 1} 3 {4, 2, 0} >= 3 {2, 1, 1} (d17) true (c18) /* 4.18 */ trineq((csum(a*b)-csum(a^2)/2)*(3*csum(a*b)-5*csum(a^2)/2)/12<=K^2); 2 To prove: K >= 2 2 2 2 2 2 5 (c + b + a ) c + b + a (3 (b c + a c + a b) - ----------------) (- ------------ + b c + a c + a b) 2 2 --------------------------------------------------------------------------- 12 Expanding and collecting terms of the same sign gives: 3 3 3 3 3 3 b c a c b c a c a b a b 2 ---- + ---- + ---- + ---- + ---- + ---- + K >= 3 3 3 3 3 3 4 2 2 2 2 2 2 2 4 2 2 4 5 c 11 b c a b c 11 a c a b c a b c 5 b 11 a b 5 a ---- + -------- + ------ + -------- + ------ + ------ + ---- + -------- + ---- 48 24 6 24 6 6 48 24 48 Multiplying both sides by 48 gives: 3 3 3 3 3 3 2 16 b c + 16 a c + 16 b c + 16 a c + 16 a b + 16 a b + 48 K >= 4 2 2 2 2 2 2 2 4 2 2 5 c + 22 b c + 8 a b c + 22 a c + 8 a b c + 8 a b c + 5 b + 22 a b 4 + 5 a Replacing K^2 by F^2 gives: 3 3 3 3 3 2 (16 b + 16 a) c + (16 b + 16 a ) c + 16 a b + 16 a b + 48 F >= 4 2 2 2 2 2 4 2 2 5 c + (22 b + 8 a b + 22 a ) c + (8 a b + 8 a b) c + 5 b + 22 a b 4 + 5 a Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 4 3 2 2 2 3 3 4 - 3 c + (16 b + 16 a) c + (6 b + 6 a ) c + (16 b + 16 a ) c - 3 b 3 2 2 3 4 + 16 a b + 6 a b + 16 a b - 3 a >= 4 2 2 2 2 2 4 2 2 5 c + (22 b + 8 a b + 22 a ) c + (8 a b + 8 a b) c + 5 b + 22 a b 4 + 5 a Expanding and collecting terms of the same sign gives: 3 3 3 3 3 3 16 b c + 16 a c + 16 b c + 16 a c + 16 a b + 16 a b >= 4 2 2 2 2 2 2 2 4 2 2 8 c + 16 b c + 8 a b c + 16 a c + 8 a b c + 8 a b c + 8 b + 16 a b 4 + 8 a Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 4 3 2 2 2 2 z + (6 y + 6 x) z + (6 y + 12 x y + 6 x ) z 3 2 2 3 4 3 2 2 3 + (6 y + 12 x y + 12 x y + 6 x ) z + 2 y + 6 x y + 6 x y + 6 x y 4 4 3 2 2 2 + 2 x >= 2 z + (5 y + 5 x) z + (8 y + 12 x y + 8 x ) z 3 2 2 3 4 3 2 2 3 + (5 y + 12 x y + 12 x y + 5 x ) z + 2 y + 5 x y + 8 x y + 5 x y 4 + 2 x Expanding and collecting terms of the same sign gives: 3 3 3 3 3 3 2 2 2 2 2 2 y z + x z + y z + x z + x y + x y >= 2 y z + 2 x z + 2 x y Expressing in terms of symmetric polynomials gives: {3, 1, 0} >= {2, 2, 0} This result follows from the majorization theorem. (d18) true (c19) trineq(K^2<=(csum(a*b)-csum(a^2)/2)^2/12); 2 2 2 c + b + a 2 (- ------------ + b c + a c + a b) 2 2 To prove: ----------------------------------- >= K 12 Expanding and collecting terms of the same sign gives: 4 2 2 2 2 2 2 2 4 2 2 4 c b c a b c a c a b c a b c b a b a -- + ----- + ------ + ----- + ------ + ------ + -- + ----- + -- >= 48 8 12 8 12 12 48 8 48 3 3 3 3 3 3 b c a c b c a c a b a b 2 ---- + ---- + ---- + ---- + ---- + ---- + K 12 12 12 12 12 12 Multiplying both sides by 48 gives: 4 2 2 2 2 2 2 2 4 2 2 4 c + 6 b c + 4 a b c + 6 a c + 4 a b c + 4 a b c + b + 6 a b + a >= 3 3 3 3 3 3 2 4 b c + 4 a c + 4 b c + 4 a c + 4 a b + 4 a b + 48 K Replacing K^2 by F^2 gives: 4 2 2 2 2 2 4 2 2 4 c + (6 b + 4 a b + 6 a ) c + (4 a b + 4 a b) c + b + 6 a b + a >= 3 3 3 3 3 2 (4 b + 4 a) c + (4 b + 4 a ) c + 4 a b + 4 a b + 48 F Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 4 2 2 2 2 2 4 2 2 4 c + (6 b + 4 a b + 6 a ) c + (4 a b + 4 a b) c + b + 6 a b + a >= 4 3 2 2 2 3 3 4 3 - 3 c + (4 b + 4 a) c + (6 b + 6 a ) c + (4 b + 4 a ) c - 3 b + 4 a b 2 2 3 4 + 6 a b + 4 a b - 3 a Expanding and collecting terms of the same sign gives: 4 2 2 2 4 4 4 c + 4 a b c + 4 a b c + 4 a b c + 4 b + 4 a >= 3 3 3 3 3 3 4 b c + 4 a c + 4 b c + 4 a c + 4 a b + 4 a b Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 4 3 2 2 2 (z + (3 y + 3 x) z + (5 y + 4 x y + 5 x ) z 3 2 2 3 4 3 2 2 3 4 + (3 y + 4 x y + 4 x y + 3 x ) z + y + 3 x y + 5 x y + 3 x y + x ) 4 3 2 2 2 /2 >= (z + (3 y + 3 x) z + (3 y + 6 x y + 3 x ) z 3 2 2 3 4 3 2 2 3 4 + (3 y + 6 x y + 6 x y + 3 x ) z + y + 3 x y + 3 x y + 3 x y + x )/2 Multiplying both sides by 2 gives: 4 3 3 2 2 2 2 2 3 2 z + 3 y z + 3 x z + 5 y z + 4 x y z + 5 x z + 3 y z + 4 x y z 2 3 4 3 2 2 3 4 + 4 x y z + 3 x z + y + 3 x y + 5 x y + 3 x y + x >= 4 3 3 2 2 2 2 2 3 2 z + 3 y z + 3 x z + 3 y z + 6 x y z + 3 x z + 3 y z + 6 x y z 2 3 4 3 2 2 3 4 + 6 x y z + 3 x z + y + 3 x y + 3 x y + 3 x y + x Expanding and collecting terms of the same sign gives: 2 2 2 2 2 2 2 2 2 2 y z + 2 x z + 2 x y >= 2 x y z + 2 x y z + 2 x y z Dividing both sides by 2 gives: 2 2 2 2 2 2 2 2 2 y z + x z + x y >= x y z + x y z + x y z Expressing in terms of symmetric polynomials gives: {2, 2, 0} >= {2, 1, 1} This result follows from the majorization theorem. (d19) true (c20) /* 4.20 */ trineq(27*cprod(b^2+c^2-a^2)^2<=(4*K)^6); 6 2 2 2 2 2 2 2 2 2 2 2 2 To prove: 4096 K >= 27 (- c + b + a ) (c - b + a ) (c + b - a ) Expanding and collecting terms of the same sign gives: 2 10 2 10 4 8 4 8 2 4 6 4 2 6 54 b c + 54 a c + 27 b c + 27 a c + 108 a b c + 108 a b c 8 4 2 6 4 6 2 4 8 4 10 2 4 6 2 + 27 b c + 108 a b c + 108 a b c + 27 a c + 54 b c + 108 a b c 6 4 2 10 2 2 10 4 8 8 4 10 2 + 108 a b c + 54 a c + 54 a b + 27 a b + 27 a b + 54 a b 6 12 2 2 8 6 6 6 6 4 4 4 + 4096 K >= 27 c + 162 a b c + 108 b c + 108 a c + 270 a b c 2 8 2 8 2 2 12 6 6 12 + 162 a b c + 162 a b c + 27 b + 108 a b + 27 a Replacing K^2 by F^2 gives: 2 2 10 4 4 8 2 4 4 2 6 (54 b + 54 a ) c + (27 b + 27 a ) c + (108 a b + 108 a b ) c 8 2 6 6 2 8 4 + (27 b + 108 a b + 108 a b + 27 a ) c 10 4 6 6 4 10 2 2 10 4 8 + (54 b + 108 a b + 108 a b + 54 a ) c + 54 a b + 27 a b 8 4 10 2 6 12 2 2 8 + 27 a b + 54 a b + 4096 F >= 27 c + 162 a b c 6 6 6 4 4 4 2 8 8 2 2 12 + (108 b + 108 a ) c + 270 a b c + (162 a b + 162 a b ) c + 27 b 6 6 12 + 108 a b + 27 a Let F = sqrt(s*(s-a)*(s-b)*(s-c)) . Let s = (c+b+a)/2 . We get: 12 2 2 10 4 2 2 4 8 - c + (60 b + 60 a ) c + (12 b - 18 a b + 12 a ) c 6 2 4 4 2 6 6 + (20 b + 120 a b + 120 a b + 20 a ) c 8 2 6 4 4 6 2 8 4 + (12 b + 120 a b + 6 a b + 120 a b + 12 a ) c 10 2 8 4 6 6 4 8 2 10 2 12 + (60 b - 18 a b + 120 a b + 120 a b - 18 a b + 60 a ) c - b 2 10 4 8 6 6 8 4 10 2 12 + 60 a b + 12 a b + 20 a b + 12 a b + 60 a b - a >= 12 2 2 8 6 6 6 4 4 4 27 c + 162 a b c + (108 b + 108 a ) c + 270 a b c 2 8 8 2 2 12 6 6 12 + (162 a b + 162 a b ) c + 27 b + 108 a b + 27 a Expanding and collecting terms of the same sign gives: 2 10 2 10 4 8 4 8 2 4 6 4 2 6 60 b c + 60 a c + 12 b c + 12 a c + 120 a b c + 120 a b c 8 4 2 6 4 6 2 4 8 4 10 2 4 6 2 + 12 b c + 120 a b c + 120 a b c + 12 a c + 60 b c + 120 a b c 6 4 2 10 2 2 10 4 8 8 4 10 2 + 120 a b c + 60 a c + 60 a b + 12 a b + 12 a b + 60 a b >= 12 2 2 8 6 6 6 6 4 4 4 2 8 2 28 c + 180 a b c + 88 b c + 88 a c + 264 a b c + 180 a b c 8 2 2 12 6 6 12 + 180 a b c + 28 b + 88 a b + 28 a Let a=(y+z)/2, b=(z+x)/2, c=(x+y)/2, to get: 12 11 2 2 10 (18 z + (108 y + 108 x) z + (441 y + 486 x y + 441 x ) z 3 2 2 3 9 + (1215 y + 1665 x y + 1665 x y + 1215 x ) z 4 3 2 2 3 4 8 + (2367 y + 4341 x y + 4122 x y + 4341 x y + 2367 x ) z 5 4 2 3 3 2 4 5 7 + (3366 y + 8202 x y + 8472 x y + 8472 x y + 8202 x y + 3366 x ) z 6 5 2 4 3 3 4 2 5 + (3744 y + 10974 x y + 13746 x y + 14208 x y + 13746 x y + 10974 x y 6 6 7 6 2 5 3 4 + 3744 x ) z + (3366 y + 10974 x y + 15948 x y + 20064 x y 4 3 5 2 6 7 5 + 20064 x y + 15948 x y + 10974 x y + 3366 x ) z 8 7 2 6 3 5 4 4 5 3 + (2367 y + 8202 x y + 13746 x y + 20064 x y + 24480 x y + 20064 x y 6 2 7 8 4 + 13746 x y + 8202 x y + 2367 x ) z 9 8 2 7 3 6 4 5 5 4 + (1215 y + 4341 x y + 8472 x y + 14208 x y + 20064 x y + 20064 x y 6 3 7 2 8 9 3 + 14208 x y + 8472 x y + 4341 x y + 1215 x ) z 10 9 2 8 3 7 4 6 5 5 + (441 y + 1665 x y + 4122 x y + 8472 x y + 13746 x y + 15948 x y 6 4 7 3 8 2 9 10 2 + 13746 x y + 8472 x y + 4122 x y + 1665 x y + 441 x ) z 11 10 2 9 3 8 4 7 5 6 + (108 y + 486 x y + 1665 x y + 4341 x y + 8202 x y + 10974 x y 6 5 7 4 8 3 9 2 10 11 + 10974 x y + 8202 x y + 4341 x y + 1665 x y + 486 x y + 108 x ) z 12 11 2 10 3 9 4 8 5 7 + 18 y + 108 x y + 441 x y + 1215 x y + 2367 x y + 3366 x y 6 6 7 5 8 4 9 3 10 2 11 + 3744 x y + 3366 x y + 2367 x y + 1215 x y + 441 x y + 108 x y 12 12 11 + 18 x )/512 >= (18 z + (108 y + 108 x) z 2 2 10 3 2 2 + (441 y + 486 x y + 441 x ) z + (1215 y + 1665 x y + 1665 x y 3 9 4 3 2 2 3 4 8 + 1215 x ) z + (2583 y + 3477 x y + 5418 x y + 3477 x y + 2583 x ) z 5 4 2 3 3 2 4 5 7 + (4230 y + 5610 x y + 10200 x y + 10200 x y + 5610 x y + 4230 x ) z 6 5 2 4 3 3 4 2 5 + (5040 y + 7518 x y + 14178 x y + 17152 x y + 14178 x y + 7518 x y 6 6 7 6 2 5 3 4 4 3 + 5040 x ) z + (4230 y + 7518 x y + 15948 x y + 21120 x y + 21120 x y 5 2 6 7 5 + 15948 x y + 7518 x y + 4230 x ) z 8 7 2 6 3 5 4 4 5 3 + (2583 y + 5610 x y + 14178 x y + 21120 x y + 23568 x y + 21120 x y 6 2 7 8 4 + 14178 x y + 5610 x y + 2583 x ) z 9 8 2 7 3 6 4 5 5 4 + (1215 y + 3477 x y + 10200 x y + 17152 x y + 21120 x y + 21120 x y 6 3 7 2 8 9 3 + 17152 x y + 10200 x y + 3477 x y + 1215 x ) z 10 9 2 8 3 7 4 6 5 5 + (441 y + 1665 x y + 5418 x y + 10200 x y + 14178 x y + 15948 x y 6 4 7 3 8 2 9 10 2 + 14178 x y + 10200 x y + 5418 x y + 1665 x y + 441 x ) z 11 10 2 9 3 8 4 7 5 6 + (108 y + 486 x y + 1665 x y + 3477 x y + 5610 x y + 7518 x y 6 5 7 4 8 3 9 2 10 11 + 7518 x y + 5610 x y + 3477 x y + 1665 x y + 486 x y + 108 x ) z 12 11 2 10 3 9 4 8 5 7 + 18 y + 108 x y + 441 x y + 1215 x y + 2583 x y + 4230 x y 6 6 7 5 8 4 9 3 10 2 11 + 5040 x y + 4230 x y + 2583 x y + 1215 x y + 441 x y + 108 x y 12 + 18 x )/512 Multiplying both sides by 512 gives: 12 11 11 2 10 10 2 10 18 z + 108 y z + 108 x z + 441 y z + 486 x y z + 441 x z 3 9 2 9 2 9 3 9 4 8 + 1215 y z + 1665 x y z + 1665 x y z + 1215 x z + 2367 y z 3 8 2 2 8 3 8 4 8 5 7 + 4341 x y z + 4122 x y z + 4341 x y z + 2367 x z + 3366 y z 4 7 2 3 7 3 2 7 4 7 5 7 + 8202 x y z + 8472 x y z + 8472 x y z + 8202 x y z + 3366 x z 6 6 5 6 2 4 6 3 3 6 + 3744 y z + 10974 x y z + 13746 x y z + 14208 x y z 4 2 6 5 6 6 6 7 5 6 5 + 13746 x y z + 10974 x y z + 3744 x z + 3366 y z + 10974 x y z 2 5 5 3 4 5 4 3 5 5 2 5 + 15948 x y z + 20064 x y z + 20064 x y z + 15948 x y z 6 5 7 5 8 4 7 4 2 6 4 + 10974 x y z + 3366 x z + 2367 y z + 8202 x y z + 13746 x y z 3 5 4 4 4 4 5 3 4 6 2 4 + 20064 x y z + 24480 x y z + 20064 x y z + 13746 x y z 7 4 8 4 9 3 8 3 2 7 3 + 8202 x y z + 2367 x z + 1215 y z + 4341 x y z + 8472 x y z 3 6 3 4 5 3 5 4 3 6 3 3 + 14208 x y z + 20064 x y z + 20064 x y z + 14208 x y z 7 2 3 8 3 9 3 10 2 9 2 + 8472 x y z + 4341 x y z + 1215 x z + 441 y z + 1665 x y z 2 8 2 3 7 2 4 6 2 5 5 2 + 4122 x y z + 8472 x y z + 13746 x y z + 15948 x y z 6 4 2 7 3 2 8 2 2 9 2 10 2 + 13746 x y z + 8472 x y z + 4122 x y z + 1665 x y z + 441 x z 11 10 2 9 3 8 4 7 + 108 y z + 486 x y z + 1665 x y z + 4341 x y z + 8202 x y z 5 6 6 5 7 4 8 3 9 2 + 10974 x y z + 10974 x y z + 8202 x y z + 4341 x y z + 1665 x y z 10 11 12 11 2 10 3 9 + 486 x y z + 108 x z + 18 y + 108 x y + 441 x y + 1215 x y 4 8 5 7 6 6 7 5 8 4 9 3 + 2367 x y + 3366 x y + 3744 x y + 3366 x y + 2367 x y + 1215 x y 10 2 11 12 12 11 11 + 441 x y + 108 x y + 18 x >= 18 z + 108 y z + 108 x z 2 10 10 2 10 3 9 2 9 + 441 y z + 486 x y z + 441 x z + 1215 y z + 1665 x y z 2 9 3 9 4 8 3 8 2 2 8 + 1665 x y z + 1215 x z + 2583 y z + 3477 x y z + 5418 x y z 3 8 4 8 5 7 4 7 2 3 7 + 3477 x y z + 2583 x z + 4230 y z + 5610 x y z + 10200 x y z 3 2 7 4 7 5 7 6 6 5 6 + 10200 x y z + 5610 x y z + 4230 x z + 5040 y z + 7518 x y z 2 4 6 3 3 6 4 2 6 5 6 6 6 + 14178 x y z + 17152 x y z + 14178 x y z + 7518 x y z + 5040 x z 7 5 6 5 2 5 5 3 4 5 4 3 5 + 4230 y z + 7518 x y z + 15948 x y z + 21120 x y z + 21120 x y z 5 2 5 6 5 7 5 8 4 7 4 + 15948 x y z + 7518 x y z + 4230 x z + 2583 y z + 5610 x y z 2 6 4 3 5 4 4 4 4 5 3 4 + 14178 x y z + 21120 x y z + 23568 x y z + 21120 x y z 6 2 4 7 4 8 4 9 3 8 3 + 14178 x y z + 5610 x y z + 2583 x z + 1215 y z + 3477 x y z 2 7 3 3 6 3 4 5 3 5 4 3 + 10200 x y z + 17152 x y z + 21120 x y z + 21120 x y z 6 3 3 7 2 3 8 3 9 3 10 2 + 17152 x y z + 10200 x y z + 3477 x y z + 1215 x z + 441 y z 9 2 2 8 2 3 7 2 4 6 2 + 1665 x y z + 5418 x y z + 10200 x y z + 14178 x y z 5 5 2 6 4 2 7 3 2 8 2 2 + 15948 x y z + 14178 x y z + 10200 x y z + 5418 x y z 9 2 10 2 11 10 2 9 + 1665 x y z + 441 x z + 108 y z + 486 x y z + 1665 x y z 3 8 4 7 5 6 6 5 7 4 + 3477 x y z + 5610 x y z + 7518 x y z + 7518 x y z + 5610 x y z 8 3 9 2 10 11 12 11 + 3477 x y z + 1665 x y z + 486 x y z + 108 x z + 18 y + 108 x y 2 10 3 9 4 8 5 7 6 6 7 5 + 441 x y + 1215 x y + 2583 x y + 4230 x y + 5040 x y + 4230 x y 8 4 9 3 10 2 11 12 + 2583 x y + 1215 x y + 441 x y + 108 x y + 18 x Expanding and collecting terms of the same sign gives: 3 8 3 8 4 7 4 7 5 6 864 x y z + 864 x y z + 2592 x y z + 2592 x y z + 3456 x y z 5 6 6 5 6 5 7 4 4 4 4 + 3456 x y z + 3456 x y z + 3456 x y z + 2592 x y z + 912 x y z 7 4 8 3 8 3 3 8 4 7 + 2592 x y z + 864 x y z + 864 x y z + 864 x y z + 2592 x y z 5 6 6 5 7 4 8 3 + 3456 x y z + 3456 x y z + 2592 x y z + 864 x y z >= 4 8 2 2 8 4 8 5 7 2 3 7 216 y z + 1296 x y z + 216 x z + 864 y z + 1728 x y z 3 2 7 5 7 6 6 2 4 6 3 3 6 + 1728 x y z + 864 x z + 1296 y z + 432 x y z + 2944 x y z 4 2 6 6 6 7 5 3 4 5 4 3 5 + 432 x y z + 1296 x z + 864 y z + 1056 x y z + 1056 x y z 7 5 8 4 2 6 4 3 5 4 5 3 4 + 864 x z + 216 y z + 432 x y z + 1056 x y z + 1056 x y z 6 2 4 8 4 2 7 3 3 6 3 4 5 3 + 432 x y z + 216 x z + 1728 x y z + 2944 x y z + 1056 x y z 5 4 3 6 3 3 7 2 3 2 8 2 + 1056 x y z + 2944 x y z + 1728 x y z + 1296 x y z 3 7 2 4 6 2 6 4 2 7 3 2 8 2 2 + 1728 x y z + 432 x y z + 432 x y z + 1728 x y z + 1296 x y z 4 8 5 7 6 6 7 5 8 4 + 216 x y + 864 x y + 1296 x y + 864 x y + 216 x y Dividing both sides by 8 gives: 3 8 3 8 4 7 4 7 5 6 108 x y z + 108 x y z + 324 x y z + 324 x y z + 432 x y z 5 6 6 5 6 5 7 4 4 4 4 + 432 x y z + 432 x y z + 432 x y z + 324 x y z + 114 x y z 7 4 8 3 8 3 3 8 4 7 + 324 x y z + 108 x y z + 108 x y z + 108 x y z + 324 x y z 5 6 6 5 7 4 8 3 + 432 x y z + 432 x y z + 324 x y z + 108 x y z >= 4 8 2 2 8 4 8 5 7 2 3 7 3 2 7 27 y z + 162 x y z + 27 x z + 108 y z + 216 x y z + 216 x y z 5 7 6 6 2 4 6 3 3 6 4 2 6 6 6 + 108 x z + 162 y z + 54 x y z + 368 x y z + 54 x y z + 162 x z 7 5 3 4 5 4 3 5 7 5 8 4 2 6 4 + 108 y z + 132 x y z + 132 x y z + 108 x z + 27 y z + 54 x y z 3 5 4 5 3 4 6 2 4 8 4 2 7 3 + 132 x y z + 132 x y z + 54 x y z + 27 x z + 216 x y z 3 6 3 4 5 3 5 4 3 6 3 3 7 2 3 + 368 x y z + 132 x y z + 132 x y z + 368 x y z + 216 x y z 2 8 2 3 7 2 4 6 2 6 4 2 7 3 2 + 162 x y z + 216 x y z + 54 x y z + 54 x y z + 216 x y z 8 2 2 4 8 5 7 6 6 7 5 8 4 + 162 x y z + 27 x y + 108 x y + 162 x y + 108 x y + 27 x y Expressing in terms of symmetric polynomials gives: 108 {8, 3, 1} + 324 {7, 4, 1} + 432 {6, 5, 1} + 19 {4, 4, 4} >= 27 {8, 4, 0} + 81 {8, 2, 2} + 108 {7, 5, 0} + 216 {7, 3, 2} + 81 {6, 6, 0} + 54 {6, 4, 2} + 184 {6, 3, 3} + 132 {5, 4, 3} This follows from the following majorizations: 81 {8, 3, 1} >= 81 {8, 2, 2} left side: [19 {4, 4, 4}, 432 {6, 5, 1}, 324 {7, 4, 1}, 108 {8, 3, 1}] right side: [132 {5, 4, 3}, 184 {6, 3, 3}, 54 {6, 4, 2}, 81 {6, 6, 0}, 216 {7, 3, 2}, 108 {7, 5, 0}, 81 {8, 2, 2}, 27 {8, 4, 0}] (d20) notsure (c21) print("Summary:") $ Summary: (c22) print("Proved",triangtrue,"inequalities out of",triangcount,".") $ Proved 13 inequalities out of 17 . (d23) BATCH DONE (c24)