神秘化简问题, 仅仅是移项甚至只是对调了一下不等式的方向就不行了.
原问题是在一定条件下化简一个复杂的不等式, 预期结果是true或false, 没有达到预期结果, 结果是part1 > part2, 找不出原因的情况下, 我尝试直接化简part1 > part2, 并且将part1 > part2稍微变形或原样添加进assum, 也就是assum的第二部分.
原样添加进assum的时候, 可以得到true, 说明Simplify能够这样工作.
前两行的Simplify[expr,assum]的assum的第二部分是part1 > part2经过稍微简单移项得到的, 最后一行甚至只对调了不等式方向, 变成part2 < part1, 完全没有移项, 也得不出结果.
part1 = Sr t1 + a (1 + t1 + \[Gamma]);
part2 = c + t1 + a Sr t1 + \[Gamma] + a \[Lambda];
Simplify[
part1 > part2, {0 < a < 1,
c < (Sr t1 + a (1 + t1 + \[Gamma])) - (t1 + a Sr t1 + \[Gamma] +
a \[Lambda]), 0 < \[Lambda] < 1, t1 > 0, 1 > \[Gamma] > 0,
0 < Sr < 1}]
Simplify[
part1 > part2, {0 < a < 1,
a (1 + t1 + \[Gamma]) >
c + t1 + a Sr t1 + \[Gamma] + a \[Lambda] - Sr t1,
0 < \[Lambda] < 1, t1 > 0, 1 > \[Gamma] > 0, 0 < Sr < 1}]
Simplify[
part1 > part2, {0 < a < 1, part1 > part2, 0 < \[Lambda] < 1, t1 > 0,
1 > \[Gamma] > 0, 0 < Sr < 1}]
Simplify[
part1 > part2, {0 < a < 1, part2 < part1, 0 < \[Lambda] < 1, t1 > 0,
1 > \[Gamma] > 0, 0 < Sr < 1}]

原问题是在一定条件下化简一个复杂的不等式, 预期结果是true或false, 没有达到预期结果, 结果是part1 > part2, 找不出原因的情况下, 我尝试直接化简part1 > part2, 并且将part1 > part2稍微变形或原样添加进assum, 也就是assum的第二部分.
原样添加进assum的时候, 可以得到true, 说明Simplify能够这样工作.
前两行的Simplify[expr,assum]的assum的第二部分是part1 > part2经过稍微简单移项得到的, 最后一行甚至只对调了不等式方向, 变成part2 < part1, 完全没有移项, 也得不出结果.
part1 = Sr t1 + a (1 + t1 + \[Gamma]);
part2 = c + t1 + a Sr t1 + \[Gamma] + a \[Lambda];
Simplify[
part1 > part2, {0 < a < 1,
c < (Sr t1 + a (1 + t1 + \[Gamma])) - (t1 + a Sr t1 + \[Gamma] +
a \[Lambda]), 0 < \[Lambda] < 1, t1 > 0, 1 > \[Gamma] > 0,
0 < Sr < 1}]
Simplify[
part1 > part2, {0 < a < 1,
a (1 + t1 + \[Gamma]) >
c + t1 + a Sr t1 + \[Gamma] + a \[Lambda] - Sr t1,
0 < \[Lambda] < 1, t1 > 0, 1 > \[Gamma] > 0, 0 < Sr < 1}]
Simplify[
part1 > part2, {0 < a < 1, part1 > part2, 0 < \[Lambda] < 1, t1 > 0,
1 > \[Gamma] > 0, 0 < Sr < 1}]
Simplify[
part1 > part2, {0 < a < 1, part2 < part1, 0 < \[Lambda] < 1, t1 > 0,
1 > \[Gamma] > 0, 0 < Sr < 1}]
