Nuprl Definition : arctan-poly
arctan-poly(x;k) == Σ{(if (i rem 2 =z 0) then x^(2 * i) + 1 else -(x^(2 * i) + 1) fi )/(2 * i) + 1 | 0≤i≤k}
Definitions occuring in Statement :
rsum: Σ{x[k] | n≤k≤m},
rnexp: x^k1,
int-rdiv: (a)/k1,
rminus: -(x),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
remainder: n rem m,
multiply: n * m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
rsum: Σ{x[k] | n≤k≤m},
int-rdiv: (a)/k1,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
remainder: n rem m,
rminus: -(x),
rnexp: x^k1,
add: n + m,
multiply: n * m,
natural_number: $n
FDL editor aliases :
arctan-poly
Latex:
arctan-poly(x;k) ==
\mSigma{}\{(if (i rem 2 =\msubz{} 0) then x\^{}(2 * i) + 1 else -(x\^{}(2 * i) + 1) fi )/(2 * i) + 1 | 0\mleq{}i\mleq{}k\}
Date html generated:
2018_05_22-PM-03_04_24
Last ObjectModification:
2017_10_23-PM-04_18_10
Theory : reals_2
Home
Index