Nuprl Lemma : summary of definitions
k-regular-seq(f) ==  ∀n,m:ℕ+.  (|(m * (f n)) - n * (f m)| ≤ ((2 * k) * (n + m)))
bdd-diff(f;g) ==  ∃B:ℕ. ∀n:ℕ+. (|(f n) - g n| ≤ B)
ℝ ==  {f:ℕ+ ─→ ℤ| regular-seq(f)} 
x = y ==  ∀n:ℕ+. (|(x n) - y n| ≤ 4)
x < y ==  ∃n:{ℕ+| (x n) + 4 < y n}
accelerate(k;f) ==  eval k2 = 2 * k in λn.eval m = k2 * n in (f m) ÷ k2
a + b ==  accelerate(2;reg-seq-list-add([a; b]))
rminus(x) ==  λn.(-(x n))
rmax(x;y) ==  λn.imax(x n;y n)
|x| ==  rmax(x;rminus(x))
a * b ==
  eval a1 = a in
  eval b1 = b in
    accelerate((2 * imax(canonical-bound(a1);canonical-bound(b1))) + 1;reg-seq-mul(a1;b1))⋅
Latex:
k-regular-seq(f)  ==    \mforall{}n,m:\mBbbN{}\msupplus{}.    (|(m  *  (f  n))  -  n  *  (f  m)|  \mleq{}  ((2  *  k)  *  (n  +  m)))
bdd-diff(f;g)  ==    \mexists{}B:\mBbbN{}.  \mforall{}n:\mBbbN{}\msupplus{}.  (|(f  n)  -  g  n|  \mleq{}  B)
\mBbbR{}  ==    \{f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  regular-seq(f)\} 
x  =  y  ==    \mforall{}n:\mBbbN{}\msupplus{}.  (|(x  n)  -  y  n|  \mleq{}  4)
x  <  y  ==    \mexists{}n:\{\mBbbN{}\msupplus{}|  (x  n)  +  4  <  y  n\}
accelerate(k;f)  ==    eval  k2  =  2  *  k  in  \mlambda{}n.eval  m  =  k2  *  n  in  (f  m)  \mdiv{}  k2
a  +  b  ==    accelerate(2;reg-seq-list-add([a;  b]))
rminus(x)  ==    \mlambda{}n.(-(x  n))
rmax(x;y)  ==    \mlambda{}n.imax(x  n;y  n)
|x|  ==    rmax(x;rminus(x))
a  *  b  ==
    eval  a1  =  a  in
    eval  b1  =  b  in
        accelerate((2  *  imax(canonical-bound(a1);canonical-bound(b1)))  +  1;reg-seq-mul(a1;b1))\mcdot{}
Date html generated:
2015_07_17-PM-06_21_49
Last ObjectModification:
2014_04_10-PM-02_22_41
Home
Index