Nuprl Definition : m-reg-test
For a sequence of integers, s, we can decide is s is regular upto some bound b
because n ≤ m is decidable on integers.
For the metric version of regularity, we won't be able to decide
whether the distance z = mdist(d;x;y) is or is not less than or equal to a given
(rational) real number.
But if a < b then we can decide (a < z) ∨ (z < b).
So we set a to be the bound for 2-regularity and b the bound for 3-regularity.
Then to test whether we can add point x onto sequence s,
we will either find that the extended sequence is not 2-regular,
m-not-reg(d;s;n),or that it is (still) 3-regular.
A 2-regular sequence, s, has ∀n:ℕ. m-not-reg(d;s;n) = ff,
(see Error :m-regular-not-m-not-reg)
and ∀n:ℕb. m-not-reg(d;s;n) = ff implies that s is at least 3-regular
(see Error :not-m-not-reg-3regular).⋅
m-reg-test(d;b;s;x) ==
int-seg-case(0;b;λn.rless-case((r(2)/r(n + 1)) + (r(2)/r(b + 1));(r(3)/r(n + 1)) + (r(3)/r(b + 1));rlessw((r(2)/r(n
+ 1))
+ (r(2)/r(b + 1));(r(3)/r(n + 1)) + (r(3)/r(b + 1)));mdist(d;s n;x)))
Definitions occuring in Statement :
mdist: mdist(d;x;y),
rless-case: rless-case(x;y;n;z),
rdiv: (x/y),
rlessw: rlessw(x;y),
radd: a + b,
int-to-real: r(n),
int-seg-case: int-seg-case(i;j;d),
apply: f a,
lambda: λx.A[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
int-seg-case: int-seg-case(i;j;d),
lambda: λx.A[x],
rless-case: rless-case(x;y;n;z),
rlessw: rlessw(x;y),
radd: a + b,
rdiv: (x/y),
int-to-real: r(n),
add: n + m,
natural_number: $n,
mdist: mdist(d;x;y),
apply: f a
FDL editor aliases :
m-reg-test
Latex:
m-reg-test(d;b;s;x) ==
int-seg-case(0;b;\mlambda{}n.rless-case((r(2)/r(n + 1)) + (r(2)/r(b + 1));(r(3)/r(n + 1))
+ (r(3)/r(b + 1));rlessw((r(2)/r(n + 1)) + (r(2)/r(b + 1));(r(3)/r(n + 1))
+ (r(3)/r(b + 1)));mdist(d;s n;x)))
Date html generated:
2019_10_30-AM-06_59_28
Last ObjectModification:
2019_10_11-PM-00_46_02
Theory : reals
Home
Index