Description:

• infnorm(f,range) computes an interval bounding the infinity norm of the given function f on the interval I, e.g. computes an interval J such that max {|f(x)|, x in I} C J.
• If filename is given, a proof in English will be produced (and stored in file called filename) proving that max {|f(x)|, x in I} C J.
• If a list IList of intervals I1, ... ,In is given, the infinity norm will be computed on I \ (I1 U ... U I2).
• The function f is assumed to be at least twice continuous on I. More generally, if f is Ck, global variables hopitalrecursions and taylorrecursions must have values not greater than k.
• If the interval is reduced to a single point, the result of infnorm is an interval containing the exact absolute value of f at this point.
• If the interval is not bound, the result will be [0, +Inf] which is correct but perfectly useless. infnorm is not meant to be used with infinite intervals.
• The result of this command depends on the global variables prec, diam, taylorrecursions and hopitalrecursions. The contribution of each variable is not easy even to analyse.
  • The algorithm uses interval arithmetic with precision prec. The precision should thus be set high enough to ensure that no critical cancellation will occur.
  • When an evaluation is performed on an interval [a,b], if the result is considered being too large, the interval is split into [a,(a+b)/2] and [(a+b)/2,b] and so on recursively. This recursion step is not performed if the (b-a) < d*|I| where d is the value of variable diam. In other words, diam controls the minimum length of an interval during the algorithm.
  • To perform the evaluation of a function on an interval, Taylor's rule is applied, e.g. f([a,b]) C f(m) + [a-m, b-m]*f'([a,b]) where m=(a+b)/2. This rule is recursively applied n times where n is the value of variable taylorrecursions. Roughly speaking, the evaluations will avoid decorrelation up to order n.
  • When a function of the form g/h has to be evaluated on an interval [a,b] and when g and h vanish at a same point z of the interval, the ratio may be defined even if the expression g(z)/h(z)=0/0 does not make any sense. In this case, L'Hopital's rule may be used and (g/h)([a,b]) C (g'/h')([a,b]). Since the same can occur with the ratio g'/h', the rule is applied recursively. The variable hopitalrecursions controls the number of recursion steps.
• The algorithm used for this command is quite complex to be explained here. Please find a complete description in the following article:
  S. Chevillard and C. Lauter
  A certified infinity norm for the implementation of elementary functions
  LIP Research Report number RR2007-26
  http://prunel.ccsd.cnrs.fr/ensl-00119810
  
• Users should be aware about the fact that the algorithm behind infnorm is inefficient in most cases and that other, better suited algorithms, such as supnorm, are available inside Sollya. As a matter of fact, while infnorm is maintained for compatibility reasons with legacy Sollya codes, users are advised to avoid using infnorm in new Sollya scripts and to replace it, where possible, by the supnorm command.