Nuprl Definition : find-approx-fp
find-approx-fp(n;f;e) ==
if n=0
then <Ax, Ax>
else let k = mu-ge(λm.(unit-ball-ex-decider(m;n)
(λq.case isr(rless-case((r(2) * e/r(3));e;(((rlessw(((r(2) * e/r(3)) * r(3)) * rinv(r(3));(e
* r(3))
* rinv(r(3)))
* 20)
+ 1)
* 20)
+ 1;d(f
(λi.eval k = m in
λn.if (k) < (0)
then -((r(q i) (2 * n)) ÷ (-2) * k)
else ((r(q i) (2 * n)) ÷ 2 * k));λi.eval k = m in
λn.if (k) < (0)
then -((r(q i)
(2 * n)) ÷ (-2) * k)
else ((r(q i) (2 * n)) ÷ 2
* k))))
of inl(x) =>
inl x
| inr(x) =>
inr (λx.Ax) ));1) in
case unit-ball-ex-decider(k;n)
(λq.case isr(rless-case((r(2) * e/r(3));e;(((rlessw(((r(2) * e/r(3)) * r(3)) * rinv(r(3));(e * r(3))
* rinv(r(3)))
* 20)
+ 1)
* 20)
+ 1;d(f
(λi.eval k = k in
λn.if (k) < (0)
then -((r(q i) (2 * n)) ÷ (-2) * k)
else ((r(q i) (2 * n)) ÷ 2 * k));λi.eval k = k in
λn.if (k) < (0)
then -((r(q i) (2 * n)) ÷ (-2) * k)
else ((r(q i) (2 * n)) ÷ 2 * k))))
of inl(x) =>
inl x
| inr(x) =>
inr (λx.Ax) )
of inl(x) =>
let q,%8 = x
in <λi.eval k = k in
λn.if (k) < (0) then -((r(q i) (2 * n)) ÷ (-2) * k) else ((r(q i) (2 * n)) ÷ 2 * k)
, Ax
>
| inr(x) =>
let q,%8 = fix((λx.x))
in <λi.eval k = k in
λn.if (k) < (0) then -((r(q i) (2 * n)) ÷ (-2) * k) else ((r(q i) (2 * n)) ÷ 2 * k)
, Ax
>
Definitions occuring in Statement :
unit-ball-ex-decider: unit-ball-ex-decider(k;n),
real-vec-dist: d(x;y),
rless-case: rless-case(x;y;n;z),
rdiv: (x/y),
rlessw: rlessw(x;y),
rinv: rinv(x),
rmul: a * b,
int-to-real: r(n),
mu-ge: mu-ge(f;n),
callbyvalue: callbyvalue,
isr: isr(x),
let: let,
less: if (a) < (b) then c else d,
int_eq: if a=b then c else d,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
inl: inl x,
divide: n ÷ m,
multiply: n * m,
add: n + m,
minus: -n,
natural_number: $n,
axiom: Ax
Definitions occuring in definition :
axiom: Ax,
lambda: λx.A[x],
inr: inr x ,
inl: inl x,
natural_number: $n,
multiply: n * m,
apply: f a,
int-to-real: r(n),
divide: n ÷ m,
minus: -n,
less: if (a) < (b) then c else d,
callbyvalue: callbyvalue,
real-vec-dist: d(x;y),
rinv: rinv(x),
rmul: a * b,
rdiv: (x/y),
rlessw: rlessw(x;y),
add: n + m,
rless-case: rless-case(x;y;n;z),
isr: isr(x),
decide: case b of inl(x) => s[x] | inr(y) => t[y],
unit-ball-ex-decider: unit-ball-ex-decider(k;n),
mu-ge: mu-ge(f;n),
let: let,
pair: <a, b>,
int_eq: if a=b then c else d,
spread: spread def,
fix: fix(F)
FDL editor aliases :
find-approx-fp
Latex:
find-approx-fp(n;f;e) ==
if n=0
then <Ax, Ax>
else let k = mu-ge(\mlambda{}m.(unit-ball-ex-decider(m;n)
(\mlambda{}q.case isr(rless-case((r(2) * e/r(3));e;(((rlessw(((r(2) * e/r(3))
* r(3))
* rinv(r(3));(e * r(3)) * rinv(r(3)))
* 20)
+ 1)
* 20)
+ 1;d(f
(\mlambda{}i.eval k = m in
\mlambda{}n.if (k) < (0)
then -((r(q i) (2 * n)) \mdiv{} (-2) * k)
else ((r(q i) (2 * n)) \mdiv{} 2
* k));\mlambda{}i.eval k = m in
\mlambda{}n.if (k) < (0)
then -((r(q i) (2 * n)) \mdiv{} (-2)
* k)
else ((r(q i) (2 * n)) \mdiv{} 2
* k))))
of inl(x) =>
inl x
| inr(x) =>
inr (\mlambda{}x.Ax) ));1) in
case unit-ball-ex-decider(k;n)
(\mlambda{}q.case isr(rless-case((r(2) * e/r(3));e;(((rlessw(((r(2) * e/r(3)) * r(3))
* rinv(r(3));(e * r(3)) * rinv(r(3)))
* 20)
+ 1)
* 20)
+ 1;d(f
(\mlambda{}i.eval k = k in
\mlambda{}n.if (k) < (0)
then -((r(q i) (2 * n)) \mdiv{} (-2) * k)
else ((r(q i) (2 * n)) \mdiv{} 2
* k));\mlambda{}i.eval k = k in
\mlambda{}n.if (k) < (0)
then -((r(q i) (2 * n)) \mdiv{} (-2) * k)
else ((r(q i) (2 * n)) \mdiv{} 2 * k))))
of inl(x) =>
inl x
| inr(x) =>
inr (\mlambda{}x.Ax) )
of inl(x) =>
let q,\%8 = x
in <\mlambda{}i.eval k = k in
\mlambda{}n.if (k) < (0)
then -((r(q i) (2 * n)) \mdiv{} (-2) * k)
else ((r(q i) (2 * n)) \mdiv{} 2 * k)
, Ax
>
| inr(x) =>
let q,\%8 = fix((\mlambda{}x.x))
in <\mlambda{}i.eval k = k in
\mlambda{}n.if (k) < (0)
then -((r(q i) (2 * n)) \mdiv{} (-2) * k)
else ((r(q i) (2 * n)) \mdiv{} 2 * k)
, Ax
>
Date html generated:
2019_10_30-AM-11_29_20
Last ObjectModification:
2019_07_30-PM-00_50_42
Theory : real!vectors
Home
Index