1 | initial version |
The answer will not be a one liner bool eval, that results into True
.
Instead, it is the same explanation done many, many times in such situations, that:
False
it does not mean, that the relation is a false one, instead it means that sage cannot prove the relation is true.True
. Sometimes this help is a long story, sometimes a short one. (Sometimes the programmers are not satisfied by this "need to help", but then they should try to improve the algorithm...)In this case, we have some factors, we will show that each factor is positive for a real number $d>4$.
First of all, the factor $(d+1)$...
sage: var( 'd' );
sage: assume( d>4 )
sage: bool( d+1>0 )
True
OK, this was simple. Now let us consider the factor d - sqrt(d^2 + 8*d - 8) + 4
. We try successively...
sage: var( 'd' );
sage: assume( d, 'real' )
sage: assume( d>4 )
sage: bool( d - sqrt(d^2 + 8*d - 8) + 4 > 0 )
False
sage: bool( d+4 > sqrt(d^2 + 8*d - 8) )
False
sage: bool( (d+4)^2 > sqrt(d^2 + 8*d - 8)^2 )
True
OK, this was not obvious for the computer... Then we will have more to fight with the last parenthesis.
sage: var( 'd' );
sage: assume( d>4 )
sage: assume( d, 'real' )
sage: bool( d^2 - sqrt(d^2 + 8*d - 8)*d + 23*d - sqrt(d^2 + 8*d - 8) - 26 > 0 )
False
sage: bool( d^2 + 23*d - 26 - sqrt(d^2 + 8*d - 8)*d - sqrt(d^2 + 8*d - 8) > 0 )
False
sage: bool( d^2 + 23*d - 26 - sqrt(d^2 + 8*d - 8)*(d+1) > 0 )
False
sage: bool( d^2 + 23*d - 26 > sqrt(d^2 + 8*d - 8)*(d+1) )
False
sage: bool( (d^2 + 23*d - 26)^2 > sqrt(d^2 + 8*d - 8)^2 * (d+1)^2 )
True
This is a possible way to use sage and the minimal human sense for progress while rearranging inequalites. If this is not acceptable, then i have to resign, please ignore the answer.