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