numerval



Stavros Macrakis <macrakis <at> alum.mit.edu> writes:

> 
> > 
> 
> The simple solution is assume(%e > 2.718, %e < 2.719)  (to appropriate
> precision, of course).
> 
> The problem is that, though Compar is smart enough to make simple
> deductions from this like  is(%e*100 < 300), it can't make more
> complicated ones like is(%e^2 < 10). 

    I think this is a great limitation.

  Perhaps it would'nt be very difficult to assert %e^2 < 10 (or things like
that) from assume(%e > 2.718, %e < 2.719), a very usefull tool for this purpose
is an easy test (or a database) to proof that a function is increasing:

  So that a/b < e <  a'/b' and f(x) increasing then 

         f(a/b) < f(e) < f(a'/b').

  There are a lot of cases in which is evident that f is increasing, so I think
this can paid the effort, a good ratio power/cost.

   It looks like that there is a strong need of an easy test for a function to
be increasing, I think  this can  be a first a useful first step to avoid the
above limitations.
  
 Miguel.