Nuprl Definition : cosine-medium
cosine-medium(x) ==
case rless-case((r(99))/100;r1;250;x)
of inl(_) =>
r1 - 8 * sine-small((x)/4)^2 * cosine-small((x)/4)^2
| inr(_) =>
case rless-case((r(49))/100;(r1)/2;250;x)
of inl(_) =>
cosine-small((x)/2)^2 - sine-small((x)/2)^2
| inr(_) =>
case rless-case((r(-1))/2;(r(-49))/100;250;x)
of inl(_) =>
cosine-small(x)
| inr(_) =>
case rless-case(r(-1);(r(-99))/100;250;x)
of inl(_) =>
cosine-small((x)/2)^2 - sine-small((x)/2)^2
| inr(_) =>
r1 - 8 * sine-small((x)/4)^2 * cosine-small((x)/4)^2
Definitions occuring in Statement :
cosine-small: cosine-small(x),
sine-small: sine-small(x),
rless-case: rless-case(x;y;n;z),
rnexp: x^k1,
int-rdiv: (a)/k1,
int-rmul: k1 * a,
rsub: x - y,
rmul: a * b,
int-to-real: r(n),
decide: case b of inl(x) => s[x] | inr(y) => t[y],
minus: -n,
natural_number: $n
Definitions occuring in definition :
decide: case b of inl(x) => s[x] | inr(y) => t[y],
rless-case: rless-case(x;y;n;z),
minus: -n,
rsub: x - y,
int-to-real: r(n),
int-rmul: k1 * a,
rmul: a * b,
sine-small: sine-small(x),
rnexp: x^k1,
cosine-small: cosine-small(x),
int-rdiv: (a)/k1,
natural_number: $n
FDL editor aliases :
cosine-medium
Latex:
cosine-medium(x) ==
case rless-case((r(99))/100;r1;250;x)
of inl($_{}$) =>
r1 - 8 * sine-small((x)/4)\^{}2 * cosine-small((x)/4)\^{}2
| inr($_{}$) =>
case rless-case((r(49))/100;(r1)/2;250;x)
of inl($_{}$) =>
cosine-small((x)/2)\^{}2 - sine-small((x)/2)\^{}2
| inr($_{}$) =>
case rless-case((r(-1))/2;(r(-49))/100;250;x)
of inl($_{}$) =>
cosine-small(x)
| inr($_{}$) =>
case rless-case(r(-1);(r(-99))/100;250;x)
of inl($_{}$) =>
cosine-small((x)/2)\^{}2 - sine-small((x)/2)\^{}2
| inr($_{}$) =>
r1 - 8 * sine-small((x)/4)\^{}2 * cosine-small((x)/4)\^{}2
Date html generated:
2019_10_30-AM-11_42_43
Last ObjectModification:
2019_02_03-PM-01_13_31
Theory : reals_2
Home
Index