Nuprl Definition : regularize
regularize(k;f) ==
λn.if regular-upto(k;n;f)
then f n
else eval m = mu(λn.(¬bregular-upto(k;n;f))) - 1 in
eval j = seq-min-upper(k;m;f) in
k * ((n * ((f j) + (2 * k))) ÷ j * k)
fi
Definitions occuring in Statement :
seq-min-upper: seq-min-upper(k;n;f),
regular-upto: regular-upto(k;n;f),
mu: mu(f),
callbyvalue: callbyvalue,
bnot: ¬bb,
ifthenelse: if b then t else f fi ,
apply: f a,
lambda: λx.A[x],
divide: n ÷ m,
multiply: n * m,
subtract: n - m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
multiply: n * m,
natural_number: $n,
apply: f a,
add: n + m,
divide: n ÷ m,
seq-min-upper: seq-min-upper(k;n;f),
callbyvalue: callbyvalue,
regular-upto: regular-upto(k;n;f),
bnot: ¬bb,
lambda: λx.A[x],
mu: mu(f),
subtract: n - m,
ifthenelse: if b then t else f fi
FDL editor aliases :
regularize
Latex:
regularize(k;f) ==
\mlambda{}n.if regular-upto(k;n;f)
then f n
else eval m = mu(\mlambda{}n.(\mneg{}\msubb{}regular-upto(k;n;f))) - 1 in
eval j = seq-min-upper(k;m;f) in
k * ((n * ((f j) + (2 * k))) \mdiv{} j * k)
fi
Date html generated:
2017_10_03-AM-09_07_15
Last ObjectModification:
2017_09_11-PM-04_11_19
Theory : reals
Home
Index