Nuprl Definition : sine-medium
sine-medium(x) ==
case rless-case((r(99))/100;r1;250;x)
of inl(_) =>
4 * cosine-small((x)/4) * (sine-small((x)/4) - 2 * sine-small((x)/4)^3)
| inr(_) =>
case rless-case((r(49))/100;(r1)/2;250;x)
of inl(_) =>
2 * sine-small((x)/2) * cosine-small((x)/2)
| inr(_) =>
case rless-case((r(-1))/2;(r(-49))/100;250;x)
of inl(_) =>
sine-small(x)
| inr(_) =>
case rless-case(r(-1);(r(-99))/100;250;x)
of inl(_) =>
2 * sine-small((x)/2) * cosine-small((x)/2)
| inr(_) =>
4 * cosine-small((x)/4) * (sine-small((x)/4) - 2 * sine-small((x)/4)^3)
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),
int-to-real: r(n),
minus: -n,
rmul: a * b,
cosine-small: cosine-small(x),
rsub: x - y,
int-rmul: k1 * a,
rnexp: x^k1,
sine-small: sine-small(x),
int-rdiv: (a)/k1,
natural_number: $n
FDL editor aliases :
sine-medium
Latex:
sine-medium(x) ==
case rless-case((r(99))/100;r1;250;x)
of inl($_{}$) =>
4 * cosine-small((x)/4) * (sine-small((x)/4) - 2 * sine-small((x)/4)\^{}3)
| inr($_{}$) =>
case rless-case((r(49))/100;(r1)/2;250;x)
of inl($_{}$) =>
2 * sine-small((x)/2) * cosine-small((x)/2)
| inr($_{}$) =>
case rless-case((r(-1))/2;(r(-49))/100;250;x)
of inl($_{}$) =>
sine-small(x)
| inr($_{}$) =>
case rless-case(r(-1);(r(-99))/100;250;x)
of inl($_{}$) =>
2 * sine-small((x)/2) * cosine-small((x)/2)
| inr($_{}$) =>
4 * cosine-small((x)/4) * (sine-small((x)/4) - 2 * sine-small((x)/4)\^{}3)
Date html generated:
2019_10_30-AM-11_42_13
Last ObjectModification:
2019_02_03-PM-00_58_10
Theory : reals_2
Home
Index