Nuprl Definition : atan-approx
atan-approx(k;x;N) ==
eval u = poly-approx(λi.(r(if (i rem 2 =z 0) then 1 else -1 fi ))/(2 * i) + 1;x * x;k;2 * N) in
eval b = |u| + 1 in
eval z = x b in
(u * z) ÷ 4 * b
Definitions occuring in Statement :
poly-approx: poly-approx(a;x;k;N),
int-rdiv: (a)/k1,
rmul: a * b,
int-to-real: r(n),
absval: |i|,
callbyvalue: callbyvalue,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
apply: f a,
lambda: λx.A[x],
remainder: n rem m,
divide: n ÷ m,
multiply: n * m,
add: n + m,
minus: -n,
natural_number: $n
Definitions occuring in definition :
poly-approx: poly-approx(a;x;k;N),
lambda: λx.A[x],
int-rdiv: (a)/k1,
int-to-real: r(n),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
remainder: n rem m,
minus: -n,
rmul: a * b,
add: n + m,
absval: |i|,
callbyvalue: callbyvalue,
apply: f a,
divide: n ÷ m,
multiply: n * m,
natural_number: $n
FDL editor aliases :
atan-approx
Latex:
atan-approx(k;x;N) ==
eval u = poly-approx(\mlambda{}i.(r(if (i rem 2 =\msubz{} 0) then 1 else -1 fi ))/(2 * i) + 1;x * x;k;2 * N) in
eval b = |u| + 1 in
eval z = x b in
(u * z) \mdiv{} 4 * b
Date html generated:
2018_05_22-PM-03_04_54
Last ObjectModification:
2017_10_25-PM-09_31_26
Theory : reals_2
Home
Index