Nuprl Lemma : summary of definitions

k-regular-seq(f) ==  ∀n,m:ℕ+.  (|(m (f n)) (f m)| ≤ ((2 k) (n m)))

bdd-diff(f;g) ==  ∃B:ℕ. ∀n:ℕ+(|(f n) n| ≤ B)

ℝ ==  {f:ℕ+ ─→ ℤregular-seq(f)} 

==  ∀n:ℕ+(|(x n) n| ≤ 4)

x < ==  ∃n:{ℕ+(x n) 4 < n}

accelerate(k;f) ==  eval k2 in λn.eval k2 in (f m) ÷ k2

==  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))

==
  eval a1 in
  eval b1 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