Nuprl Definition : seq-min-upper

seq-min-upper(k;n;f) ==
  primrec(n;1;λi,r. if ((i + 1) * (f r)) + ((2 * k) * (i + 1)) ≤z (r * (f (i + 1))) + ((2 * k) * r)
                   then r
                   else i + 1
                   fi )


Definitions occuring in Statement :  le_int: i ≤z j,  primrec: primrec(n;b;c),  ifthenelse: if b then t else f fi ,  apply: f a,  lambda: λx.A[x],  multiply: n * m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  natural_number: $n,  add: n + m,  multiply: n * m,  apply: f a,  le_int: i ≤z j,  ifthenelse: if b then t else f fi ,  lambda: λx.A[x],  primrec: primrec(n;b;c)
FDL editor aliases :  seq-min-upper
Latex:
seq-min-upper(k;n;f)  ==
    primrec(n;1;\mlambda{}i,r.  if  ((i  +  1)  *  (f  r))  +  ((2  *  k)  *  (i  +  1))  \mleq{}z  (r  *  (f  (i  +  1)))  +  ((2  *  k)  *  r)
                                      then  r
                                      else  i  +  1
                                      fi  )


Date html generated: 2017_10_03-AM-08_43_14
Last ObjectModification: 2017_09_09-AM-08_10_20

Theory : reals


Home Index