Nuprl Definition : regular-int-seq

The factor ⌜2⌝ on the right of the inequality is essential to prove accelerate_wf

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

Definitions occuring in Statement :  absval: |i| nat_plus: + le: A ≤ B all: x:A. B[x] apply: a multiply: m subtract: m add: m natural_number: $n
Definitions occuring in definition :  all: x:A. B[x] nat_plus: + le: A ≤ B absval: |i| subtract: m apply: a multiply: m natural_number: $n add: m
FDL editor aliases :  k-reg-seq

k-regular-seq(f)  ==    \mforall{}n,m:\mBbbN{}\msupplus{}.    (|(m  *  (f  n))  -  n  *  (f  m)|  \mleq{}  ((2  *  k)  *  (n  +  m)))

Date html generated: 2016_07_08-PM-06_30_10
Last ObjectModification: 2015_09_23-AM-09_00_35

Theory : reals

Home Index