Nuprl Definition : m-regularize
For any sequence of points s, we "regularize" s by testing if there
is a failure of 2-regularity. If so, we make the regularized sequence
become constant from that index on. Otherwise, the sequence will be
unchanged, and will be at least 3-regular.
We know that any 2-regular sequence s has m-regularize(d;s) = s
(see Error :m-regularize-of-regular)
and the regularization of any sequence s is a Cauchy sequence
(with modulus of Cauchyness λk.(6 * k) )
(see Error :m-regularize-mcauchy)⋅
m-regularize(d;s) == λn.eval m = first-m-not-reg(d;s;n + 1) in if 0 <z m then s (m - 2) else s n fi
Definitions occuring in Statement :
first-m-not-reg: first-m-not-reg(d;s;k),
callbyvalue: callbyvalue,
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
apply: f a,
lambda: λx.A[x],
subtract: n - m,
add: n + m,
natural_number: $n
Definitions occuring in definition :
lambda: λx.A[x],
callbyvalue: callbyvalue,
first-m-not-reg: first-m-not-reg(d;s;k),
add: n + m,
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
subtract: n - m,
natural_number: $n,
apply: f a
FDL editor aliases :
m-regularize
Latex:
m-regularize(d;s) ==
\mlambda{}n.eval m = first-m-not-reg(d;s;n + 1) in
if 0 <z m then s (m - 2) else s n fi
Date html generated:
2019_10_30-AM-07_02_37
Last ObjectModification:
2019_10_11-PM-01_03_43
Theory : reals
Home
Index