Nuprl Definition : seq-max-lower

seq-max-lower(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 i + 1 else r 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,  subtract: n - m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  natural_number: $n,  add: n + m,  multiply: n * m,  apply: f a,  subtract: n - m,  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-max-lower
Latex:
seq-max-lower(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  i  +  1
                                      else  r
                                      fi  )


Date html generated: 2017_10_03-AM-08_43_49
Last ObjectModification: 2017_09_12-PM-00_24_45

Theory : reals


Home Index