# symbolic functions and bool

d=var('d') $d$ is integer and $d>4$

f(d)=1/6*(d^2 - sqrt(d^2 + 8*d - 8)*d + 23*d - sqrt(d^2 + 8*d - 8) - 26)*(d - sqrt(d^2 + 8*d - 8) + 4)/(d + 1)


How can I show that $f(d)\ge 0$

bool(f(d)>=0) and bool(f(d)<0) return false

edit retag close merge delete

Sort by » oldest newest most voted

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:

• When sage bool-evaluates such an expression to False it does not mean, that the relation is a false one, instead it means that sage cannot prove the relation is true.
• And that we have to help sage find the 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.

more

Acturally, I have so many equations, which similar to f(d). So, I can not adjust each equation by human sense. But I'm really appreciate for your advice:)

( 2017-07-10 03:48:33 -0500 )edit

To give a different point of view on @dan_fulea's answer, note that even Boolean satisfiability is NP-complete. If you include some transcendentals it isn't solvable at all. So it's not surprising that even with better algorithms some combination of $\sqrt{stuff}$ and polynomials might be hard to solve in this fashion.

more