Nuprl Definition : approx-arg-interval

If the derivative of f on interval [l, u] is bounded in absolute value
by B, then we can compute the function on an arbitrary real x ∈ [l, u]
by approximating x to a rational number (or one of the endpoints).⋅
approx-arg-interval(f;l;u;B;x) ==
  accelerate(1 + (2 * B);λn.eval a = x n in
                            eval m = 2 * n in
                            eval x' = if (a * 2) < ((l m) + 2)
                                         then l
                                         else if ((u m) - 2) < (a * 2)  then u  else (r(a))/m in
                              f x' n)


Definitions occuring in Statement :  int-rdiv: (a)/k1,  int-to-real: r(n),  accelerate: accelerate(k;f),  callbyvalue: callbyvalue,  less: if (a) < (b)  then c  else d,  apply: f a,  lambda: λx.A[x],  multiply: n * m,  subtract: n - m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  apply: f a,  int-to-real: r(n),  int-rdiv: (a)/k1,  natural_number: $n,  multiply: n * m,  subtract: n - m,  less: if (a) < (b)  then c  else d,  add: n + m,  callbyvalue: callbyvalue,  lambda: λx.A[x],  accelerate: accelerate(k;f)
FDL editor aliases :  approx-arg-interval
Latex:
approx-arg-interval(f;l;u;B;x)  ==
    accelerate(1  +  (2  *  B);\mlambda{}n.eval  a  =  x  n  in
                                                        eval  m  =  2  *  n  in
                                                        eval  x'  =  if  (a  *  2)  <  ((l  m)  +  2)
                                                                                  then  l
                                                                                  else  if  ((u  m)  -  2)  <  (a  *  2)    then  u    else  (r(a))/m  in
                                                            f  x'  n)


Date html generated: 2017_01_09-AM-09_05_16
Last ObjectModification: 2016_11_28-PM-06_44_19

Theory : reals


Home Index