I want to prove that
expression1[u,v] <= 0 for all real u, v satisfying 0<=u<=2 and v^2<=u^3
where the formula for expression1
is algebraic but very large and messy. Based on numerical experiments, I strongly believe this statement is true.
In other words, I want to compute
Reduce[expression1[u,v]<=0 && 0<=u<=2 && v^2<=u^3, {u,v}]
However, I am unable to compute this on my laptop (not enough computational resources I suppose, Reduce
keeps running even after several hours). So I have two questions:
(1) Is there a way to monitor the progress of Reduce[]
?
(2) I have access to powerful computing clusters as well as AWS. Is there a way to use these resources to solve this problem in a reasonable amount of time?
I have attached the explicit formula for expression1
.
Attachments: