- function represents the function whose infinity norm is to be checked
- range represents the infinity norm is to be considered on
- constant represents the upper bound the infinity norm is to be checked to

- The command checkinfnorm checks whether the infinity norm of the given
function function in the range range can be proven (by Sollya) to
be less than the given bound bound. This means, if checkinfnorm
evaluates to true, the infinity norm has been proven (by Sollya's
interval arithmetic) to be less than the bound. If checkinfnorm evaluates
to false, there are two possibilities: either the bound is less than
or equal to the infinity norm of the function or the bound is greater
than the infinity norm but Sollya could not conclude using its
internal interval arithmetic.

checkinfnorm is sensitive to the global variable diam. The smaller diam, the more time Sollya will spend on the evaluation of checkinfnorm in order to prove the bound before returning false although the infinity norm is bounded by the bound. If diam is equal to 0, Sollya will eventually spend infinite time on instances where the given bound bound is less or equal to the infinity norm of the function function in range range. In contrast, with diam being zero, checkinfnorm evaluates to true iff the infinity norm of the function in the range is bounded by the given bound.

true

> checkinfnorm(sin(x),[0;1.75], 1/2); checkinfnorm(sin(x),[0;20/39],1/2);

false

true

> b = dirtyinfnorm(p - exp(x), [-1;1]);

> checkinfnorm(p - exp(x), [-1;1], b);

false

> b1 = round(b, 15, RU);

> checkinfnorm(p - exp(x), [-1;1], b1);

true

> b2 = round(b, 25, RU);

> checkinfnorm(p - exp(x), [-1;1], b2);

false

> diam = 1b-20!;

> checkinfnorm(p - exp(x), [-1;1], b2);

true